Take the 2-minute tour ×

Having the following:

sig Queue { root: Node }
sig Node { next: lone Node }
fact nextNotReflexive { no n:Node | n = n.next }
fact nextNotCyclic { no n:Node | n in n.^next }

Can anyone help on the implementation of the Enq and Deq?

pred Enq[q,q':Queue, n:Node]{}
pred Deq [q,q':Queue]{}

Any help is appreciated.

share|improve this question
what exactly are you having trouble with? –  Aleksandar Milicevic Mar 19 '13 at 17:48
add comment

1 Answer

You can define enqueue easily:

pred Enq[q, q': Queue, n: Node] {
  q'.root = n and n.next = q.root

But dequeue is not nearly as easy. The problem is that you need to modify a Node, not a Queue, in order to make the change to the last node that's required to dequeue an element. You actually need to replace the second-to-last Node in the Queue with a different Node whose "next" field is empty -- but since you're using atom identity to represent node uniqueness, that Node will actually be a different Node.

share|improve this answer
add comment

Your Answer


