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 , , 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.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine