Go backward to
Adding Liveness
Go up to
Top
Go forward to
Fairness
Liveness as TLA Formulas
always
[
A
]
f
is TLA formula.
not
always
[
not
A
]
f
<=>
eventually
not
[
not
A
]
f
<=>
eventually
not
(
not
A
or
f'=f
)
<=>
eventually
(
A
and
f'
notequal
f
)
<
A
>
f
<=>
A
and
f'
notequal
f
<
A
>
f
is TLA formula.
Reformulation of
Phi
:
Phi
<=>
Init
Phi
and
always
A
_<
x, y
>
and
always
eventually
<
A
1
>_<
x, y
>
and
always
eventually
<
A
2
>_<
x, y
>
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998