Question

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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top