Go backward to The Formula Psi
Go up to Top
Go forward to The Fairness Requirement

The Next-State Relation

alpha₁ step:
- Starts in state with pc₁ = "a" (first process is at control point alpha₁) and 0 $<$ sem (no process in critical section).
- Ends in staet with pc₁ = "b" (first process is at control point beta₁).
- Decrements sem and does not change $x$ , $y$ , pc₂.
A₁ step:
- alpha₁ step or beta₁ step or gamma₁ step.
- Execution of atomic operation by first process.
A step:
- Step of either process.
- The program's next-state relation.

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