爲Alloy中的每個關係創建對象

Question

我有以下def。在合金：

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

我要添加一組約束，使得對於每個關係B1：乙存在一個且僅一個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 

我想知道如果任何人有更多的簡潔的方式來表達我的意圖中的合金事實方面。如果它使生活更輕鬆，我願意使用合金util包。

感謝

Answer 1

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

Answer 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 }