The Fairness Requirement
- Psi shall implement Phi.
- x and y must be incremented infinitely often.
- Infinitely many A1 and A2 steps must occur.
- Assume only A2 steps occur.
- Does WFw(A1) rule out this?
- Enabled alpha1 <=> (pc1 = "a") and (0 <
sem).
- alpha1 is enabled and disabled infinitely often.
- <A1>w is disabled infinitely often.
- WFw(A1) still holds for this behavior!
- Does SFw(A1) rule out this?
- Either <A1>w is eventually disabled
forever, or infinitely many <A1>w steps occur.
- <A1>w is enabled infinitely often.
- SFw(A1) does not hold for this behavior!
Need strong fairness condition!
Author: Wolfgang Schreiner
Last Modification: May 14, 1998