- Something
*eventually*happens. - Termination
`eventually``terminated`.

- Service
- If process has requested service, it is eventually served.
`requested`$|->$`served`.

- Message delivery
- If a message is sent often enough, it is eventually delivered.
- (
`always``eventually``sent`) $=>$`eventually``delivered`.

- $P$ $|->$ $Q$.
`Phi`*and*($n$ in**Nat**) $=>$`eventually`($x>n$)`Phi`$=>$(($n$ in**Nat***and*$x=n$) $|->$`eventually`($x=n+1$))

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

$$Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine $$