So I have the following bit of code in Alloy:
sig Node { }
sig Queue { root : Node }
pred SomePred {
no q, q' : Queue | q.root = q'.root
}
run SomePred for 3
but this won't yield any instance containing a Queue, I wonder why. It only shows up instances with Nodes. I've tried the equivalent predicate
pred SomePred' {
all q, q' : Queue | q.root != q'.root
}
but the output is the same.
Am I missing something?
There's a logic flaw in there:
fact SomeFact {
no q, q' : Queue | q.root = q'.root
}
Assume there is an instance with a single queue Q
that has a given root R
. When running SomeFact
, it'd test the only queue available, Q
, and it'd find it that Q.root = Q.root
, thus, excluding the given instance from coming to life.
The same reasoning can be made for instances with an arbitrary number of queues.
Here is a working version:
sig Node {
}
sig Queue {
root : Node
}
fact sss {
all disj q, q' : Queue | q.root != q'.root
}
pred abc() {
}
run abc for 3