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.