如何表示一組值應該是不同的？

Question

有沒有一種合理的方式來表示n個元素需要相互區分？具體來說，我有類似下面這樣的簽名：

sig Node { 
up: lone Node, 
left: lone Node, 
right: lone Node, 
left_down: lone Node, 
right_down: lone Node 
} 

，並希望寫一個事實，即這些定義是不同的對於任何給定的節點。我相當肯定，我可以把它寫成NxN矩陣，如下所示：

fact { 
all n: Node | n.up != n.left && n.up != n.right && n.up != n.left_down ... 
} 

但這看起來非常冗長而且相當難看。什麼是正確的方法來做到這一點？

Answer 1

你提出的建議表明每個集合應該是不同的，而不是每個集合都是不相交的。要檢查集合是否不相交，可以簡單地檢查它們的交集（&）是否爲空。

你可以這樣寫：

sig Node { 
    up: lone Node, 
    left: lone Node, 
    right: lone Node, 
    left_down: lone Node, 
    right_down: lone Node 
}{ 
    up & left=none and 
    right & left_down=none and 
    (up + left)& (right + left_down)=none and 
    (up + left + right + left_down)&right_down=none 
} 

做事的那麼詳細，但不太美觀的方法是通過總結每個節點的交集與集合，並確保總和始終是0或1。

sig Node { 
    up: lone Node, 
    left: lone Node, 
    right: lone Node, 
    left_down: lone Node, 
    right_down: lone Node 
}{ 
    all n:Node | add[add[add[add[#(n&up),#(n&left)],#(n&right)],#(n&left_down)],#(n&right_down)] in 0+1 
}