Go backward to More About Invariance Proofs
Go up to Top
Go forward to Example
Must be derived from fairness condition!
- Something eventually happens.
- 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.
- Phi and ( in Nat) eventually ()
- Phi (( in Nat and )
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine