feat(runtime): interrupt an inline do body between its statements

[devin-ai-integration]

What and why

A state's inline do action { s1; s2; s3; } was lowered to one lower.StateBehavior whose block executeBehavior ran to its end in one call, so a do round advanced the whole body as one action and a transition out of the state could interrupt it only between rounds — never between s1 and s2. The one-action-per-statement do { action a; action b; } form already interleaved per statement; state_anonymous_do_atomic pinned the difference (123456 against 124356), and spec-compliance.md carried it as a Known Limitation.

Now a do behavior's statement block yields after each statement it performs, and the do round resumes it one statement at a time:

• bodyRun gains yields (set by startDoRun for do behaviors only) and performed; bodyPause gains yielded. Context.yieldBody pauses the body before its next statement once one has performed since the last resume; Context.bodyPerformed marks one. bodyRun.resume clears performed, so a paused run always makes progress when resumed.
• stmtEngine.run calls yieldBody before each statement after the first, loop/forLoop before each iteration, blockFlow before each node, and marks the body performed after every statement that completes — a simple one, or a compound one (if, a loop) whose branch or iterations performed nothing themselves, so an if selecting an empty branch is a round too. The statements inside a compound one are rounds of their own, so an iteration of two statements is two rounds, and a transition triggered between them leaves the iteration's second statement unrun with the iterations after it. The stmtListFrame/loopFrame/flowNodeFrame cursors already on the continuation stack are what the pause keeps, so locals, nested blocks and loop collections resume exactly where they left off.
• A body stating a token flow (lowerBehaviorBody → stateStmtHost.runFlow → ActionExecutor.driveSubflow) yields after a step in which a token performed a node (an action, a statement node), before the next step that would perform one — control nodes (initial, fork, join, merge, decision) and the end of a wait are routed through without spending a round. With several tokens (after a fork) each steps one node in the round.
• doRun.resume resumes a yielded pause as it does a wait's; doRun.resumable reports a yielded body due at once, so runDoRound picks it through the existing chooseDoAction (entry order by default, seed:<n> draws, explore sweeps). No new choice kind, and choice lines are spelled as before.
• Interruption reuses bodyRun.end: stopDoAction/endDoRun end a yielded run as they end one paused on a wait, so leaving the state (a transition from it or an ancestor, the region left, the machine terminated, the executor released) drops the pending statements with the behavior, and the exit behavior runs after, as before. check spells such a body as yielded between statements.

internal/core/lower is unchanged: the Block the behavior is lowered to already indexes its statements.

Two showcases moved with the granularity, both reproduced by hand against the built binary:

• examples/runtime-showcase/spacecraft-comms.sysml: the transmitData and recharge do behaviors are token flows. At the instant the drain, frame-send and charge timers expire together, the drain and the charge each run in that round (in the schedule's order) and the drain's decision reads the battery in the round after, when the charge's 1 % is in whichever way the round went — so BatteryLow goes out at t=80 with 50 frames sent under every schedule, where the schedules used to differ (t=79/49 frames under reverse/declared, t=80/50 under seed:7/seed:42). The end is the same: transmitted | notRecharging at t=241, 100 frames, battery 100. The summary reads 592 choice points and 808 do behavior actions. README and internal/repl/spacecraft_showcase_test.go follow the observed run.
• state_terminate_entry_do_exit_behaviors: with the go signal queued before the run, the do body is now interrupted after assign later := 5 and never reaches the terminate the fixture is about. The transition out is timed (accept after 1) so the body reaches it; what the fixture proves — terminate in an entry, do or exit body ends that behavior at the statement, the state stays active — is unchanged.

robustness_test.go:testStateDoBodyAcceptRunsBeforeTheChoiceReads keeps its contract (the do behavior goes on with the signal before the transition fires, and the choice reads the rewritten guard); it now also checks that the node after flip runs in the following round rather than the same one.

state_anonymous_do_atomic.trace.golden, before and after

Before, lwork's body ran whole in its round (1, 2, 3), then rwork's (4, 5, 6): 123456. After (entry order, the default policy):

do: lwork                       # round 1: only lwork is active yet — seq 0 → 1
  stmt assign seq … -> 1
exit: rstart / enter: rwork     # the right region reaches rwork
choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first)
do: lwork                       # round 2: lwork's 2nd statement — 1 → 12
  stmt assign seq … -> 12
do: rwork                       # rwork's 1st statement — 12 → 124
  stmt assign seq … -> 124
choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first)
do: lwork                       # round 3: lwork's 3rd statement — 124 → 1243; its body ends
  stmt assign seq … -> 1243
do: rwork                       # rwork's 2nd statement — 1243 → 12435
  stmt assign seq … -> 12435
exit: lwork / enter: ldone      # lwork completed, its succession fires
do: rwork                       # round 4: rwork's 3rd statement, alone — 12435 → 124356
  stmt assign seq … -> 124356
exit: rwork / enter: rdone

124356 is what state_concurrent_do's one-action-per-statement form reaches in entry order; the fixture's .expected.json now admits the same four interleavings (124356, 124536, 142356, 142536), derived in docs/project/behavior-semantic-oracle.md § "Do behaviors of sibling regions active at one instant".

Specification basis

SysML v2 §7.18.3 (state transition semantics), step 1: the source state's do action, "if it is still being performed, is interrupted" when the transition is triggered — now also between the statements of a body written as one inline action. KerML StatePerformances.kerml: the do behavior is a middle performance no succession joins to another region's, so orthogonal regions' bodies interleave.

docs/project/spec-compliance.md: the Known Limitations bullet ("an inline entry/do/exit body is one action…") is removed and the State Machine map row "An inline body is one action, so a do round runs it to its end" is restated as the interruption/interleaving row, ✅ Faithful. docs/guide/06-behavior.md describes the do body as one statement per round. Changelog fragment changes/unreleased/resumable-inline-do-body.changed.md.

How it was verified

New coverage:

• state_do_body_interrupted_by_signal.sysml + .expected.json + trace golden: three statements, Stop accepted after the first — the trace shows s1, the exit behavior and the accept; s2 and s3 never run.
• state_concurrent_inline_do_bodies.sysml + .expected.json + .check.expected.json + default/declared/seed:1 trace goldens: a for loop and an if block in two regions' inline bodies interleave one iteration / one nested statement a round and reach exactly the four interleavings of state_concurrent_do.
• state_anonymous_do_atomic regenerated with -update-traces (above), its .expected.json now an admissible set, .check.expected.json and policy goldens added.
• robustness_resumable_inline_do_body_test.go (TestRuntimeRobustnessResumableInlineDoBody): a for body left mid-loop drops its pending iterations with no frame, do work, clock wait or goroutine left; one left after the first statement of an iteration drops the iteration's second statement too; an if with an empty branch and a while ended at once each spend a round; a body left at a clock wait after a loop leaves the clock empty; a non-terminating loop and a non-terminating stated flow each end with ErrStepLimitExceeded.
• Trace goldens that moved with the granularity: state_do_action_successions_first_start (nodes a and b in two rounds), state_terminate_this_ends_performer (the terminate in the round after the assignment), state_terminate_entry_do_exit_behaviors (see above).

Unchanged: state_concurrent_do.*, the state_terminate_*/action_terminate_* fixtures other than the two named, state_do_action_* sources and expectations, every internal/core/lower test.

Gates:

go build ./...                                            ok
go vet ./...                                              ok
gofmt -l .                                                (empty)
go test ./...                                             ok (all packages)
make lint                                                 ✓ Lint passed
OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 \
  go test -count=1 ./internal/core/model -run 'TestTrainingExamples|TestPilotCorpora'   ok
make docs-check                                           OK
python3 scripts/changelog.py check                        OK
mkdocs build --strict                                     ok
./scripts/download-pssm-suite.sh && go run ./cmd/pssm-referee -check
  pass 46 / fail 17 / not-expressible 38 / differs-by-design 2 — baseline unchanged, no row moved

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

[devin-ai-integration]

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

• Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
• Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

• Disable automatic comment, CI, and merge conflict monitoring