Проблема с предикатом в сплаве

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