🔀 Petri Nets

Model and analyze concurrent systems with places, transitions, and tokens

Overview

A Petri net is a mathematical formalism for modeling concurrent and distributed systems. Tokens flow through a bipartite graph of places (holding resources/conditions) and transitions (representing events/actions), connected by directed arcs with weights.

This implementation goes beyond basic simulation: it includes full reachability graph construction, boundedness analysis, deadlock detection, liveness checking, and incidence matrix computation — the core analyses used in verification of concurrent protocols.

Core Data Structures

type place = { name : string; id : int }
type transition = { t_name : string; t_id : int }

type arc =
  | PlaceToTrans of int * int * int   (* place_id, trans_id, weight *)
  | TransToPlace of int * int * int   (* trans_id, place_id, weight *)

type marking = int array   (* tokens per place *)

type petri_net = {
  places      : place array;
  transitions : transition array;
  arcs        : arc list;
  initial     : marking;
}

Firing Rules

(* A transition is enabled when every input place has enough tokens *)
let is_enabled net marking t_id =
  List.for_all (fun (p_id, weight) ->
    marking.(p_id) >= weight
  ) (inputs net t_id)

(* Firing: consume input tokens, produce output tokens *)
let fire net marking t_id =
  let m = copy_marking marking in
  List.iter (fun (p, w) -> m.(p) <- m.(p) - w) (inputs net t_id);
  List.iter (fun (p, w) -> m.(p) <- m.(p) + w) (outputs net t_id);
  m

Analysis Capabilities

Analysis	What It Checks	Complexity
Reachability Graph	Explores all reachable markings via BFS (bounded to 10,000 states)	Exponential in places (bounded)
Boundedness	Whether token counts in any place grow unboundedly	Linear scan of reachability graph
Deadlock Detection	Markings where no transition is enabled (system stuck)	Linear scan of reachability graph
Liveness	Whether every transition can eventually fire from any reachable state	Linear in \|states\| × \|transitions\|
Incidence Matrix	Net effect of each transition on each place (for algebraic analysis)	O(\|arcs\|)

Built-in Example Nets

Mutex — mutual exclusion with a shared lock token, proving two processes can't both be in the critical section
Producer-Consumer — bounded buffer with producer/consumer synchronization
Workflow — sequential task pipeline with fork/join parallelism
Dining Philosophers — the classic deadlock-prone concurrency problem

(* Dining Philosophers: 5 philosophers, 5 forks *)
(* Places: think_i, eat_i, fork_i *)
(* Transitions: pickup_i (needs fork_i and fork_(i+1)%5) *)
(*              putdown_i (releases both forks) *)
(* Analysis reveals: deadlock is reachable when all pick up left fork *)

Simulation Output

(* The simulator prints each step with visual token placement *)
Step 0: [P0:1] [P1:0] [P2:1] — T0 enabled
  Fire T0 → [P0:0] [P1:1] [P2:1]
Step 1: [P0:0] [P1:1] [P2:1] — T1 enabled
  Fire T1 → [P0:0] [P1:0] [P2:0]
Step 2: [P0:0] [P1:0] [P2:0] — DEADLOCK (no transitions enabled)

OCaml Concepts Demonstrated

Mutable arrays as state — markings use int array for efficient token manipulation
Set module for graph exploration — MarkingSet tracks visited states using Set.Make functor
List.for_all / List.iter — declarative enabling checks and firing logic
Record types — places, transitions, and nets use named fields for clarity
Array.copy — defensive copying ensures firing doesn't corrupt the source marking
BFS with queue — reachability graph built using standard breadth-first search

Running It

# Compile and run all examples with analysis
ocamlfind ocamlopt petri_net.ml -o petri_net
./petri_net

# Output includes simulation traces and analysis reports for
# each built-in net (mutex, producer-consumer, workflow, dining philosophers)