Go backward to Describing Programs with RTLA
Go up to Top
Go forward to Adding Liveness
TLA
- Formula Phi is too simple.
- Should allow stuttering steps
- Leave both and unchanged.
- Example: clock specification.
- Clock with hours and minutes .
- Clock with hours , minutes , seconds .
- should statisfy specification of .
- But has 59 steps where and do not change!
- Such stuttering steps should be ignored.
- Modification of Phi:
- Phi Init
and always (A or ( and))
- Phi Init
and always A_<>
- [A] := A or
- TLA is subset of RTLA
- Elementary formulas of form always [A]
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine