Design notes

Decisions that shape the library's behaviour, with the reasoning behind them. Each entry states what was decided and why; changes to any of them are breaking changes.

Analysis runs on the skeleton

Tokens are arbitrary terms, and transitions may carry a guard and an action that inspect them. Analysis ignores both: it runs on the skeleton, the net with tokens counted and every guard taken as true.

Results are therefore exact for the skeleton and conservative for the guarded net. A guard can only remove firings, so a marking the skeleton cannot reach is unreachable in the guarded net too, and a bound proven on the skeleton holds for it. The converse does not hold: a deadlock or a reachable marking found on the skeleton may be excluded by guards.

Identifiers

Place and transition identifiers are atoms (other than nil) or strings, and the two share a single namespace, as in PNML, where every id in a document is unique. Identifiers are not otherwise restricted: :"my place" and "3rd" are valid. Mapping them to PNML ids, which are far more constrained, is the encoder's job (see PNML identifiers).

Definition order

Petrex.Net records the order in which places and transitions were defined. Place order fixes each place's position in the count tuples used internally by analysis. Transition order is the order in which enabled transitions are reported and the default conflict-resolution order of the executor, which makes step sequences reproducible.

Arcs and weights

Arcs carry a positive integer weight and nothing else: no expressions, no variables. Weight 0 and negative weights are rejected by validation rather than interpreted. Between a given place and transition there is at most one normal arc in each direction and at most one inhibitor arc; parallel arcs are rejected rather than summed, so that a net has one canonical form and PNML round-trips are unambiguous.

The PNML decoder is the exception: some tools emit parallel arcs and expect their weights to be summed. The decoder sums them and reports each merge as a warning in its result; the builder and Petrex.Net.validate/1 keep rejecting parallel arcs.

Inhibitor arcs are weighted

An inhibitor arc runs from a place to a transition and has a weight w ≥ 1. The transition is enabled only while the place holds fewer than w tokens. Weight 1, the builder's default, is the classic "place is empty" test. An inhibitor arc consumes nothing and therefore contributes nothing to the incidence matrix or to invariants.

"Fewer than w" is the usual semantics of weighted inhibitor arcs in the literature, and it is the semantics of TINA (checked against TINA 4.0.0: with an inhibitor arc of weight 2, the transition fires when the place holds one token and is dead when it holds two, both from .net input, q?-2, and from PNML input). Storing the weight from the start keeps the model and its interchange representations aligned. LoLA 2.0 has no inhibitor arcs.

Inhibitor arcs make reachability undecidable in general (they give nets the power of counter machines). Consequently, on nets that contain them, coverability analysis is refused and reachability is explored only up to the configured marking limit, with the result marked as partial when the limit is reached.

Analysis results: exact, partial, or refused

Explicit exploration is bounded by a marking (or tree node) limit, so an analysis can end before it has seen the whole state space. Rather than return an answer that looks definitive, analysis functions tag it:

• {:ok, result} — exact.
• {:partial, result} — the limit was reached. Each function documents what a partial result still guarantees: a partial list of deadlocks contains only real deadlocks but may miss some, a partial list of dead transitions is a superset of the real one, a partial bound is a lower bound (except :unbounded, which is always certain).
• {:error, reason} — the analysis does not apply, for example Karp–Miller coverability on a net with inhibitor arcs.

A truncated exploration never produces a verdict. deadlocks/3 returns {:partial, []} where it found none, never {:ok, []}; dead_transitions/3 returns candidates; sound?/2 returns {:partial, :limit_reached} rather than an answer. A caller that matches only {:ok, ...} therefore fails to match rather than mistaking "not found" for "not there".

Nets with inhibitor arcs are explored explicitly, but a completed exploration is exact for them too: what inhibitor arcs remove is the guarantee that the exploration terminates, not the correctness of one that did.

Boolean functions (bounded?, safe?) cannot express "unknown". They answer when a partial result already decides the question (an :unbounded place found before the limit makes a net unbounded regardless) and raise Petrex.InconclusiveError otherwise. They never guess.

The choice of engine follows from what each question needs. Bounds and dead transitions come from the coverability tree, which decides both exactly for unbounded nets too. Deadlocks need actual markings and come from the reachability graph, so on unbounded nets they are always partial. On nets with inhibitor arcs everything comes from the reachability graph.

The reachability graph keeps its edges unless asked not to

For a million markings the edge list is several million tuples, larger than the markings themselves: dropping it halves the graph (measured 1.9x on the nine dining philosophers, 2,786 markings and 16,209 edges). Deadlocks, the edge count and the transitions seen enabled are collected during the search, so reachability/3 with edges: false still answers those, and the analyses that do not need edges use it. The edge list remains the default because the graph is what callers exporting a state space or following a witness path are asking for.

Invariants are minimal-support semiflows

invariants/1 returns the minimal-support semi-positive P- and T-invariants (also called semiflows), computed with the Farkas algorithm in integer arithmetic, each normalised so its coefficients have no common divisor. This set is unique for a given net and generates every semi-positive invariant, which makes it comparable one-to-one with the semiflows reported by external tools. A basis of general (possibly negative) invariants is not unique and is not returned. Inhibitor arcs and self-loops do not change token counts and do not appear in the incidence matrix.

Workflow nets and soundness

A workflow net has one source place, one sink place, and every node on a path between them. Only normal arcs form that flow relation: an inhibitor arc is a read-only test, so it neither makes a place a non-source nor puts a node on a path. It still constrains firing, and therefore soundness.

sound?/2 always starts from one token in the source and ignores the net's own initial marking, because soundness is a property of the workflow, not of one marking. The final marking is one token in the sink and nothing elsewhere.

Petrex checks classical soundness (van der Aalst 1997). Relaxed, weak and lazy soundness are weaker variants defined in later literature and are not checked. Soundness is checked directly from the definition on the reachability graph: option to complete, proper completion, no dead transition. That is equivalent to the short-circuited net being live and bounded, and the equivalence is what makes the property checkable by tools that have never heard of soundness: the cross-check exports the short-circuited net and compares against TINA's and LoLA's liveness and boundedness verdicts. The definition is used directly in the library because it yields a witness -- the marking that cannot complete, the marking that covers the final one, the dead transition -- where liveness of the short-circuited net would only answer yes or no.

Proper completion compares against the final marking rather than counting tokens in the sink: a token stranded elsewhere while the sink holds exactly one is already a violation, and in some nets the sink never holds two.

The checks are ordered so that the most fundamental violation is reported: unboundedness, then improper completion, then no option to complete, then a dead transition. A net can violate several at once.

Builder errors and validation errors

The builder raises ArgumentError only for input that cannot be represented in a Petrex.Net: a reused identifier, a malformed option, a negative token count. Everything representable but wrong (a zero weight, an arc to an undefined place, an inhibitor arc leaving a transition) is stored as given and reported by Petrex.Net.validate/1, which returns every problem at once with a path to the offending element. Nets decoded from PNML or built by hand go through the same validation.

Verification against external tools

Expected verdicts written by hand for test fixtures share their assumptions with the analyser under test, so they are not treated as independent evidence. Analysis results (reachable marking counts, boundedness, deadlocks, dead transitions) are cross-checked against TINA and LoLA: fixtures are exported to PNML, the external tools are run on them, and their outputs are committed so that the comparison also runs where the tools are not installed. Tests that invoke the tools directly are skipped, with a warning, when the tools are absent.

For each fixture the comparison covers:

TINA's graph is compared marking by marking and edge by edge, not only by size, so two state spaces of equal size but different content do not pass. LoLA provides a second, independent implementation for the verdicts. The recorded outputs live in test/oracle/<fixture>/ and are regenerated with PETREX_ORACLE_RECORD=1 mix test --only oracle_live.

PNML

PNML export covers the PT-net type: places, transitions, arc weights, initial markings and names.

Inhibitor arcs in PNML

The PT-net type has no inhibitor arcs. The convention adopted is the one TINA reads and writes: an ordinary <arc> from the place to the transition, with the weight as its inscription and a <type> child.

<arc id="a1" source="q" target="t">
  <inscription><text>2</text></inscription>
  <type value="inhibitor"/>
</arc>

TINA accepts this inside a net declared with the ptnet type, and reads back what the encoder writes. Read (test) arcs use <type value="test"/> in the same convention; Petrex does not model them, and the decoder refuses a document containing one rather than silently treating it as an ordinary arc.

What decoding refuses

decode/1 reads documents Petrex did not write, so it refuses what it cannot represent rather than guessing: an initial marking or arc weight that is not a non-negative integer ({:invalid_marking, text}, {:invalid_weight, text}), a read arc ({:unsupported_arc_type, "test"}), repeated ids, a net type other than the PT-net one. An initial marking is materialised as a list of tokens, so a count in a document is an allocation request: above ten million it is refused with {:marking_too_large, n}.

A document holding several nets decodes its first one and reports {:nets_ignored, n}, because a Petrex.Net is one net.

What decoding keeps and what it drops

decode/1 reads places, transitions, arc weights and types, initial markings and names. Anything else it finds in a place, transition, arc or net element -- graphics, other tools' toolspecific elements, arc names -- is kept verbatim in simple XML form on that element's extra field and written back by encode/2, so a document from another tool survives a round-trip through Petrex with its annotations intact. Their position within the element is not preserved: extras are written after the elements Petrex generates.

A document split over several pages decodes into one net, and re-encoding writes a single page. Page structure is presentation, not semantics.

One detail is not reversible: a label identical to the identifier's own string form is what the encoder writes for an element without a label, so it decodes as no label. Petrex.place(:p, name: "p") and Petrex.place(:p) produce the same document.

PNML identifiers

A PNML id is an xsd:ID: it must start with a letter or underscore, contains no spaces, and is unique across the whole document. Petrex identifiers such as :"my place" or "3rd" would produce documents that are not valid PNML, so identifiers never reach the id attribute unchanged.

Encoding. Every identifier goes through a deterministic sanitiser:

1. The identifier is converted to a string (atoms by Atom.to_string/1).
2. Every character outside A–Z a–z 0–9 . - _ is replaced by _. The allowed set is deliberately ASCII-only, narrower than xsd:ID, because not every tool accepts non-ASCII names.
3. If the result is empty or does not start with a letter or _, it is prefixed with _.
4. Collisions are resolved by appending -2, -3, … (the first suffix not already taken). Ids are assigned in a fixed order — places in definition order, then transitions, then arcs, then the net and page elements — so the same net always yields the same document.

Each element's <name> carries the place's or transition's name label if it has one, and otherwise the original identifier as a string. Labels need not be unique. With the names: :ids option, <name> holds the PNML id instead (see Known tool quirks). The exact original identifier, with its type, is also recorded in a Petrex tool-specific element, so that Petrex-to-Petrex round-trips are exact:

<place id="my_place">
  <name><text>my place</text></name>
  <toolspecific tool="petrex" version="1">
    <id type="atom">my place</id>
  </toolspecific>
  <initialMarking><text>2</text></initialMarking>
</place>

Other tools ignore the tool-specific element, as the PNML standard requires.

Decoding. The identifier of a decoded place or transition is chosen in this order:

1. The Petrex tool-specific <id>, when present. type="string" yields the string. type="atom" yields the atom only if it already exists in the running system (String.to_existing_atom/1); otherwise the string is kept and a warning is added to the result. Decoding never creates atoms, because atoms are not garbage-collected and a document could exhaust the atom table.
2. Otherwise the <name> text, if it is non-empty and unique among the decoded places and transitions.
3. Otherwise the PNML id attribute, as a string.

A net that did not originate in Petrex therefore decodes with string identifiers taken from its names where they are usable, and from its ids where they are not.

The executor is a small, passive GenServer

Petrex.Runner holds one net instance and fires only when asked: step/1, run/2, fire/2. Nothing happens on a timer, and there is no scheduling, retry or persistence. A net that should advance on its own belongs under a process that calls step/1; keeping that out of the library is what stops it from becoming a job runner.

Guards and actions run inside the runner process, which is what makes a firing atomic with respect to the marking. A slow action therefore blocks the net, and the documented pattern is an action that hands work to another process and returns at once, that process later calling put/3.

An action must return exactly the token counts the arc weights specify. Anything else is refused with {:error, {:invalid_action, detail}} and the marking is left alone, because a runner producing a different number of tokens would be running a different net from the one that was analysed.

The executor distinguishes two ways of stopping, matching the analysis vocabulary: :deadlock when no transition is structurally enabled, which is what deadlocks/3 reports, and :quiescent when transitions are enabled but every guard refused. Only the first is a property of the net; the second depends on tokens and can be undone by put/3.

run/2 with :infinity does not return on a net that can keep firing. That is a property of the net, not a bug in the runner, and the analyser is what tells the two apart.

Known tool quirks

Behaviour of external tools that affects nets exported by Petrex. The encoder is not adapted to any of them: it writes standard PNML, and whatever a tool needs is applied on the way to that tool.

TINA merges nodes with the same name

TINA (checked with 4.0.0) identifies places and transitions by their <name> when one is present, not by their id. Two places with different ids but the same name become a single place, silently, and every result TINA reports is then about a different net. PNML allows repeated names, and Petrex.PNML.encode/2 writes labels as names by default, so a net with two places labelled "Buffer" is valid PNML that TINA misreads.

For TINA, export with names: :ids. Every <name> then holds the element's PNML id, which is unique. The external cross-check does this for every net.

TINA does not require ids to be valid xsd:ID, but it fails to read a document in which a place and a transition share an id; Petrex never writes one.

LoLA reads no PNML and restricts names

LoLA 2.0 reads only its own .lola format; TINA's ndrio -PNML -lola in.pnml out.lola converts PNML to it, copying names unchanged. LoLA names cannot contain whitespace or any of , ; : ( ) { }, and cannot be keywords such as PLACE or SAFE. In formulas an all-digit name is read as a number, a name made only of the letters A E F G R U X is read as a temporal operator, and - may be read as subtraction. Exporting with names: :ids removes whitespace and punctuation but not the other cases, so the external cross-check does not pass Petrex identifiers to LoLA at all: every net is sent under positional names (p0, p1, … for places and t0, t1, … for transitions, in definition order) and LoLA's verdicts are mapped back by position. Any identifier, including :EF or "42", can be cross-checked without renaming the model.

State-space statistics from LoLA (--check=full) are only complete with --stubborn=off: its partial-order reduction is otherwise applied and reports fewer markings and edges than the net has.

LoLA occasionally crashes

LoLA 2.0 built for macOS arm64 is occasionally killed by a signal (SIGSEGV, sometimes SIGBUS) on an input it handles correctly on the next run: about 3 runs in 1,000 for a coverability query on a three-place net, with or without --timelimit, and at the same rate in a build without the source fixes applied by tools/install.sh. The external cross-check retries a LoLA run that ends by a signal, up to three attempts, and takes results only from a run that exits normally and reports no error. A crash is never read as an answer.

TINA and inhibitor arcs

TINA reads inhibitor arcs from PNML and applies them correctly in tina -R, but two of its other paths do not:

• tina -C (coverability graph) ignores inhibitor arcs entirely. On a net whose only bound comes from an inhibitor arc, it reports the place as unbounded. Bounds for such nets therefore come from the reachability graph, never from -C.
• tina -R applies a stopping test that aborts the enumeration as soon as a firing sequence increases a marking, printing net possibly unbounded, because boundedness is undecidable with inhibitor arcs. -s 0 turns the test off and enumerates fully, which only terminates for a bounded net.

ndrio -lola refuses nets with inhibitor arcs (net with special arcs), and LoLA 2.0 has no equivalent, so nets with inhibitor arcs are cross-checked against TINA alone.

Hostnames in LoLA JSON output

LoLA's --json output records the host name and build triple of the machine that ran it. The cross-check stores only the analysis results extracted from it, never the raw JSON.