Skip to content
flowss
Start freeChecking your session
Petri Nets templates

Producer / consumer

Bounded buffer between a producer and a consumer — tokens represent buffer slots and items.

Petri NetsUML & SoftwarePetri Nets syntax docs
Template previewPetri Nets
Producer / ConsumerProducer ready≤1produceenabledBuffer≤3Free slots≤3consumeConsumer ready≤1Reachable 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: Buffer + Free 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 search.Conservation law: Consumer ready = 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 ready = 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 Producer / Consumer

place    P_Ready  tokens 1 "Producer ready"
transition T_Produce "produce"
place    Buffer   tokens 0 "Buffer"
place    Slots    tokens 3 "Free slots"
transition T_Consume "consume"
place    C_Ready  tokens 1 "Consumer ready"

P_Ready -> T_Produce
Slots   -> T_Produce
T_Produce -> Buffer
T_Produce -> P_Ready

Buffer  -> T_Consume
C_Ready -> T_Consume
T_Consume -> Slots
T_Consume -> C_Ready