---------------------------- MODULE dequeue0----------------------------
EXTENDS Status, FiniteSequences, Naturals
VARIABLES head, qTail, pc, mem, tail, nextNode, qHead, retVal, queue, out

CONSTANT Ref, T, null, N, empty, undef

ABS0[q \in FiniteSeq(T, N), h \in Ref \union {null}] == (h = null => Len(q)=0) /\
                   (h /= null => Len(q) /= 0 /\ mem[h][1]=Head(q) /\ ABS0[Tail(q), mem[h][2]])
ABS == ((qHead /= null /\ qTail /= null) =>
        (((mem[qTail][2] = null => (qTail = qHead \/ (Len(queue) /= 0 /\ mem[qTail][1] = queue[Len(queue)])))
        /\ (mem[qTail][2] /= null => (Len(queue) > 1 /\ mem[qTail][1] = queue[Len(queue)-1]) 
             \/ (Len(queue) = 1 /\ qTail = qHead))) 
      /\ ABS0[queue, mem[qHead][2]]))

INV ==  (pc=0 => ( qHead /= null 
                  /\ (qHead /= qTail => mem[qHead][2] /= null)))
    /\ (pc=19 => ( qHead /= null 
                  /\ (qHead /= qTail => mem[qHead][2] /= null)))

STATUS ==  ((pc = 0 => (TRUE))
            /\ (pc = 19 => (TRUE)))
	
Exec ==  (((pc = 33 /\ pc' = 34) \/ (pc = 52 /\ pc'= 53)) /\ TRUE) 
	 \/ (((pc = 21 /\ pc' = 22 /\ Len(queue) = 0)) /\ TRUE /\ UNCHANGED<<queue>>) 
	 \/ (((pc = 22 /\ pc' = 24 /\ Len(queue) = 0)) /\ ((TRUE) \/ (UNCHANGED<<queue>> 
                 /\ out' = out /\ UNCHANGED<<>>))) 
	 \/ (((pc = 22) \/ (pc = 26 /\ pc' /=  27)) /\ UNCHANGED<<queue>> /\ UNCHANGED<<>>) 

Init == /\ queue \in FiniteSeq(T, N) /\ qHead \in Ref \union {null} /\ qTail \in Ref \union {null}
        /\ mem \in [Ref ->(T \X (Ref \union {null})) \union {undef}] 
        /\ ABS 
        /\ head = null /\ pc = 0 /\ tail = null /\ nextNode = null /\ retVal = 0 
        /\ INV /\ out = 0 /\ STATUS
 

dequeue0 ==  pc = 0 /\ pc' = 19  /\ UNCHANGED<<head,qTail,mem,tail,nextNode,qHead,retVal,queue,out>> 

Spec ==  Init /\ [][dequeue0]_<<head, qTail, pc, mem, tail, nextNode, qHead, retVal, queue, out>> 

=============================================================================