libpetri — Coloured Time Petri Net Engine

A high-performance Petri net engine with formal verification support.

Quick Start

use libpetri::*;

let p1 = Place::<i32>::new("input");
let p2 = Place::<i32>::new("output");

let t = Transition::builder("process")
    .input(one(&p1))
    .output(out_place(&p2))
    .action(fork())
    .build();

let net = PetriNet::builder("example").transition(t).build();

let mut marking = Marking::new();
marking.add(&p1, Token::at(42, 0));

let mut executor = BitmapNetExecutor::<NoopEventStore>::new(
    &net, marking, ExecutorOptions::default(),
);
executor.run_sync();

assert_eq!(*executor.marking().peek(&p2).unwrap(), 42);

Example: Basic Chain

Example: Order Processing Pipeline

A showcase net demonstrating all arc types (input, output, read, inhibitor, reset), both place types (regular + environment), all timing modes (immediate, deadline, delayed, window, exact), and patterns (AND-fork, AND-join, XOR, priority).

Crate Structure

• [core] — Places, tokens, transitions, timing, actions
• [event] — Event store for recording execution events
• [runtime] — Bitmap-based executor (sync + async)
• [export] — DOT/Graphviz export pipeline
• [verification] — Formal verification (P-invariants, state class graphs, SMT)

Executors

Two executors are available:

• [BitmapNetExecutor] — General-purpose, bitmap-based enablement checks
• [PrecompiledNetExecutor] — High-performance alternative with ring buffers, opcode dispatch, and two-level summary bitmaps

Feature Flags