petra-nn 0.2.0

Petri-Net Trained Architecture — formally-verified learnable process intelligence

PETRA

Not a developer? Start with the Business Analyst Guide — a no-code, no-maths walkthrough of every concept in this framework (Petri nets, BPMN translation, coloured tokens, bisimulation, training, rule extraction, the lot) aimed at process analysts, compliance officers, and project managers.

PETRA (Petri-Net Trained Architecture) learns how a discrete-event system routes through its structure from its execution logs — fitting per-transition firing propensities conditional on the input marking, over a Petri-net substrate that you either supply or have PETRA discover from the same logs — and turns the learned dynamics into four things you can act on:

• Readable decision rules — distilled from the trained weights in domain vocabulary, e.g. "if amount > £1,000 → credit-review."
• Anomaly scores — pinned to specific named elements, not opaque whole-trace numbers.
• Formal equivalence proofs — strong bisimulation between two variants, before either is deployed.
• Cost rankings — over behaviour-preserving refactorings, fitted to your observed workload.

Take a loan-approval process and 10,000 recorded loans. PETRA tells you which rules the actual decisions follow ("if amount > £1,000 the application gets a credit-review"), flags loans that took unusual paths (someone skipped the credit check on a high-value application), and lets you compare two candidate redesigns of the process — proving they do the same thing and showing which one costs less to run on the observed workload. The same primitives cover distributed-system protocols, manufacturing lines, laboratory recipes, multi-agent coordination, IT incident management, and biology signalling pathways.

PETRA's two inputs are a Petri net describing the system's structure and an execution log of how it actually ran. You can supply both, or supply only the log and have PETRA discover the Petri net from it via the basic Inductive Miner — a single log can drive the entire pipeline. A Petri net is the standard formal model for this class of system:

• places hold tokens (work items, requests, messages);
• transitions move tokens between places (a step firing);
• arcs between places and transitions capture the control flow.

PETRA compiles the Petri net into a neural network whose topology is the Petri net — one trainable weight per arc, one trainable threshold per transition, nothing else can be learned. Training fits the network to the log. Because every parameter corresponds to a named element of the original structure, the trained model stays interpretable: every parameter has a name from your domain, and rule extraction, anomaly scoring, counterfactuals, and sensitivity analysis all speak in those names.

---

What this unlocks (the non-obvious parts)

The framework name says "Petri-Net Trained Architecture", which sounds narrowly technical. The practical wins are larger than the name suggests:

1. A business process is one kind of process — and the same machinery handles all the others. Loan approvals, distributed-system protocols, manufacturing lines, biological signalling pathways, IT incident flows, laboratory procedures, multi-agent coordination, network protocols. The 21 shipped scenarios deliberately span eleven domains to make the point that process is a category that crosses industries — PETRA's substrate sits at that general level, not at the BPMN level.

2. Process refactoring becomes as safe as code refactoring. Bisimulation proves two designs behave identically before deployment; cost ranking picks the cheaper of the equivalent ones. The same shift that made software's iterate-fast culture possible in the 1990s, applied to operating-model design. The safe_refactoring and cost_ranked_refactoring scenarios pin this end to end.

3. Regulator-grade model documentation is mechanical. Counterfactuals on declined cases, sensitivity rankings of which inputs the model leans on, bootstrap CIs on the learned thresholds, plain-English prose helpers — the four artefacts GDPR Article 22, SR 11-7, and the EU AI Act all expect on automated decisioning models — are produced by single function calls. See regulator_ready_credit_approval for the four together on one business case.

4. The trained model deploys anywhere. The same .onnx file serves from JVM workflow engines, C++ inference servers, browser-based decisioning UIs (onnxruntime-web), mobile devices, and accelerator stacks (TensorRT, OpenVINO, DirectML). A FastAPI app over the same module exposes inference, anomaly scoring, counterfactuals, and sensitivity over HTTP for any non-Python consumer. Pin evidence: onnx_deployment verifies parity-to-1e-4 against the torch module under onnxruntime; rest_serving exercises every REST endpoint through TestClient.

5. Log-only is a first-class entry path. If you have history but no model, the basic Inductive Miner mines a sound Petri net directly from the log and discover_and_train chains discover → verify → compile → train in a single call. For very noisy logs, ProM's noise-filtering miners stay the recommended pre-step — PETRA reads their PNML output unchanged. See discover_and_train_pipeline.

6. Every scenario is declarative. No Python boilerplate per scenario. The 21 shipped scenarios are TOML configs plus a standard test harness; adding a new one is one TOML file plus one paired test. The framework is also honest about its limits — the Business Analyst Guide §17 carries a long-form treatment of where coverability hits the inhibitor-arc Turing-undecidability boundary. That honesty is what makes §22's substrate-for-a-self-organising-system claim credible rather than handwavy: knowing exactly where the formal-tractability boundary sits is what lets you build above it without descending into chaos. PETRA stays inside its boundary and tells you precisely where the boundary is, which is the precondition for anything else sitting safely on top.

The rest of this README is the formal story behind those six — guarantees, comparisons with classical Petri-net tools, the toolchain walkthrough on a bank-loan unification case, and the economic framing of where the value sits.

---

Three layers of guarantee

PETRA's positioning sits at the intersection of formal methods and learned dynamics. It's worth being precise about which guarantees come from where, because the three layers are genuinely different:

1. The Petri-net substrate is structurally verified. Bisimulation (strong and weak), Aalst soundness, deadlock localisation, CTL temporal-logic model checking all operate on the Petri net itself and its reachable-marking graph. These are mathematical proofs about the structure — not about anything that has been learned.

2. The compiled neural topology preserves the substrate. By construction, parameters exist only at the arcs and transitions of the Petri net (one trainable weight per arc, one trainable threshold per transition). The structural constraint of layer 1 carries through verbatim into the trained model — there is no weight outside the flow relation that could "learn around" the verified structure.

3. The learned parameters are interpretable and testable — not themselves formally verified. Rule extraction reads them as decision rules; bootstrap CIs report their stability under data resampling; counterfactual analysis and per-input sensitivity make the dependence on inputs auditable; cross-variant comparison reports empirical agreement over a chosen input domain. These are empirical guarantees about learned dynamics, not formal guarantees in the layer-1 sense — and that distinction matters when you're talking to a regulator or a model-risk committee.

Equivalence proofs and cost-ranked refactoring exist at the intersection of these layers — the structural equivalence check is layer 1, the cost numbers come from layer 3's trained firing-probability outputs, and the layer-2 topology preservation is what makes the two compose.

---

What it works on

PETRA fits any finite-state, terminating, discrete-event system for which you have observable execution traces of multiple instances. That class is much larger than it sounds — for each domain below, the second column says why it doesn't look like an ML target at first glance, and the third says why the substrate fits anyway:

Domain	Why this isn't obvious	Why it fits anyway	Shipped scenarios
Business processes	BPM tools handle workflows; generic ML handles logs. The two are usually treated as separate problems with separate tools.	A BPMN diagram is a Petri net. The structural verification supplies interpretability and formal analysis; the logs supply the learning signal. Both at once, in one trained model.	cost_ranked_refactoring, credit_approval_coloured, incident_management
Distributed-system protocols	Protocols are hand-specified state machines. You write the spec; you don't learn it.	The spec gives the structure. Production traces show how the deployed system actually behaves — including attack patterns and Byzantine faults that aren't in the spec. PETRA flags the deviations.	distributed_consensus (2PC), network_protocol (TCP)
Multi-agent coordination	Multi-agent systems are usually studied with game theory or reinforcement learning, not formal models.	Coordination protocols (contract-net, FIPA-ACL) are explicit message-passing flows. Each agent's state machine plus the inter-agent message places compose as a multi-pool Petri net naturally.	multi_agent_coordination
Manufacturing & supply chain	Simulated with domain-specific tools (Simio, AnyLogic); ML in this space usually means demand forecasting, not workflow modelling.	Production lines literally are discrete-event token systems — parts moving between stations, batches accumulating, quality gates routing. The Phase 9 primitives (multi-token arcs, durations, inhibitor arcs) model these directly.	manufacturing_cell, paint_shop, batch_packaging
Operational coordination	Priority dispatch and mutex feel like OS-level concerns, not "process intelligence".	Any system using these primitives has them in its control flow. Modelling at the Petri-net level lets you analyse the system's actual coordination against the protocol it declares.	priority_dispatch, resource_lock
Laboratory & clinical protocols	Lab protocols feel domain-specific (chemistry, biology) and are usually owned by proprietary LIMS systems.	A protocol is a sequenced, gated workflow with deviations to flag — same shape as a business process. The lab's electronic logs are already structured.	scientific_workflow (PCR)
Cell-biology signalling pathways	Pathway analysis is a biology problem; ML usually means gene expression or protein structure, not "train a model of the pathway".	Reactome-style pathway databases literally store pathways as Petri-net structures: places are molecule pools, transitions are reactions. The activation channel is the natural soft analogue of pathway flux.	biological_signalling, mapk_pathway (real Pathway Commons SIF)

The same primitives cover more ground than the shipped scenarios exercise: state machines in embedded software, regulatory and compliance workflows, games with bounded state, contract / treaty / agreement workflows, scientific data pipelines, RPA scripts.

PETRA works best when all four properties below hold:

Property	What it means
Discrete events	State changes at identifiable moments (a transition firing), rather than continuously over time.
Multiple-instance trace data	You have many recorded runs of the system to learn from. One run isn't enough.
Stable structure for training	The place/transition graph stays fixed while you learn the dynamics within it.
Tractably finite state space	The compiled Petri net fits in memory and trains in reasonable time. Thousands of places and transitions work fine; problems that need a whole economy or the entire internet at full resolution don't fit.

Fluid dynamics, classical mechanics, analogue control, and similar continuous-time / continuous-state physics need a different substrate — Petri nets are discrete by design.

What you get out of it

PETRA combines a fixed verified topology with learned dynamics within it. Each individual capability below is possible in isolation with some other tool — but only PETRA gives you all four over a single trained model:

Capability	What it means in practice
Interpretability at named domain elements	Every parameter corresponds to a BPMN task, a biological pathway component, a protocol state — not an opaque vector index.
Formal equivalence checks	Strong bisimulation between two trained models, before either is deployed: "this redesign behaves identically to the old version."
Anomaly detection at the transition level	Residuals pinned to specific transitions — "the credit-check step didn't fire when the data says it should have" — not opaque whole-trace scores.
Cost-ranked refactoring	Provably-equivalent variants compared by realised-execution cost on the trained firing distribution: "Variant B is provably equivalent to Variant A and 6× cheaper."

PETRA's shape fits problems with explicit place/transition structure. Arbitrary sequence modelling (free-text, unrestricted time-series) fits something else.

---

Don't have a Petri net yet? Native discovery from logs

If you have execution logs but no structural model, PETRA discovers one — one library call:

from petri_net_nn import discover_and_train, parse_xes

traces = parse_xes("history.xes")
net, module, losses = discover_and_train(
    traces,
    attribute_to_marking=lambda t: {},
)

net is a Petri net sound by construction; module is trained against the same log. Every capability above — rule extraction, anomaly scoring, counterfactuals, sensitivity, bisimulation, CTL, cost ranking — applies unchanged.

The same pipeline runs declaratively from a TOML config: see examples/discover_and_train_pipeline/ for the worked artefact — net.source = "discover" in the scenario config invokes the Inductive Miner directly from load_scenario, with end-to-end test coverage pinning soundness, replay, and training-loss convergence.

Honest framing. PETRA discovers structure from clean-to-moderately-noisy logs, and uniquely couples that discovery with a trainable, formally-verifiable, interpretable model of the same process. For very noisy logs, pre-filter with ProM and feed the PNML to PETRA — the rest of the pipeline applies unchanged.

Where PETRA's native discovery works well	Where ProM-then-PETRA is the better path
Logs from BPM engines (Camunda / Activiti / Flowable history exports)	Highly variable real-world logs with noise
Synthetic or instrumented logs	Logs with concept drift over time
Well-defined activity vocabularies	Logs where body-only loops dominate (e.g. (a, b, a, b) patterns)

The miner is the basic Inductive Miner (Leemans, Fahland, van der Aalst, 2013) — it covers the four canonical structural patterns (sequence, exclusive choice, parallel, loop with redo). Noise-tolerant variants (IMf, IMi) live in ProM today; PETRA reads ProM's PNML output directly via parse_pnml, so the bridge is a one-liner.

PETRA's unique contribution is what happens after the structure is in hand — training, verification, rule extraction, anomaly detection, counterfactual explanation, cost-ranked refactoring — none of which the discovery tools do. PETRA and ProM are complementary, not alternatives. For a clean log, PETRA's native discovery is enough on its own. For a noisy log, you run ProM's noise-filtering miners first, then hand the resulting PNML to PETRA — same pipeline, either way.

---

What makes this approach unusual

Capability	Most ML	Classical Petri-net analysis	This framework
Learns from execution traces	✓	✗	✓
Preserves verified structure	✗	✓	✓
Bisimulation-based equivalence	✗	partial	✓
Interpretable at named elements	✗	n/a (no learning)	✓
Detects structurally-grounded anomalies	weak	✗	✓
Ranks behaviour-preserving variants by cost	✗	✗	✓

The bisimulation + cost-ranking combination is what makes provably-safe process refactoring possible: refactor a process, prove the new version is behaviourally equivalent to the old one, then rank the variants by realised-execution cost. Nobody else has that running with tests.

---

How PETRA fits with classical Petri-net tools

PETRA is complementary, not competitive, to the established Petri-net tool ecosystem. Each classical tool answers a different question over the same Petri-net structure:

Tool	What it's best at	Where PETRA differs
CPN Tools (Aarhus)	Reference implementation of Coloured Petri Nets — full ML-style colour-set typing, state-space verification, mature GUI simulator.	CPN Tools verifies a given CPN; PETRA trains a model of how the net's transitions are actually used from execution traces, including learning guard thresholds from per-token values rather than taking them as given. CPN Tools' colour sets are far richer than PETRA's CPN-lite scalar token values.
GreatSPN (Turin)	Generalised Stochastic Petri Nets — exponentially-distributed firing times, analytical CTMC throughput, performance bounds.	GreatSPN gives closed-form stationary throughput under a stipulated rate model; PETRA's stochastic rates are compiler-level multipliers used during training. Different question.
TINA (LAAS-CNRS)	Time Petri nets with intervals, state-space exploration, integrated CTL/LTL model checking via NuSMV.	TINA proves temporal-logic invariants about the specified behaviour; PETRA fits transition-firing propensities to observed traces and flags deviations from those learned propensities. Phase 11 wires CTL in directly (check_ctl).
ProM (Eindhoven)	Process mining — Alpha / Inductive / Heuristics miners discover a Petri net from execution logs; conformance checking; large plugin ecosystem.	PETRA now does structure discovery natively too, via the basic Inductive Miner (discover_inductive). For very noisy logs ProM's noise-tolerant variants (IMf / IMi) remain the recommended pre-filter — PETRA reads the PNML they emit directly. The tools stay a natural pair: clean log → PETRA alone; noisy log → ProM then PETRA.

The thing PETRA does that none of them do: combine a learned-from-traces dynamics model with a structurally verified Petri-net substrate, then extract interpretable rules from the learned weights and rank behaviour-preserving refactorings by cost. None of those four tools touch any of those four capabilities.

A complementary analysis stack

The five tools naturally compose end-to-end on the same model:

1. ProM discovers the structure from logs.
2. CPN Tools verifies its soundness.
3. GreatSPN gives stochastic throughput bounds.
4. TINA proves temporal invariants.
5. PETRA learns the dynamics that actually occur in production, distils the routing rules, detects deviations, and ranks refactorings.

PNML support is the bridge that makes this stack possible — any of those tools' output can now feed straight into PETRA. That's why PNML is high-leverage despite being only a few hundred lines of code: it converts PETRA from a standalone Python library into an ecosystem citizen, one PNML file away from any of the above.

---

Using the whole toolchain together

Suppose a bank wants to unify the loan-approval process across two regional offices that have drifted apart over the years. The shared starting point is the offices' logs — tens of thousands of recorded applications each, all the routing decisions captured, no documented "correct" process to refer back to.

The five tools work through it in order:

1. ProM runs an inductive miner over each office's log and produces a Petri net per office. You now have two structural models discovered directly from data, where before there was nothing.

2. CPN Tools opens each net and verifies elementary soundness — proper completion, deadlock-freedom, boundedness. Both pass; the offices' actual behaviour does conform to a sound workflow net.

3. GreatSPN annotates the nets with stochastic firing rates derived from the same logs and computes closed-form throughput bounds. Office A maxes out at ~250 applications/day, Office B at ~180/day.

4. TINA specifies the regulatory invariants the bank's compliance team cares about — "every approved loan eventually fires the audit-log transition", "no decline fires without a prior credit-check" — and model-checks each net against them via CTL. Office A passes both; Office B violates the audit-log invariant on a small subset of paths, surfaced as a counterexample trace.

5. PETRA takes the verified nets plus the original logs and:

   • Trains each into a differentiable model whose weights correspond to the offices' actual routing decisions.
   • Distils the trained weights into readable rules — Office A approves at amount > £5,000 with a strict credit-check gate; Office B at amount > £8,000 with a more lenient gate. Same shape, different thresholds.
   • Runs strong bisimulation between the two trained nets. They are not equivalent — which is the answer to "are the offices doing the same thing?" (they aren't).
   • Scores held-out applications for anomalies pinned to specific transitions, so the compliance team can see which Office B traces actually skipped the audit-log.
   • Ranks two proposed unified processes by realised-execution cost on the combined trace distribution, with bisimulation proving each is behaviourally equivalent to a reference variant.

The output is something the bank's process team can act on:

• an evidence-backed comparison of the two offices,
• a verified equivalence claim (or proof that one doesn't hold),
• a cost-ranked redesign, and
• a list of compliance-flagged traces to investigate.

None of the five tools alone produces all of that. The PNML format is the bridge — each tool's output can be read by the next without bespoke glue.

---

Why this matters

The walkthrough above isn't just a tidy demo. It collapses several pieces of work that today require separate teams and months of effort into one analytical pipeline. Three questions worth asking about it: how valuable is the capability, what are organisations paying today to approximate it, and why is it genuinely hard.

How valuable is this capability?

In one pass over real logs, the chain produces four things any large institution would want about its own operating model:

• Evidence-backed comparison of how two units actually operate, not how they think they operate.
• Verified equivalence claims — proof that a redesign hasn't silently changed behaviour.
• Cost-ranked redesigns fitted to real workload, not stipulated by consultants.
• Transition-level compliance flags that point a regulator (or an audit team) at specific named traces and the specific named transition each one diverged at.

The strategic frame is unlocking process change at organisational scale. Most large institutions are stuck in the change-aversion equilibrium the ROADMAP describes: redesigns are risky, so they don't happen, so legacy variation accumulates, so the next redesign is even riskier. Making refactoring safe is the same shift that transformed software engineering in the 1990s and 2000s. Applied to banks, insurers, hospitals, telcos, this is operating-model-level value, not tooling-level.

What do organisations pay today to approximate this?

The work is currently spread across several budget lines, none of which delivers the full chain:

Spend category	Typical scale
Process-mining licences (Celonis, Signavio, UiPath Process Mining, Disco, Apromore)	£50k–£500k+/year per enterprise deployment; Celonis enterprise contracts routinely run into seven figures annually.
Business-process / management consulting for redesign and harmonisation (McKinsey, BCG, Bain, Deloitte, Accenture)	£2k–£5k+ per consultant-day; a typical "unify the two offices" project runs £500k–£5M over 6–18 months.
Compliance and audit tooling plus dedicated compliance headcount	Varies widely; for a regulated bank, easily £1M+/year on a single workflow class.
BPM platforms (Camunda, Pega, Appian, IBM BPM)	Six- to seven-figure annual licences, plus implementation partners on top.

Crucially, no current vendor sells the equivalence-proof + cost-ranked-refactoring combination the walkthrough produces. Process mining tells you what happened; it doesn't prove two redesigns are behaviourally equivalent, and it doesn't rank them by cost with formal guarantees. That gap is where the consulting spend goes — and consultants reach a judgement, not a proof.

Why is it hard to get today?

Several difficulties compound:

• Skill scarcity. The chain needs process mining, formal methods (bisimulation, model checking), stochastic modelling, ML, and domain expertise. Almost nobody has all of these; assembled teams pay an integration tax.
• Tool fragmentation. ProM, CPN Tools, GreatSPN, and TINA each have their own input formats, UIs, and learning curves. PNML helps, but stitching the chain into a deployable workflow is bespoke work each time.
• Equivalence proofs aren't actually being established. Even with the tools in place, the load-bearing claim — that a redesign behaves identically to the original — is rarely proved. Teams settle for "it passes UAT" and "stakeholders signed off," which is why redesigns stay risky.
• Months-to-years cycle time. Process redesign at large institutions is a multi-quarter project; ERP-class reimplementations run multiple years. The risk is high enough that change-aversion is rational — which keeps the cycle long, which keeps the risk high.
• Outputs aren't actionable at the transition level. Process-mining heatmaps tell you "this area is slow" but rarely give a compliance officer a list of specific named traces and the specific named transition each one diverged at. The walkthrough above does exactly that.

Net: the capability is valuable, current spend on partial substitutes is large and fragmented, and the gap PETRA targets — verified equivalence and cost-ranked refactoring grounded in real logs — isn't actually filled by anything else on the market.

What gets disrupted, and what doesn't

A reasonable follow-up question — does this vaporise the change-management market? The honest answer is yes for the largest slice, but with three explicit qualifiers.

Where the framing holds. The change-management market is largely sized by the risk of process change. Consultants get paid in proportion to that risk, because someone has to absorb it — through interviews, workshops, target-state modelling, shadow-running, UAT, post-go-live war rooms. If a redesign can be mechanically proven to behave identically to the original and ranked by realised cost against the actual workload, the risk collapses. A lot of the spend that exists to manage that risk loses its reason to exist. The walkthrough's four outputs replace expensive judgement calls with cheap, repeatable, auditable artefacts. That is the same shape as what happened to manual QA once test automation matured, or to manual deployment once CI/CD matured.

Where it doesn't. Three slices of the change-management market survive intact:

Slice	Why it survives
The people side	Stakeholder alignment, training, communications, org redesign, incentive restructuring. PETRA proves a redesign is behaviourally equivalent — it doesn't make people accept it or rewire who reports to whom.
Deciding which redesigns to propose	The substrate verifies and ranks candidates; it doesn't generate them. Until candidate-generation is automated (the ROADMAP flags this as missing on top of PETRA), someone still has to imagine the alternatives — that's domain consulting work.
The regulated-industry layer	Compliance sign-off, regulator engagement, model-risk governance. A formal proof helps but doesn't replace the regulatory dance — and in some jurisdictions the regulator wants a human on the line.

Net: PETRA collapses the risk-absorption slice of the market — which is the largest and most expensive — but leaves the judgement, change, and governance slices intact. Roughly: the McKinsey/BCG/Bain redesign-engagement layer shrinks dramatically; the Prosci/ADKAR change-adoption layer doesn't.

---

Worked examples

PETRA ships with 21 end-to-end scenarios under examples/, each a self-contained TOML configuration plus a paired test driving the full pipeline. They span deliberately different domains — provably-safe process refactoring, native log-to-net discovery, real BPI Challenge incidents, distributed consensus, TCP handshakes, contract-net coordination, manufacturing cells, mutex / inhibitor patterns, multi-token batching, transition durations, firing-rate priors, laboratory protocols, biological signalling cascades — to make the point that the substrate isn't just for business processes.

The full table, sorted by use case rather than chronology of addition, lives in its own document so the README stays focused on the framing:

→ docs/WORKED_EXAMPLES.md

Run any individual scenario with python -m pytest tests/scenarios/test_<scenario_name>.py, or the whole set with python -m pytest tests/scenarios/.

---

Quick start

pip install petra-nn

Requires Python 3.11+ and brings torch in as a dependency.

from petri_net_nn import load_scenario

# Each example/ subfolder contains a self-contained scenario as
# a TOML config plus an explanatory README.
ctx = load_scenario("examples/cost_ranked_refactoring/scenario.toml")
module, losses = ctx.train()
rules = ctx.extract_rules(module)
print(rules["xor"][0].description())

The PyPI distribution name is petra-nn (the bare petra was already taken on PyPI); the importable Python package is petri_net_nn. For the framework-level API (build a PetriNet by hand, compile, train, extract rules, score anomalies), see docs/DEV_MANUAL.md.

---

Repository layout

petri_net_nn/         # the framework
  petri_net.py        # PetriNet dataclass + token-game semantics
  bpmn.py             # BPMN 2.0 → PetriNet parser
  pnml.py             # PNML 2009 P/T-net import / export
  sif.py              # Pathway Commons SIF import (biology pathways)
  compiler.py         # PetriNet → differentiable nn.Module
  subnets.py          # five hand-built reference subnets
  traces.py           # training, anomaly score, expected-cost, AUC
  xes.py              # IEEE XES log loader (plain + gzipped)
  anomalies.py        # corruption generators + frequency baseline
  interpretability.py # distil learned weights into rules
  bisimulation.py     # strong + weak bisimulation equivalence checking
  soundness.py        # Aalst soundness + deadlock localisation
  coverability.py     # Karp-Miller coverability for unbounded nets
  ctl.py              # CTL temporal-logic model checking
  adapter.py          # config-driven scenario loader

examples/             # 21 end-to-end scenarios — see docs/WORKED_EXAMPLES.md
tests/                # framework + scenario tests
docs/
  BUSINESS_ANALYST_GUIDE.md  # plain-English concepts primer for non-coders
  ROADMAP.md                 # product roadmap, phase status, framing
  DEV_MANUAL.md              # framework + adapter usage guide

---

Reading order

The full set of long-form docs is also published at pcoz.github.io/formally-verified-learnable-process-intelligence (MkDocs Material site, auto-built and deployed on every push to main, includes an auto-generated API reference pulled from the package's docstrings).

1. This README — what PETRA is and what to do with it.
2. docs/BUSINESS_ANALYST_GUIDE.md — a no-code, no-maths walkthrough of every framework concept (Petri nets, BPMN translation, coloured tokens, bisimulation, the lot) aimed at process analysts, compliance officers, and project managers.
3. docs/ROADMAP.md — framing, phase status, what's next.
4. docs/WORKED_EXAMPLES.md — the twenty-one scenarios under examples/ sorted by the use case each represents; from here drill into any individual scenario's own README for the long-form story.
5. docs/DEV_MANUAL.md — adapter config and framework API reference.

---

Running tests

python -m pytest                          # full suite (~492 tests)
python -m pytest tests/scenarios/         # only end-to-end scenarios
python -m pytest tests/test_compiler.py   # only the compiler