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

changes/unreleased/resumable-inline-do-body.changed.md

@@ -0,0 +1 @@
+- **A state's inline `do` body is interrupted between its statements.** `do action { s1; s2; s3; }` runs one statement per do round — each statement of a `for` or `while` iteration, of a nested block or branch its own, one step of a flow the body states (each of its tokens one node) — so a transition out of the state triggered after `s1` leaves `s2` and `s3` unrun, as §7.18.3 has the source state's do action interrupted "if it is still being performed"; the `exit` behavior runs as before. The inline bodies of orthogonal regions interleave statement by statement, as the one-action-per-statement `do { … }` form does, the order within a round the same do-round choice point. A body paused mid-loop when its state is left drops the rest of the iteration and the iterations after it with nothing kept on the clock, and a non-terminating inline body still ends with the do-step budget.

docs/guide/06-behavior.md

@@ -336,16 +336,17 @@ body stating no flow still runs its statements in declaration order. The three b
 in *when* they run: entry and exit are performed whole at the instant the state is entered or
 left (as is a transition's `do` effect), so a body of theirs that waits on the clock is refused
 with `state behavior waits for the clock`; the `do` behavior runs while the state is active,
-one action per round, and may wait. An `accept after` in a do body parks it on the shared clock
-and `%advance` moves it; an `accept Sig` parks it until a matching signal is sent — `%send Sig`
-takes it though no transition fires on it, reporting that the do behavior goes on. A do behavior
-performs once — when its body ends, the state has completed and a completion transition out of
-it, if any, fires — and leaving the state for any other reason abandons what is left of it: its
-waits leave the clock, nothing after the wait runs, and an `inout` pin writes its value back to
-the bound attribute only when the performance ends (an `inout` pin valued by an enumeration
-literal or another constant, `inout mode = Mode::idle`, starts from that value and writes back
-nowhere). `Poll` below counts once at `t=3.0`, the
-state is left at `t=10.0`, and `ticks` reads `1`:
+one statement per round — each statement of a `for` or `while` iteration and of a nested block
+or branch its own, one step of a flow the body states, each of its tokens one node — and may wait. An `accept after` in a do body parks it on the shared clock and `%advance`
+moves it; an `accept Sig` parks it until a matching signal is sent — `%send Sig` takes it though
+no transition fires on it, reporting that the do behavior goes on. A do behavior performs once —
+when its body ends, the state has completed and a completion transition out of it, if any, fires
+— and leaving the state for any other reason abandons what is left of it: the statements after
+the one it last ran do not run, its waits leave the clock, and an `inout` pin writes its value
+back to the bound attribute only when the performance ends (an `inout` pin valued by an
+enumeration literal or another constant, `inout mode = Mode::idle`, starts from that value and
+writes back nowhere). `Poll` below counts once at `t=3.0`, the state is left at `t=10.0`, and
+`ticks` reads `1`:
 
 ```sysml
 sysml> package Watch {

docs/project/behavior-semantic-oracle.md

@@ -853,7 +853,8 @@ A completion event precedes both, never drawn.
 
 ### Do behaviors of sibling regions active at one instant: each proceeds, in which order is open
 
-Fixtures: `state_concurrent_do` (golden, explored), `state_concurrent_do_action_bodies_timed`
+Fixtures: `state_concurrent_do` (golden, explored), `state_anonymous_do_atomic` (golden, explored),
+`state_concurrent_inline_do_bodies` (golden, explored), `state_concurrent_do_action_bodies_timed`
 (golden, explored).
 
 ```
@@ -884,7 +885,13 @@ this section. The order is a choice point under every policy, reported as `choic
 t=0.0: states lwork, rwork react (unordered; took lwork first)`: `declared` and `reverse` take the
 order the states were entered in — a tool-defined order — and the default golden pins that
 linearization (`124356`); `seed:<n>` draws the order; `explore` varies it and must reach all four
-values and no other. `state_concurrent_do_action_bodies_timed` is the shape with action bodies
+values and no other. `state_anonymous_do_atomic` is the same machine with each body written as one
+inline action, `do action { … }`, of three statements: an inline body yields after each statement,
+so it interleaves as the one-action-per-statement form does and reaches the same four values, not
+`123456`. `state_concurrent_inline_do_bodies` writes the left body as a `for` loop over 1..2 followed
+by a statement and the right one as a statement followed by an `if` block of two: an iteration and a
+statement of a nested block are each one step, so the same four values and no other are reached.
+`state_concurrent_do_action_bodies_timed` is the shape with action bodies
 that wait on the clock: both behaviors pause at an `accept after 2 [s]` and are due again in the
 round at `t=2.0`, where the order of the two counts is open (`1324` entering order, `3124` the
 other), while the counts at `t=4.0` and `t=5.0` are alone in their rounds.

docs/project/spec-compliance.md

@@ -758,7 +758,7 @@ checked after the result is bound is not a form the runtime offers, and none is
 | An entry, do or exit behavior written as an inline action body (`entry action { … }`, `do action named { … }`, `exit action { … }`) executes the statements it states, locals and loops among them, in any nesting of composite states; an empty body is a behavior that does nothing | `lower/state_behavior.go` `LowerBehaviors`/`lowerStateBehavior` (the body is lowered to a `Block`, its locals in the block's own frame), `lower/state_graph.go` `StateGraph.Behaviors`; `runtime/state_statements.go` `executeBehavior`/`stateStmtHost` | `parser/testdata/parse/state_anonymous_action_body.golden`, `state_anonymous_action_body.sysml` + trace golden (entry/do/exit ordering, nesting, empty bodies), `robustness_test.go:testEmptyAnonymousActionBody`, `:testNonTerminatingAnonymousDoBody` (`ErrStepLimitExceeded`) | ✅ Faithful |
 | An inline entry, do or exit body that states a token flow of its own — successions (`first start; then action a; then done;`, `first a then b;`), forks, joins, decisions with guards, and action nodes with a flow of their own — runs that flow as a standalone action's body does: `then done` completes the behavior, the attributes the body declares are the performance's own (defaults evaluated where written, a node's assignment read by the next, shadowing the machine's without writing it), a dangling or unstartable succession, or the body or a node of it declaring `return`, is a typed error before any node runs; a flow no `first` starts begins at its one node no succession leads to (`do action poll { action wait accept after 3 [s]; then action count assign ticks := ticks + 1; }`), two such nodes or a cycle leaving the start unstated and reported, in the flow a nested node states as in the body's own | `lower/state_behavior.go` `lowerBehaviorBody` (a body stating a flow, `statesOwnFlow`, is lowered through `ToActionGraph` to a stated `Block`, `lower/case_body.go` `StartFlow`/`CaseFlowStart` giving it its declaration-order start; one stating none stays a statement block), `lower/action_subflow.go` `lowerActionNode` (a nested node's flow is started the same way); `runtime/state_statements.go` `stateStmtHost.runFlow`/`runOwnFlow`/`setFeature` (the block runs through the behavior's own `ActionExecutor`: `checkResultParameters`, `declareRootFeatures`, `declareAcceptPayloads`, `initializeAttributes`, `runSubflow`; `noFlowStart` names the unpreceded nodes or the cycle) | `parser/testdata/parse/state_action_body_successions.golden`, `lower/state_behavior_test.go`, `state_do_action_successions_first_start.sysml` + trace golden, `state_do_action_successions_named_first.sysml`, `state_do_action_fork_join_decision.sysml`, `state_do_action_body_attributes.sysml`, `state_entry_exit_action_successions.sysml` + trace golden, `robustness_test.go:testStateBlockNodeOwnFlowRuns`, `:testStateDoBodyNodeReturnParameter`, `:testStateDoBodyReturnParameter`, `:testStateDoBodyDanglingSuccession`, `:testStateDoBodyFirstThenUndefined`, `:testStateDoBodyFlowWithoutStart`, `:testStateDoBodyNestedNodeDanglingSuccession`, `:testStateEntryBodyDanglingSuccession`, `:testStateDoBodyFlowThatNeverEnds`, `:testStateDoBodyFlowWithTwoStarts`, `:testStateDoBodyStartsAtItsUnprecededStep`, `:testActionFlowStartsAtItsUnprecededStep`, `:testActionFlowWithTwoStarts`, `:testActionFlowCycleWithoutStart`, `:testStateDoBodyNestedNodeStartsAtItsUnprecededStep`, `:testActionNestedNodeStartsAtItsUnprecededStep`, `:testActionNestedNodeWithTwoStarts`, `lower/state_behavior_test.go:TestStateBehaviorBodyStartsAtItsOneUnprecededStep`, `:TestStateBehaviorBodyWithAmbiguousStartKeepsNoInitial`, `lower/action_subflow_test.go:TestActionNodeSubflowStartsAtItsOneUnprecededStep`, `:TestActionNodeSubflowWithoutOneStartKeepsNoInitial`, `lower/action_succession_test.go:TestStartFlow`, conformance `state_do_action_declaration_order.sysml` + trace golden | ✅ Faithful |
 | A state machine's own entry, do and exit behaviors (`state def M { entry action { … } then s; … exit action { … } }`) frame its run whether or not it has orthogonal regions of its own: the entry behavior runs when the machine starts, before its entry transitions are tried and the start state entered, the do behavior runs alongside its states, and the exit behavior runs once a completing transition has left its last state (SysML v2 §7.16 `StateDefinition`: a state definition is itself a `StateAction` with `entryAction`, `doAction`, `exitAction`) | `lower/state_graph.go` `StateGraph.Machine`, `machineState` (the graph-only root state, built for every machine); `runtime/state_executor.go` `enterMachine` (from `initialize`), `exitMachine` (from `completeIfDone`) | conformance `state_machine_own_behaviors.sysml` (a machine without regions; on the earlier reading its own entry and exit behaviors were skipped), `state_entry_transition_nested_regions.sysml` (an `entry assign` read by the machine's own guards), `state_parallel_entry_behavior.sysml` (a parallel machine) | ✅ Faithful |
-| An inline body is one action, so a do round runs it to its end: orthogonal regions interleave between rounds, not inside a body. The one-action-per-statement `do { … }` form is what interleaves statement by statement | `runtime/state_statements.go` `executeBehavior`; `state_executor.go` runDoRound | `state_anonymous_do_atomic.sysml` + trace golden (123456), against `state_concurrent_do.sysml` (124356) | ✅ Faithful |
+| An inline do body is interrupted where a transition out of its state is triggered (§7.18.3: the source state's do action, "if it is still being performed, is interrupted"), whether it was written as one action or as one action per statement: a do round runs one statement of the body — a statement of a `for`/`while`/`loop` iteration, of a nested block or of a branch taken is one of its own, one step of a token flow the body states (each of its tokens one node) is one — then yields, so the pending statements of a body under way are dropped with the behavior when the state is left, and orthogonal regions' inline bodies interleave statement by statement as the one-action-per-statement `do { … }` form does, the order within a round the do round's choice | `runtime/state_statements.go` `doRun` (`startDoRun`, `resume`, `resumable`: a body run with `bodyRun.yields` pauses at the statement boundary after the statement it performed, `bodyPause.yielded`, and is due again in the next round); `runtime/statements.go` `stmtEngine.run`/`loop`/`forLoop`/`blockFlow` (`Context.yieldBody` before the next statement, iteration or node once one performed); `runtime/action_subflow.go` `driveSubflow` (a stated flow yields before the next node a token performs, control nodes and waits aside); `state_executor.go` `runDoRound`, `stopDoAction` → `bodyRun.end` (the frames of a body yielded between statements are abandoned as those of one paused on a wait are) | `state_do_body_interrupted_by_signal.sysml` + trace golden (`s1`, the accept, the exit behavior, neither `s2` nor `s3`); `state_concurrent_inline_do_bodies.sysml` + `.expected.json` + trace goldens (a `for` and an `if` in two regions' inline bodies, the four interleavings of `state_concurrent_do`); `state_anonymous_do_atomic.sysml` + `.expected.json` + trace goldens (one inline action of three statements per region: 124356 in entry order, the same four values as `state_concurrent_do`); `state_do_action_successions_first_start.trace.golden` (one flow step a round); `state_terminate_entry_do_exit_behaviors.trace.golden` (`terminate` reached in the round after the statement before it); `robustness_resumable_inline_do_body_test.go` (a `for` body left mid-loop drops its pending iterations with no frame, do work, clock wait or goroutine left behind; 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`) | ✅ Faithful |
 | A statement of an inline body may perform an action (`entry action { assign c := c + 1; perform Bump; }`), the performed action being lowered as an effect rather than an unsupported usage | `lower/action_graph.go` `lowerStatement` (an action usage naming what it performs → `Effect{EffectPerform}`); `runtime/state_statements.go` `stateStmtHost.effect` | `state_anonymous_body_perform.sysml` conformance | ✅ Faithful |
 | A typed do, entry or exit usage whose body declares the pins of the action it performs and nothing else (`do action poll : Poll { inout n = ticks; }`; SysML v2 §7.16: a `StateSubactionMembership` owns an `ActionUsage`, whose body may bind its parameters as any action node's does) performs that action as the one node of the behavior's flow, its `in` and `inout` pins read from the bound features when the performance starts and an `inout` pin written back to its feature when the performance ends — not before, so a performance the state's exit abandons writes nothing back. A behavior that both performs an action and states executable steps of its own is still reported rather than one of the two being chosen silently | `lower/state_behavior.go` `lowerStateBehavior` (a performing usage with `declaresOnlyFeatures` lowers to a one-node `Block` through `lowerBlockFlow`; one with steps to `Unsupported`), `lower/action_graph.go` `lowerFeatures`/`inoutValueBinding` (an `inout` pin valued by a feature name is a `PinBinding` to that feature, `FromValue` marking it as read from the pin's value); `runtime/action_frame.go` `writeOutputs` (an `inout` pin valued by a name the enclosing performance holds no feature of — an enumeration literal, `inout mode = Mode::idle` or an imported `idle` — was initialized by it and writes nothing back; one valued by a feature name that the performance holds writes back to it, and an `out` pin bound to a name nothing holds is still `ErrBindingEnd`); `runtime/state_statements.go` `stateStmtHost.runFlow` (the node performs through the behavior's `ActionExecutor`, its bindings checked as a standalone action's are: `ErrUnboundParameter` names an `in` pin nothing binds, `ErrUnresolvedReference` a pin bound to a feature the state does not declare) | conformance `state_do_action_typed_inout_writes_back.sysml` + trace golden (`ticks` counted once, written back at the performance's end), `state_do_action_typed_inout_cancelled_on_exit.sysml` + trace golden (the exit at 10 s ends a performance paused until 33 s; `ticks` keeps its 5), `state_do_action_typed_inout_valued_by_a_literal.sysml` + `.expected.json` (`inout mode = Mode::idle` beside `inout n = ticks`: `ticks` written back, the literal written nowhere), `robustness_test.go:testStateDoTypedActionInputUnbound`, `:testStateDoTypedActionPinBoundToMissingFeature`, `:testStateDoTypedActionInoutValuedByAnImportedLiteral` (`inout mode = idle` through `import Mode::*`), `:testBehaviorPerformingAnActionAndStatingABody` (the mixed form) | ✅ Faithful for the pin-binding form; ⚠️ Approximate for the mixed form (rejected at execution, not at parse: the pinned `SysML.xtext` reads `entry action mixed : Bump { … }` as a `PerformActionUsage` with a body (`StateActionUsage` → `PerformedActionUsage ActionBody`), and neither the pinned validator nor we report anything on either form, so what is unadjudicated is the *meaning* of executable steps beside a performed action, which the reference cannot execute. Whether an `inout` pin of an abandoned performance writes back is self-assessed from `Performances.kerml`: a binding of a parameter holds for the whole performance, and an abandoned one has no end to hand its value out at) |
 | Concurrently active states interleave their do behaviors one action per round; which of the states with an action due acts first in a round is a choice point (KerML `StatePerformances.kerml`: the do behavior is a `middle` performance of its state, ordered after its entry and before its exit, and no succession joins a step of one region's to a step of another's) | `state_executor.go` `runDoRound` (the behaviors with an action due — a next behavior, or a paused one whose wait has ended — each perform one action, in the order `chooseDoAction` draws from the scheduling policy: entry order under `declared` and `reverse`, a draw under `seed:<n>`, every order under `explore`), `chooseDoAction`/`regionOrderChoice` (`choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first)`; one due alone is no choice), `doAction.due` | `state_concurrent_do.sysml` + `.expected.json` (`outcomes`: the four values two rounds of two orders reach, derived in [the semantic oracle](behavior-semantic-oracle.md)) + trace goldens under the default, `declared` and `seed:1`; `state_concurrent_do_action_bodies_timed.sysml` + `.expected.json` + trace goldens (two action bodies each parked at `accept after 2 [s]`, due together at `t=2.0`); `state_do_action_test.go:TestDoBehaviorsOfOrthogonalRegionsInterleave` | ✅ Faithful |
@@ -2714,9 +2714,6 @@ the `@type` mapping and the comparison choices.
 ### Known Limitations (Non-blocking)
 
 **Runtime:**
-- an inline entry/do/exit body is one action, so an outgoing transition interrupts a do
-  body only between rounds, never between its statements; the one-action-per-statement
-  `do { … }` form is the interruptible spelling
 - entering a composite state runs its own entry body before the region's initial
   transition reaches the substate, so a parent's do body can run before a substate's
   entry body (`state_anonymous_action_body.trace.golden`). Pre-existing region-entry