# An introduction to dsh-petrinet *A workflow-net runtime for the DeepSeek Harness. It exists so that a plan which **can** deadlock is refused before it runs — not discovered forty hours in.* > This is the argument for the design. For the reference documentation — tools, configuration, module layout — see the [README](../README.md). --- ## Plans that share things Picture a long-running agent plan with two branches. Both need the repository lock and a CI slot. One branch takes the lock first; the other takes the slot first. Most runs are fine. Occasionally each grabs one and waits for the other, and the plan stops making progress. What makes this hazard distinctive is that it is not about the order of the work. Every step sits in a sensible position and nothing is missing. The trouble lives in *who is holding what at a given moment* — it is a property of the plan's state, and it surfaces only on particular interleavings, which is what makes it easy to run into and hard to reproduce. Long-horizon work runs into this class of problem often, because that is where plans get long enough to hold several things at once. So dsh-petrinet models a plan as state. That turns *"can this plan get stuck?"* into a question with a computable answer — one you can ask once, before any work begins. --- ## Put the resources in the graph A workflow net expresses *state*, not just order. 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 does an enormous amount of work. A place holding *k* tokens **is** a *k*-way semaphore — no scheduler required, because the firing rule already refuses. ```mermaid flowchart TB slots(("ci_slots
0 of 2 free")) b1(("branch 1")) --> t1["acquire"] b2(("branch 2")) --> t2["acquire"] b3(("branch 3
•")) --> t3["acquire
blocked"] t1 --> r1(("running
•")) t2 --> r2(("running
•")) t3 -.-> r3(("running")) slots --> t1 slots --> t2 slots -.->|needs 1, holds 0| t3 ``` *Three branches each want one `ci_slots` token. Two acquired and are running; the resource place is now empty, so the third simply cannot fire. Nothing in the driver enforces this — the firing rule does. When a branch finishes it returns its token and the third unblocks.* In the spec that compiles to this net, the entire concurrency policy is one line: ```js resources: [{ id: "ci_slots", capacity: 2 }] ``` The same model carries three more things directly. A loop is a cycle in the structure, so retry-until-good and poll-until-ready are ordinary shapes rather than special cases. A fan-out can be *n* tokens wide where *n* is discovered at runtime. And "wait for every branch" and "take exactly one branch" are structurally distinct, which is what lets the analyser reason about each correctly. --- ## Now the deadlock is in the graph, so it can be found This is the part worth the whole design. Because resources are ordinary places, a plan's deadlocks are ordinary reachable states — and sixty years of Petri net theory knows how to look for them. Every plan is analysed *before* it enters the durable log. Within an exploration budget the verdict is a proof, not a heuristic: the three soundness conditions checked over the concretely enumerated reachability graph. Can the plan always still finish? Does finishing leave nothing behind? Is every step reachable at all? Here is a plan that reads as perfectly sensible — 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" }}}}}} ]}} ``` It is refused: ``` PETRI_UNSOUND_PLAN: net is unsound: 2 deadlock marking(s) reachable; 1 reachable marking(s) can no longer reach the final marking ``` And the analyser hands back the exact state it would have died in, which is what makes the message actionable rather than merely discouraging: ```mermaid flowchart TB b1(("branch 1 •
holds lock A")) --> ab["acquire B
blocked"] b2(("branch 2 •
holds lock B")) --> aa["acquire A
blocked"] lockA(("lock A
0 free")) lockB(("lock B
0 free")) lockB -.->|needs 1, holds 0| ab lockA -.->|needs 1, holds 0| aa ``` ```json { "deadlockExample": { "p.guard.g1.body": 1, "p.guard.g3.body": 1 } } ``` Each branch holds one lock and needs the other; both lock places are empty, so neither blocked transition can ever fire. Branch 1 took A then wanted B, branch 2 took B then wanted A — that opposite ordering *is* the bug. Acquire in a consistent order, or widen either resource, and the same plan verifies `SOUND`. ### It says so when it does not know Exhaustive exploration has a budget, and a tool that quietly reports success when it ran out of room is worse than no tool. Past the cap the verdict is `UNKNOWN`, never an optimistic `SOUND`. Violations found by concrete counterexample stay definite even under a cap — a deadlock marking has no enabled transitions regardless of what went unexplored — so the two kinds of answer are kept honestly apart. --- ## The model writes structure, not arcs Language models are good at nested task structure and bad at emitting places, transitions and arc weights. So the Petri net is the *intermediate representation* and never the thing anyone types. What the model writes is a small pattern language: | node | meaning | |---|---| | `task` | one unit of real work, dispatched to a subagent | | `seq` | run in order | | `parallel` | split, run concurrently, join when all finish | | `choice` | take exactly one branch | | `loop` | repeat until the exit branch is taken | | `foreach` | discover *n* items at runtime, run the body per item, gather | | `guard` | hold a semaphore for the duration of the body | Every one of these lowers to a fragment with exactly one entry place and one exit place, and composing such fragments is closed under the workflow-net shape. The consequence is worth stating plainly: **the control-flow patterns are sound by construction.** You cannot write a malformed join or an unreachable branch through this language. Which is what lets the analyser concentrate on the question composition leaves open: resource-induced deadlock. That is the hazard which appears only when independent branches contend for the same things, and it is the one most worth knowing about before a run rather than during it. --- ## Nothing self-certifies A subagent that believes it succeeded is not evidence that it did. So every firing is two-phase, and the phases are separated by an independent adjudication. ``` stage input place the firing output place ───────────────────────────────────────────────────────────── 1 · enabled ● ▮ ○ token available 2 · claimed ○ ▮ ● ○ reserved, not destroyed 3 · reported ○ ▮ ● "exit 0" ○ nothing has moved 4 · verified ○ ▮ ● committed ``` Claiming reserves the input tokens under a lease. The worker's report is a *declaration about the environment* and moves nothing at all. Only independent verification produces the output token — and on a failed verdict the reserved tokens return to where they came from and the step burns one attempt. A confident-but-wrong subagent cannot advance the net. One consequence is worth spelling out: the marking is **derived, never stored**. Re-folding the session log reconstructs the exact runtime state, so crash recovery, replay and time-travel debugging are not features anyone had to build. A worker that dies silently simply has its lease expire, its tokens returned, and its transition re-enabled. --- ## The log was already an event log Here is the pleasing part. The durable event stream — case identifier, activity, order, outcome — is, with no extra instrumentation whatsoever, exactly the input format for process mining. And process mining's canonical *output* is a Petri net. The thing you plan in and the thing you learn in turn out to be the same object. So the system can score a proposed plan against what actually happened rather than against a model's own optimism. That gives a blunt and useful rule: *a repair that fits history worse than the plan it replaces is not a repair.* Repair runs cheapest-first. The free layer reads the session's own history and proposes concrete parameter changes, each backed by a counted observation — a retry budget that was demonstrably too tight, a semaphore that sat drained while work queued behind it. Only if that finds nothing does the model get asked to author a replacement plan, and it authors it in the same pattern language everyone else uses. Both proposals then pass the same soundness gate as a human plan. That gate is the whole difference between a system that adapts and a system that quietly rewrites itself into a corner: a model that proposes a deadlock gets a rejection, not a stuck net. --- ## What it does not do - **Soundness is bounded, and says so.** Past the exploration cap the answer is `UNKNOWN`. Large plans with many concurrent resource holders are where you will meet it. - **Structural change is never automatic.** Mining reports a step that never fired; it does not delete it. Widening a budget is reversible arithmetic. Rewriting a plan is a decision, and stays one. - **Patience is capped.** A step that has never once succeeded gets exactly one extra attempt, once. Past that the tool says so in the rationale it emits rather than ratcheting its own budget upward run after run. - **Mining inherits the alpha algorithm's blind spots** — short loops, duplicated activities, invisible routing steps. A low fitness score is a question worth asking, not a verdict. --- ## Three tools, one habit ```bash dsh plugin add @yxie2/petrinet ``` The habit worth forming is calling `petri_analyze` before `petri_plan`. It compiles and checks a candidate plan without committing anything, which turns a deadlock from a lost run into a free correction made while the plan is still a draft. `petri_insights` then closes the loop, reporting what the last run actually taught you. Defaults cost nothing: deterministic choice, no repair, no model calls beyond the planning itself. `repair: adaptive` is also free — it reads history rather than a model — and is the first thing worth turning on. The engine underneath — firing semantics, lowering, analysis, fold, mining — has zero runtime dependencies and its suites run under Node's type stripping with no install and no build. A regression there is a regression in the mathematics, not in the integration, and it is meant to stay that way. --- Built for the [DeepSeek Harness](https://github.com/deepseek-ai/deepseek-harness), and indebted to [dsh-mission](https://github.com/qiaoy01/dsh-mission), whose principle — *agents propose, the environment adjudicates, the runtime commits* — this package adopts wholesale, along with its event-sourced, compare-and-set approach to durable planning state. The two install side by side. Standing on van der Aalst on workflow nets and soundness, the Workflow Patterns catalogue and YAWL, and Rozinat & van der Aalst on conformance checking.