Skip to content
flowss
Start freeChecking your session
Petri Nets templates

Petri — mutex (binary semaphore)

Two processes contending for a single shared resource.

Petri NetsUML & SoftwarePetri Nets syntax docs
Template previewPetri Nets
Binary semaphoreProcess 1 ready≤1Process 2 ready≤1Mutex≤1Process 1 in CS≤1Process 2 in CS≤1T1aenabledT1bT2aenabledT2bReachable markings35 places · 4 transitionsTerminatesneverruns for everLive transitions4/4every one firesSafe places5/5bound ≤ 1 tokenConservation laws3every place covered3 reachable markings, 5 places, 4 transitions — bounded, deadlock-free, and every transition fires.Conservation law: Mutex + Process 1 in CS + Process 2 in CS = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not obse…Conservation law: Process 2 ready + Process 2 in CS = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed ove…Conservation law: Process 1 ready + Process 1 in CS = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed ove…

Make it your own.

title "Binary semaphore"
place P1 tokens 1 "Process 1 ready"
place P2 tokens 1 "Process 2 ready"
place lock tokens 1 "Mutex"
place C1 tokens 0 "Process 1 in CS"
place C2 tokens 0 "Process 2 in CS"
transition T1a
transition T1b
transition T2a
transition T2b
P1 -> T1a
lock -> T1a
T1a -> C1
C1 -> T1b
T1b -> P1
T1b -> lock
P2 -> T2a
lock -> T2a
T2a -> C2
C2 -> T2b
T2b -> P2
T2b -> lock