Alloy 中的关系连接和运算符

Question

我大致复习了 Alloy 并发现了一些我需要了解的概念。

首先，. （点连接）。我知道它是如何处理简单的例子的，但在这样的情况下：

sig B {}
sig A {
rel: B -> C
}
sig C {
rel1: B -> A
}
rel = {(a1,b1,c1), (a2,b2,c2)}
rel1 = {(c1,b1,a1),(c2,b2,a2)}
rel.rel1 = {(a1,b1,b1,a1),(a2,b2,b2,a2)}
rel1.rel = {(c1,b1,b1,c1),(c2,b2,b2,c2)

我没有得到 rel.rel1 或 rel1.rel 的结果。 有人可以解释一下它是如何工作的吗？

我也遇到了 <: 和 >: 运算符的问题。

提前致谢。

Answer 1

这在我的书（Software Abstractions，麻省理工学院出版社，2012 年）中通过大量示例进行了详细解释。

另外，您可能会发现这些 slides 来自旧演讲的内容很有帮助：

从幻灯片 80 开始，有一个各种点连接的扩展示例。