Go backward to Liveness as TLA Formulas
Go up to Top
Go forward to Fairness
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.
- Fairness:
- If operation possible, program must eventually execute it.
- Weak fairness:
- Operation must be executed if it remains possible to do so for long
enough time.
- (eventually executed) or (eventually impossible)
- Strong fairness:
- Operation must be executed if it is often enough possible to do
so.
- (eventually executed) or (eventually always impossible)
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine