Go backward to Proposition
Go up to Top
Go forward to The Decomposition Theorem

Two Queues in Series

Components:
- Queue 1: exists $q$ ₁: Init_M^[1]
  and always [A_M^[1] and ( $o'=o$ )]_{<i.ack, z.snd, q₁>} and ICL^[1]
- Queue 2: exists $q$ ₂: Init_M^[2]
  and always [A_M^[2] and ( $i'=i$ )]_{<z.ack, o.snd, q₂>} and ICL^[2]
- Environment: Init_E
  and always [A_E and ( $z' = z$ )]_{<i.snd, o.ack>}
Interleaving representation required:
- Conjoining $o'=o$ , $i'=i$ , $z'=z$
From Proposition:
- Equivalence to CDQ

Wolfgang.Schreiner@risc.uni-linz.ac.at

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

Prev

Next