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>.
- impossible not Enabled <A>.
- Fairness conditions:
- WF(A) (always eventually <A
>) or (always eventually not Enabled <A>)
- SF(A) (always eventually <A
>) or (eventually always not Enabled <A>)
- SF(A) WF(A)
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine