formal-methods - 合金中的谓词问题

Question

所以我在Alloy中有以下代码：

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
}

但输出是一样的。

我错过了什么吗？

score 0 · Accepted Answer

里面有一个逻辑缺陷：

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

Q假设有一个具有给定 root的单个队列的实例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

1 回答 1