Skip to content
flowss
Start freeChecking your session
Petri Nets templates

Petri — dining philosophers (2)

Two-philosopher version of the dining-philosophers problem.

Petri NetsUML & SoftwarePetri Nets syntax docs
Template previewPetri Nets
Dining philosophers (2)Phil 1 thinking≤1Phil 2 thinking≤1Fork A≤1Fork B≤1Phil 1 eating≤1Phil 2 eating≤1T1aenabledT1bT2aenabledT2bReachable 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 B + Phil 1 eating + Phil 2 eating = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observe…Conservation law: Fork A + Phil 1 eating + Phil 2 eating = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observe…Conservation law: Phil 2 thinking + Phil 2 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 …Conservation law: Phil 1 thinking + Phil 1 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 …

Make it your own.

title "Dining philosophers (2)"
place think1 tokens 1 "Phil 1 thinking"
place think2 tokens 1 "Phil 2 thinking"
place fork1 tokens 1 "Fork A"
place fork2 tokens 1 "Fork B"
place eat1 tokens 0 "Phil 1 eating"
place eat2 tokens 0 "Phil 2 eating"
transition T1a
transition T1b
transition T2a
transition T2b
think1 -> T1a
fork1 -> T1a
fork2 -> T1a
T1a -> eat1
eat1 -> T1b
T1b -> think1
T1b -> fork1
T1b -> fork2
think2 -> T2a
fork1 -> T2a
fork2 -> T2a
T2a -> eat2
eat2 -> T2b
T2b -> think2
T2b -> fork1
T2b -> fork2