Semaphore mutual exclusion with a firing sequence

Scenario

Processes A and B each cycle Ready → Enter → Critical → Exit and back. A single Semaphore token is shared between them, so only one process can be in its critical section at a time. The net also replays a short run — A enters and leaves, then B enters — so you see the state after those three steps instead of the starting state.

Annotation key

• layout: lr — lay the net out left to right
• place Name *1 — a place holding one token at the start; no * means empty
• transition Name — an action that moves tokens
• A -> B — an arc from a place to a transition, or from a transition to a place
• fire: EnterA, ExitA, EnterB — transitions to fire in order, starting from the initial marking

How to read

The two process cycles mirror each other, with the Semaphore between them feeding both Enter transitions and refilled by both Exit transitions. After the firing sequence, A is back in ReadyA, B holds its token in CriticalB, and the Semaphore is empty. So EnterA cannot fire — it needs the semaphore token — and the only enabled transition is ExitB. No marking ever puts tokens in CriticalA and CriticalB together; that is the mutual-exclusion guarantee.