Metadata-Version: 2.4
Name: petra-nn
Version: 0.2.0
Summary: Petri-Net Trained Architecture — formally-verified learnable process intelligence
Author-email: Edward Chalk <edward@fleetingswallow.com>
License-Expression: MIT
Project-URL: Homepage, https://fleetingswallow.com
Project-URL: Repository, https://github.com/pcoz/formally-verified-learnable-process-intelligence
Project-URL: Documentation, https://github.com/pcoz/formally-verified-learnable-process-intelligence#readme
Project-URL: Changelog, https://github.com/pcoz/formally-verified-learnable-process-intelligence/blob/main/docs/CHANGELOG.md
Keywords: petri-net,process-mining,bpmn,neural-network,interpretable-ml,formal-verification,bisimulation,anomaly-detection,workflow
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Topic :: Scientific/Engineering :: Information Analysis
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Operating System :: OS Independent
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: torch>=2.0
Provides-Extra: dev
Requires-Dist: pytest>=7; extra == "dev"
Requires-Dist: httpx>=0.27; extra == "dev"
Provides-Extra: docs
Requires-Dist: mkdocs>=1.5; extra == "docs"
Requires-Dist: mkdocs-material>=9.5; extra == "docs"
Requires-Dist: mkdocstrings[python]>=0.24; extra == "docs"
Provides-Extra: onnx
Requires-Dist: onnx>=1.15; extra == "onnx"
Requires-Dist: onnxruntime>=1.16; extra == "onnx"
Provides-Extra: rest
Requires-Dist: fastapi>=0.115; extra == "rest"
Requires-Dist: uvicorn>=0.30; extra == "rest"
Dynamic: license-file

# PETRA

[![PyPI](https://img.shields.io/pypi/v/petra-nn.svg)](https://pypi.org/project/petra-nn/)
[![Python](https://img.shields.io/pypi/pyversions/petra-nn.svg)](https://pypi.org/project/petra-nn/)
[![tests](https://github.com/pcoz/formally-verified-learnable-process-intelligence/actions/workflows/test.yml/badge.svg)](https://github.com/pcoz/formally-verified-learnable-process-intelligence/actions/workflows/test.yml)
[![docs](https://github.com/pcoz/formally-verified-learnable-process-intelligence/actions/workflows/docs.yml/badge.svg)](https://pcoz.github.io/formally-verified-learnable-process-intelligence/)
[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](LICENSE)

> **Not a developer?** Start with the
> [**Business Analyst Guide**](docs/BUSINESS_ANALYST_GUIDE.md) —
> 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](#dont-have-a-petri-net-yet-native-discovery-from-logs)
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](docs/WORKED_EXAMPLES.md)
   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`](examples/safe_refactoring/)
   and [`cost_ranked_refactoring`](examples/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`](examples/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`](examples/onnx_deployment/)
   verifies parity-to-1e-4 against the torch module under
   `onnxruntime`; [`rest_serving`](examples/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`](examples/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](docs/BUSINESS_ANALYST_GUIDE.md)
   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`](examples/cost_ranked_refactoring/), [`credit_approval_coloured`](examples/credit_approval_coloured/), [`incident_management`](examples/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`](examples/distributed_consensus/) (2PC), [`network_protocol`](examples/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`](examples/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`](examples/manufacturing_cell/), [`paint_shop`](examples/paint_shop/), [`batch_packaging`](examples/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`](examples/priority_dispatch/), [`resource_lock`](examples/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`](examples/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`](examples/biological_signalling/), [`mapk_pathway`](examples/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**:

```python
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/`](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](https://www.promtools.org/) 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](https://doi.org/10.1007/978-3-642-38697-8_17)
(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](docs/ROADMAP.md) 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](docs/ROADMAP.md) 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/`](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`](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.

```python
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`](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](https://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`](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`](docs/ROADMAP.md) — framing, phase status,
   what's next.
4. [`docs/WORKED_EXAMPLES.md`](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`](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
```
