Model, simulate, and generate applications from Petri nets
Define any system as places, transitions, and arcs — then generate Go backends, ES module frontends, and GraphQL APIs from a single model.
Petri nets are a mathematical formalism for modeling systems with state and flow —
from business workflows and game mechanics to biochemical reactions and network protocols.
Draw models visually, generate full-stack
applications here, and prove
execution with zero-knowledge proofs.
Define places (state), transitions (actions), and
arcs (connections). Petri-Pilot supports several
model types, each suited to a different class
of problem.
Browse all models, visualize their structure, and run ODE simulations. Design new nets from scratch with pflow.xyz, then generate code here.
Paste code, get a Petri net. Analyzes source code structure — state machines, control flow, concurrency, resource pools — and produces a formal, executable Petri net model. Any language.
Start here. Places, transitions, arcs, and tokens — the four concepts behind every demo on this site. A visual primer with interactive examples, no math required.
Patterns and properties. State machines, fork/join, resource pools, mutual exclusion, deadlock — the design patterns behind every demo, with a suggested learning path.
How structure becomes behavior. Mass-action kinetics turns any Petri net into a system of differential equations. See how the Tic-Tac-Toe net discovers strategy without search.
Prove without revealing. How gnark circuits verify Petri net transitions cryptographically — MiMC hashing, enabledness checks, and Groth16 proofs from net topology alone.
Petri net → ODE → ZK → on-chain. A 33-place, 35-transition Petri net defines the state machine, an ODE solver derives scores, a Groth16 proof verifies the computation, and a contract checks consistency at ~450k gas.
MCP tools for Claude and any AI agent. Design models, simulate behavior, generate full-stack apps, seal models with invariants, and browse the public catalog — all from your AI assistant via Smithery.
Turn-based and concurrent games where tokens represent game state and transitions encode legal moves.
Introductory model. Nine board cells as places, player moves as transitions. ODE simulation computes strategic value from net topology alone.
Zero-knowledge variant. Same game, but moves are verified cryptographically using gnark circuits. Proves valid play without revealing strategy.
Multi-player state machine. Five players, four betting rounds, role-based actions (fold, check, raise). Turn tokens control whose transition fires next.
Systems where tokens represent consumable or reusable resources with capacity constraints and flow rates.
Inventory and flow. Weighted arcs consume beans, milk, and cups per order. Rates drive continuous flow. The ODE predicts when supplies run out.
Optimization. Classic 0/1 knapsack as a Petri net. Items compete for limited capacity via mass-action kinetics. ODE reveals optimal item selection.
Bounded buffer. A producer and consumer share a fixed-size buffer. Capacity tokens block the producer when full and the consumer when empty.
Scheduling simulator. Staff, rooms, and equipment as resource tokens. Service mix routing with piecewise ODE. Financial dashboard tracks revenue and utilization.
Lotka-Volterra dynamics. Two places and three transitions produce classic population oscillations via mass-action kinetics. Tune parameters and observe phase-space orbits.
Michaelis-Menten. Substrate binds enzyme to form a complex, which either unbinds or catalyzes into product. Four places and three transitions produce the classic saturation curve.
Business processes with sequential stages, parallel branches, role-based access, and fork-join synchronization.
Fork-join pipeline. Parallel credit and employment reviews with role-based access. The Petri net enforces the synchronization barrier before final decision.
Multi-stage process. Phone screen, parallel technical and culture interviews, then offer. Four roles (recruiter, engineer, manager, candidate) control different stages.
Protocol state machines and control systems where discrete state changes drive system behavior.
Protocol state machine. The classic 3-way handshake (SYN, SYN-ACK, ACK) and connection teardown as two parallel state machines linked by shared transitions.
Feedback control. A bang-bang controller with ODE dynamics. Temperature rises when the heater is on and decays naturally. Watch the feedback loop oscillate around the setpoint.
Concurrency and deadlock. Five philosophers, five forks, one classic problem. Step through transitions to observe mutual exclusion and circular wait.
Cyclic state machine. A traffic light cycling through red, green, and yellow. The simplest example of a live, bounded Petri net with no deadlocks.
Binomial distribution. 256 balls drop through 8 rows of pegs. Each peg is two competing transitions. Topology alone produces Pascal's triangle.
Pattern-matching nets where tokens flow through structural detectors. No code — the net topology itself is the classifier.