表示合金中的数学关系答案

【问题标题】：Representing mathematical relations in Alloy表示合金中的数学关系
【发布时间】：2015-10-11 01:08:11
【问题描述】：

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

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

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

以下合金片段是否是“rel”的正确表示？

sig S2 {}

sig S1 {rel: S2}

我如何将这种关系限制为非自反和传递的？

【问题讨论】：

标签： alloy

【解决方案1】：

是的，您的模型将rel 定义为集合S1 和S2 之间的关系。要约束关系，您可以编写如下内容：

fact antireflexive { no iden & rel }

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

和

fact transitive { rel = ^rel }

意味着rel 等于它的传递闭包，因此是传递的。

【讨论】：

再次查看您的片段后，我注意到您已经限制了您的关系，以便它将 S1 中的每个元素映射到 S2 中的一个元素，如果您希望它是一个不受限制的关系，您应该写rel:set S2
感谢您的回复。这有帮助

【解决方案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

【讨论】：