Go backward to Adding Liveness
Go up to Top
Go forward to Fairness
Liveness as TLA Formulas
- always [A] is TLA formula.
- not always [not A]
eventually not [not A]
eventually not (not A or )
eventually (A and notequal )
- <A> A and notequal
- <A> is TLA formula.
- Reformulation of Phi:
- Phi Init
and always A_<>
and always eventually <A>_<>
and always eventually <A>_<>
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine