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 — which is why a state machine can say "the order is paid" but not "two workers are running while three slots are free". Petrex is the general case, and it answers 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.

Two packages live here.

Package	Purpose
petrex	The library: net model, analysis, PNML interchange, OTP executor. Zero runtime dependencies.
petrex_oban	Answers two questions about an Oban workflow. Does not depend on Oban.

The adapter is the shortest way to see the point. Given a workflow's jobs, their dependencies and the queues they run on:

# Will it finish? A dependency cycle never does, and Oban will not say so.
Petrex.Oban.cycles(%{
  jobs: [%{id: :fetch, deps: [:index]},
         %{id: :parse, deps: [:fetch]},
         %{id: :index, deps: [:parse]}]
})
#=> [[:fetch, :index, :parse]]

# How much of each queue does it really use, over every possible
# interleaving rather than one sampled run?
Petrex.Oban.max_concurrency(%{
  jobs: [%{id: :fetch, deps: [], queue: :network},
         %{id: :thumbnail, deps: [:fetch], queue: :cpu},
         %{id: :transcode, deps: [:fetch], queue: :cpu}],
  queues: %{network: 5, cpu: 8}
})
#=> {:ok, %{network: 1, cpu: 2}}
# Eight CPU workers configured; this workflow never runs more than two.

The library underneath does the same for nets you build yourself, and packages/petrex/README.md starts there.

Verified against other tools

Analysis results are cross-checked against TINA and LoLA on twenty-two nets: reachability graphs compared marking by marking and edge by edge, plus deadlocks, dead transitions, bounds, semiflows and soundness. The tools' own output is committed, so the comparison runs without them installed, and tools/install.sh rebuilds that environment in one command.

Expected verdicts written by hand are not treated as evidence — they share their assumptions with the analyser under test.

Documentation

• packages/petrex/README.md — the library, with the soundness example
• packages/petrex/NOTES.md — every design decision, its reasoning, and the quirks of the tools Petrex is checked against
• packages/petrex/BENCH.md — what a state space costs: a million markings in 690 MiB and 1.3 seconds for a narrow net
• packages/petrex_oban/README.md — the Oban adapter
• tools/README.md — the external checkers and how they are driven

Elixir 1.17 and OTP 26 or later. Licensed under MIT.