Petri net
modeling and simulation

Petrinaut is a visual editor and simulation engine for various kinds of Petri Nets. Model, simulate, and share complex systems straight from the canvas.

GitHubView on GitHubRead the docsLaunch the demo

Used by

What is Petrinaut?

A canvas for the systems
you actually want to model

Classic Petri nets give you places, transitions, and arcs — a precise way to describe how things move, queue, and combine. Petrinaut takes that foundation and extends it for modern modelling, layering on typed tokens, continuous dynamics, and stochastic firings.

The result is SDCPN: a single notation that can express discrete workflows, continuous physical systems, and everything in between — all in a tool that runs in your browser and exports cleanly to JSON or TikZ.

Petrinaut is published as @hashintel/petrinaut — an embeddable React component you can drop into your own app, or use as a hosted editor at demo.petrinaut.org.

Why Petri Nets?

A formalism that lets you
prove things about your model

Invented by Carl Adam Petri in 1962 and studied intensively ever since, Petri nets are a mathematical formalism for modelling concurrent, distributed, and asynchronous systems. The notation is simple — places, transitions, and arcs — but the underlying object is a rigorously-defined mathematical graph, which means we can reason about it rather than just draw it.

That grounding makes a surprising number of questions about a system computationally tractable — often decidable, and in many cases efficiently so:

  • Reachability

    Can a given state (marking) be reached from the initial marking? Decidable, and the starting point for most other analyses.

  • Boundedness

    Will any place, queue, or resource grow without bound? Decidable and computable via the Karp–Miller coverability tree.

  • Safeness

    Will any place ever hold more than one token? A 1-bounded net rules out resource conflicts and simplifies verification.

  • Deadlock-freedom

    Is there a reachable marking in which no transition can fire? A central correctness property for workflows, protocols, and schedulers.

  • Livelock-freedom

    Will the system keep making meaningful progress, or can it get stuck cycling through states that never deliver a useful outcome?

  • Liveness

    Can every transition still fire from every reachable marking? The strongest guarantee of progress — and the backbone of fairness arguments.

  • Coverability

    Can we reach a marking that dominates a target marking? A weaker-but-decidable stand-in when full reachability is too expensive.

  • Persistence

    Once a transition becomes enabled, does it remain enabled until fired? A key property for confluent and diamond-property systems.

  • Structural invariants

    Linear-algebraic P-invariants and T-invariants summarise what must hold over any execution, no matter how you schedule it.

Because Petri nets map cleanly onto established model checkers and verification pipelines, they allow moving directly from intelligible visual representations to machine-checked proofs without leaving the formalism — providing a clean, clear, shared language for exchange between domain experts, engineers, and computer programs, as well as AI agents.

Features

Everything you need to model
real-world dynamics

Petrinaut is opinionated about the things that matter most when modelling stochastic, dynamic, and coloured systems.

Typed tokens

Coloured nets let each place hold typed tokens with named dimensions, so you can model heterogeneous flows the way you actually think about them.

Continuous dynamics

Drop differential equations onto places to integrate continuous quantities — alongside discrete firings.

Stochastic transitions

Transitions can fire stochastically with first-class distributions, kernels, and guards — for honest models of uncertainty.

Live visualizers

Render any place with a custom visualizer during simulation. Watch your model as it unfolds, not after the fact.

Code that helps you

A built-in Monaco editor with diagnostics, completions, hovers, and signatures — so authoring dynamics feels like writing code, not configuration.

Portable nets

Import and export models as JSON for sharing and version control, or export to TikZ for publication-ready figures.

Examples

Built-in models to learn from

Open the demo and pick an example from the menu — every model loads directly into the editor, ready to inspect, run, and remix.

SIR epidemic

Model the spread of disease through Susceptible, Infected, and Recovered compartments.

Supply chain

Trace orders, inventory, and lead times across a multi-stage logistics pipeline.

Deployment pipeline

Watch builds, reviews, and releases flow through a continuous-delivery workflow.

Production machines

Capture queues, throughput, and failure modes in a connected manufacturing line.

Satellites in orbit

Combine continuous orbital dynamics with discrete handover events between ground stations.

Build your own

Start from a blank canvas — places, transitions, and arcs are just a few clicks away.

Embed in your app

Drop the editor
into your own UI

Petrinaut ships as a React component with a typed SDCPN definition and an Immer/Automerge-friendly mutator API. Keep your own persistence and routing — Petrinaut handles the canvas, simulation, and authoring tooling.

Open-source dual-licensed under:MITApache 2.0
import { Petrinaut, type SDCPN } from "@hashintel/petrinaut";
import "@hashintel/petrinaut/dist/main.css";

export function MyEditor({
  net,
  onChange,
}: {
  net: SDCPN;
  onChange: (mutate: (draft: SDCPN) => void) => void;
}) {
  return (
    <Petrinaut
      petriNetDefinition={net}
      mutatePetriNetDefinition={onChange}
    />
  );
}

Get started

Three, two, one, simulate

Open the editor in your browser — no install, no sign-up. When you're ready, embed it in your own app.

Launch the demoRead the docsGitHubView source