Go backward to TLA
Go up to Top
Go forward to Liveness as TLA Formulas
Adding Liveness
- Modified Phi also not acceptable:
- might be never changed!
- Phi only expresses safety property.
- Program must not execute other than described steps.
- Liveness properties:
- Something does eventually happen.
- Program must eventually perform described steps.
- Dijkstra semantics:
- Infinitely many steps increase or .
- Phi Init
and always A_<>
and always eventually A.
- Add fairness requirement:
- Infinitely many steps increase and .
- Phi Init
and always A_<>
and always eventually A and always eventually A.
Problem: Both are not TLA formulas!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine