Go backward to Proving Psi Implements Phi
Go up to Top
Go forward to Hiding Variables

Proof of Fairness

Psi => WF_<x,y>(A₁)
- $x$ is incremented infinitely often.
- Application of SF₂.
- Use beta₁ for A.
- Strengthen A by invariant I through application of INV2.
- I $<=>$ x in Nat
  and (((sem=1) and (pc₁ = pc₂ = "a"))
     or ((sem=0)
        and (((pc₁ = "a") and (pc₂ in {"b", "g"}))
           or ((pc₂ = "a")
              and (pc₁ in {"b", "g"})))))

For details, see the paper.

Wolfgang.Schreiner@risc.uni-linz.ac.at

Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine

Prev

Next