Go backward to
Fairness
Go up to
Top
Go forward to
Examining Formula Phi
Rewriting the Fairness Requirement
Machine-closed
Pair (
Init
and
always
[
A
]
f
,
F
) is
machine-closed
<=>
Init
and
always
[
A
]
f
and
F
does not add additional safety properties.
If
F
is conjunciton of conditions WF
f
(
A
) and/or SF
f
(
A
), where each <
A
>
f
implies
A
, then
Init
and
always
[
A
]
v
and
F
is machine-closed.
Fairness requirements:
Rewrite
always
eventually
<
A
1
>_<
x, y
>
and
always
eventually
<
A
2
>_<
x, y
> as fairness conditons.
Enabled
<
A
1
>_<
x, y
> =
Enabled
<
A
2
>_<
x, y
> =
true
WF_<
x, y
>(
A
1
) =
always
eventually
<
A
1
>_<
x, y
>
WF_<
x, y
>(
A
2
) =
always
eventually
<
A
2
>_<
x, y
>
Phi
<=>
Init
Phi
and
always
A
_<
x, y
>
and
WF_<
x, y
>(
A
1
)
and
WF_<
x, y
>(
A
2
)
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998