@yxie2/petrinet

Readme

# dsh-petrinet

A **workflow-net runtime** for the [DeepSeek Harness](https://github.com/deepseek-ai/deepseek-harness). It models a long-horizon plan as *state* — tokens sitting in places, transitions consuming and producing them — which gives it three properties:

1. **Resource-aware concurrency.** A semaphore, a mutex, an API quota, a "only one agent may touch the repo at a time" rule — all one declaration, enforced by the same firing rule that drives everything else.
2. **Native loops and runtime fan-out.** Retry-until-good, poll-until-ready, and "run once per item you discover" are ordinary structure.
3. **Static soundness checking before a plan becomes durable.** A plan that can deadlock is *refused at commit time*, with a concrete counterexample — before any work begins.

On top of that it mines its own execution log to propose evidence-backed improvements to the plan.

```bash
dsh plugin add @yxie2/petrinet
```

New here? **[Read the introduction](docs/introduction.md)** — the case for the design, from the shape of the problem to what the runtime does about it. This README is the reference. 中文读者请看**[中文简介](docs/introduction.zh-CN.md)**。

---

## What a workflow net models

Places hold tokens. Transitions consume tokens from their input places and produce them into their output places. A transition may fire only when every input place holds enough. That single rule carries a lot:

| | how it is expressed |
|---|---|
| **Concurrency limits** | a place holding *k* tokens **is** a *k*-way semaphore |
| **Loops** | a cycle in the structure |
| **Runtime fan-out width** | *n* tokens in a place = *n* parallel work items |
| **AND-join vs XOR-join** | structurally distinct |

And because it is a Petri net, sixty years of analysis comes with it: reachability, boundedness, conservation laws, and a decidable notion of **soundness**.

---

## The soundness gate

This is the feature worth the whole design.

Every plan is statically analysed before it enters the durable log. Within an exploration budget the verdict is a **proof**, not a heuristic — van der Aalst's three conditions checked over the concretely enumerated reachability graph:

1. **Option to complete** — every reachable state can still reach the end.
2. **Proper completion** — reaching the end means nothing is left behind.
3. **No dead transitions** — every step is reachable somewhere.

Here is a plan that looks entirely reasonable. Two branches, each needing two locks:

```json
{
  "resources": [{ "id": "A", "capacity": 1 }, { "id": "B", "capacity": 1 }],
  "flow": { "parallel": [
    { "guard": { "resource": "A", "body": { "guard": { "resource": "B", "body": { "task": { "id": "w1" } } } } } },
    { "guard": { "resource": "B", "body": { "guard": { "resource": "A", "body": { "task": { "id": "w2" } } } } } }
  ] }
}
```

`petri_plan` refuses it:

```
PETRI_UNSOUND_PLAN: net is unsound: 2 deadlock marking(s) reachable;
1 reachable marking(s) can no longer reach the final marking
```

and `petri_analyze` hands back the state it would have died in:

```json
{ "deadlockExample": { "p.guard.g1.body": 1, "p.guard.g3.body": 1 } }
```

Both branches holding one lock, each waiting for the other. Classic lock inversion, caught before a single token was spent. Widen either resource, or acquire in a consistent order, and the same plan verifies `SOUND`.

**When the answer isn't known, it says so.** Past the exploration cap the verdict is `UNKNOWN`, never an optimistic `SOUND`. Violations found by concrete counterexample stay definite even under a cap, because a deadlock marking has no enabled transitions regardless of what went unexplored.

---

## The model writes structure, not arcs

Models are good at nested task structure and bad at emitting places, transitions and arc weights. So the Petri net is the **intermediate representation**, never the surface syntax. The model writes a small pattern DSL:

```json
{
  "resources": [{ "id": "repo_lock", "capacity": 1 }, { "id": "ci_slots", "capacity": 3 }],
  "flow": { "seq": [
    { "task": { "id": "survey", "name": "Survey the codebase" } },
    { "foreach": { "id": "each_pkg", "over": "packages needing migration",
                   "body": { "guard": { "resource": "ci_slots",
                             "body": { "task": { "id": "migrate" } } } } } },
    { "guard": { "resource": "repo_lock",
                 "body": { "loop": { "id": "green", "maxIterations": 5,
                           "body": { "task": { "id": "fix_tests" } } } } } }
  ] }
}
```

| node | meaning |
|---|---|
| `task` | one unit of real work, dispatched to a subagent |
| `seq` | run in order |
| `parallel` | AND-split, run concurrently, join when all finish |
| `choice` | XOR-split, take exactly one branch |
| `loop` | repeat until the exit branch is taken (`maxIterations` bounds it) |
| `foreach` | discover *n* items at runtime, run the body once per item, gather |
| `guard` | hold a semaphore for the duration of the body |

Every pattern lowers to a fragment with exactly one entry and one exit place, and composition of such fragments is closed under the workflow-net shape. **The control-flow patterns are therefore sound by construction.** The analyser exists to catch what composition cannot guarantee: resource-induced deadlock — which is where real long-running plans actually fail.

---

## Tokens move only on verification

Every firing is two-phase, and the phases are separated by adjudication:

```
claim    consume the input tokens under a lease   (reserved, not destroyed)
   |
execute  dispatch a subagent
   |
report   the worker's DECLARATION about the environment   <- moves nothing
   |
verify   independent adjudication                          <- the only thing that moves tokens
   |
   +-- passed  -> produce the output tokens
   +-- failed  -> return the consumed tokens, burn one attempt
```

A confident-but-wrong subagent cannot advance the net. Nothing self-certifies.

The marking is **derived, never stored** — re-folding the session log reconstructs the exact runtime state, so crash recovery, replay, and time-travel debugging come free. A worker that dies silently has its lease expire, its tokens returned, and its transition re-enabled.

---

## Concurrency comes from the net

The driver does not schedule. It fires whatever the net enables, and the net's resource places decide how much of that can happen at once:

```js
resources: [{ id: 'slots', capacity: 2 }]
```

is the entire implementation of a two-way concurrency cap. From the test suite:

```
capacity 1 -> peak concurrency 1
capacity 2 -> peak concurrency 2
capacity 3 -> peak concurrency 3
```

`maxConcurrency` on the driver is a second, coarser ceiling on top of that — a safety limit, not the mechanism.

---

## Learning from the log

The event stream is, with no extra instrumentation, a **process-mining event log**: case id (the net revision), activity (the transition), order, outcome. That is the canonical input to a field whose canonical *output* is a Petri net. The loop closes on itself.

`petri_insights` reports two things:

**Conformance.** Token-replay fitness of a candidate plan against what actually happened. This is how a proposed repair is judged against history instead of against the model's own optimism — *a repair that scores worse than the plan it replaces is not a repair*.

**Adaptations.** Concrete numbers, each backed by a counted observation:

```json
[
  { "kind": "maxAttempts", "target": "t.flaky", "current": 3, "suggested": 4,
    "rationale": "hit its budget of 3 yet committed elsewhere in history (worst streak 3); the failures are transient" },
  { "kind": "resourceCapacity", "target": "ci_slots", "current": 3, "suggested": 4,
    "rationale": "drained to zero while 18 further acquisition(s) were otherwise ready; widening it raises real concurrency" }
]
```

`alphaMine` additionally rediscovers a net from observed behaviour, so you can diff *what you planned* against *what actually happens*.

### Self-repair, cheapest first

When a net dies, the driver repairs it in layers:

1. **`adaptive`** — free. Derives parameter changes from the session's own history. No model call, every change backed by an observation.
2. **`llm`** — the model authors a replacement **workflow spec**, which goes through the same compiler as the human path and inherits the same sound-by-construction patterns. It is handed the analysis report verbatim, including the concrete deadlock marking, because *"here is the exact state you got stuck in"* is far more actionable than *"your plan failed"*.

**Both proposals pass the soundness gate before committing.** A model that proposes a deadlock gets a rejection, not a stuck net. That gate is what separates this from unbounded self-modification.

Structural change is never applied automatically from mining — a dead-transition observation is *reported*, never acted on. Widening a budget is reversible arithmetic; rewriting the plan is a decision.

Honest limits, stated up front:
- The retry probe is capped (`RETRY_PROBE_CEILING`). A step that has never succeeded gets exactly one more attempt, once — past that, more patience is not the answer, and the code says so in the rationale it emits.
- The alpha algorithm cannot see loops of length one or two, duplicate activities, or invisible routing steps. Treat a low fitness score as a question, not a verdict.

---

## Tools

| tool | purpose |
|---|---|
| `petri_create` | open a net for a long-horizon objective |
| `petri_analyze` | **compile and check a candidate plan without committing it** |
| `petri_plan` | commit a plan as the next revision (CAS; refused if unsound) |
| `petri_status` | marking, enabled transitions, choice points, every firing |
| `petri_insights` | conformance against history + evidence-backed adaptations |
| `petri_cancel` | abort the current net |

Plus a `/petri` slash command (`status` / `analyze` / `cancel` / `<objective>`).

`petri_analyze` is the one worth encouraging: it turns a deadlock from a forty-hour loss into a free planning-time correction.

---

## Configuration

Defaults cost nothing — deterministic choice, no repair:

```yaml
- id: petri-driver
  name: '@yxie2/petrinet/driver-host'
  config:
    decider: llm          # deterministic (default) | llm — only consulted at real choice points
    repair: both          # off (default) | adaptive | llm | both
    maxConcurrency: 4
    approveRepairs: false
```

`repair: adaptive` is **also free** — it reads history, not a model — so it is the first thing worth turning on.

The `llm` decider is only consulted where transitions genuinely compete for the same tokens. Uncontested progress and control transitions cost no model calls at all.

---

## Architecture

```
compile.ts     workflow DSL  ->  workflow net        (sound by construction)
soundness.ts   structural | invariants | reachability (the gate)
net.ts         the firing rule: enabling, conflict, marking algebra
fold.ts        events -> state (the marking is derived, never stored)
validate.ts    admissibility, incl. the soundness gate on every revision
mining.ts      traces, alpha algorithm, conformance, adaptations
  |
  +-- zero runtime dependencies; runs under `node --experimental-strip-types`
  |
driver.ts      the concurrent firing loop
service.ts     ctx.petri  — event-sourced, CAS revisions
tools.ts / trigger.ts / driver-host.ts / invariant.ts / projection.ts
```

The whole engine — semantics, lowering, analysis, fold, mining — is deliberately free of harness dependencies. Its test suites need no install and no build:

```bash
node --experimental-strip-types tests/net.test.mjs
```

A regression there is a regression in the mathematics, not in the integration.

```bash
npm test         # all suites
npm run build    # typecheck + emit lib/
```

---

## Prior art

This is applied work, not invented theory. It leans on:

- **W.M.P. van der Aalst**, *The Application of Petri Nets to Workflow Management* (1998) — workflow nets and soundness.
- **van der Aalst, ter Hofstede et al.**, *Workflow Patterns* (2003) and **YAWL** — the pattern set the DSL implements.
- **van der Aalst**, *Process Mining* — the alpha algorithm and token-replay conformance.
- **Rozinat & van der Aalst**, *Conformance Checking of Processes Based on Monitoring Real Behavior* (2008) — the fitness metric.
- **[dsh-mission](https://github.com/qiaoy01/dsh-mission)** — the principle this package adopts wholesale (*agents propose, the environment adjudicates, the runtime commits*), together with its event-sourced, compare-and-set approach to durable planning state. The two install side by side.

## Licence

MIT