我是Alloy的新手，我仍然很困惑 . 我对数学关系比较满意，但不确定如何将它们转化为Alloy .
假设我有（数学）关系的以下定义
rel = {(x, y) | x \in S1, y \in S2}
以下Alloy片段是'rel'的正确表示吗？
sig S2 {} sig S1 {rel: S2}
我如何将这种关系限制为无反射和传递？
是的，您的模型将 rel 定义为集合 S1 和 S2 之间的关系 . 要约束关系，你可以编写类似的东西：
rel
S1
S2
fact antireflexive { no iden & rel }
也就是说， rel 中没有元素映射到自身
和
fact transitive { rel = ^rel }
这意味着 rel 等于其传递闭包，因此具有传递性 .
首先定义类型：
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
2 回答
是的，您的模型将
rel定义为集合S1和S2之间的关系 . 要约束关系，你可以编写类似的东西：也就是说，
rel中没有元素映射到自身和
这意味着
rel等于其传递闭包，因此具有传递性 .首先定义类型：
然后，您可以使用以下等效语法定义
rel关系