Skip to content
flowss
Start freeChecking your session
Petri Nets templates

Petri — producer / consumer

Bounded-buffer producer / consumer with capacity 3.

Petri NetsUML & SoftwarePetri Nets syntax docs
Template previewPetri Nets
Bounded bufferEmpty slots≤3Filled slots≤3Producer idle≤1Consumer idle≤1ProduceenabledConsumeReachable markings44 places · 2 transitionsTerminatesneverruns for everLive transitions2/2every one firesSafe places2/4bound ≤ 1 tokenConservation laws3every place covered4 reachable markings, 4 places, 2 transitions — bounded, deadlock-free, and every transition fires.Conservation law: Empty slots + Filled slots = 3, 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 sea…Conservation law: Consumer idle = 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: Producer idle = 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 "Bounded buffer"
place ready tokens 3 "Empty slots"
place full  tokens 0 "Filled slots"
place prod  tokens 1 "Producer idle"
place cons  tokens 1 "Consumer idle"
transition P "Produce"
transition C "Consume"
prod -> P
ready -> P
P -> full
P -> prod
cons -> C
full -> C
C -> ready
C -> cons