Go backward to The Next-State Relation
Go up to Top
Go forward to Proving Psi Implements Phi
The Fairness Requirement
- Psi shall implement Phi.
- and must be incremented infinitely often.
- Infinitely many A and A steps must occur.
- Assume only A steps occur.
- Does WF(A) rule out this?
- Enabled alpha (pc = "a") and (0 <
sem).
- alpha is enabled and disabled infinitely often.
- <A> is disabled infinitely often.
- WF(A) still holds for this behavior!
- Does SF(A) rule out this?
- Either <A> is eventually disabled
forever, or infinitely many <A> steps occur.
- <A> is enabled infinitely often.
- SF(A) does not hold for this behavior!
Need strong fairness condition!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine