Go backward to Liveness as TLA Formulas
Go up to Top
Go forward to Fairness
- Arbitrary liveness properties dangerous:
- Used to express fairness requirements.
- May unexpectedly add safety properties.
- Add: always eventually .
- Consequence: never changes!
- Solution: express liveness by fairness.
- If operation possible, program must eventually execute it.
- Weak fairness:
- Operation must be executed if it remains possible to do so for long
- (eventually executed) or (eventually impossible)
- Strong fairness:
- Operation must be executed if it is often enough possible to do
- (eventually executed) or (eventually always impossible)
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine