Question

J'ai donc le morceau de code suivant en alliage:

sig Node { }
sig Queue { root : Node }

pred SomePred {
    no q, q' : Queue | q.root = q'.root
}

run SomePred for 3

Mais cela ne donnera aucune instance contenant une file d'attente, je me demande pourquoi. Il n'apparaît que des instances avec des nœuds. J'ai essayé le prédicat équivalent

pred SomePred' {
    all q, q' : Queue | q.root != q'.root
}

Mais la sortie est la même.

Est-ce que je manque quelque chose?

Pas de solution correcte

Licencié sous: CC-BY-SA avec attribution
Non affilié à StackOverflow
scroll top