問題與合金

Question

謂詞所以我的代碼在合金以下位：

sig Node { } 
sig Queue { root : Node } 

pred SomePred { 
    no q, q' : Queue | q.root = q'.root 
} 

run SomePred for 3 

但這不會產生含有一個隊列任何情況下，我不知道爲什麼。它只顯示帶有節點的實例。我試過了等效謂詞

pred SomePred' { 
    all q, q' : Queue | q.root != q'.root 
} 

但輸出是一樣的。

我錯過了什麼嗎？

Answer 1

有一個在那裏邏輯缺陷：

fact SomeFact { 
    no q, q' : Queue | q.root = q'.root 
} 

假設存在與單個隊列Q具有給定的根R一個實例。當運行SomeFact時，它會測試唯一可用的隊列Q，並且它會發現它是Q.root = Q.root，因此排除給定實例不復存在。

可以對具有任意數量的隊列的實例進行相同的推理。

這裏是一個工作版本：

sig Node { 
} 

sig Queue { 
    root : Node 
} 

fact sss { 
    all disj q, q' : Queue | q.root != q'.root 
} 

pred abc() { 
} 

run abc for 3