formal-methods - Alloy の述語の問題

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