Go backward to Queue Component
Go up to Top
Go forward to Conjoining Specifications

Queue Component

Non-interleaving Specification

QMni <=> exists q: IQMni
IQMni <=> InitM and always [AMni]<i.ack, o.snd, q>
and WF<i.ack, o.snd, q>(AMni)
InitM <=> CInit(o) and (q = <>)

AMni <=> Enqni or Deqni or DeqEnqni

Ani <=> |q| < N
and Ack(i) and (q' = q o <i.val>)
and o.snd' = o.snd
Deqni <=> |q| > 0
and Send(Head(q), o) and (q' = Tail(q))
and (i.ack' = i.ack)
DeqEnqni <=> |q| > 0
and Send(Head(q), o)
and Ack(i) and q' = Tail(q) o <i.val>)

Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine

Prev Up Next