Go backward to
Fairness
Go up to
Top
Go forward to
Rewriting the Fairness Requirement
Fairness
Fairness at all times:
always
((
eventually
executed)
or
(
eventually
impossible))
always
((
eventually
executed)
or
(
eventually
always
impossible))
Equivalent to:
(
always
eventually
executed)
or
(
always
eventually
impossible)
(
always
eventually
executed)
or
(
eventually
always
impossible))
Formalization:
executed
<=>
<
A
>
f
.
impossible
<=>
not
Enabled
<
A
>
f
.
Fairness conditions:
WF
f
(
A
)
<=>
(
always
eventually
<
A
>
f
)
or
(
always
eventually
not
Enabled
<
A
>
f
)
SF
f
(
A
)
<=>
(
always
eventually
<
A
>
f
)
or
(
eventually
always
not
Enabled
<
A
>
f
)
SF
f
(
A
)
=>
WF
f
(
A
)
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998