Go backward to The Queue Example
Go up to Top
Go forward to Implementation
TLA Specification of Queue
- Environment actions
- ()
- (exists in Nat: (,))
and ()
- () and ()
- or
- Component actions
- () and ( = <>)
- || and ()
and ( = o <>)
and ()
- || 0
and ((), )
and ( = ()) and ()
- or
- Complete System Specification
-
WF()
- and
and always [( and ()) or ]
and
- exists :
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine