Petrex

Place/transition Petri nets for the BEAM, with analysis as the primary product.

A finite-state machine is a Petri net with exactly one token. That token is in one place at a time, which is why a state machine can say "the order is paid" but not "two workers are running while three slots are free". The moment two things are in flight and share a resource, the general case is needed: several tokens, moving independently, meeting at transitions that only fire when every input has enough of them.

Petrex is that general case, and it can answer questions about a net before the net runs: whether it stays bounded, whether it can deadlock, which transitions can never fire, what stays invariant, and whether a workflow is sound. It explores a million reachable markings in 1.3 seconds and 690 MiB, or 570 MiB with an ETS visited set (BENCH.md), and it checks its answers against TINA and LoLA rather than against its own expectations.

# A case is split in two, and each branch finishes it on its own.
workflow =
  Petrex.new()
  |> Petrex.place(:start, tokens: 1)
  |> Petrex.place(:left)
  |> Petrex.place(:right)
  |> Petrex.place(:finish)
  |> Petrex.transition(:split, in: [:start], out: [:left, :right])
  |> Petrex.transition(:finish_left, in: [:left], out: [:finish])
  |> Petrex.transition(:finish_right, in: [:right], out: [:finish])

Petrex.Analysis.sound?(workflow)
#=> {:error, {:improper_completion, %{start: 0, left: 0, right: 1, finish: 1}}}

The workflow reports itself finished while the right branch is still running, and the answer says which marking shows it. Join the branches instead, and the same call returns {:ok, :sound}.

What it does

• Analysis — reachability graph, Karp–Miller coverability tree with ω, per-place bounds, deadlocks, dead transitions, P- and T-invariants, workflow nets and classical soundness. Every answer says whether it is exact: a search stopped by its limit returns {:partial, result}, and never a verdict.
• Interchange — PNML (ISO/IEC 15909-2) import and export, including inhibitor arcs, keeping elements it does not interpret so a document from another tool survives the round-trip.
• Execution — one small GenServer per net instance, firing when asked, with guards and actions over arbitrary tokens.
• No runtime dependencies, no NIFs. :xmerl comes with OTP.

Tokens are arbitrary terms and arcs carry weights. Analysis runs on the skeleton — tokens counted, guards ignored — so its results are exact for the skeleton and conservative for the guarded net. Coloured nets, timed and stochastic transitions are out of scope; see NOTES.md for that and for every other decision behind the library.

Installation

def deps do
  [{:petrex, "~> 1.0"}]
end

Requires Elixir 1.17 and OTP 26 or later. No runtime dependencies.

Documentation

• NOTES.md — design decisions, their reasoning, and the quirks of the tools Petrex is checked against
• BENCH.md — how much time and memory a state space costs
• CHANGELOG.md

Licensed under MIT.