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
(x=0)
.
Consequence:
x
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)
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998