petrex

# 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](BENCH.md)), and it checks its
answers against
[TINA](https://projects.laas.fr/tina/) and
[LoLA](https://theo.informatik.uni-rostock.de/theo-forschung/tools/lola/)
rather than against its own expectations.

```elixir
# 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](NOTES.md) for that and for every other decision behind the
library.

## Installation

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

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

## Documentation

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

Licensed under MIT.