为合金中的每个关系创建一个对象答案

【问题标题】：Creating an object for each relation in Alloy为合金中的每个关系创建一个对象
【发布时间】：2015-01-09 23:26:23
【问题描述】：

我有以下定义。在合金中：

sig A {b : set B}
sig B{}
sig Q {s: A , t: B}

我想添加一组约束，使得对于每个关系 b1:b 存在一个且只有一个 Q1:Q 其中 Q1.s 和 Q1.t分别指 b1 的源和目标。例如，如果我有一个包含 A1 和 B1 且 b1 连接它们的实例（即 b1：A1->B1），那么我还希望有一个 Q1，其中 Q1.s=A1 和 Q1.t=B1。

显然Q的数（基数）等于b关系的数（基数）。

我设法写了一个如下的约束：

t in s.b 
all q1,q2:Q | q1.s=q2.s and q1.t=q2.t => q1=q2
all a1:A,b1:B | a1->b1 in b => some q:Q | q.s=a1 and q.t=b1

我想知道是否有人有更简洁的方式来表达我在合金事实方面的意图。如果 Alloy util 包能让生活更轻松，我愿意使用它。

谢谢

【问题讨论】：

标签： alloy

【解决方案1】：

sig A { b : set B }
sig B {}
sig Q { ab : A -> B }{ one ab }
fact { b = Q.ab and #Q = #b }

【讨论】：

【解决方案2】：

我将通过添加两个关系 s 和 t 来完成@user1513683 的答案，使其成为问题的完整答案：

sig A { b : set B }
sig B {}
sig Q { ab : A -> B , s:A, t:B}{ one ab and t=ab[s]}
fact { b = Q.ab and #Q = #b }

【讨论】：