Pregunta

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 hay solución correcta

Licenciado bajo: CC-BY-SA con atribución
No afiliado a StackOverflow
scroll top