Go backward to Implementation
Go up to Top
Go forward to Specification

Two Queues in Series

ICDQ <=> InitE and Init[1]M and Init[2]M
and always [(QE and <q1, q2, z>' = <q1, q2, z>)
   or (Q[1]M and <q2, o>' = <q2, o>)
   or (Q[2]M and <q1, i>' = <q1, i>)]<i, o, z, q1, q2>
and ICL[1] and ICL[2]
CDQ <=> exists q1, q2: ICDQ

Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine

Prev Up Next