dsh-petrinet

A workflow-net runtime for the 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.

dsh plugin add @yxie2/petrinet

New here? Read the introduction — the case for the design, from the shape of the problem to what the runtime does about it. This README is the reference.

---

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:

{
  "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:

{ "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:

{
  "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:

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:

[
  { "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:

- 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:

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

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

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 — 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