Go backward to More About Invariance Proofs
Go up to Top
Go forward to Example

Eventuality Properties

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

Must be derived from fairness condition!

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