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