A high-performance Coloured Time Petri Net runtime — a Turing-complete execution engine where typed tokens flow through places, transitions fire under real-time constraints, and async actions execute concurrently. Formal verification proves safety properties via SMT/IC3.

See spec/ for the language-agnostic contract all implementations follow.

Specification

• Executable formal models — Not a simulator. A production runtime where Petri nets are the program: typed tokens are data, transitions are instructions, timing constraints are deadlines, and the executor is a scheduler. Suitable for agent orchestration, workflow automation, protocol modeling, game logic, UI state machines, and anything with concurrency.
• Three implementations, one spec — Java, TypeScript, and Rust share 145 language-agnostic requirements covering every arc type, timing variant, and execution phase. Same behavior, verified independently.
• Turing-complete — Coloured Petri Nets with inhibitor arcs can simulate any Turing machine. libpetri's nets can model arbitrary computation, not just finite-state workflows.

import org.libpetri.core.*;
import org.libpetri.runtime.BitmapNetExecutor;
import java.time.Duration;
import java.util.*;
import java.util.concurrent.*;

var request  = Place.of("Request", String.class);
var response = Place.of("Response", String.class);

var process = Transition.builder("Process")
    .inputs(In.one(request))
    .outputs(Out.place(response))
    .timing(Timing.deadline(Duration.ofSeconds(5)))
    .action(ctx -> {
        String req = ctx.input(request);
        ctx.output(response, "Processed: " + req);
        return CompletableFuture.completedFuture(null);
    })
    .build();

var net = PetriNet.builder("Example")
    .transitions(process)
    .build();

try (var executor = BitmapNetExecutor.builder(net, Map.of(
            request, List.of(Token.of("hello"))))
        .executor(Executors.newVirtualThreadPerTaskExecutor())
        .build()) {
    Marking result = executor.run();
    System.out.println(result.peekFirst(response).value());
    // → "Processed: hello"
}

cd java && ./mvnw verify

import {
  place, tokenOf, one, outPlace, deadline,
  Transition, PetriNet, BitmapNetExecutor
} from 'libpetri';

const request  = place<string>('Request');
const response = place<string>('Response');

const process = Transition.builder('Process')
  .inputs(one(request))
  .outputs(outPlace(response))
  .timing(deadline(5000))
  .action(async (ctx) => {
    const req = ctx.input(request);
    ctx.output(response, `Processed: ${req}`);
  })
  .build();

const net = PetriNet.builder('Example')
  .transitions(process)
  .build();

const executor = new BitmapNetExecutor(net, new Map([
  [request, [tokenOf('hello')]],
]));
const result = await executor.run();
console.log(result.peekFirst(response)?.value);
// → "Processed: hello"

cd typescript && npm install && npm test

use libpetri::*;
use libpetri::runtime::environment::ExternalEvent;

let request  = Place::<String>::new("Request");
let response = Place::<String>::new("Response");

let process = Transition::builder("Process")
    .input(one(&request))
    .output(out_place(&response))
    .timing(deadline(5000))
    .action(async_action(|mut ctx| async move {
        let req: std::sync::Arc<String> = ctx.input("Request")?;
        ctx.output("Response", format!("Processed: {req}"))?;
        Ok(ctx)
    }))
    .build();

let net = PetriNet::builder("Example").transition(process).build();

let mut marking = Marking::new();
marking.add(&request, Token::at("hello".to_string(), 0));

let mut executor = BitmapNetExecutor::<NoopEventStore>::new(
    &net, marking, ExecutorOptions::default(),
);
let (_tx, rx) = tokio::sync::mpsc::unbounded_channel::<ExternalEvent>();
executor.run_async(rx).await;
// → "Processed: hello"

cd rust && cargo test

The libpetri debug UI is itself a Coloured Time Petri Net — 53 transitions, 51 places (including 30 environment places). The entire UI lifecycle (WebSocket connection, session management, message dispatch, diagram rendering, replay playback, live debugging, breakpoints, search, session archives) is modeled and executed as a CTPN.

Subnet breakdown:

Patterns at work:

• Environment places — WebSocket open/close/message events, DOM user interactions (clicks, slider, form submissions), and requestAnimationFrame ticks are injected as external events
• Dirty-flag fan-out — A single stateDirty token AND-forks into three independent UI update channels, each gated by a rafTick environment place for frame-rate throttling
• Resource places — uiState, breakpoints, filterState, searchState are consumed and re-produced by their transitions, ensuring mutual exclusion on state updates
• Timing — delayed(2000) for reconnect backoff; all other transitions are immediate()
• Guard predicates — Message dispatch transitions use typed guards (msg.type === 'event', etc.) on the wsMessage environment place to route messages to the correct handler

// Connection transitions
const t_connect = Transition.builder('t_connect')
  .inputs(one(idle))
  .outputs(outPlace(connecting))
  .timing(immediate())
  .action(async (ctx) => { /* createWebSocket, setConnecting */ })
  .build();

const t_on_open = Transition.builder('t_on_open')
  .inputs(one(connecting), one(wsOpenSignal.place))
  .outputs(outPlace(connected))
  .timing(immediate())
  .action(async (ctx) => { /* setConnected, refreshSessions */ })
  .build();

const t_reconnect = Transition.builder('t_reconnect')
  .inputs(one(waitReconnect))
  .outputs(outPlace(idle))
  .timing(delayed(2000))  // 2s backoff
  .action(async (ctx) => { ctx.output(idle, undefined); })
  .build();

// Message dispatch with guard predicates
const t_on_event = Transition.builder('t_on_event')
  .inputs(one(uiState), one(wsMessage.place, (msg) => msg.type === 'event'))
  .outputs(and(outPlace(uiState), outPlace(stateDirty)))
  .timing(immediate())
  .action(async (ctx) => { /* applyEventToState, updateTimeline */ })
  .build();

// UI fan-out: stateDirty → 3 parallel updates
const t_fan_out_dirty = Transition.builder('t_fan_out_dirty')
  .inputs(one(stateDirty))
  .outputs(and(outPlace(highlightDirty), outPlace(logDirty), outPlace(markingDirty)))
  .timing(immediate())
  .build();

// Frame-rate gated UI updates
const t_update_highlighting = Transition.builder('t_update_highlighting')
  .inputs(one(highlightDirty), one(rafTick.place))
  .reads(svgReady, uiState)
  .timing(immediate())
  .action(async (ctx) => { /* updateDiagramHighlighting */ })
  .build();

// ... 53 transitions total
const net = PetriNet.builder('DebugUI')
  .transitions(t_connect, t_on_open, /* ... */)
  .build();

The examples/java-parser/ module implements a complete Java 25 parser as a Coloured Time Petri Net — 167 grammar productions compiled into 2,335 places and 2,326 transitions. This is a stress test demonstrating that Petri net execution overhead is acceptable even under extreme workloads, not a competitor to javac's hand-tuned recursive descent parser.

Grammar fragment — 3 productions compiled to a 33-place, 31-transition net, showing the hierarchical structure of compiled grammar rules:

Full parser net — all 167 productions, 2,335 places, 2,326 transitions:

How it works:

• Coloured tokens — A single ParseState token carries position, call stack, and AST through the net. No global mutable state.
• Grammar-to-net compilation — Each grammar element (terminal, sequence, choice, repetition, optional, non-terminal call/return) maps to a specific net pattern. The compiler produces a PetriNet from an EBNF-like Grammar definition.
• Structural sharing — Non-terminal calls push a return-site ID onto the token's call stack; a shared return-dispatch transition routes the token back to the correct call site via XOR guards.
• PrecompiledNetExecutor — The flat-array executor with skipOutputValidation handles the 2,300+ transitions efficiently. Standard BitmapNetExecutor works too, but the precompiled path is faster at this scale.

Self-parse results: Parses all 85 libpetri core Java source files (17,395 lines) in ~500ms (~34,000 lines/sec). The overhead is measurable compared to javac, but the fact that a general-purpose Petri net runtime can parse a full programming language at all — and do so correctly across 85 real-world files — proves CTPN execution scales far beyond typical workflow orchestration.

All three implementations include structural verification (P-invariants, siphon/trap analysis, state class graphs). Java and TypeScript additionally support SMT-based verification via Z3 using the IC3/PDR algorithm. Rust has Z3 SMT feature-gated but not yet wired.

Pipeline: structural siphon/trap analysis → P-invariant computation (Farkas) → XOR branch analysis → SMT encoding → IC3/PDR solving

Prove that a circular token-passing net is deadlock-free — proven structurally via Commoner's theorem without invoking the SMT solver:

import org.libpetri.core.*;
import org.libpetri.smt.*;
import java.time.Duration;

var pA = Place.of("A", Void.class);
var pB = Place.of("B", Void.class);

var net = PetriNet.builder("TokenRing")
    .transitions(
        Transition.builder("AtoB").inputs(In.one(pA)).outputs(Out.place(pB)).build(),
        Transition.builder("BtoA").inputs(In.one(pB)).outputs(Out.place(pA)).build())
    .build();

var result = SmtVerifier.forNet(net)
    .initialMarking(m -> m.tokens(pA, 1))
    .property(SmtProperty.deadlockFree())
    .timeout(Duration.ofSeconds(30))
    .verify();

System.out.println(result.verdict());  // Proven[method=structural, ...]

Prove that a circular token-passing net is deadlock-free — proven structurally via Commoner's theorem without invoking the SMT solver:

import { SmtVerifier, deadlockFree } from 'libpetri/verification';

const pA = place('A');
const pB = place('B');
const net = PetriNet.builder('TokenRing')
  .transitions(
    Transition.builder('AtoB').inputs(one(pA)).outputs(outPlace(pB)).build(),
    Transition.builder('BtoA').inputs(one(pB)).outputs(outPlace(pA)).build(),
  )
  .build();

const result = await SmtVerifier.forNet(net)
  .initialMarking(m => m.tokens(pA, 1))
  .property(deadlockFree())
  .timeout(30_000)
  .verify();

console.log(result.verdict.type);   // 'proven'
console.log(result.verdict.method); // 'structural' (Commoner's theorem)

The executor runs a single-threaded orchestration loop with six phases per cycle:

1. Process completions — collect outputs from finished async actions
2. Process events — inject tokens from environment places
3. Update enablement — re-evaluate only dirty transitions via bitmap masks
4. Enforce deadlines — force-disable transitions past their deadline (urgent semantics)
5. Fire transitions — select by priority, then FIFO by enablement time
6. Await work — sleep until an action completes, a timer fires, or an event arrives

All three share the same architecture: immutable net definitions, builder-pattern construction, bitmap-based enablement with dirty-set optimization, and a single-threaded orchestrator dispatching async actions to a separate task pool. Rust uses a tokio feature flag for async execution and a debug feature flag for the debug protocol.

The BitmapNetExecutor interprets the net definition on every firing: it pattern-matches on sealed arc types, looks up tokens in HashMaps, and sorts enabled transitions by priority. The PrecompiledNetExecutor eliminates all of this by precompiling the net into flat arrays and operation sequences for direct execution.

Compilation. PrecompiledNet.compile(net) transforms a PetriNet into flat arrays and operation sequences. Each transition's input and reset arcs become a sequence of integer opcodes:

CONSUME_ONE(0)      placeId
CONSUME_N(1)        placeId  count
CONSUME_ALL(2)      placeId
CONSUME_ATLEAST(3)  placeId  minimum
RESET(4)            placeId

Timing constraints are precomputed to milliseconds. Priority levels are pre-sorted and indexed. Output specs are analyzed so that the common case (single output place) is a direct array lookup. The compiled PrecompiledNet is immutable and can be reused across executor instances — in Rust, the executor borrows &PrecompiledNet for zero-cost reuse.

Execution. The precompiled executor replaces every abstraction on the hot path with flat-array operations:

Java and Rust additionally use ring buffers for token storage and two-level summary bitmaps for dirty/enabled iteration. Rust-specific optimizations: precomputed Arc<str> name arrays, reusable HashMap buffers, sparse enablement masks (Empty/Single/Multi variants).

The execution loop has the same six phases as BitmapNetExecutor and produces identical results. In Java it passes the same 141-test suite via abstract base class inheritance; in Rust it has its own 25-test suite. The concurrency model is also identical: single orchestrator thread with concurrent async actions (virtual threads in Java, Tokio tasks in Rust).

Where the speedup comes from. On pure-sync chains, the compiled path does almost no allocation and touches only contiguous arrays, giving 1.4–4× speedup that grows with scale. On async-dominated workloads the scheduling cost dominates both executors equally, so the speedup converges to ~1× for small chains and emerges at scale. Mixed workloads (the common real-world pattern) see 1.3–3.6×.

Measured with noop event store. Java uses JMH (1 fork, 2 warmup, 3 measurement iterations); TypeScript uses vitest bench; Rust uses Criterion. All times in microseconds (µs/op, lower is better). Java and Rust columns show both the standard BitmapNetExecutor and the PrecompiledNetExecutor (a precompiled flat-array executor that compiles nets to operation sequences).

Scaling note: Thanks to dirty-set optimization, the executor only re-evaluates transitions whose input places changed. The times below therefore reflect cost per transition that is enabled and fires — adding more transitions to a net does not increase per-cycle cost unless they actually fire.

Concurrency model note: In Java the orchestrator runs on its own virtual thread and dispatches each action to a separate virtual thread, so no action can ever block the runtime loop. This gives true multicore parallelism for CPU-bound actions. In TypeScript the orchestrator and all actions share a single-core event loop with zero scheduling overhead but no parallelism. In Rust the sync executor is single-threaded with no runtime overhead; the async executor uses Tokio's multi-threaded task pool for true parallelism. In these benchmarks all actions are trivial, so Java's per-thread scheduling cost is visible while its multicore advantage is not. For real workloads with CPU-bound actions Java and Rust scale across cores while TypeScript remains single-threaded.

All transitions use synchronous (passthrough) actions.

All transitions dispatch to a virtual thread / microtask / Tokio task.

Two transitions are async, the rest synchronous — the common real-world pattern.

One dispatch transition fans out to N parallel async branches, then joins.

Impact of different event store implementations on the complex workflow:

*inMemory appearing faster than noop is within measurement noise.

Time to compile a PetriNet into a CompiledNet / PrecompiledNet (bitmap masks, reverse indexes, opcode sequences).

cd java && ./mvnw test-compile exec:exec -Pjmh    # JMH → benchmark-results.json
cd typescript && npm run bench                      # vitest bench → stdout
cd rust && cargo bench                              # Criterion → target/criterion/

The spec/ directory defines the complete engine contract — 145 requirements across 10 files.

Priority: 110 MUST · 29 SHOULD · 6 MAY

See spec/00-index.md for the full cross-reference index and coverage matrix.

cd java
./mvnw verify                                          # Full build + tests
./mvnw test                                            # Run all tests
./mvnw test -Dtest="org.libpetri.core.PetriNetTest"    # Single test class
./mvnw test -Dtest="*BitmapNetExecutor*"               # Wildcard match
./mvnw test-compile exec:exec -Pjmh                    # Run JMH benchmarks
./mvnw javadoc:javadoc                                 # Generate Javadocs

Java 25 (no preview features — all used features are finalized). Uses Maven 3.9.x via wrapper.

cd typescript
npm install              # Install dependencies
npm run build            # Build with tsup
npm run check            # Type-check (tsc --noEmit)
npm test                 # Run vitest
npm run test:watch       # Watch mode
npm test -- core         # Run tests matching "core"

TypeScript 5.7, ESM-only, strict mode. Built with tsup, tested with vitest.

cd rust
cargo build                       # Build all crates
cargo test                        # Run all tests (256 pass, 2 ignored)
cargo test -p libpetri-core       # Single crate
cargo bench                       # Criterion benchmarks

Rust 2024 edition, workspace with 6 crates. Feature flags: tokio (async executor), z3 (SMT verification, not yet wired).

Apache License 2.0

Specification