Проблема с предикатом в 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
}

но вывод такой же.

Я что-то упустил?

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