Go backward to Interleaving Representations
Go up to Top
Go forward to TLA Specification of Queue
The Queue Example
- Channel is initially ready for sending:
- () ()
- Sending a value on channel
- (, )
and = <, >
and
- Acknowledging recept of value on
- () notequal
and
and
- Representation as complete system
- Add environment that sends arbitrary numbers over and
acknowledges values on .
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine