Home Articles

在Alloy中为每个关系创建一个对象

Asked
Viewed 1723 times
0

我有以下def . 在合金中:

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包 .

谢谢

2 Answers

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

    我将通过添加两个关系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 }
    

Related