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], ) is
machine-closed
Init and always [A] and does not add
additional safety properties.
- If is conjunciton of conditions WF(A) and/or
SF(A), where each <A> implies
A, then Init and always [A] and is
machine-closed.
- Fairness requirements:
- Rewrite
always eventually <A>_<>
and always eventually <A>_<> as fairness
conditons.
- Enabled <A>_<> =
Enabled <A>_<> = true
- WF_<>(A) =
always eventually <A>_<>
WF_<>(A) =
always eventually <A>_<>
- Phi Init
and always A_<>
andWF_<>(A)
and WF_<>(A)
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine