Alloy 中的谓词问题

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