Go backward to TLA
Go up to Top
Go forward to Liveness as TLA Formulas

Adding Liveness

Modified Phi also not acceptable:
- $x,y$ 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 $x$ or $y$ .
- Phi $<=>$ Init_Phi and always A_< $x, y$ > and always eventually A.
Add fairness requirement:
- Infinitely many steps increase $x$ and $y$ .
- Phi $<=>$ Init_Phi and always A_< $x, y$ > and always eventually A₁ and always eventually A₂.

Problem: Both are not TLA formulas!

Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine