qstate qout STAUTDEF queueStaut [ Inp :: QueueOp; Outp :: Int ] ( ) ::= STATE qstate, qout VAR buf :: IntList INIT qstate { buf := Nil } Inp ? qop [[ isDeq(qop) /\ not(isNil(buf)) ]] Outp ! hd(buf) { buf := tl(buf) } Inp ? qop [[ isEnq(qop) ]] { buf := add(val(qop),buf) } Inp ? qop [[ isDeq(qop) /\ isNil(buf) ]]