Problem with predicate in Alloy

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?

Answer 1

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