FE-761: Petri-net semantic alignment for Petrinaut visualization#156
FE-761: Petri-net semantic alignment for Petrinaut visualization#156kostandinang wants to merge 10 commits into
Conversation
|
Warning This pull request is not mergeable via GitHub because a downstack PR is open. Once all requirements are satisfied, merge this PR as a stack on Graphite.
This stack of pull requests is managed by Graphite. Learn more about stacking. |
kostandinang
changed the title
kostandinang
changed the base branch from
ka/fe-747-petri-declarative-routing
to
graphite-base/156
kostandinang
force-pushed
the
ka/fe-761-petri-petrinaut-semantics
branch
from
778f22f to
8ddb5c1
Compare
kostandinang
changed the base branch from
graphite-base/156
to
ka/fe-755-cook-codebase-mode
kostandinang
force-pushed
the
ka/fe-755-cook-codebase-mode
branch
from
e549e84 to
ecc2cc5
Compare
kostandinang
force-pushed
the
ka/fe-761-petri-petrinaut-semantics
branch
from
8ddb5c1 to
e4be997
Compare
PR SummaryMedium Risk Overview Branching no longer picks output sets inside Long-running steps use Topology counts rise (e.g. Reviewed by Cursor Bugbot for commit 94351f0. Bugbot is set up for automated code reviews on this repo. Configure here. |
Re-apply the four Petrinaut sub-track frontiers committed during the 2026-05-26 cross-team alignment: - petri-petrinaut-semantics (FE-761) — Petri-net-faithful refactor of FE-747 conditional outputs + start/end pairs for agent dispatch. - petri-blueprint-export (FE-762) — Petrinaut-format JSON of NetBlueprint per cook run. - petri-event-stream (FE-763) — initial markings + transition firings in the cross-team-agreed payload shape. - petri-sync-server (FE-764) — transport, brunch -> Petrinaut, one-way v1. Plus Sequencing -> Active item 3 referencing umbrella FE-760 and the Dependencies -> TRACK F branch under petri-declarative-routing. Adds memory/CARDS.md with the FE-761 prepared scope-card queue (Slice 1: sibling transitions for conditional branching; Slice 2 to be scoped after Slice 1 lands). Retires HANDOFF.md per its retirement rule. Co-authored-by: Amp <amp@ampcode.com>
…lingGuard infra
Establishes the producer + sibling-passthrough pattern for Petri-net-faithful
conditional branching. Each conditional action-transition will eventually
decompose into:
1. one producer (kind: action) that runs the work synchronously, attaches
the resulting reportId to the output token, and emits to a single new
intermediate place 'slice:<sliceId>:<step>:reported'
2. N sibling passthroughs that consume from the intermediate place,
evaluate an EnablingGuard against the token's attached report, and
emit to a single fixed output set
Sibling mutual exclusion is enforced at peek time: PetriNet.isEnabled now
evaluates an optional TransitionDef.guard against the first token in each
input place before considering the transition enabled. Complementary guards
across siblings (truthy / falsy on the same report field) ensure exactly
one sibling fires per intermediate token.
This commit applies the pattern to the 'evaluate' transition only. The
remaining branching transitions (run-tests, assess-semantic, verify-epic)
will be decomposed in subsequent Slice 1 commits — each carries stateful
budget / halt concerns that the scope card's risk note authorized to keep
in fire closures for Slice 1.
Topology delta per slice (so far): +1 place (evaluate:reported), +2
transitions (evaluate:done, evaluate:more).
Engine-contract suite (43 tests) green — runtime equivalence preserved.
Co-authored-by: Amp <amp@ampcode.com>
…ss-semantic, verify-epic Extends Slice 1a's producer + sibling-passthrough pattern to the remaining conditional transitions: - run-tests: producer emits to slice:<sid>:run-tests:reported with retry budget; siblings run-tests:pass / run-tests:fail branch via enabling guards. Fail-side halt/budget exhaustion still in fire closure (deferred to Slice 2). - assess-semantic: producer emits to slice:<sid>:assess-semantic:reported; siblings assess-semantic:satisfied / assess-semantic:rejected branch via guards. Rework budget handling remains in fire closure. - verify-epic: producer emits to epic:<epicId>:verify:reported; siblings for pass/fail branch via guards. SiblingPassthroughDescriptor gains optional onFire; verify-epic siblings use onFire to mark epic completed or halted in ctx. All 95 orchestrator tests pass; topology goldens updated for new intermediate places and sibling transitions. Full verify gate green (fmt + lint + build). Refs FE-761 Co-authored-by: Amp <amp@ampcode.com>
…tion) Slice 1 (sibling-transition decomposition for conditional branching) landed across commits 3b7b860 (1a: evaluate + EnablingGuard infra) and 8b76629 (1b: run-tests + assess-semantic + verify-epic). All 95 orchestrator tests green; full verify gate passes. Scope Slice 2 as full scope card: split each producer transition into dispatch:<step> + running:<step>:<scopeId> + complete:<step>:<outcome> sibling pair; retire ctx.halted in favor of a halted:<scopeId> place. This extends the Slice 1 report-bearing-token contract with async completion, unblocking handler invocation from the petri-net step loop. Refs FE-761 Co-authored-by: Amp <amp@ampcode.com>
First tracer of Slice 2 (dispatch/complete decomposition). Makes halt observable at the topology level without yet retiring ctx.halted or introducing async dispatch — those follow in Slice 2b. - New places: slice:<sid>:halted for every slice (retry / semantic-rework exhaustion sink); epic:<eid>:halted for every epic with verification (verify-epic-fail sink). - run-tests producer: on retry exhaustion, emits halt token to slice:<sid>:halted (in addition to legacy ctx.halted mutation). - assess-semantic producer: on rework exhaustion, emits halt token to slice:<sid>:halted similarly. - verify-epic fail sibling: outputs now [epic:<eid>:halted] instead of []; onFire halt-epic still mutates ctx for now. - petri-net.ts BENIGN_RESIDUAL_PLACES: 'halted' added so halt tokens do not trigger spurious net_deadlocked events. Topology tests pin the new halted-place declarations; engine-contract adapter counts updated (simplePlan 16→17 places, depPlan 30→32). All 98 orchestrator tests pass; full verify gate green. Refs FE-761 Co-authored-by: Amp <amp@ampcode.com>
Completes the halted-as-place refactor begun in Slice 2a. Halt is now purely structural: the engine's halt signal is net.hasHaltToken() reading tokens on :halted places, and the halt reason is carried on the halt token itself (Token.haltReason). Changes: - petri-net.ts: Token gains optional haltReason. PetriNet gains hasHaltToken() and getHaltTokens() introspection that scan all places whose suffix is ':halted'. - types.ts: RunCtx loses halted and haltReason fields; doc comment explains the place-token derivation that replaces them. - engine.ts: shouldHalt uses net.hasHaltToken(); post-run derives result.reason from net.getHaltTokens() (first halt token's haltReason) and falls back to 'Some slices or epics were never reached' when outcomes are missing. - net-compiler.ts: run-tests and assess-semantic producers emit a halt token carrying haltReason on budget exhaustion instead of mutating ctx. Sibling-passthrough fire honors a new attach-halt-reason onFire variant by stamping haltReason on the forwarded token; verify-epic fail sibling switched to that variant. - net-blueprint.ts: SiblingPassthroughDescriptor.onFire halt-variant renamed halt-epic → attach-halt-reason; producer doc comments updated to reflect halted-as-place final state. - engine-contract.test.ts: two RunCtx fixtures drop halted: false; the net_halted retry-exhaustion test now uses net.hasHaltToken() as the shouldHalt callback (and is renamed accordingly). All 98 orchestrator tests pass; full verify gate green. Refs FE-761 Co-authored-by: Amp <amp@ampcode.com>
…tch/complete async) Slice 2 landed as two tracers — Slice 2a (commit d2878f9) added the halted:<scopeId> places and emitted halt tokens to them; Slice 2b (commit c58ee62) retired ctx.halted/haltReason entirely, with the engine reading halt status from net.hasHaltToken() and halt reason from the halt token's haltReason field. Original scope card bundled halted-as-place with the dispatch/complete async refactor. In practice those are independent: structural place addition + ctx retirement vs runtime-loop architectural lift. Splitting them shipped a clean structural win without taking on async risk in the same commit window. Dispatch/complete is now Slice 3, still next in queue. Refs FE-761 Co-authored-by: Amp <amp@ampcode.com>
Decouples handler invocation from synchronous fire(), letting the engine
step other independent transitions while handlers are in flight. Chosen
shape: PetriNet exposes scheduleDeferred() that producer fire closures
use to enqueue asynchronous follow-up work, rather than restructuring the
topology into explicit dispatch+complete sibling pairs.
Rationale for the scope adjustment: the original Slice 3 card called for
a topology split (running:* places + complete:<outcome> sibling pairs per
producer). In practice that would have entangled ~6 existing tests that
hardcode <slice>:<step> transition ids while delivering no new
observable runtime behavior beyond what the deferred-fire pattern
already provides. The deferred-fire approach ships the runtime
acceptance criterion (async-completion-ordering) with zero test churn
and preserves all existing topology assertions. The topology split
remains a possible future refinement if richer in-flight observability
is needed.
Changes:
- petri-net.ts: PetriNet.scheduleDeferred(transitionId, contract,
consumedPlaces, work) enqueues a Promise whose resolved output tokens
are deposited into the net when it settles (and a transition_fired
event is emitted for the deferred completion). runSerial and runParallel
await an in-flight deferred completion before declaring deadlock when
no transition is immediately enabled. Errors from deferred work
surface on the next loop iteration via this.deferredError.
- net-compiler.ts: all four producer fire closures (action, run-tests,
assess-semantic, verify-epic) restructured to schedule their handler
invocation as deferred work and return [] synchronously. Agent and
budget tokens stay 'checked out' for the duration of the handler,
preserving pool-size = handler-concurrency-limit invariants.
- engine-contract.test.ts: two test expectations updated to reflect the
new async-dispatch semantics:
* Serial policy now allows concurrent handlers (bounded by agent
pool); test renamed and assertion changed from maxConcurrent === 1
to maxConcurrent > 1.
* Parallel-vs-serial wall-clock test renamed; assertion relaxed to
'parallel no slower than serial + small slack' since both policies
now enable handler overlap.
All 98 orchestrator tests pass; full verify gate green.
Refs FE-761
Co-authored-by: Amp <amp@ampcode.com>
…Slice 4 (Petrinaut topology split) Slice 3 landed via deferred-fire pattern (commit 3f5358d) rather than the original topology split scoped in the card. That delivers the runtime async-completion-ordering acceptance criterion at low cost but does not satisfy FE-761 acceptance criterion (3) — Petrinaut's blueprint export (FE-762) still needs the dispatch + running:* + complete shape to render in-flight state. Scope Slice 4 to deliver that topology piece on top of Slice 3's runtime async substrate. Refs FE-761 Co-authored-by: Amp <amp@ampcode.com>
Petrinaut (FE-762) needs the in-flight phase of every long-running producer to be visible at the net-shape level. Slice 3 delivered async runtime via the deferred-fire substrate but kept the topology unchanged; this slice reifies that runtime split as explicit topology. For each of the 5 per-slice producers (evaluate, write-tests, write-code, run-tests, assess-semantic) and the per-verified-epic verify-epic producer: inputs -> [<step>:dispatch] -> <step>:running -> [<step>:complete] -> outputs The :dispatch transition is synchronous (kind 'dispatch', new descriptor variant): it forwards the work token to the running:* sentinel place, stashing retryCount / reworkCount from the companion budget token so the complete-phase handler can read it back without an extra input arc. The :complete transition keeps the original handler descriptor (action / run-tests / assess-semantic / verify-epic) and continues to schedule the deferred handler invocation. Outcome routing still happens in the existing slice-1 sibling-passthroughs off the :reported intermediate, so no new complete:*:<outcome> siblings were needed. Topology deltas: - simplePlan: +5 places, +5 transitions (17->22 / 14->19) - depPlan: +10 places, +10 transitions (32->42 / 27->37) - verifyPlan: +6 places, +6 transitions (per verified epic) Tests: - topology.test.ts: producer lookups migrated to <sid>:<step>:complete; new golden pinning dispatch-> running:* shape for all 5 producers (+1 test). - engine-contract.test.ts: count goldens updated; descriptor-kinds includes 'dispatch'; event-vocab asserts both :dispatch and :complete fire. - 99 orchestrator tests pass (was 98); npm run fix / check / build all green. Co-authored-by: Amp <amp@ampcode.com>
kostandinang
force-pushed
the
ka/fe-755-cook-codebase-mode
branch
from
ecc2cc5 to
3cc97a2
Compare
kostandinang
force-pushed
the
ka/fe-761-petri-petrinaut-semantics
branch
from
e4be997 to
94351f0
Compare
🤖 Augment PR SummarySummary: Refactors the orchestrator Petri-net compiler/runtime to better match Petrinaut’s visualization semantics (fixed-output transitions + instantaneous firings). Changes:
Technical Notes: Deferred completions now unblock deadlock detection by awaiting in-flight work when no transitions are enabled; halt reason is derived from 🤖 Was this summary useful? React with 👍 or 👎 |
![augmentcode[bot]](https://avatars.githubusercontent.com/in/1027498?s=60&v=4){kind=small}
| haltReason = 'Some slices or epics were never reached'; | ||
| } | ||
|
|
||
| const halted = haltReason !== undefined; |
There was a problem hiding this comment.
src/orchestrator/src/engine.ts:71 — halted is derived solely from haltReason, so a halt token without a haltReason would currently report status: 'completed' even though net.hasHaltToken() was true during the run. It seems safer to derive halted from the structural halt signal (net.hasHaltToken() / getHaltTokens().length) and treat the reason as optional metadata.
Severity: medium
🤖 Was this useful? React with 👍 or 👎, or 🚀 if it prevented an incident/outage.
| this.addToken(place, token); | ||
| producedPlaces.push(place); | ||
| } | ||
| this.deferredEventSink?.emit({ |
There was a problem hiding this comment.
src/orchestrator/src/petri-net.ts:164 — scheduleDeferred() emits a second transition_fired event for the same transitionId that already emitted in depositClaim, which means deferred transitions will appear to “fire” twice in the event stream. If downstream consumers (e.g., Petrinaut/FE-763) assume 1 event per transition firing, this could be a correctness issue.
Severity: medium
🤖 Was this useful? React with 👍 or 👎, or 🚀 if it prevented an incident/outage.
| return out; | ||
| })(); | ||
| net.scheduleDeferred(skel.id, skel.contract, skel.inputs, deferred); | ||
| return []; |
There was a problem hiding this comment.
src/orchestrator/src/net-compiler.ts:642 — Returning [] from these :complete transitions means they consume the running:* token immediately, so the running:* place won’t stay marked for the duration of the async handler (reducing in-flight observability for Petrinaut). This same pattern appears in the other producer completes as well.
Severity: medium
Other Locations
src/orchestrator/src/net-compiler.ts:739src/orchestrator/src/net-compiler.ts:794src/orchestrator/src/net-compiler.ts:876
🤖 Was this useful? React with 👍 or 👎, or 🚀 if it prevented an incident/outage.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 2 potential issues.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 94351f0. Configure here.
| case 'assess-semantic': | ||
| for (const p of h.onSatisfied) out.add(p); | ||
| for (const p of h.onRejected) out.add(p); | ||
| out.add(h.intermediatePlace); |
There was a problem hiding this comment.
Halt place missing from topology output enumerator
Medium Severity
enumerateCandidateOutputs for run-tests and assess-semantic only returns intermediatePlace and budgetPlace, but the fire closures in wireHandlers can also emit to p(sliceId, 'halted') on budget exhaustion. Previously the halt path returned [] so the enumerator was correct, but now that halt emits a token to a real place, this output is invisible to the function documented as the "topology-only enumeration of reachable output places" for "static analyzers (reachability, deadlock detection, simulation)."
Additional Locations (2)
Reviewed by Cursor Bugbot for commit 94351f0. Configure here.
| sliceIdsForEpicVerifyMerge, | ||
| } from './epic-sandbox-merge.js'; | ||
| import { evalRouteGuard } from './net-blueprint.js'; | ||
| import { evalEnablingGuard, evalRouteGuard } from './net-blueprint.js'; |
There was a problem hiding this comment.
Unused evalRouteGuard import in net-compiler
Low Severity
evalRouteGuard is imported but no longer used anywhere in net-compiler.ts. All former call sites were replaced by direct field checks or by evalEnablingGuard in the sibling-passthrough refactor.
Reviewed by Cursor Bugbot for commit 94351f0. Configure here.
1 participant
Summary
evaluate,run-tests,assess-semantic, andverify-epicno longer select between output sets; each producer emits a report-bearing token to a single:reportedintermediate place, and a pair of sibling-passthrough transitions with complementaryEnablingGuards does the routing.slice:<sid>:halted/epic:<eid>:haltedplaces replacectx.halted/ctx.haltReason; the engine derives halt status fromnet.hasHaltToken()and reason from the halt token'shaltReasonfield.<step>:dispatch(sync, kinddispatch) →<step>:running(sentinel place) →<step>:complete(existing handler descriptor, scheduled deferred). Handler invocation no longer blocks the petri-net step loop.Context
HandlerDescriptoroutput-set selection (onTrue/onFalse/onPass/onFail/onSatisfied/onRejected) which this frontier dismantles in favor of sibling transitions.reportId, consistent with the cross-team-agreed payload shape.What changed
net-blueprint.ts: newEnablingGuardtype (peek-time predicate over the input token's attached report); newSiblingPassthroughDescriptor(with optionalonFirehook for epic-completion mark / halt-reason stamp); newDispatchDescriptor;enumerateCandidateOutputsupdated for the new variants. The producer descriptors (action/run-tests/assess-semantic/verify-epic) lost their branching fields and now each emit one fixed output set.net-compiler.ts: per slice, every former producer compiles as two transitions (:dispatch→:complete) around a new:runningsentinel place, plus the existing:reportedintermediate + sibling-passthrough pair.wireHandlersgot adispatchcase (forwards the work token to the running place, stashingretryCount/reworkCountfrom the companion budget token so the complete-phase handler can read it back).run-tests/assess-semanticcomplete handlers updated accordingly.petri-net.ts:TransitionDef.guardenforces peek-timeEnablingGuardmutual exclusion inisEnabled.Tokengains optionalhaltReason.PetriNetgainshasHaltToken()/getHaltTokens()introspection andscheduleDeferred(transitionId, contract, consumedPlaces, work);runSerial/runParallelawait in-flight deferred completions before declaring deadlock.engine.ts/types.ts:RunCtx.halted/RunCtx.haltReasonremoved; engine's halt signal isnet.hasHaltToken()and reason is derived from halt tokens.simplePlan(1 slice): 17 → 22 places, 14 → 19 transitions.depPlan(2 slices): 32 → 42 places, 27 → 37 transitions.verify:runningplace, +1:haltedplace, +1:dispatchtransition.Verification
fixtures/txt/semantics; deferred-fire substrate proven by serial-policy concurrency oracle (maxConcurrent > 1under serial when handler-bound).npm run verify(check + test + build) green.Out of scope
petri-blueprint-export, FE-762).petri-event-stream, FE-763).petri-sync-server, FE-764).Traceability
petri-petrinaut-semanticsinmemory/PLAN.md; scope cards 1–4 inmemory/CARDS.md; stacks on FE-747.