Skip to content
pflow-xyzPublic

About

Petri net library — ODE, SSA & SDE simulation, parameter fitting, and formal verification, in Go

Topics

Resources

Stars

11 stars

Watchers

1 watching

Forks

Latest commit

 

History

281 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

go-pflow

A Petri-net dynamical modeling engine in Go. You declare one model — places, transitions, arcs, rates — and go-pflow runs it under three simulation semantics from that single declaration: a deterministic mass-action ODE relaxation, an exact SSA jump process (Gillespie), and a chemical-Langevin SDE with the net's own intrinsic firing noise. Around the engines sit system identification and parameter fitting (gradient-free, and gradient-based with forward or adjoint sensitivities), structural analysis and verification (reachability, P/T-invariants, declarative properties with proved / refuted / unknown verdicts and counterexamples), and a cross-language compatibility contract: byte-exact SSA and editor-shape parse goldens held against the pflow.xyz JavaScript engine, with pflow-rs replaying the SSA half and pflow-jl replaying both on a branch not yet merged to its default (see Compatibility for the full matrix).

For the long form, read the book; for why the byte-exact contract exists, the four-language SSA writeup.

What go-pflow is, and is not

It is

  • a Go library: the modeling and runtime core of the pflow ecosystem;
  • one declared net, three engines — stochastic.Solve dispatches to ODE, SSA or SDE, and refuses combinations it cannot honour rather than guessing (see Which engine for which question);
  • a fitting toolkit that learns rates while preserving structure — every fitted parameter is a transition rate, and the fitted model is still analyzable;
  • a verification toolkit whose verdicts carry a method (structural, exhaustive, witness, partial) and, on refutation, a replayable trace (see Model correctness);
  • the reference reading of the pflow.xyz editor format.

It is not

  • an AI/ML library. It implements structural, dynamical computation based on Petri nets and differential equations. learn fits mechanistic models, not opaque ones; see Why Petri Nets?;
  • an MCP server. MCP orchestration — the petri_* tools an agent calls — lives in petri-pilot, which imports this library;
  • a service. Nothing here listens on a port by default;
  • the editor. pflow.xyz is the editor; this repo parses what it saves.

Architecture

flowchart LR
    subgraph model [Model]
        JSONLD["pflow.xyz JSON-LD<br/>(editor shape, CID identity)"]
        P["parser.ModelFromJSON"]
        MM["metamodel.Model<br/>(engine input, shape B)"]
        JSONLD --> P --> MM
    end
    subgraph engines [Engines]
        ODE["solver<br/>ODE relaxation"]
        SSA["stochastic<br/>SSA jump process"]
        SDE["stochastic<br/>SDE chemical Langevin"]
    end
    subgraph learn [Learn]
        FIT["learn / stochastic.FitDiscrete<br/>fitting, forward + adjoint sensitivities"]
    end
    subgraph analysis [Analysis]
        R["reachability<br/>state space, invariants"]
        V["verify<br/>properties, verdicts"]
        M["mining / eventlog<br/>discovery, conformance"]
    end
    subgraph surfaces [Surfaces]
        PILOT["petri-pilot<br/>MCP tools"]
        PORTS["pflow-xyz JS, pflow-jl, pflow-rs<br/>held to shared goldens"]
    end
    MM --> ODE & SSA & SDE
    ODE & SSA --> FIT
    MM --> R & V & M
    engines & learn & analysis --> PILOT
    MM -. "cross-language goldens" .-> PORTS
Loading

Two JSON shapes, one rule

shape role
pflow.xyz JSON-LD (@context: https://pflow.xyz/schema; places and transitions keyed by id, source/target, per-color vectors, inhibitTransition, CID as @id) the editor's wire and identity format. Every saved model is addressed by a CID over it, so it does not change.
metamodel (arrays of {id}, from/to, type: read|inhibitor, kinetic, rate, schedule, stages, parameters) the only shape the engines and analyses read.

The rule: an editor document reaches an engine through exactly one converter, parser.ModelFromJSON. Colors unfold to place.color, an output-side inhibitor becomes an explicit read arc, per-color capacity is summed. The seven goldens under parser/testdata/editor-shape/ pin that reading (go run ./cmd/shape-goldens regenerates them). pflow-xyz keeps byte-identical copies as parity/editor-shape/ and replays them in CI from public/petri-shape_test.ts; pflow-jl keeps the same bytes as test/testdata/editor-shape/ and replays them from test/test_editor_shape.jl, but on its algebraic-petri branch — not yet on its default branch, main. pflow-rs has no editor-shape parser yet; it replays the SSA goldens, plus (a separate contract) go-pflow's ODE parity corpus and the generated-learn goldens.

Installation

go get github.com/pflow-xyz/go-pflow

Quick start

The canonical end-to-end example is the café:

go run ./examples/cafe

It walks one model through the whole stack — declare, observe, fit, ODE / SSA / SDE, compare the engines, sensitivities, verify — and ends at the same model the petri-pilot MCP tools serve. It reuses the café fixtures from the pflow showcase rather than inventing a toy. Which engine to believe on which question is docs/engine-selection.md; the capability table is docs/solver-matrix.md.

The smallest program that shows the dispatch:

m := &metamodel.Model{
    Name: "sir",
    Places: []metamodel.Place{
        {ID: "S", Initial: 990}, {ID: "I", Initial: 10}, {ID: "R"},
    },
    Transitions: []metamodel.Transition{
        {ID: "infect", Rate: 0.0005}, {ID: "recover", Rate: 0.1},
    },
    Arcs: []metamodel.Arc{
        {From: "S", To: "infect"}, {From: "I", To: "infect"}, {From: "infect", To: "I", Weight: 2},
        {From: "I", To: "recover"}, {From: "recover", To: "R"},
    },
}

for _, method := range []stochastic.Method{stochastic.MethodODE, stochastic.MethodSSA, stochastic.MethodSDE} {
    res, err := stochastic.Solve(m, nil, stochastic.Options{
        Method: method, Horizon: 40, Samples: 81, Realizations: 100, Seed: 42,
    })
    if err != nil {
        log.Fatal(err)
    }
    fmt.Println(res.Method, "final R:", res.Final["R"], "caveats:", res.Caveats)
}

The three answers agree on the mean here because no input arc has weight above one and nothing gates a firing. Add a read arc, an inhibitor or a reached capacity and the ODE and SDE paths set Diverged and say why instead of returning a smooth curve for a constrained system.

The petri builder and solver remain the direct ODE path when you have no metamodel:

net, rates := petri.Build().
    Place("S", 999).Place("I", 1).Place("R", 0).
    Transition("infect").Transition("recover").
    Arc("S", "infect", 1).Arc("I", "infect", 1).Arc("infect", "I", 2).
    Arc("I", "recover", 1).Arc("recover", "R", 1).
    WithCustomRates(map[string]float64{"infect": 0.3, "recover": 0.1})

prob := solver.NewProblem(net, net.SetState(nil), [2]float64{0, 100}, rates)
sol := solver.Solve(prob, solver.Tsit5(), solver.DefaultOptions())
fmt.Println("Final state:", sol.GetFinalState())

See The go-pflow Library for the full API guide.

What you can model, and where the edges are

The formalism is Turing-complete once inhibitor arcs are in play, so the question is never can it be expressed but whether the tooling makes it natural. Natural today:

  • Anything with a discrete state and countable resources — workflows, queues, inventories, protocols, game rules, token standards. Places hold integer counts, transitions fire, and every analysis package reads the same net.
  • Population dynamics — epidemics, chemical kinetics, market flows — where the same net runs as a mass-action ODE, an exact Gillespie sample path, or a chemical Langevin SDE. Which engine for which question says when each one is telling the truth.
  • Correctness questions, not just trajectories: invariants, deadlocks, boundedness, declared properties with counterexamples, conformance against event logs, and a Groth16 proof of an execution. The ladder is in MODEL-CORRECTNESS.md.

Where you will be working against the grain:

You want What exists What it costs you
Tokens that carry data (a struct per token) Vector-valued tokens: a fixed set of colors, unfolded by petri.ExpandColors Encode the data as places or colors; predicates over token fields become guard strings
Guards enforced in simulation stochastic.Options.Guard is an injected evaluator; stochastic/markingguard decides guards over tokens(...) A nil evaluator caveats every guard rather than enforcing it — read Result.Caveats
Deterministic durations delay on a transition: inputs consumed at start, outputs exactly delay later, one clock per enabling; stages for an Erlang-k approximation Only the discrete engine honours delay, byte-exact in all four languages; the ODE and SDE refuse it. Deadlines and pre-emption are still outside the net
Exhaustive analysis of a large state space reachability enumerates explicitly Fine for a café, not for a board game; the chess example is N-Queens for that reason
Continuous dynamics with gating stochastic.Forecast refuses a gated net rather than running it unconstrained Use Simulate (SSA); the refusal is the engine doing its job

Packages

Package Purpose Book chapter
metamodel The engine input schema; NewBundle composes typed subnets into a *Bundle, and Bundle.Flatten lowers it to one Model Ch 4: Token Language
parser pflow.xyz JSON-LD import/export; ModelFromJSON is the one editor-shape → metamodel converter Ch 17: Visual Editor
petri Core net types, colors, fluent Builder Ch 1: Why Petri Nets?
solver ODE solvers (Tsit5, RK45, implicit), equilibrium detection Ch 3: Discrete to Continuous
stochastic Solve dispatch; Gillespie SSA, schedules (Options.ContinueStreams keeps one random stream per realization across segments), chemical-Langevin SDE, FitDiscrete CTMC likelihood fitting. Options{Portable: true} is byte-exact with pflow-rs and pflow-xyz, and with pflow-jl on its algebraic-petri branch (goldens in stochastic/testdata/portable/, make ssa-goldens) Ch 3: Discrete to Continuous
learn ODE parameter fitting and system identification: Nelder-Mead, Adam, forward and adjoint sensitivities, tied parameters, hybrid MLP rates Ch 19: go-pflow Library
sensitivity Parameter sensitivity analysis Ch 19: go-pflow Library
derive Evaluation variants of a declared net —
reachability Discrete state space, deadlock/liveness, Farkas P/T-invariants, unboundedness witnesses Ch 2: Mathematics of Flow
verify Declarative property checking — proved / refuted / unknown + counterexample Model correctness
validation Structural validation with located errors and suggested fixes Ch 13: Topology-Driven Verification
eventlog, mining, monitoring Event log parsing, process discovery and conformance, real-time prediction and SLA alerts Ch 11: Process Mining
hypothesis Move evaluation for game AI Ch 6: Game Mechanics
statemachine, workflow, actor Statecharts, task dependencies and SLAs, message-passing actors — all on a Petri-net backend Ch 10: Complex State Machines
tokenmodel (+ dsl, petri, subnet, windowing, dataflow) Token model schemas, S-expression DSL, Beam-style streaming pipelines Ch 4: Token Language
codegen/solidity, templates Solidity generation from token models; common net patterns Ch 18: Code Generation
prover, zkcompile Groth16 proofs of state transitions with gnark; net → circuit compilation Ch 12: Zero-Knowledge Proofs
eventsource, graphql, results, compat Event sourcing, GraphQL over models, structured simulation output, bridge between the two Petri implementations. schema/ beside them is JSON Schema and JSON-LD assets, not a Go package Ch 16: Declarative Infrastructure
visualization, plotter, cache, stateutil SVG rendering, time-series plots, simulation memoization, state-map utilities Ch 19: go-pflow Library

Examples

examples/cafe is the one to start with. The rest each map to a book chapter; see examples/README.md for the full table, run commands and a complexity progression.

Example Domain Book chapter
basic Token flow fundamentals Ch 1
coffeeshop Resource modeling, actors, workflows Ch 5
neural, dataset_comparison Parameter fitting, calibration Ch 3
tictactoe, connect4, nim Game AI, move evaluation Ch 6
sudoku, chess, knapsack Constraint satisfaction, optimization Ch 7, Ch 8
poker Complex state machines Ch 10
mining_demo, monitoring_demo, incident_simulator Process mining, SLA prediction Ch 11
erc Token standards, Solidity codegen Ch 4

The book

book.pflow.xyz covers everything from foundations to advanced topics:

Part I: Foundations — Why Petri Nets, Mathematics of Flow, Discrete to Continuous, Token Language

Part II: Applications — Resource Modeling, Game Mechanics, Constraint Satisfaction, Optimization, Enzyme Kinetics, Complex State Machines

Part III: Advanced — Process Mining, Zero-Knowledge Proofs, Topology-Driven Verification, On-Chain ZK Verification, Exponential Weights and Scoring Systems, Declarative Infrastructure

Part IV: Building — Visual Editor, Code Generation, go-pflow Library, Dual Implementation

Epilogue — What the Abstraction Sits On

Testing

go test ./...

Bazel (hermetic, with nogo) also works: bazel test //... — see CLAUDE.md.

CLI

The pflow CLI provides simulation, analysis, verification and plotting from the command line. See cmd/pflow/README.md.

Compatibility

See CHANGELOG.md for breaking changes since the last tag.

  • Go 1.24.9+ (the go directive in go.mod; CI builds on 1.24)
  • Reads and writes the pflow.xyz JSON-LD format
  • SSA goldens (stochastic/testdata/portable/, produced under stochastic.Options{Portable: true}) are replayed byte-for-byte by pflow-xyz in JS and by pflow-rs in Rust; pflow-jl replays them on its algebraic-petri branch, not yet on its default branch
  • Editor-shape parse goldens (parser/testdata/editor-shape/) are replayed by pflow-xyz in JS, and by pflow-jl on algebraic-petri; pflow-rs has no editor-shape parser yet

License

MIT License - see LICENSE for details.

Related

About

Petri net library — ODE, SSA & SDE simulation, parameter fitting, and formal verification, in Go

Topics

Resources

Stars

11 stars

Watchers

1 watching

Forks

Releases

Packages

Contributors

Languages