问题与合金

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