@yxie2/petrinet
DeepSeek Harness 的工作流网运行时：支持资源感知并发、原生循环和扇出，在计划持久化前进行静态正确性检查，并基于其自身的事件日志进行流程挖掘。
插件会安装到这里；不确定时保持 web。
npx -y @deepseek-ai/dsh plugin --profile web add github:yxie2/dsh-petrinet#66526c27796aa67827206727db64c27ab1ffa3ffPetrinet 以 @yxie2/petrinet 发布，当前版本为 0.1.0。Plugin Hub 会校验它的 manifest，并保存精确安装来源，便于复现安装结果。
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:
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.
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.
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:
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.
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.
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.
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.
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.
When a net dies, the driver repairs it in layers:
adaptive — free. Derives parameter changes from the session's own history. No model call, every change backed by an observation.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:
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.| 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.
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.
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/
This is applied work, not invented theory. It leans on:
MIT