Skip to content
flowss
Start freeChecking your session
Petri Nets templates

Dining philosophers (2 of 5)

Compact two-philosopher slice of the classic deadlock-prone Petri net — thinking, hungry, eating, with forks as shared resources.

Petri NetsUML & SoftwarePetri Nets syntax docs
Template previewPetri Nets
Dining philosophers (slice)P1 thinking≤1P2 thinking≤1Fork 1≤1Fork 2≤1P1 picks forksenabledP2 picks forksenabledP1 eating≤1P2 eating≤1P1 doneP2 doneReachable markings36 places · 4 transitionsTerminatesneverruns for everLive transitions4/4every one firesSafe places6/6bound ≤ 1 tokenConservation laws4every place covered3 reachable markings, 6 places, 4 transitions — bounded, deadlock-free, and every transition fires.Conservation law: Fork 2 + P1 eating + P2 eating = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed over a…Conservation law: Fork 1 + P1 eating + P2 eating = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed over a…Conservation law: P2 thinking + P2 eating = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed over a search.Conservation law: P1 thinking + P1 eating = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed over a search.

Make it your own.

title Dining philosophers (slice)

place P1_Think  tokens 1 "P1 thinking"
place P2_Think  tokens 1 "P2 thinking"
place F1        tokens 1 "Fork 1"
place F2        tokens 1 "Fork 2"

transition T1_Pick "P1 picks forks"
transition T2_Pick "P2 picks forks"
place P1_Eat "P1 eating"
place P2_Eat "P2 eating"
transition T1_Done "P1 done"
transition T2_Done "P2 done"

P1_Think -> T1_Pick
F1       -> T1_Pick
F2       -> T1_Pick
T1_Pick  -> P1_Eat

P1_Eat   -> T1_Done
T1_Done  -> F1
T1_Done  -> F2
T1_Done  -> P1_Think

P2_Think -> T2_Pick
F2       -> T2_Pick
F1       -> T2_Pick
T2_Pick  -> P2_Eat

P2_Eat   -> T2_Done
T2_Done  -> F2
T2_Done  -> F1
T2_Done  -> P2_Think