Go backward to TLAGo up to TopGo forward to Liveness as TLA Formulas |

- 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`.

- Infinitely many steps increase
- Add fairness requirement:
- Infinitely many steps increase
*x**and**y*. `Phi`*<=>*`Init`_{Phi}*and*`always``A`_<*x, y*>*and*`always``eventually``A`_{1}*and*`always``eventually``A`._{2}

- Infinitely many steps increase

*Problem: Both are not TLA formulas!*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998