Declare a net — places, transitions, rates — and simulate it, fit it, and verify it without leaving the same model.
Arc topology is the rate law: a double arc fires quadratically with concentration, a weighted arc scales a flow. Start with ODE — the fastest way to watch a model move — then reach for exact stochastic simulation, parameter fitting, or formal verification against the same declared net.
| Model | Simulate | Fit | Verify |
|---|---|---|---|
| Places, transitions, weighted arcs — stored as JSON-LD with content-addressed identity. Arc topology is the rate law: a double arc makes a transition fire quadratically with concentration. | Tsit5/RK45 ODE relaxation, exact Gillespie SSA, and chemical-Langevin SDE — three semantics from one declaration. | Gradient-free and gradient-based (forward + adjoint sensitivity) parameter fitting. Every fitted value is still a transition rate. | Reachability, P/T-invariants, and declarative property checking with proved/refuted/unknown verdicts and counterexamples. |
| pflow.xyz | go-pflow/solver | go-pflow/learn | go-pflow/verify |
Same declared model, byte-exact across languages: JS (pflow.xyz), Go (go-pflow), Rust (pflow-rs), and Julia (pflow-jl, bridged to AlgebraicPetri.jl).
| Demo | What it shows | Link |
|---|---|---|
| Predator-Prey | Lotka-Volterra dynamics, continuous simulation | Run |
| Enzyme Kinetics | Michaelis-Menten, biochemical modeling | Run |
| Knapsack | Optimization via mass-action kinetics | Run |
| ODE Simulation & Prediction | Walkthrough of the solver itself | Run |
ODE is the fastest way to see a model move, not the whole toolkit — the same declared net also drives exact stochastic simulation, parameter fitting, and formal verification (see the table above). More examples — discrete state machines, workflows, ZK proofs, games — live one level down, in the individual project READMEs below.
| Repository | Purpose |
|---|---|
| go-pflow | Core Go library. ODE/SSA/SDE engines, parameter fitting, reachability & verification. The reference implementation. |
| pflow-xyz | Visual editor + browser ODE simulator, held byte-exact to go-pflow. |
| pflow-rs | Rust port — ODE solvers, token-model DSL, ZK provers. |
| pflow-jl | Julia port, bridged to AlgebraicPetri.jl for categorical composition and mass-action ODEs. |
| petri-pilot | MCP server for AI-assisted model design + deterministic app generation from a validated model. |
| book-pflow-xyz | "Petri Nets as a Universal Abstraction" — practitioner's guide. |
Model (pflow.xyz) ──▶ go-pflow (ODE · SSA · SDE · fit · verify) ──▶ pflow-rs / pflow-jl (byte-exact ports)
│
▼
petri-pilot (app generation, MCP)
petri-pilot exposes MCP tools so an agent can design, simulate and verify a model directly:
claude mcp add --transport http petri-pilot https://pilot.pflow.xyz/mcp
petri_validate → Check model structure
petri_simulate → Fire transitions, trace state (ODE/SSA/SDE)
petri_analyze → Reachability, deadlocks, liveness
petri_codegen → Generate Go backend
petri_application → Full-stack app from high-level spec
petri_extend → Modify existing models
The LLM designs the net. The engines decide what it does. No LLM-generated math in the output.
- Visual Editor: pflow.xyz
- ODE Engine: go-pflow
- Demos: pilot.pflow.xyz
- Book: book.pflow.xyz
- Blog: blog.stackdump.com
