feat(runtime): draw a due do step against the dispatch under check, replay and explore - #438
Open
devin-ai-integration[bot] wants to merge 13 commits into
Open
devin-ai-integration[bot] wants to merge 13 commits into
devin-ai-integration[bot] wants to merge 13 commits into
Conversation
…eplay and explore Under one-move scheduling the state executor offers one step of each due do action and the dispatch the machine would make now together, recorded as a ChoiceStepOrder (`at t=<instant>: next do <state>, dispatch <event>`); once every due do action has stepped the dispatch owed is made before another round opens. The fixed policies keep running the whole do round before dispatching, so no default trace moves. The checker's enabledMoves mirrors that unit, and a change condition's transition is now named deterministically. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
…s suite state_do_step_or_dispatch and state_do_step_among_completions record the draw between a due do step and the dispatch under default, declared, seed:1 and check; the robustness suite refuses step-order lines naming a move the unit does not offer and bounds an endless do behavior under explore. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ts occurrence A dispatch that would defer or drop the occurrence at the head of the pool is not drawn against a due do step: the due step may be the accept that takes it, so the occurrence waits for the round to close, as under the fixed policies. The join fixtures lose the incomplete-join outcome the draw reached through a completion or timer that could not act, and the semantic oracle states the rule. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ce map and PSSM baseline Behavior 003 A moves to pass; Exiting 002 moves to fail on the order the suite registers for the same race in Behavior 003 A and not for this test, recorded as the suite's defect; Terminate 002 and Transition 017 reach the do step's admitted places and stay on their remaining reasons. The design record states the implemented grain, one step of a do action, and the token-move grain that follows the resumable inline do body. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ne after the self-model's choice kind count moved Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ng the dispatch against a due do step A dispatch tied between an event that would fire and one that would be dropped was judged as a whole and not drawn, so check and explore missed the schedules where the firing event dispatches before the do step. dueDispatch now previews the tied events one by one; the acting ones alone are the step order's dispatch alternatives, and nextEvent draws among the same set when that alternative is taken, so replay and the checker's picks name the event the runtime dispatches. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…eue would dispatch it A message in flight is queued behind the events already there before the next event is taken, so the dispatch offered against a due do step is the head of the queue with the signal counted in, not the signal itself: a queued event nothing accepts hides it until the round closes, a queued event that acts is drawn by its own name, and the signal is named (dispatch accept <signal>) only once nothing is ahead of it. The checker's moves, replay and the run draw among that same set. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…step-order Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/pilot-differential-baseline.json
…step-order Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/pilot-differential-baseline.json # examples/self-model/execution.sysml # internal/exec/runtime/robustness_region_do_step_test.go # internal/exec/runtime/step_order_pending_signal_test.go # internal/exec/runtime/step_order_tied_test.go # internal/exec/runtime/testdata/conformance/state_do_step_among_completions.check.expected.json # internal/exec/runtime/testdata/conformance/state_do_step_among_completions.declared.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_among_completions.expected.json # internal/exec/runtime/testdata/conformance/state_do_step_among_completions.seed-1.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_among_completions.sysml # internal/exec/runtime/testdata/conformance/state_do_step_among_completions.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_or_dispatch.check.expected.json # internal/exec/runtime/testdata/conformance/state_do_step_or_dispatch.declared.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_or_dispatch.expected.json # internal/exec/runtime/testdata/conformance/state_do_step_or_dispatch.seed-1.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_or_dispatch.sysml # internal/exec/runtime/testdata/conformance/state_do_step_or_dispatch.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_or_tied_dispatch.check.expected.json # internal/exec/runtime/testdata/conformance/state_do_step_or_tied_dispatch.declared.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_or_tied_dispatch.expected.json # internal/exec/runtime/testdata/conformance/state_do_step_or_tied_dispatch.seed-1.trace.golden # internal/exec/runtime/testdata/conformance/state_do_step_or_tied_dispatch.sysml # internal/exec/runtime/testdata/conformance/state_do_step_or_tied_dispatch.trace.golden
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What and why
Implements the do-step site of
docs/internals/design/region-order-scheduling.md: undercheck,replayandexplorethe state executor no longer runs a whole do round before it dispatches. At each unit it offers one step of each due do action and the dispatch the machine would make now together, drawn under the newChoiceStepOrderand recorded aswith
do <state>per due state (round order) followed bydispatch <event>/dispatch change <transition>, or a baredispatchwhere tied events leave the event to their own draw. Once every due do action has stepped, the dispatch owed is made before another round opens.declared,reverseandseed:<n>keep running the whole round (runStep→runDoRound) and dispatch after it, so no default, declared or seed trace golden moves;runUnitroutes only one-move scheduling (scheduler.oneMove()) throughoneUnit.enabledMovesmirrorsoneUnit(closed round → its dispatch alone; a due round with an acting dispatch → the do steps picked by place, the dispatch moves prefixed with the picklen(due); either alone → picked only where a draw is made), socheckandexploreagree.risenChangerecords the transitions in observation order so the change-trigger alternative is named deterministically.A dispatch is drawn only where it acts.
dueDispatchpreviews the dispatch (eventActs, under the same probeDecideuses, rolled back): a dispatch that would fire a transition or let a do behavior parked at anacceptgo on competes with the due do step; one that would defer or drop the occurrence does not, since the due step may be theacceptthat takes it, so the occurrence waits for the round to close as under the fixed policies. Without that rule the draw spent an occurrence a do behavior was one action from accepting — a run no policy of the runtime makes and none the library orders. The two join fixtures (state_join_completion_segment_waits_for_do_behavior,state_join_completion_is_not_a_timers_expiry) therefore keep their four outcomes;behavior-semantic-oracle.mdstates the rule and the new fixtures' sets. Events tied at the head are judged one by one:dueDispatchpreviews each, the acting ones alone are the step order's dispatch alternatives (one by name, several as the baredispatchwhose dispatch order is then drawn among them alone), andnextEventdraws among that same set when the dispatch alternative is taken, so the checker's picks, replay and the runtime name one event. A tied trigger the dispatch would drop therefore hides no tied trigger it would fire (state_do_step_or_tied_dispatch: a guarded and an unguarded timer tied at the instant the do step is due, outcomesdid one,did two,two). A signal in flight is read the same way:dueDispatchtakes the head, or the tied events, of the queue asdeliverPendingSignalleaves it (EventQueue.With, a copy with the signal pushed under the ID and instantenqueueSignalgives it), so the signal is drawn as the queue would dispatch it — hidden by a queued event nothing accepts until the round closes, behind a queued event that acts drawn by that event's name, and nameddispatch accept <signal>only once nothing is ahead of it; the descriptor never offers a dispatch the queue would not make.Design delta. The record specified the draw at token-move granularity: a due do behavior's flow stepped one token move at a time with the machine free to dispatch after each, so a dispatch may cut a sweep anywhere. That depends on the resumable inline do body pausing per token (
executeBehavior/doRun), owned elsewhere. This PR draws at do-action-step granularity: one move is onestepDoAction— one statement of an inline do body, one action of a do behavior given as actions, the unitrunDoRoundalready steps — against the head-of-pool dispatch. That is the granularity reachable today and the one Behavior 003 A needs. Kept until the token refinement, and stated as a known limitation inspec-compliance.mdand the record:checkstill names do round before dispatch as not enumerated where a step left a token standing before a dispatch (state_do_action_loop_timed_exitkeeps its fixed-policyexpected.json; the record's "exactoutcomesset" for it is the token-granularity follow-up). The record's do-step section is rewritten to describe what is implemented, the acting-dispatch rule, and what the token grain changes (stepRoundalone).Finding 11 (a completion pending inside the entry front) is not in this PR: it is independent of the do-step site and stays on its own branch; the rows attributed to it in
pssm-referee.mdare unchanged.PSSM referee (
go run -C tools ./cmd/pssm-referee,-check,-filter "Behavior 003")Before: 51 pass / 13 fail / 38 not-expressible / 1 differs-by-design. After: 51 / 13 / 38 / 1, with these rows moved and adjudicated per row in
pssm-referee.md(baseline re-recorded with-update):fail→pass: both admitted orders reached (S1(entry)::S1(doActivityPartI)andS1(entry)alone, the dispatch first).pass→fail: now also reachesS1(exit)— the tester'sContinuedispatched before the do activity's first segment, which the exit aborts. The suite registers exactly this order for the same race one test earlier (Behavior 003 A) and not here; recorded as the suite's defect inomg-issues.md(new section and table row), nodiffers-by-designrow added.fail→fail, reason changed: the two admitted traces with the terminating completion before the do activity's first segment are reached; the one trace left,S1(entry)::S1.1(entry)::S1.1(doActivityPartI)::S2.1(entry), is finding 11's.fail→fail, reason changed: every admitted place ofdeep(doActivity)among the completion effects is reached; the two remaining traces are the suite defect already recorded, no new row.Specification basis
StatePerformances.kermlStatePerformance(succession do.startShot then nonDoMiddle.startShot;middle then exit),TransitionPerformances.kermlStateTransitionPerformance(accept then transitionLinkSource.exit), PSSM 1.0 §8.5.5 do-activity concurrency, as derived indocs/internals/design/region-order-scheduling.md. Adds a row tospec-compliance.md(How it was verified
go build ./...,go vet ./...,gofmt -l .(empty),go test ./...(full,-count=1),make lint— green at this head (merged withorigin/developafter its layering refactor; the new tests and fixtures live underinternal/exec/runtime/).OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 go test -count=1 ./tests/corpus -run 'TestTrainingExamples|TestPilotCorpora'— pass (both gates ran, corpora present).make docs-check(0 broken links),python3 scripts/changelog.py check,mkdocs build --strict— green.-checkpasses against the re-recorded baseline;-filter "Behavior 003"2 pass / 0 fail.go run -C tools ./cmd/pilot-diff -checkreproduces every count (378 files, 347 fully agreeing; 38 agreed / 38 only ours / 1185 only the pilot's); only theexamplesdigest moved, because the self-model'schoiceKindCountis now 10, sopilot-differential-baseline.jsonis re-recorded with-update(digest and date only).state_do_step_or_dispatch(outcomesdid stop,stop),state_do_step_among_completions(did m r,m did r,m r did) andstate_do_step_or_tied_dispatch(did one,did two,two) with.expected.json,.check.expected.jsonand default/declared/seed-1 trace goldens;TestExecutionConformance,TestExecutionTrace,TestCheckConformanceOraclescover them.robustness_region_do_step_test.go(TestRuntimeRobustnessRegionDoStep): a witness naming a state with no due do step, a dispatch not at the head, a draw at a unit offering none — each refused withErrReplayRefusedand the run restored; an endless do body underexploreends inErrDoStepLimitExceeded.step_order_tied_test.go(TestStepOrderDrawsTheActingTiedEventAlone): the check over the tied fixture is complete with the three outcomes, every witness's one step order isdo top, dispatch time top 2->idle, the dispatch order is drawn exactly when the step goes first, and each witness replays to its own trace.step_order_pending_signal_test.go(TestStepOrderDrawsThePendingSignalAsQueued): withStopin flight while a do step is due, a queuedNoisenothing accepts yields the one outcomedid stopand no step order, a queuedGoyieldsdid go/gowith the step order amongdo top, dispatch accept Go, and the signal alone yieldsdid stop/stopamongdo top, dispatch accept Stop; every witness replays to its own trace.TestReplayRefusedJoinDrawChangesNothing(the witness loses the step-order line the acting rule no longer draws; refusal at move 4, state restored), round trips of everyChoiceStepOrderspelling.Checklist
make testandmake lintpass locallychanges/unreleased/<slug>.<section>.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (compliance rows need nothing: the census is counted at docs build)F4,K5) in the body, docs, or changelog