Changelog

1.0.0 — 2026-09-18

Added

• Petrex.Net model with places, transitions, weighted normal and inhibitor arcs, and a token-list initial marking.
• Builder: Petrex.new/0, Petrex.place/3, Petrex.transition/3.
• Petrex.Net.validate/1 (also as Petrex.validate/1) reporting every structural error with a path, and Petrex.InvalidNetError for the functions that require a valid net.
• Petrex.Marking conversions between token and skeleton markings.
• Petrex.Analysis.enabled/2 and Petrex.Analysis.fire/3 on the skeleton.
• Petrex.Analysis.reachability/3: breadth-first reachability graph with a marking limit and a choice of map or ETS visited set, returned as a Petrex.Analysis.ReachabilityGraph with accessors for its markings, edges, deadlocks and fired transitions.
• Petrex.Analysis.coverability/3: Karp–Miller coverability tree with ω, returned as a Petrex.Analysis.CoverabilityTree with accessors for its nodes, bounds and the path to a node.
• bound/3, deadlocks/3 and dead_transitions/3, distinguishing exact from partial results, and bounded?/3 and safe?/3, which answer with a boolean or raise Petrex.InconclusiveError rather than guess.
• Petrex.Analysis.invariants/1: minimal-support P- and T-semiflows (Farkas algorithm, integer arithmetic).
• Petrex.PNML.encode/2: PT-net export with sanitised ids, names and the original identifiers preserved in a tool-specific element; names: :ids for tools that identify nodes by name.
• Petrex.PNML.ids/1: the PNML id assigned to each place and transition.
• Petrex.Analysis.workflow_net?/1 and workflow_net/1: workflow net structure, with the reason a net does not qualify.
• Petrex.Analysis.short_circuit/2: the short-circuited net.
• Petrex.Analysis.sound?/2: soundness of a workflow net from one token in the source, with a witness marking or transition.
• reachability/3 option edges: false, which drops the edge list (a quarter to a half of the memory) and still answers state counts, deadlocks and fired transitions.
• Petrex.PNML.decode/1: reads PT-net documents, resolving identifiers from the Petrex element, <name> or the PNML id, summing parallel arcs and reporting each decision as a warning.
• Petrex.PNML.encode/2 writes inhibitor arcs (<type value="inhibitor"/>).
• extra fields on Petrex.Place, Petrex.Transition, Petrex.Arc and Petrex.Net carry elements Petrex does not interpret, including graphics, through a round-trip.
• Petrex.Runner: a GenServer running one net instance, with step/1, run/2, fire/2, put/3, marking/1, ref/1, snapshot/1, restore/2, child_spec/1, conflict-resolution policies, and {:petrex, ref, event} messages to a subscriber.
• Petrex.Analysis.ReachabilityGraph.edges/1 and successors/2, and Petrex.Analysis.CoverabilityTree.node/2, nodes/1 and path_to/2.