代表合金中的数学关系

Question

我是Alloy的新手，我仍然很困惑。我对数学关系比较满意，但不确定如何将它们转化为Alloy。

假设我有（数学）关系的以下定义

rel = {(x, y) | x \in S1, y \in S2}

以下Alloy片段是'rel'的正确表示吗？

sig S2 {}

sig S1 {rel: S2}

我如何将这种关系限制为无反射和传递？

Answer 1

是的，您的模型将rel定义为集合S1和S2之间的关系。要限制关系，你可以编写类似的东西：

fact antireflexive { no iden & rel }

也就是说，在rel中没有映射到自身的元素

和

fact transitive { rel = ^rel }

这意味着rel等于它的传递闭包，因此具有传递性。

Answer 2

首先定义类型：

 sig S1, S2 {}

然后，您可以使用以下等效语法定义rel关系

let rel = { x : univ, y : univ | x in S1 and y in S2 }
let rel = { x : S1, y : S2 }
let rel = S1 -> S2