- 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 $x$
- 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 $x$

Wolfgang.Schreiner@risc.uni-linz.ac.at

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