Queue Component

Non-interleaving Specification

QM$ni$ exists $q$: IQM$ni$
IQM$ni$ Init$$_M and always [A$$_Mⁿⁱ]$$_{<i.ack, o.snd, q>}
and WF$$_{<i.ack, o.snd, q>}(A$$_Mⁿⁱ)
Init$$_M CInit($o$) and ($q$ = <>)

A$$_Mⁿⁱ Enq$ni$ or Deq$ni$ or DeqEnq$ni$

A$ni$ |$q$| $N$
and Ack($i$) and ($q\text{'}$ = $q$ o <$i.val$>)
and $o.snd$' = $o.snd$
Deq$ni$ |$q$| $>$ 0
and Send(Head($q$), $o$) and ($q\text{'}$ = Tail($q$))
and ($i.ack\text{'}\; =\; i.ack$)
DeqEnq$ni$ |$q$| $>$ 0
and Send(Head($q$), $o$)
and Ack($i$) and $q\text{'}$ = Tail($q$) o <$i.val$>)