Non-interleaving Specification
QM exists : IQM
IQM Init
and always [A]
and WF(A)
Init CInit() and ( = <>)
A Enq or Deq
or DeqEnq
A ||
and Ack() and ( = o <>)
and ' =
Deq || 0
and Send(Head(), )
and ( = Tail())
and ()
DeqEnq || 0
and Send(Head(), )
and Ack()
and = Tail() o <>)