Petri Net Workflow Demo
Mountain refuge shed tasklet preloaded — click transitions to fire, or use the 5 “explainer” buttons.
Net view (SVG)
Ready Click a transition ▭ to fire
Legend: ▭ transition, ◯ place. Enabled transitions glow green; click to fire. S-invariants highlight places in amber.
Tip: Use Branch Explorer when multiple transitions are enabled — each click forks a new schedule path tab.
Explainers + Panels
Paths (forked schedules)
—
Markings = “what’s true right now”. Different path tabs = different feasible schedules (different firing sequences).
Marking Panel
green = pre-places satisfied for an enabled transition
PlaceidTokens
Sequence Panel
click breadcrumb to rewind
Goal (JSON)
Example: {"painted":1} or {"complete":1,"crew":2}. Place ids are in the table.
Audit Panel (live JSON receipt)

            


            

              
Conservation (S-invariants)

              

              

                Click ∑ Show Conservation to compute invariants from the incidence matrix (kernel of Cᵀ).
              

            


            

              
Reachability result

              

              

                The reachability check is a bounded BFS from M₀ (initial marking) — if goal is found it shows a witness firing sequence; otherwise it shows a deadlock frontier and which preconditions fail.