Petri-Pilot

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.

Model Types

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.

Tools

Petri Net Viewer

Browse all models, visualize their structure, and run ODE simulations. Design new nets from scratch with pflow.xyz, then generate code here.

editor visualization ODE
🔄

Code to Flow

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.

converter any language AI
📚

What is a Petri Net?

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.

beginner primer visual
🧩

Thinking in Petri Nets

Patterns and properties. State machines, fork/join, resource pools, mutual exclusion, deadlock — the design patterns behind every demo, with a suggested learning path.

patterns concurrency design
📈

ODE Simulation & Prediction

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.

ODE mass-action analysis
🔐

Zero-Knowledge Proofs

Prove without revealing. How gnark circuits verify Petri net transitions cryptographically — MiMC hashing, enabledness checks, and Groth16 proofs from net topology alone.

gnark ZK proofs Groth16

Verifiable Computation

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.

Groth16 177k constraints ~450k gas
🤖

AI Agent Integration

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.

MCP Claude Smithery

Games

GameNet

Turn-based and concurrent games where tokens represent game state and transitions encode legal moves.

Tic-Tac-Toe

Introductory model. Nine board cells as places, player moves as transitions. ODE simulation computes strategic value from net topology alone.

beginner ODE strategy
🔒

ZK Tic-Tac-Toe

Zero-knowledge variant. Same game, but moves are verified cryptographically using gnark circuits. Proves valid play without revealing strategy.

zk-proofs gnark verification
🃏

Texas Hold'em

Multi-player state machine. Five players, four betting rounds, role-based actions (fold, check, raise). Turn tokens control whose transition fires next.

roles guards events

Resources

ResourceNet

Systems where tokens represent consumable or reusable resources with capacity constraints and flow rates.

Coffee Shop

Inventory and flow. Weighted arcs consume beans, milk, and cups per order. Rates drive continuous flow. The ODE predicts when supplies run out.

capacity weighted arcs rates
🎒

Knapsack

Optimization. Classic 0/1 knapsack as a Petri net. Items compete for limited capacity via mass-action kinetics. ODE reveals optimal item selection.

optimization ODE mass-action
📦

Producer-Consumer

Bounded buffer. A producer and consumer share a fixed-size buffer. Capacity tokens block the producer when full and the consumer when empty.

synchronization capacity concurrency
🏥

Vet Clinic

Scheduling simulator. Staff, rooms, and equipment as resource tokens. Service mix routing with piecewise ODE. Financial dashboard tracks revenue and utilization.

scheduling ODE simulation
🐺

Predator-Prey

Lotka-Volterra dynamics. Two places and three transitions produce classic population oscillations via mass-action kinetics. Tune parameters and observe phase-space orbits.

ODE ecology mass-action
🧬

Enzyme Kinetics

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.

biochemistry ODE Michaelis-Menten

Workflows

WorkflowNet

Business processes with sequential stages, parallel branches, role-based access, and fork-join synchronization.

🏦

Loan Approval

Fork-join pipeline. Parallel credit and employment reviews with role-based access. The Petri net enforces the synchronization barrier before final decision.

BPMN roles fork-join
👔

Hiring Pipeline

Multi-stage process. Phone screen, parallel technical and culture interviews, then offer. Four roles (recruiter, engineer, manager, candidate) control different stages.

BPMN roles kanban

Computation

ComputationNet

Protocol state machines and control systems where discrete state changes drive system behavior.

🔌

TCP Handshake

Protocol state machine. The classic 3-way handshake (SYN, SYN-ACK, ACK) and connection teardown as two parallel state machines linked by shared transitions.

protocol state machine networking
🌡

Thermostat

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.

control feedback ODE
🍴

Dining Philosophers

Concurrency and deadlock. Five philosophers, five forks, one classic problem. Step through transitions to observe mutual exclusion and circular wait.

concurrency deadlock mutual exclusion
🚦

Stoplight

Cyclic state machine. A traffic light cycling through red, green, and yellow. The simplest example of a live, bounded Petri net with no deadlocks.

state machine cyclic bounded
🔻

Galton Board

Binomial distribution. 256 balls drop through 8 rows of pegs. Each peg is two competing transitions. Topology alone produces Pascal's triangle.

probability topology mass-action

Classification

ClassificationNet

Pattern-matching nets where tokens flow through structural detectors. No code — the net topology itself is the classifier.

🃑

Poker Hand

Structural classifier. Cards are tokens in rank and suit places. Pattern-detection transitions fire when the right combination is present — pairs, flushes, straights, full houses.

pattern detection combinatorics tokens