From c603ba2b8e82fff3bdee281ba44d04b0e5ce2e6b Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Thu, 17 Sep 2026 04:36:00 +0000 Subject: [PATCH 1/4] feat(runtime): run an inline do body one statement a round, dropping its rest at exit Co-Authored-By: jason.han --- docs/project/behavior-semantic-oracle.md | 9 +- internal/core/runtime/action_body_run.go | 44 ++++- internal/core/runtime/action_subflow.go | 70 +++++-- internal/core/runtime/check_body.go | 8 +- ...obustness_resumable_inline_do_body_test.go | 181 ++++++++++++++++++ internal/core/runtime/robustness_test.go | 18 +- internal/core/runtime/state_executor.go | 8 +- internal/core/runtime/state_statements.go | 25 ++- internal/core/runtime/statements.go | 50 ++++- ...te_anonymous_do_atomic.check.expected.json | 5 + ..._anonymous_do_atomic.declared.trace.golden | 58 ++++++ .../state_anonymous_do_atomic.expected.json | 23 ++- ...te_anonymous_do_atomic.seed-1.trace.golden | 58 ++++++ .../state_anonymous_do_atomic.sysml | 9 +- .../state_anonymous_do_atomic.trace.golden | 46 +++-- ...rrent_inline_do_bodies.check.expected.json | 5 + ...ent_inline_do_bodies.declared.trace.golden | 68 +++++++ ..._concurrent_inline_do_bodies.expected.json | 23 +++ ...rrent_inline_do_bodies.seed-1.trace.golden | 68 +++++++ .../state_concurrent_inline_do_bodies.sysml | 49 +++++ ...e_concurrent_inline_do_bodies.trace.golden | 68 +++++++ ...ction_successions_first_start.trace.golden | 1 + ...o_body_interrupted_by_signal.expected.json | 10 + .../state_do_body_interrupted_by_signal.sysml | 28 +++ ...do_body_interrupted_by_signal.trace.golden | 14 ++ ...nate_entry_do_exit_behaviors.expected.json | 1 - ...te_terminate_entry_do_exit_behaviors.sysml | 8 +- ...inate_entry_do_exit_behaviors.trace.golden | 3 +- ...terminate_this_ends_performer.trace.golden | 1 + 29 files changed, 882 insertions(+), 77 deletions(-) create mode 100644 internal/core/runtime/robustness_resumable_inline_do_body_test.go create mode 100644 internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.check.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.declared.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.seed-1.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.check.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.trace.golden diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md index 5627344d6c..d4aaf62239 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -853,8 +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` -(golden, explored). +Fixtures: `state_concurrent_do` (golden, explored), `state_anonymous_do_atomic` (golden, explored), +`state_concurrent_do_action_bodies_timed` (golden, explored). ``` Interleave parallel { left: lwork { do { seq := seq*10+1; seq := seq*10+2; seq := seq*10+3 } } @@ -884,7 +884,10 @@ 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:` 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_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. diff --git a/internal/core/runtime/action_body_run.go b/internal/core/runtime/action_body_run.go index ca0f84906c..28a79f0357 100644 --- a/internal/core/runtime/action_body_run.go +++ b/internal/core/runtime/action_body_run.go @@ -42,8 +42,9 @@ type bodyFrame interface { spell(*stateSpeller) string } -// bodyRun is the work of one body: a breakpoint met inside it, or a wait on the -// clock, pauses it there until resumed, its frames kept in cursor. +// bodyRun is the work of one body: a breakpoint met inside it, a wait on the +// clock, or a statement boundary where it yields, pauses it there until +// resumed, its frames kept in cursor. type bodyRun struct { work bodyWork // err is what ended the work, once ended: its own failure, or its abandonment. @@ -63,13 +64,18 @@ type bodyRun struct { // awaitsMessages lets the run pause for a message too, as a do behavior does // while its machine goes on; a token's step run waits only on the clock. awaitsMessages bool + // yields has the run pause at the statement boundary after the statement, + // loop iteration or flow step it performed since resumed, which performed marks. + yields, performed bool } -// bodyPause is why a body run paused: at the breakpoint, or on a wait. +// bodyPause is why a body run paused: at the breakpoint, on a wait, or yielded +// at a statement boundary, to go on with the next statement when resumed. type bodyPause struct { breakpoint breakpointStop onWait bool wait bodyWait + yielded bool } // bodyWait is the wait a body's run paused on: of the action it performs (held), @@ -113,6 +119,7 @@ func (run *bodyRun) resume(ctx *Context) (bodyPause, bool) { outer := ctx.body ctx.body = run run.resuming, run.cursor = run.cursor, nil + run.performed = false base := ctx.trace.nesting() run.traceBase = base ctx.trace.setNesting(base + run.traceLevels) @@ -142,8 +149,11 @@ func (run *bodyRun) end(ctx *Context) { f.abandon(ctx) } run.cursor, run.ended = nil, true - where := "on a wait" - if !run.paused.onWait { + where := "between statements" + switch { + case run.paused.onWait: + where = "on a wait" + case !run.paused.yielded: where = fmt.Sprintf("at breakpoint %q", run.paused.breakpoint.name) } run.err = fmt.Errorf("%w: the run paused %s was abandoned", ErrActionDeadlock, where) @@ -490,6 +500,30 @@ func (ctx *Context) pauseBody(pause bodyPause) error { return errPaused } +// yieldBody pauses the body on the stack before its next statement where its run +// goes one at a time and has performed one since resumed; nil, going on, else. +func (ctx *Context) yieldBody() error { + if ctx.body == nil || !ctx.body.yields || !ctx.body.performed { + return nil + } + return ctx.pauseBody(bodyPause{yielded: true}) +} + +// bodyPerformed notes a statement, loop iteration or flow step of the body on the +// stack done, after which a run going one at a time yields. +func (ctx *Context) bodyPerformed() { + if ctx.body != nil { + ctx.body.performed = true + } +} + +// yieldedHere reports the frame just popped as the one the body yielded in: its +// next statement begins afresh there, where a frame paused inside one resumes it. +func (ctx *Context) yieldedHere() bool { + run := ctx.body + return run != nil && len(run.resuming) == 0 && run.paused.yielded +} + // pauseForClock pauses the body on the stack while wait, a wait on the clock, // goes on; nil where none is on the stack. func (ctx *Context) pauseForClock(wait bodyWait) error { diff --git a/internal/core/runtime/action_subflow.go b/internal/core/runtime/action_subflow.go index e77384de84..6ff495ddc1 100644 --- a/internal/core/runtime/action_subflow.go +++ b/internal/core/runtime/action_subflow.go @@ -129,7 +129,8 @@ func (e *ActionExecutor) enterBodyFlow(perf *actionFrame) (*subflowFrame, error) } // driveSubflow steps the flow's tokens until its last one retires, pausing the -// body where a breakpoint is met or the flow waits. +// body where a breakpoint is met or the flow waits; a body run one statement at +// a time yields once a node is performed, before the next node to perform. func (e *ActionExecutor) driveSubflow(f *subflowFrame) error { perf := f.perf for perf.live > 0 { @@ -141,7 +142,7 @@ func (e *ActionExecutor) driveSubflow(f *subflowFrame) error { if err := e.chargeActionStep(); err != nil { return err } - moved, err := e.stepSubflow(perf) + moved, performed, err := e.stepSubflow(perf) if err != nil { return err } @@ -156,7 +157,15 @@ func (e *ActionExecutor) driveSubflow(f *subflowFrame) error { return err } } + if performed { + e.ctx.bodyPerformed() + } if moved { + if e.nextStepPerforms(perf) { + if err := e.ctx.yieldBody(); err != nil { + return err + } + } continue } if e.waitsOnClock(perf) && !e.hasDueTimeWait(perf) && !e.hasDueHeldRun(perf) { @@ -187,14 +196,15 @@ func (e *ActionExecutor) driveSubflow(f *subflowFrame) error { return nil } -// stepSubflow steps every token of perf's flow once and reports whether any moved, -// which a retired, forked or relocated token did. -func (e *ActionExecutor) stepSubflow(perf *actionFrame) (bool, error) { +// stepSubflow steps every token of perf's flow once and reports whether any moved +// — which a retired, forked or relocated token did — and whether one performed +// the node it stood at. +func (e *ActionExecutor) stepSubflow(perf *actionFrame) (moved, performed bool, err error) { before := e.subflowLocations(perf) + performing := e.performingTokens(perf) defer e.beginSweep()() order := e.beginStepOrder() endWrites := e.beginStepWrites(e.stepCount + 1) - var err error eligible := func(t Token) bool { return t.inFlowOf(perf) } if e.ctx.scheduling().oneMove() { // Paused work that would only pause again is no alternative to pick. @@ -220,18 +230,21 @@ func (e *ActionExecutor) stepSubflow(perf *actionFrame) (bool, error) { err = refused } if err != nil { - return false, err + return false, false, err } after := e.subflowLocations(perf) - if len(after) != len(before) { - return true, nil - } + moved = len(after) != len(before) for id, location := range after { if before[id] != location { - return true, nil + moved = true + } + } + for id := range performing { + if at, ok := after[id]; !ok || at != before[id] { + moved, performed = true, true } } - return false, nil + return moved, performed, nil } // subflowLocations returns where each token of perf's flow sits, by token ID. @@ -243,6 +256,39 @@ func (e *ActionExecutor) subflowLocations(perf *actionFrame) map[int64]ast.Node return locations } +// performingTokens returns the IDs of the tokens of perf's flow standing at a node +// their next step performs. +func (e *ActionExecutor) performingTokens(perf *actionFrame) map[int64]bool { + performing := make(map[int64]bool) + for _, idx := range e.tokensIn(perf) { + if t := e.tokens[idx]; e.performs(t.frame, t.Location) { + performing[t.ID] = true + } + } + return performing +} + +// nextStepPerforms reports whether a token of perf's flow stands at a node its +// next step performs. +func (e *ActionExecutor) nextStepPerforms(perf *actionFrame) bool { + return len(e.performingTokens(perf)) > 0 +} + +// performs reports a node a token's step performs — an action or a statement node +// — rather than routes through (a control node) or waits at (an accept, whose +// step is its wait's end). +func (e *ActionExecutor) performs(frame *actionFrame, node ast.Node) bool { + switch n := node.(type) { + case *ast.Usage: + _, accept := e.graphOf(frame).Accepts[n] + return !accept + case *ast.ActionExecutionNode, *ast.WhileLoopActionNode, *ast.IfActionNode, + *ast.AssignmentActionNode, *ast.SendStatement, *ast.TerminateStatement: + return true + } + return false +} + // tokensIn returns the indices of the tokens running in perf's flow or one nested // in it; every token's for nil. func (e *ActionExecutor) tokensIn(perf *actionFrame) []int { diff --git a/internal/core/runtime/check_body.go b/internal/core/runtime/check_body.go index 1f61442022..84404a0e8d 100644 --- a/internal/core/runtime/check_body.go +++ b/internal/core/runtime/check_body.go @@ -25,9 +25,13 @@ func (s *stateSpeller) body(run *bodyRun) string { return b.String() } -// pause spells why a body paused: the breakpoint it met, or the wait it is in — -// the callee held by its caller, whole, else the performance whose flow waits. +// pause spells why a body paused: the statement boundary it yielded at, the +// breakpoint it met, or the wait it is in — the callee held by its caller, whole, +// else the performance whose flow waits. func (s *stateSpeller) pause(p bodyPause) string { + if p.yielded { + return "yielded between statements" + } if !p.onWait { return fmt.Sprintf("at breakpoint %q", p.breakpoint) } diff --git a/internal/core/runtime/robustness_resumable_inline_do_body_test.go b/internal/core/runtime/robustness_resumable_inline_do_body_test.go new file mode 100644 index 0000000000..cdfe73c86c --- /dev/null +++ b/internal/core/runtime/robustness_resumable_inline_do_body_test.go @@ -0,0 +1,181 @@ +package runtime + +import ( + "errors" + goruntime "runtime" + "testing" +) + +// TestRuntimeRobustnessResumableInlineDoBody exercises an inline do body run one +// statement a round: what an exit leaves behind of a body paused mid-loop, and the +// budget a body that never ends runs into. +func TestRuntimeRobustnessResumableInlineDoBody(t *testing.T) { + t.Run("exit_mid_loop_drops_the_pending_iterations", testDoBodyExitMidLoopDropsThePendingIterations) + t.Run("exit_on_a_clock_wait_after_a_loop_leaves_no_timer", testDoBodyExitOnAClockWaitAfterALoopLeavesNoTimer) + t.Run("non_terminating_body_exceeds_the_step_limit", testDoBodyNonTerminatingExceedsTheStepLimit) + t.Run("non_terminating_flow_body_exceeds_the_step_limit", testDoBodyNonTerminatingFlowExceedsTheStepLimit) +} + +// doBodyMachine is a machine whose `active` state runs body as its do behavior +// until a Stop is dispatched to it. +func doBodyMachine(body string) string { + return `package test { + private import ScalarValues::*; + attribute def Stop; + state Machine { + attribute total : Integer = 0; + attribute after : Integer = 0; + entry; then active; + state active { + do action work { ` + body + ` } + exit action leave { assign after := total; } + } + state stopped; + transition first active accept Stop then stopped; + } + }` +} + +// assertDoBodyAbandoned checks the run of the do body exited with the state is +// ended as abandoned and nothing of it is left due, waiting, or running. +func assertDoBodyAbandoned(t *testing.T, exec *StateExecutor, run *doRun, goroutines int) { + t.Helper() + if !run.body.ended || !errors.Is(run.body.err, ErrActionDeadlock) { + t.Errorf("the paused body ended = %v with %v; want it abandoned with ErrActionDeadlock", run.body.ended, run.body.err) + } + if len(run.body.cursor) != 0 || len(run.body.resuming) != 0 { + t.Errorf("frames %d kept and %d resuming after the abandonment; want none", len(run.body.cursor), len(run.body.resuming)) + } + if exec.HasPendingDoWork() || len(exec.doActions) != 0 { + t.Errorf("%d do behaviors, pending work %v after the exit; want none", len(exec.doActions), exec.HasPendingDoWork()) + } + if waits := exec.ctx.Clock().Waits(); len(waits) != 0 { + t.Errorf("%d wait(s) left on the clock; want none", len(waits)) + } + if got := goruntime.NumGoroutine(); got > goroutines { + t.Errorf("%d goroutines after the run, %d before; want none left behind", got, goroutines) + } + if leaf := activeLeaf(exec); leaf != "stopped" { + t.Errorf("active state %s; want stopped", leaf) + } +} + +// begunDoRun runs the first do round and returns the one do behavior it began. +func begunDoRun(t *testing.T, exec *StateExecutor) *doRun { + t.Helper() + if ran, err := exec.RunDoRound(); err != nil || ran != 1 { + t.Fatalf("first do round ran %d with %v; want the one behavior begun", ran, err) + } + if len(exec.doActions) != 1 || exec.doActions[0].run == nil { + t.Fatalf("%d do behaviors after the first round; want the one under way", len(exec.doActions)) + } + return exec.doActions[0].run +} + +// pausedDoRun is begunDoRun for a body paused between statements. +func pausedDoRun(t *testing.T, exec *StateExecutor) *doRun { + t.Helper() + run := begunDoRun(t, exec) + if !run.body.paused.yielded { + t.Fatalf("the body paused %+v; want yielded between statements", run.body.paused) + } + return run +} + +// testDoBodyExitMidLoopDropsThePendingIterations: a `for` body yields after each +// iteration; the Stop, dispatched after the round that ran the third, drops the +// two left with the behavior, the exit behavior runs, and nothing of the loop +// stays behind. +func testDoBodyExitMidLoopDropsThePendingIterations(t *testing.T) { + goroutines := goruntime.NumGoroutine() + exec := stateExecutorForSource(t, "Machine", doBodyMachine(` + for i in 1..5 { + assign total := total + i; + } + `)) + run := pausedDoRun(t, exec) + if _, err := exec.RunDoRound(); err != nil { + t.Fatalf("second do round: %v", err) + } + if total := exec.StateData()["total"]; !valueEqual(total, integerValue(3)) { + t.Fatalf("total = %v after two rounds; want 3, one iteration a round", total) + } + exec.SendSignal("Stop", nil) + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("run to completion: %v", err) + } + data := exec.StateData() + if !valueEqual(data["total"], integerValue(6)) || !valueEqual(data["after"], integerValue(6)) { + t.Errorf("total = %v, after = %v; want 6 and 6: one iteration in the round before the Stop, none after, the exit behavior did run", data["total"], data["after"]) + } + assertDoBodyAbandoned(t, exec, run, goroutines) +} + +// testDoBodyExitOnAClockWaitAfterALoopLeavesNoTimer: a body whose flow loops in +// one node, then waits on the clock at the next — the one round performs the node +// and parks the token at the wait — is exited by the Stop while the wait is armed; +// the wait goes with the behavior, so the clock holds nothing of the state left. +func testDoBodyExitOnAClockWaitAfterALoopLeavesNoTimer(t *testing.T) { + goroutines := goruntime.NumGoroutine() + exec := stateExecutorForSource(t, "Machine", doBodyMachine(` + first start; + then action sum { for i in 1..2 { assign total := total + i; } } + then action pause accept after 10; + then action reset assign total := 0; + then done; + `)) + run := begunDoRun(t, exec) + if !run.body.paused.onWait { + t.Fatalf("the body paused %+v; want a wait on the clock after the loop", run.body.paused) + } + if waits := exec.ctx.Clock().Waits(); len(waits) != 1 { + t.Fatalf("%d wait(s) on the clock; want the body's one", len(waits)) + } + if exec.HasPendingDoWork() { + t.Fatal("the body is due while its wait on the clock goes on") + } + exec.SendSignal("Stop", nil) + if err := exec.RunToQuiescence(); err != nil { + t.Fatalf("run to quiescence: %v", err) + } + data := exec.StateData() + if !valueEqual(data["total"], integerValue(3)) || !valueEqual(data["after"], integerValue(3)) { + t.Errorf("total = %v, after = %v; want 3 and 3: the body ended at its wait", data["total"], data["after"]) + } + assertDoBodyAbandoned(t, exec, run, goroutines) +} + +// testDoBodyNonTerminatingExceedsTheStepLimit: a loop that never ends spends the +// budget one iteration a round, and the run ends with the typed error rather than +// hanging. +func testDoBodyNonTerminatingExceedsTheStepLimit(t *testing.T) { + exec := stateExecutorForSource(t, "Machine", doBodyMachine(` + loop { + assign total := total + 1; + } + `)) + pausedDoRun(t, exec) + err := exec.RunToCompletion() + if !errors.Is(err, ErrStepLimitExceeded) { + t.Fatalf("run to completion = %v; want ErrStepLimitExceeded", err) + } + if total := exec.StateData()["total"]; total.Kind != ValConst || total.Const.Int < 2 { + t.Errorf("total = %v; want the iterations run one a round before the budget ran out", total) + } +} + +// testDoBodyNonTerminatingFlowExceedsTheStepLimit: a body stating a token flow +// that cycles through a merge never retires its token; one node a round, it +// ends with the typed error. +func testDoBodyNonTerminatingFlowExceedsTheStepLimit(t *testing.T) { + exec := stateExecutorForSource(t, "Machine", doBodyMachine(` + first start; + then merge again; + then action bump { assign total := total + 1; } + then again; + `)) + err := exec.RunToCompletion() + if !errors.Is(err, ErrStepLimitExceeded) { + t.Fatalf("run to completion = %v; want ErrStepLimitExceeded", err) + } +} diff --git a/internal/core/runtime/robustness_test.go b/internal/core/runtime/robustness_test.go index cf3ef63e6d..36b7580346 100644 --- a/internal/core/runtime/robustness_test.go +++ b/internal/core/runtime/robustness_test.go @@ -15030,9 +15030,10 @@ func testStateDoBodyAcceptYieldsToATransitionIntoItsRegion(t *testing.T) { } // testStateDoBodyAcceptRunsBeforeTheChoiceReads: the do behaviors go on with the -// signal before the chosen transition fires, and a choice on its route reads its -// guards only then, so a do behavior that rewrites the guard on its way sends the -// transition down the branch the rewritten data selects. +// signal — the node after the accept, then yield — before the chosen transition +// fires, and a choice on its route reads its guards only then, so a do behavior +// that rewrites the guard on its way sends the transition down the branch the +// rewritten data selects; the node after runs in the round after the dispatch. func testStateDoBodyAcceptRunsBeforeTheChoiceReads(t *testing.T) { src := ` private import ScalarValues::*; @@ -15081,8 +15082,17 @@ func testStateDoBodyAcceptRunsBeforeTheChoiceReads(t *testing.T) { if activeLeaf(exec) != "other" || len(ctx.PendingMessages()) != 0 { t.Errorf("state %s with %d messages in flight, want other with the one message consumed: the choice read stay after the do behavior cleared it", activeLeaf(exec), len(ctx.PendingMessages())) } + if total := exec.StateData()["total"]; !valueEqual(total, integerValue(100)) { + t.Errorf("total = %v, want 100: the entry of other, the do behavior yielded after flip with count still to run", total) + } + if !exec.HasPendingDoWork() { + t.Fatal("the do behavior must be due to go on with count") + } + if _, err := exec.RunDoRound(); err != nil { + t.Fatalf("run the do round: %v", err) + } if total := exec.StateData()["total"]; !valueEqual(total, integerValue(110)) { - t.Errorf("total = %v, want 110: the do behavior's count, then the entry of other", total) + t.Errorf("total = %v, want 110: the do behavior's count in the round after the dispatch", total) } } diff --git a/internal/core/runtime/state_executor.go b/internal/core/runtime/state_executor.go index 2eecccb21b..4da3d8032e 100644 --- a/internal/core/runtime/state_executor.go +++ b/internal/core/runtime/state_executor.go @@ -151,13 +151,13 @@ type StateExecutor struct { type doAction struct { state *ast.StateNode pending []lower.StateBehavior - // run is the behavior under way, paused where its flow waits on the clock or - // for a message; nil between behaviors. + // run is the behavior under way, paused between two statements or where its + // flow waits on the clock or for a message; nil between behaviors. run *doRun } -// due reports work of the do behavior runnable now: a paused behavior whose wait -// has ended, or the next behavior where none is under way. +// due reports work of the do behavior runnable now: a paused behavior with its +// next statement due, or the next behavior where none is under way. func (act *doAction) due(ctx *Context) bool { if act.run != nil { return act.run.resumable(ctx) diff --git a/internal/core/runtime/state_statements.go b/internal/core/runtime/state_statements.go index 7b3e1b31bf..f5c9ff48be 100644 --- a/internal/core/runtime/state_statements.go +++ b/internal/core/runtime/state_statements.go @@ -99,9 +99,10 @@ func (h *stateStmtHost) perform() error { return h.run() } // clone is the host itself: what its run changes is the flow's, captured with it. func (h *stateStmtHost) clone() bodyWork { return h } -// doRun is a do behavior under way as a body run: a wait on the clock or for a -// message in its flow pauses it there, to be resumed once the wait ends or -// ended when the state is exited, while the machine goes on around it. +// doRun is a do behavior under way as a body run: it yields after each statement +// of its body, and a wait on the clock or for a message in its flow pauses it +// there, to be resumed in a later round or ended when the state is exited, while +// the machine goes on around it. type doRun struct { host *stateStmtHost body *bodyRun @@ -110,19 +111,19 @@ type doRun struct { mail []Message } -// startDoRun begins a do behavior, pausing it where it first waits; nil once it -// has ended, with the error that ended it. +// startDoRun begins a do behavior, performing its first statement and pausing it +// there; nil once it has ended, with the error that ended it. func (e *StateExecutor) startDoRun(behavior lower.StateBehavior) (*doRun, error) { if len(behavior.Body) == 0 { return nil, nil } host := e.behaviorHost(behavior) - body := &bodyRun{work: host, awaitsMessages: true} + body := &bodyRun{work: host, awaitsMessages: true, yields: true} run := &doRun{host: host, body: body} return run.resume(e.ctx) } -// resume lets the run go on to where it next waits, or to its end. +// resume lets the run go on to its next statement boundary or wait, or to its end. func (run *doRun) resume(ctx *Context) (*doRun, error) { defer ctx.readingMail(&run.mail)() defer func() { run.mail = nil }() @@ -131,7 +132,7 @@ func (run *doRun) resume(ctx *Context) (*doRun, error) { if !paused { return nil, run.body.err } - if pause.onWait { + if pause.onWait || pause.yielded { return run, nil } } @@ -144,9 +145,13 @@ func (run *doRun) offer(ctx *Context, m Message) (*doRun, error) { return run.resume(ctx) } -// resumable reports a run whose wait on the clock has ended: a run parked for a -// message stays until its machine dispatches one to it. +// resumable reports a run due to go on: one yielded between statements, or one +// whose wait on the clock has ended; a run parked for a message stays until its +// machine dispatches one to it. func (run *doRun) resumable(ctx *Context) bool { + if run.body.paused.yielded { + return true + } defer ctx.readingMail(&run.mail)() return !run.body.paused.wait.goesOn() } diff --git a/internal/core/runtime/statements.go b/internal/core/runtime/statements.go index 4862ad3358..f30ef0418e 100644 --- a/internal/core/runtime/statements.go +++ b/internal/core/runtime/statements.go @@ -295,7 +295,8 @@ func (f *stmtListFrame) abandon(*Context) { f.run.elements = f.elements } func (f *stmtListFrame) clone() bodyFrame { c := *f; return &c } // run executes statements in declaration order, stopping at a `return`; a body -// pausing in one is re-entered at that statement. +// pausing in one is re-entered at that statement, one yielding between two at +// the next. func (e *stmtEngine) run(stmts []lower.Statement) (stmtFlow, error) { f, resumed, err := popFrame[*stmtListFrame](e.ctx) if err != nil { @@ -304,16 +305,33 @@ func (e *stmtEngine) run(stmts []lower.Statement) (stmtFlow, error) { if !resumed { f = &stmtListFrame{} } + resumed = resumed && !e.ctx.yieldedHere() for ; f.i < len(stmts); f.i++ { + if err := e.ctx.yieldBody(); err != nil { + return flowNext, e.ctx.pausing(f, err) + } flow, err := e.statement(stmts[f.i], f, resumed) resumed = false if err != nil || flow == flowReturn { return flow, e.ctx.pausing(f, err) } + if !compound(stmts[f.i]) { + e.ctx.bodyPerformed() + } } return flowNext, nil } +// compound reports a statement whose own statements, iterations or nodes are the +// steps of a body run one at a time, not the statement as a whole. +func compound(stmt lower.Statement) bool { + switch stmt.(type) { + case lower.If, lower.Loop, lower.Block: + return true + } + return false +} + // statement executes one lowered statement, recording it in the trace with the // evaluations and nested statements it produces underneath it; one paused keeps // its trace level and elements open until it is resumed and ends. @@ -451,6 +469,7 @@ func (e *stmtEngine) ifStatement(stmt lower.If) (stmtFlow, error) { return flowNext, err } if !holds && stmt.Else == nil { + e.ctx.bodyPerformed() return flowNext, nil } f = &branchFrame{elseBranch: !holds} @@ -541,7 +560,8 @@ func (f *flowNodeFrame) clone() bodyFrame { c := *f; return &c } // blockFlow runs a block that is a token flow of its own (lower/block_graph.go): // a token starts at the block's initial node and passes along the successions the -// block states, running each node it reaches until one succeeds to none. +// block states, running each node it reaches until one succeeds to none; a body +// run one statement at a time yields between two nodes. func (e *stmtEngine) blockFlow(block lower.Block) (stmtFlow, error) { graph := block.Graph f, resumed, err := popFrame[*flowNodeFrame](e.ctx) @@ -551,7 +571,11 @@ func (e *stmtEngine) blockFlow(block lower.Block) (stmtFlow, error) { if !resumed { f = &flowNodeFrame{node: graph.Initial} } + resumed = resumed && !e.ctx.yieldedHere() for f.node != nil { + if err := e.ctx.yieldBody(); err != nil { + return flowNext, e.ctx.pausing(f, err) + } // A node reached spends a step, so a flow that does not end fails the run. if !resumed { if err := e.ctx.incrementStep(); err != nil { @@ -563,6 +587,7 @@ func (e *stmtEngine) blockFlow(block lower.Block) (stmtFlow, error) { if err != nil || flow == flowReturn { return flow, e.ctx.pausing(f, err) } + e.ctx.bodyPerformed() successors := graph.Edges[f.node] if len(successors) == 0 { return flowNext, nil @@ -677,7 +702,8 @@ func (e *stmtEngine) endIteration(f *loopFrame, err error) { // loop runs a loop to termination or to the `return` its body reaches. Every // iteration spends one step of the budget, so a non-terminating loop fails with -// ErrStepLimitExceeded instead of hanging its caller. +// ErrStepLimitExceeded instead of hanging its caller. A body run one statement +// at a time yields between two iterations. func (e *stmtEngine) loop(stmt lower.Loop) (stmtFlow, error) { if stmt.Kind == ast.LoopFor { return e.forLoop(stmt) @@ -689,10 +715,14 @@ func (e *stmtEngine) loop(stmt lower.Loop) (stmtFlow, error) { if !resumed { f = &loopFrame{} } + resumed = resumed && !e.ctx.yieldedHere() leave := e.enterLoop(f) defer leave() for { + if err := e.ctx.yieldBody(); err != nil { + return flowNext, e.ctx.pausing(f, err) + } if !resumed { if err := e.ctx.incrementStep(); err != nil { return flowNext, err @@ -700,9 +730,15 @@ func (e *stmtEngine) loop(stmt lower.Loop) (stmtFlow, error) { } flow, done, err := e.iteration(stmt, f, resumed) resumed = false + // A first iteration ended by the condition is the loop's one step; a later + // one ended so performed nothing since the yield before it. + if done && err == nil && f.iteration == 1 { + e.ctx.bodyPerformed() + } if err != nil || done || flow == flowReturn { return flow, e.ctx.pausing(f, err) } + e.ctx.bodyPerformed() } } @@ -767,11 +803,18 @@ func (e *stmtEngine) forLoop(stmt lower.Loop) (stmtFlow, error) { return flowNext, fmt.Errorf("%s: %w", e.host.describe(), err) } f = &loopFrame{elements: elements} + if len(elements) == 0 { + e.ctx.bodyPerformed() + } } + resumed = resumed && !e.ctx.yieldedHere() leave := e.enterLoop(f) defer leave() for f.iteration < len(f.elements) || resumed { + if err := e.ctx.yieldBody(); err != nil { + return flowNext, e.ctx.pausing(f, err) + } if !resumed { if err := e.ctx.incrementStep(); err != nil { return flowNext, err @@ -782,6 +825,7 @@ func (e *stmtEngine) forLoop(stmt lower.Loop) (stmtFlow, error) { if err != nil || flow == flowReturn { return flow, e.ctx.pausing(f, err) } + e.ctx.bodyPerformed() } return flowNext, nil } diff --git a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.check.expected.json b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.check.expected.json new file mode 100644 index 0000000000..cfe0e7bdf2 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.check.expected.json @@ -0,0 +1,5 @@ +{ + "verdict": "divergent", + "divergent": {"seq": ["124356", "124536", "142356", "142536"]}, + "agreed": {"finalState": "ldone+rdone"} +} diff --git a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.declared.trace.golden b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.declared.trace.golden new file mode 100644 index 0000000000..b2c41ce010 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.declared.trace.golden @@ -0,0 +1,58 @@ +exit: lstart +enter: lwork +transition: lstart -> lwork +do: lwork +stmt action body + stmt assign seq + eval feature seq -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval literal 1 -> 1 + eval operator + -> 1 +exit: rstart +enter: rwork +transition: rstart -> rwork +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + stmt assign seq + eval feature seq -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval literal 2 -> 2 + eval operator + -> 12 +do: rwork +stmt action body + stmt assign seq + eval feature seq -> 12 + eval literal 10 -> 10 + eval operator * -> 120 + eval literal 4 -> 4 + eval operator + -> 124 +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + stmt assign seq + eval feature seq -> 124 + eval literal 10 -> 10 + eval operator * -> 1240 + eval literal 3 -> 3 + eval operator + -> 1243 +do: rwork + stmt assign seq + eval feature seq -> 1243 + eval literal 10 -> 10 + eval operator * -> 12430 + eval literal 5 -> 5 + eval operator + -> 12435 +exit: lwork +enter: ldone +transition: lwork -> ldone +do: rwork + stmt assign seq + eval feature seq -> 12435 + eval literal 10 -> 10 + eval operator * -> 124350 + eval literal 6 -> 6 + eval operator + -> 124356 +exit: rwork +enter: rdone +transition: rwork -> rdone diff --git a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.expected.json b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.expected.json index 1ac9cba15b..4ed076b7f5 100644 --- a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.expected.json +++ b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.expected.json @@ -1,7 +1,22 @@ { "type": "state", - "finalState": "ldone+rdone", - "outputs": { - "seq": { "type": "Integer", "value": 123456 } - } + "outcomes": [ + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 124356 } } + }, + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 142356 } } + }, + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 124536 } } + }, + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 142536 } } + } + ], + "admissible": "Do behaviors of sibling regions active at one instant: each proceeds, in which order is open" } diff --git a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.seed-1.trace.golden b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.seed-1.trace.golden new file mode 100644 index 0000000000..bc06d5e60b --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.seed-1.trace.golden @@ -0,0 +1,58 @@ +exit: lstart +enter: lwork +transition: lstart -> lwork +do: lwork +stmt action body + stmt assign seq + eval feature seq -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval literal 1 -> 1 + eval operator + -> 1 +exit: rstart +enter: rwork +transition: rstart -> rwork +choice do round at t=0.0: states lwork, rwork react (unordered; took rwork first) +do: rwork +stmt action body + stmt assign seq + eval feature seq -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval literal 4 -> 4 + eval operator + -> 14 +do: lwork + stmt assign seq + eval feature seq -> 14 + eval literal 10 -> 10 + eval operator * -> 140 + eval literal 2 -> 2 + eval operator + -> 142 +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + stmt assign seq + eval feature seq -> 142 + eval literal 10 -> 10 + eval operator * -> 1420 + eval literal 3 -> 3 + eval operator + -> 1423 +do: rwork + stmt assign seq + eval feature seq -> 1423 + eval literal 10 -> 10 + eval operator * -> 14230 + eval literal 5 -> 5 + eval operator + -> 14235 +exit: lwork +enter: ldone +transition: lwork -> ldone +do: rwork + stmt assign seq + eval feature seq -> 14235 + eval literal 10 -> 10 + eval operator * -> 142350 + eval literal 6 -> 6 + eval operator + -> 142356 +exit: rwork +enter: rdone +transition: rwork -> rdone diff --git a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.sysml b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.sysml index 96a5b6ee75..23cd48c775 100644 --- a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.sysml +++ b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.sysml @@ -1,8 +1,9 @@ package Test { - // An anonymous do body is a single action the machine runs to completion in - // one round, so the two regions cannot interleave inside it: this gives - // 123456, where state_concurrent_do's one-action-per-statement `do { … }` - // form gives 124356 for the same digits. + // An anonymous do body written as one action yields after each statement, as + // state_concurrent_do's one-action-per-statement `do { … }` form does, so the + // two regions interleave inside it statement by statement: 124356 in entry + // order, the same digits in the same set of orders as that form. The body is + // not one atomic action of a round. state def AtomicDo parallel { attribute seq : Integer = 0; diff --git a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.trace.golden b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.trace.golden index be9653bb1e..b2c41ce010 100644 --- a/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.trace.golden +++ b/internal/core/runtime/testdata/conformance/state_anonymous_do_atomic.trace.golden @@ -9,44 +9,50 @@ stmt action body eval operator * -> 0 eval literal 1 -> 1 eval operator + -> 1 +exit: rstart +enter: rwork +transition: rstart -> rwork +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork stmt assign seq eval feature seq -> 1 eval literal 10 -> 10 eval operator * -> 10 eval literal 2 -> 2 eval operator + -> 12 - stmt assign seq - eval feature seq -> 12 - eval literal 10 -> 10 - eval operator * -> 120 - eval literal 3 -> 3 - eval operator + -> 123 -exit: rstart -enter: rwork -transition: rstart -> rwork do: rwork stmt action body stmt assign seq - eval feature seq -> 123 + eval feature seq -> 12 eval literal 10 -> 10 - eval operator * -> 1230 + eval operator * -> 120 eval literal 4 -> 4 - eval operator + -> 1234 + eval operator + -> 124 +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork stmt assign seq - eval feature seq -> 1234 + eval feature seq -> 124 eval literal 10 -> 10 - eval operator * -> 12340 - eval literal 5 -> 5 - eval operator + -> 12345 + eval operator * -> 1240 + eval literal 3 -> 3 + eval operator + -> 1243 +do: rwork stmt assign seq - eval feature seq -> 12345 + eval feature seq -> 1243 eval literal 10 -> 10 - eval operator * -> 123450 - eval literal 6 -> 6 - eval operator + -> 123456 + eval operator * -> 12430 + eval literal 5 -> 5 + eval operator + -> 12435 exit: lwork enter: ldone transition: lwork -> ldone +do: rwork + stmt assign seq + eval feature seq -> 12435 + eval literal 10 -> 10 + eval operator * -> 124350 + eval literal 6 -> 6 + eval operator + -> 124356 exit: rwork enter: rdone transition: rwork -> rdone diff --git a/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.check.expected.json b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.check.expected.json new file mode 100644 index 0000000000..cfe0e7bdf2 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.check.expected.json @@ -0,0 +1,5 @@ +{ + "verdict": "divergent", + "divergent": {"seq": ["124356", "124536", "142356", "142536"]}, + "agreed": {"finalState": "ldone+rdone"} +} diff --git a/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden new file mode 100644 index 0000000000..6c026245d4 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden @@ -0,0 +1,68 @@ +exit: lstart +enter: lwork +transition: lstart -> lwork +do: lwork +stmt action body + stmt for i + eval literal 1 -> 1 + eval literal 2 -> 2 + eval operator .. -> (1, 2) + iteration 1 + stmt assign seq + eval feature seq -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval feature i -> 1 + eval operator + -> 1 +exit: rstart +enter: rwork +transition: rstart -> rwork +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + iteration 2 + stmt assign seq + eval feature seq -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval feature i -> 2 + eval operator + -> 12 +do: rwork +stmt action body + stmt assign seq + eval feature seq -> 12 + eval literal 10 -> 10 + eval operator * -> 120 + eval literal 4 -> 4 + eval operator + -> 124 +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + stmt assign seq + eval feature seq -> 124 + eval literal 10 -> 10 + eval operator * -> 1240 + eval literal 3 -> 3 + eval operator + -> 1243 +do: rwork + stmt if + eval feature seq -> 1243 + eval literal 0 -> 0 + eval operator > -> true + stmt assign seq + eval feature seq -> 1243 + eval literal 10 -> 10 + eval operator * -> 12430 + eval literal 5 -> 5 + eval operator + -> 12435 +exit: lwork +enter: ldone +transition: lwork -> ldone +do: rwork + stmt assign seq + eval feature seq -> 12435 + eval literal 10 -> 10 + eval operator * -> 124350 + eval literal 6 -> 6 + eval operator + -> 124356 +exit: rwork +enter: rdone +transition: rwork -> rdone diff --git a/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.expected.json b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.expected.json new file mode 100644 index 0000000000..c55d317fc2 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.expected.json @@ -0,0 +1,23 @@ +{ + "type": "state", + "trace": true, + "outcomes": [ + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 124356 } } + }, + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 142356 } } + }, + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 124536 } } + }, + { + "finalState": "ldone+rdone", + "outputs": { "seq": { "type": "Integer", "value": 142536 } } + } + ], + "admissible": "Do behaviors of sibling regions active at one instant: each proceeds, in which order is open" +} diff --git a/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden new file mode 100644 index 0000000000..21930d66a3 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden @@ -0,0 +1,68 @@ +exit: lstart +enter: lwork +transition: lstart -> lwork +do: lwork +stmt action body + stmt for i + eval literal 1 -> 1 + eval literal 2 -> 2 + eval operator .. -> (1, 2) + iteration 1 + stmt assign seq + eval feature seq -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval feature i -> 1 + eval operator + -> 1 +exit: rstart +enter: rwork +transition: rstart -> rwork +choice do round at t=0.0: states lwork, rwork react (unordered; took rwork first) +do: rwork +stmt action body + stmt assign seq + eval feature seq -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval literal 4 -> 4 + eval operator + -> 14 +do: lwork + iteration 2 + stmt assign seq + eval feature seq -> 14 + eval literal 10 -> 10 + eval operator * -> 140 + eval feature i -> 2 + eval operator + -> 142 +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + stmt assign seq + eval feature seq -> 142 + eval literal 10 -> 10 + eval operator * -> 1420 + eval literal 3 -> 3 + eval operator + -> 1423 +do: rwork + stmt if + eval feature seq -> 1423 + eval literal 0 -> 0 + eval operator > -> true + stmt assign seq + eval feature seq -> 1423 + eval literal 10 -> 10 + eval operator * -> 14230 + eval literal 5 -> 5 + eval operator + -> 14235 +exit: lwork +enter: ldone +transition: lwork -> ldone +do: rwork + stmt assign seq + eval feature seq -> 14235 + eval literal 10 -> 10 + eval operator * -> 142350 + eval literal 6 -> 6 + eval operator + -> 142356 +exit: rwork +enter: rdone +transition: rwork -> rdone diff --git a/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.sysml b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.sysml new file mode 100644 index 0000000000..628967437b --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.sysml @@ -0,0 +1,49 @@ +package Test { + // Two orthogonal regions whose inline do bodies loop and branch. The bodies + // yield after each statement — a `for` body after each iteration, a nested + // block after each of its statements — so the regions share the machine one + // statement at a time as state_concurrent_do's one-action-per-statement form + // does: left enters one step before right, then the two interleave, the + // order within a round a choice the policy draws (1,2,4,3,5,6 in entry + // order). A body run to its end at entry would give 1,2,3,4,5,6 instead. + private import ScalarValues::*; + + state def Interleave parallel { + state left { + entry; then lstart; + state lstart; + state lwork { + do action { + for i in 1..2 { + assign seq := seq * 10 + i; + } + assign seq := seq * 10 + 3; + } + } + state ldone; + + succession first lstart then lwork; + succession first lwork then ldone; + } + + state right { + entry; then rstart; + state rstart; + state rwork { + do action { + assign seq := seq * 10 + 4; + if seq > 0 { + assign seq := seq * 10 + 5; + assign seq := seq * 10 + 6; + } + } + } + state rdone; + + succession first rstart then rwork; + succession first rwork then rdone; + } + + attribute seq : Integer = 0; + } +} diff --git a/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden new file mode 100644 index 0000000000..6c026245d4 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden @@ -0,0 +1,68 @@ +exit: lstart +enter: lwork +transition: lstart -> lwork +do: lwork +stmt action body + stmt for i + eval literal 1 -> 1 + eval literal 2 -> 2 + eval operator .. -> (1, 2) + iteration 1 + stmt assign seq + eval feature seq -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval feature i -> 1 + eval operator + -> 1 +exit: rstart +enter: rwork +transition: rstart -> rwork +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + iteration 2 + stmt assign seq + eval feature seq -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval feature i -> 2 + eval operator + -> 12 +do: rwork +stmt action body + stmt assign seq + eval feature seq -> 12 + eval literal 10 -> 10 + eval operator * -> 120 + eval literal 4 -> 4 + eval operator + -> 124 +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first) +do: lwork + stmt assign seq + eval feature seq -> 124 + eval literal 10 -> 10 + eval operator * -> 1240 + eval literal 3 -> 3 + eval operator + -> 1243 +do: rwork + stmt if + eval feature seq -> 1243 + eval literal 0 -> 0 + eval operator > -> true + stmt assign seq + eval feature seq -> 1243 + eval literal 10 -> 10 + eval operator * -> 12430 + eval literal 5 -> 5 + eval operator + -> 12435 +exit: lwork +enter: ldone +transition: lwork -> ldone +do: rwork + stmt assign seq + eval feature seq -> 12435 + eval literal 10 -> 10 + eval operator * -> 124350 + eval literal 6 -> 6 + eval operator + -> 124356 +exit: rwork +enter: rdone +transition: rwork -> rdone diff --git a/internal/core/runtime/testdata/conformance/state_do_action_successions_first_start.trace.golden b/internal/core/runtime/testdata/conformance/state_do_action_successions_first_start.trace.golden index f5cab54ff6..6fac803725 100644 --- a/internal/core/runtime/testdata/conformance/state_do_action_successions_first_start.trace.golden +++ b/internal/core/runtime/testdata/conformance/state_do_action_successions_first_start.trace.golden @@ -7,6 +7,7 @@ enter action node: state behavior ops eval operator * -> 0 eval literal 1 -> 1 eval operator + -> 1 +do: working stmt assign seq eval feature seq -> 1 eval literal 10 -> 10 diff --git a/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.expected.json b/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.expected.json new file mode 100644 index 0000000000..cc26ad75b9 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.expected.json @@ -0,0 +1,10 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Stop"}], + "finalState": "halted", + "stateVisits": ["busy", "halted"], + "outputs": { + "log": { "type": "String", "value": "s1 exit " } + } +} diff --git a/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.sysml b/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.sysml new file mode 100644 index 0000000000..8d984a9e7d --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.sysml @@ -0,0 +1,28 @@ +package Test { + private import ScalarValues::*; + + attribute def Stop; + + // A state's inline do body is interrupted where a transition out of the state + // is triggered: the body yields after each statement, the Stop queued is + // dispatched after its first, and the transition drops the two statements + // still to run with the behavior — the exit behavior runs, s2 and s3 never do. + state def Machine { + attribute log : String = ""; + + entry; then busy; + state busy { + do action work { + assign log := log + "s1 "; + assign log := log + "s2 "; + assign log := log + "s3 "; + } + exit action leave { + assign log := log + "exit "; + } + } + state halted; + + transition first busy accept Stop then halted; + } +} diff --git a/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.trace.golden b/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.trace.golden new file mode 100644 index 0000000000..df0ba901ca --- /dev/null +++ b/internal/core/runtime/testdata/conformance/state_do_body_interrupted_by_signal.trace.golden @@ -0,0 +1,14 @@ +do: busy +stmt action body + stmt assign log + eval feature log -> "" + eval literal "s1 " -> "s1 " + eval operator + -> "s1 " +exit: busy (exit action) +stmt action body + stmt assign log + eval feature log -> "s1 " + eval literal "exit " -> "exit " + eval operator + -> "s1 exit " +enter: halted +transition: busy -> halted (event: accept Stop) diff --git a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.expected.json b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.expected.json index e5a49a13eb..95681b9e58 100644 --- a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.expected.json +++ b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.expected.json @@ -1,7 +1,6 @@ { "type": "state", "trace": true, - "events": [{"signal": "go"}], "finalState": "next", "stateVisits": ["idle", "next"], "outputs": { diff --git a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml index 953bbe77f8..d31e6d4943 100644 --- a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml +++ b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml @@ -1,10 +1,10 @@ // `terminate` in a state's entry, do or exit behavior ends that behavior at the -// statement: the state stays active and the machine keeps dispatching. +// statement: the state stays active and the machine keeps dispatching. The +// transition out is timed so the do body, run one statement a round, reaches +// its `terminate` before anything interrupts it. package test { private import ScalarValues::*; - attribute def go; - state def Machine { attribute count : Integer = 0; attribute later : Integer = 0; @@ -30,6 +30,6 @@ package test { } state next; - transition first idle accept go then next; + transition first idle accept after 1 then next; } } diff --git a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.trace.golden b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.trace.golden index a804df2f16..6a77c9f46d 100644 --- a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.trace.golden +++ b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.trace.golden @@ -2,6 +2,7 @@ do: idle stmt action body stmt assign later eval literal 5 -> 5 +do: idle stmt terminate terminate state behavior tick: no token dropped exit: idle (exit action) @@ -13,4 +14,4 @@ stmt action body stmt terminate terminate state behavior leave: no token dropped enter: next -transition: idle -> next (event: accept go) +transition: idle -> next (event: time) diff --git a/internal/core/runtime/testdata/conformance/state_terminate_this_ends_performer.trace.golden b/internal/core/runtime/testdata/conformance/state_terminate_this_ends_performer.trace.golden index b80928c272..14c36d0169 100644 --- a/internal/core/runtime/testdata/conformance/state_terminate_this_ends_performer.trace.golden +++ b/internal/core/runtime/testdata/conformance/state_terminate_this_ends_performer.trace.golden @@ -7,6 +7,7 @@ do: busy stmt action body stmt assign count eval literal 1 -> 1 +do: busy stmt terminate eval feature this -> instance#1 terminate: Worker #1 From e8944c3ef6e620b17c64a7439f2b0859e3202296 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Thu, 17 Sep 2026 05:03:34 +0000 Subject: [PATCH 2/4] docs(runtime): describe the do body's one-step rounds and the showcase's checkpoints Co-Authored-By: jason.han --- .../resumable-inline-do-body.changed.md | 1 + docs/guide/06-behavior.md | 21 ++--- docs/project/behavior-semantic-oracle.md | 8 +- docs/project/spec-compliance.md | 5 +- examples/runtime-showcase/README.md | 83 +++++++------------ internal/core/runtime/robustness_test.go | 7 +- ...te_terminate_entry_do_exit_behaviors.sysml | 3 +- internal/repl/spacecraft_showcase_test.go | 48 +++++------ 8 files changed, 76 insertions(+), 100 deletions(-) create mode 100644 changes/unreleased/resumable-inline-do-body.changed.md diff --git a/changes/unreleased/resumable-inline-do-body.changed.md b/changes/unreleased/resumable-inline-do-body.changed.md new file mode 100644 index 0000000000..bf21aab600 --- /dev/null +++ b/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 — one iteration of a `for` or `while` body, 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 its pending iterations with nothing kept on the clock, and a non-terminating inline body still ends with the do-step budget. diff --git a/docs/guide/06-behavior.md b/docs/guide/06-behavior.md index 666e8de74b..1786f88654 100644 --- a/docs/guide/06-behavior.md +++ b/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 — one iteration of a `for` or `while` body, 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 { diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md index d4aaf62239..ae90556558 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -854,7 +854,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_anonymous_do_atomic` (golden, explored), -`state_concurrent_do_action_bodies_timed` (golden, explored). +`state_concurrent_inline_do_bodies` (golden, explored), `state_concurrent_do_action_bodies_timed` +(golden, explored). ``` Interleave parallel { left: lwork { do { seq := seq*10+1; seq := seq*10+2; seq := seq*10+3 } } @@ -887,7 +888,10 @@ linearization (`124356`); `seed:` draws the order; `explore` varies it and mu 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_do_action_bodies_timed` is the shape with action bodies +`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. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 086696b0ac..d2447ab65a 100644 --- a/docs/project/spec-compliance.md +++ b/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 — one iteration of a `for`/`while`/`loop` body, one statement of a nested block, one step of a token flow the body states (each of its tokens one node) — 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:`, 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 diff --git a/examples/runtime-showcase/README.md b/examples/runtime-showcase/README.md index fcf3b687b7..a5cad5fc9c 100644 --- a/examples/runtime-showcase/README.md +++ b/examples/runtime-showcase/README.md @@ -394,8 +394,8 @@ the spacecraft's, and `-advance` runs the one clock both parts share: Current state: transmitted | notRecharging Last event at: 241.0 Remaining events: 0 - 500 choice points; %trace on to see them - Do behavior actions run: 405 + 592 choice points; %trace on to see them + Do behavior actions run: 808 standing: value (observed: 1 run under reverse) ``` @@ -413,11 +413,11 @@ printf '%s\n' \ '%state SpacecraftComms::mission.spacecraftVehicle' \ '%advance 40' \ '%eval in SpacecraftComms::mission.spacecraftVehicle : battery' \ - '%advance 39' \ + '%advance 40' \ '%eval in SpacecraftComms::mission.spacecraftVehicle : data' \ '%eval in SpacecraftComms::mission.groundStation : framesReceived' \ - '%advance 41' \ - '%advance 180' \ + '%advance 42' \ + '%advance 178' \ '%current' \ | ./bin/sysml -quiet examples/runtime-showcase/spacecraft-comms.sysml ``` @@ -429,18 +429,18 @@ printf '%s\n' \ (…) ✓ battery (on SpacecraftComms::mission.spacecraftVehicle ID: 4) = 80 -✓ Advanced to 79.0 (41 event(s) processed) +✓ Advanced to 80.0 (42 event(s) processed) Current state: lowPower | recharging - Last event at: 79.0 + Last event at: 80.0 (…) ✓ data (on SpacecraftComms::mission.spacecraftVehicle ID: 4) - = 52224 + = 51200 ✓ framesReceived (on SpacecraftComms::mission.groundStation ID: 2) - = 49 -✓ Advanced to 120.0 (1 event(s) processed) + = 50 +✓ Advanced to 122.0 (1 event(s) processed) Current state: transmitting | recharging (…) -✓ Advanced to 300.0 (55 event(s) processed) +✓ Advanced to 300.0 (54 event(s) processed) Current state: transmitted | notRecharging Last event at: 241.0 (…) @@ -453,54 +453,29 @@ Cannot progress: waiting on change condition: notRecharging: accept when (condit The ping crosses the link at t=30; ten frames later the battery is at 80 and the charging region wakes, so from here the battery loses a net 1 % a second; -at t=79 the drain takes it under 40, `BatteryLow` interrupts the transmission -with 49 frames counted at the station and 52 224 bytes left to send; charging -alone, the battery passes 80 at t=120 and the change trigger restarts the -transmission. The same cycle repeats once more — interrupted at t=162 with 91 -frames sent, resumed at t=204 — the last frame lands at t=213 and the battery +at t=80 the drain takes it under 40, `BatteryLow` interrupts the transmission +with 50 frames counted at the station and 51 200 bytes left to send; charging +alone, the battery passes 80 at t=122 and the change trigger restarts the +transmission. The same cycle repeats once more — interrupted at t=164 with 92 +frames sent, resumed at t=206 — the last frame lands at t=214 and the battery is full at t=241. The `Suspended` at the end is the machine's honest description of itself: `notRecharging` has a change trigger whose condition, `battery < 80`, is false, and nothing on the clock will make it true again. `-schedule` decides what the runtime does when several things fall due at the -same instant, and this model has such instants. At t=79 three one-second timers -expire together: the drain, the frame send and the charge. The drain runs and -then asks `battery >= lowLevel`; whether the charge has already added its 1 % -when it asks is the schedule's choice. Under `reverse` (the default) and -`declared` it has not, the battery reads 39, and `BatteryLow` goes out at t=79 -with 49 frames sent. Under `seed:7` or `seed:42` it has, the battery reads 40, -and the interruption comes a second later, at t=80, with 50 frames sent and the -battery at 39 instead of 41: - -```bash -printf '%s\n' \ - '%schedule seed:7' \ - '%instantiate SpacecraftComms::mission' \ - '%state SpacecraftComms::mission.spacecraftVehicle' \ - '%advance 80' \ - '%eval in SpacecraftComms::mission.groundStation : framesReceived' \ - '%eval in SpacecraftComms::mission.spacecraftVehicle : battery' \ - | ./bin/sysml -quiet examples/runtime-showcase/spacecraft-comms.sysml -``` - -``` -✓ Advanced to 80.0 (54 event(s) processed) - Current state: lowPower | recharging - Last event at: 80.0 - (…) -✓ framesReceived (on SpacecraftComms::mission.groundStation ID: 2) - = 50 -✓ battery (on SpacecraftComms::mission.spacecraftVehicle ID: 4) - = 39 -``` - -Both are correct runs of the model: it says nothing about which of three -simultaneous timers fires first, so the runtime is free to pick, and the -`standing` line records which policy it picked under. What the model does pin -down is the end: every one of these schedules reaches -`transmitted | notRecharging` at t=241 with 100 frames received and the battery -at 100. The values along the way are a property of one schedule; the -destination is a property of the model. +same instant, and this model has such instants: from t=42 on, three one-second +timers expire together every second — the drain, the frame send and the charge +— and every round both regions' do behaviors are due is a choice point, which +the summary counts. A do behavior's flow advances one step a round, so in the round +the timers expire the drain and the charge each run, in the order the schedule +picks, and the drain's branch asks `battery >= lowLevel` only in the round +after, when the charge's 1 % is in whichever way the round went: at t=79 the +battery reads 40 and the transmission goes on, at t=80 it reads 39 and +`BatteryLow` goes out. `reverse` (the default), `declared`, `seed:7` and +`seed:42` all pass these checkpoints, and the `standing` line records which +policy a run was observed under. What the model pins down is the end: every +schedule reaches `transmitted | notRecharging` at t=241 with 100 frames +received and the battery at 100. ## Apollo 11 diff --git a/internal/core/runtime/robustness_test.go b/internal/core/runtime/robustness_test.go index 36b7580346..133067d668 100644 --- a/internal/core/runtime/robustness_test.go +++ b/internal/core/runtime/robustness_test.go @@ -15030,10 +15030,9 @@ func testStateDoBodyAcceptYieldsToATransitionIntoItsRegion(t *testing.T) { } // testStateDoBodyAcceptRunsBeforeTheChoiceReads: the do behaviors go on with the -// signal — the node after the accept, then yield — before the chosen transition -// fires, and a choice on its route reads its guards only then, so a do behavior -// that rewrites the guard on its way sends the transition down the branch the -// rewritten data selects; the node after runs in the round after the dispatch. +// signal (one node, then yield) before the chosen transition fires, and a choice +// on its route reads its guards only then, so a do behavior that rewrites the +// guard on its way sends the transition down the branch the rewritten data selects. func testStateDoBodyAcceptRunsBeforeTheChoiceReads(t *testing.T) { src := ` private import ScalarValues::*; diff --git a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml index d31e6d4943..1ed15b207a 100644 --- a/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml +++ b/internal/core/runtime/testdata/conformance/state_terminate_entry_do_exit_behaviors.sysml @@ -1,7 +1,6 @@ // `terminate` in a state's entry, do or exit behavior ends that behavior at the // statement: the state stays active and the machine keeps dispatching. The -// transition out is timed so the do body, run one statement a round, reaches -// its `terminate` before anything interrupts it. +// transition out is timed, so the do body reaches its `terminate` first. package test { private import ScalarValues::*; diff --git a/internal/repl/spacecraft_showcase_test.go b/internal/repl/spacecraft_showcase_test.go index df1b5c61ec..f3f05dd760 100644 --- a/internal/repl/spacecraft_showcase_test.go +++ b/internal/repl/spacecraft_showcase_test.go @@ -19,46 +19,46 @@ func spacecraftSession(t *testing.T, schedule string) *Session { } // The showcase's checkpoints under the default schedule: ping at t=30, interrupted -// at t=79, resumed at t=120, every frame counted at the station by t=241. +// at t=80, resumed at t=122, every frame counted at the station by t=241. func TestSpacecraftShowcaseTransmitsEveryFrame(t *testing.T) { s := spacecraftSession(t, "reverse") wants(t, run(t, s, "%advance 40"), "Advanced to 40.0", "Current state: transmitting | notRecharging", "Last event at: 30.0") wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : battery"), "= 80") - wants(t, run(t, s, "%advance 39"), "Advanced to 79.0", "Current state: lowPower | recharging") + wants(t, run(t, s, "%advance 39"), "Advanced to 79.0", "Current state: transmitting | recharging") wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : battery"), "= 40") - wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : data"), "= 52224") wants(t, run(t, s, "%eval in SpacecraftComms::mission.groundStation : framesReceived"), "= 49") - wants(t, run(t, s, "%advance 41"), "Advanced to 120.0", "Current state: transmitting | recharging") + wants(t, run(t, s, "%advance 1"), "Advanced to 80.0", "Current state: lowPower | recharging", "Last event at: 80.0") + wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : battery"), "= 39") + wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : data"), "= 51200") + wants(t, run(t, s, "%eval in SpacecraftComms::mission.groundStation : framesReceived"), "= 50") - wants(t, run(t, s, "%advance 180"), "Advanced to 300.0", "Current state: transmitted | notRecharging", "Last event at: 241.0", "Remaining events: 0") + wants(t, run(t, s, "%advance 41"), "Advanced to 121.0", "Current state: lowPower | recharging") + wants(t, run(t, s, "%advance 1"), "Advanced to 122.0", "Current state: transmitting | recharging") + + wants(t, run(t, s, "%advance 178"), "Advanced to 300.0", "Current state: transmitted | notRecharging", "Last event at: 241.0", "Remaining events: 0") wants(t, run(t, s, "%current"), "Execution state: Suspended", "waiting on change condition: notRecharging") wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : data"), "= 0") wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : battery"), "= 100") wants(t, run(t, s, "%eval in SpacecraftComms::mission.groundStation : framesReceived"), "= 100") } -// At t=79 the drain, send and charge timers fall due together; whether the 50th -// frame gets out before lowPower is the schedule's choice, the end is not. -func TestSpacecraftShowcaseFrameCountAtLowPowerIsScheduleDependent(t *testing.T) { - cases := []struct { - schedule string - frames string - battery string - }{ - {"reverse", "= 49", "= 41"}, - {"declared", "= 49", "= 41"}, - {"seed:7", "= 50", "= 39"}, - {"seed:42", "= 50", "= 39"}, - } - for _, tc := range cases { - t.Run(tc.schedule, func(t *testing.T) { - s := spacecraftSession(t, tc.schedule) - wants(t, run(t, s, "%advance 80"), "Advanced to 80.0", "Current state: lowPower | recharging") - wants(t, run(t, s, "%eval in SpacecraftComms::mission.groundStation : framesReceived"), tc.frames) - wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : battery"), tc.battery) +// At t=79 the drain, send and charge timers fall due together; the drain's +// branch reads the battery in the round after, once the charge is in whichever +// order the schedule picked, so every schedule passes the same checkpoints. +func TestSpacecraftShowcaseLowPowerCheckpointsUnderEverySchedule(t *testing.T) { + for _, schedule := range []string{"reverse", "declared", "seed:7", "seed:42"} { + t.Run(schedule, func(t *testing.T) { + s := spacecraftSession(t, schedule) + wants(t, run(t, s, "%advance 79"), "Advanced to 79.0", "Current state: transmitting | recharging") + wants(t, run(t, s, "%eval in SpacecraftComms::mission.groundStation : framesReceived"), "= 49") + wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : battery"), "= 40") + + wants(t, run(t, s, "%advance 1"), "Advanced to 80.0", "Current state: lowPower | recharging") + wants(t, run(t, s, "%eval in SpacecraftComms::mission.groundStation : framesReceived"), "= 50") + wants(t, run(t, s, "%eval in SpacecraftComms::mission.spacecraftVehicle : battery"), "= 39") wants(t, run(t, s, "%advance 220"), "Advanced to 300.0", "Current state: transmitted | notRecharging", "Last event at: 241.0") wants(t, run(t, s, "%eval in SpacecraftComms::mission.groundStation : framesReceived"), "= 100") From e9de88279891f60d1f9f5a91bfac1e0ff42b939d Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Thu, 17 Sep 2026 05:49:30 +0000 Subject: [PATCH 3/4] test(runtime): pin a loop iteration's statements as rounds of their own Co-Authored-By: jason.han --- .../resumable-inline-do-body.changed.md | 2 +- docs/guide/06-behavior.md | 4 +- docs/project/spec-compliance.md | 2 +- ...obustness_resumable_inline_do_body_test.go | 41 +++++++++++++++++-- internal/core/runtime/statements.go | 2 +- 5 files changed, 42 insertions(+), 9 deletions(-) diff --git a/changes/unreleased/resumable-inline-do-body.changed.md b/changes/unreleased/resumable-inline-do-body.changed.md index bf21aab600..17c15c1e09 100644 --- a/changes/unreleased/resumable-inline-do-body.changed.md +++ b/changes/unreleased/resumable-inline-do-body.changed.md @@ -1 +1 @@ -- **A state's inline `do` body is interrupted between its statements.** `do action { s1; s2; s3; }` runs one statement per do round — one iteration of a `for` or `while` body, 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 its pending iterations with nothing kept on the clock, and a non-terminating inline body still ends with the do-step budget. +- **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. diff --git a/docs/guide/06-behavior.md b/docs/guide/06-behavior.md index 1786f88654..3665fbd2bf 100644 --- a/docs/guide/06-behavior.md +++ b/docs/guide/06-behavior.md @@ -336,8 +336,8 @@ 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 statement per round — one iteration of a `for` or `while` body, 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` +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 diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index d2447ab65a..e0c11bce96 100644 --- a/docs/project/spec-compliance.md +++ b/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 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 — one iteration of a `for`/`while`/`loop` body, one statement of a nested block, one step of a token flow the body states (each of its tokens one node) — 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 | +| 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:`, 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 | diff --git a/internal/core/runtime/robustness_resumable_inline_do_body_test.go b/internal/core/runtime/robustness_resumable_inline_do_body_test.go index cdfe73c86c..d0ca64d56a 100644 --- a/internal/core/runtime/robustness_resumable_inline_do_body_test.go +++ b/internal/core/runtime/robustness_resumable_inline_do_body_test.go @@ -11,6 +11,7 @@ import ( // budget a body that never ends runs into. func TestRuntimeRobustnessResumableInlineDoBody(t *testing.T) { t.Run("exit_mid_loop_drops_the_pending_iterations", testDoBodyExitMidLoopDropsThePendingIterations) + t.Run("exit_mid_iteration_drops_the_rest_of_the_iteration", testDoBodyExitMidIterationDropsTheRestOfTheIteration) t.Run("exit_on_a_clock_wait_after_a_loop_leaves_no_timer", testDoBodyExitOnAClockWaitAfterALoopLeavesNoTimer) t.Run("non_terminating_body_exceeds_the_step_limit", testDoBodyNonTerminatingExceedsTheStepLimit) t.Run("non_terminating_flow_body_exceeds_the_step_limit", testDoBodyNonTerminatingFlowExceedsTheStepLimit) @@ -82,10 +83,10 @@ func pausedDoRun(t *testing.T, exec *StateExecutor) *doRun { return run } -// testDoBodyExitMidLoopDropsThePendingIterations: a `for` body yields after each -// iteration; the Stop, dispatched after the round that ran the third, drops the -// two left with the behavior, the exit behavior runs, and nothing of the loop -// stays behind. +// testDoBodyExitMidLoopDropsThePendingIterations: a `for` body of one statement +// yields after each iteration; the Stop, dispatched after the round that ran the +// third, drops the two left with the behavior, the exit behavior runs, and +// nothing of the loop stays behind. func testDoBodyExitMidLoopDropsThePendingIterations(t *testing.T) { goroutines := goruntime.NumGoroutine() exec := stateExecutorForSource(t, "Machine", doBodyMachine(` @@ -111,6 +112,38 @@ func testDoBodyExitMidLoopDropsThePendingIterations(t *testing.T) { assertDoBodyAbandoned(t, exec, run, goroutines) } +// testDoBodyExitMidIterationDropsTheRestOfTheIteration: an iteration of two +// statements is two rounds, so the Stop dispatched after the round that ran the +// second iteration's first statement leaves its second unrun with the iterations after. +func testDoBodyExitMidIterationDropsTheRestOfTheIteration(t *testing.T) { + goroutines := goruntime.NumGoroutine() + exec := stateExecutorForSource(t, "Machine", doBodyMachine(` + for i in 1..3 { + assign total := total + i; + assign total := total * 10; + } + `)) + run := pausedDoRun(t, exec) + if total := exec.StateData()["total"]; !valueEqual(total, integerValue(1)) { + t.Fatalf("total = %v after one round; want 1, the first statement of the first iteration", total) + } + if _, err := exec.RunDoRound(); err != nil { + t.Fatalf("second do round: %v", err) + } + if total := exec.StateData()["total"]; !valueEqual(total, integerValue(10)) { + t.Fatalf("total = %v after two rounds; want 10, the first iteration's second statement", total) + } + exec.SendSignal("Stop", nil) + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("run to completion: %v", err) + } + data := exec.StateData() + if !valueEqual(data["total"], integerValue(12)) || !valueEqual(data["after"], integerValue(12)) { + t.Errorf("total = %v, after = %v; want 12 and 12: the round before the Stop ran the second iteration's `+ i`, its `* 10` and the third iteration never ran", data["total"], data["after"]) + } + assertDoBodyAbandoned(t, exec, run, goroutines) +} + // testDoBodyExitOnAClockWaitAfterALoopLeavesNoTimer: a body whose flow loops in // one node, then waits on the clock at the next — the one round performs the node // and parks the token at the wait — is exited by the Stop while the wait is armed; diff --git a/internal/core/runtime/statements.go b/internal/core/runtime/statements.go index f30ef0418e..66190e2f0d 100644 --- a/internal/core/runtime/statements.go +++ b/internal/core/runtime/statements.go @@ -703,7 +703,7 @@ func (e *stmtEngine) endIteration(f *loopFrame, err error) { // loop runs a loop to termination or to the `return` its body reaches. Every // iteration spends one step of the budget, so a non-terminating loop fails with // ErrStepLimitExceeded instead of hanging its caller. A body run one statement -// at a time yields between two iterations. +// at a time yields between two iterations as between two statements of one. func (e *stmtEngine) loop(stmt lower.Loop) (stmtFlow, error) { if stmt.Kind == ast.LoopFor { return e.forLoop(stmt) From c8957f466311fd70c5cd208f000de3ec06de4322 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Thu, 17 Sep 2026 05:56:53 +0000 Subject: [PATCH 4/4] fix(runtime): count a do body's statement performed whatever it held Co-Authored-By: jason.han --- ...obustness_resumable_inline_do_body_test.go | 25 +++++++++++++++++++ internal/core/runtime/statements.go | 20 +-------------- 2 files changed, 26 insertions(+), 19 deletions(-) diff --git a/internal/core/runtime/robustness_resumable_inline_do_body_test.go b/internal/core/runtime/robustness_resumable_inline_do_body_test.go index d0ca64d56a..47f06d2b18 100644 --- a/internal/core/runtime/robustness_resumable_inline_do_body_test.go +++ b/internal/core/runtime/robustness_resumable_inline_do_body_test.go @@ -12,6 +12,7 @@ import ( func TestRuntimeRobustnessResumableInlineDoBody(t *testing.T) { t.Run("exit_mid_loop_drops_the_pending_iterations", testDoBodyExitMidLoopDropsThePendingIterations) t.Run("exit_mid_iteration_drops_the_rest_of_the_iteration", testDoBodyExitMidIterationDropsTheRestOfTheIteration) + t.Run("empty_branch_is_a_round_of_its_own", testDoBodyEmptyBranchIsARoundOfItsOwn) t.Run("exit_on_a_clock_wait_after_a_loop_leaves_no_timer", testDoBodyExitOnAClockWaitAfterALoopLeavesNoTimer) t.Run("non_terminating_body_exceeds_the_step_limit", testDoBodyNonTerminatingExceedsTheStepLimit) t.Run("non_terminating_flow_body_exceeds_the_step_limit", testDoBodyNonTerminatingFlowExceedsTheStepLimit) @@ -144,6 +145,30 @@ func testDoBodyExitMidIterationDropsTheRestOfTheIteration(t *testing.T) { assertDoBodyAbandoned(t, exec, run, goroutines) } +// testDoBodyEmptyBranchIsARoundOfItsOwn: a conditional whose branch holds nothing +// and a loop ended by its condition at once each spend a round; the assignment +// after them runs in the next. +func testDoBodyEmptyBranchIsARoundOfItsOwn(t *testing.T) { + for _, compound := range []string{"if true { }", "if false { assign total := 5; } else { }", "while false { assign total := 5; }"} { + exec := stateExecutorForSource(t, "Machine", doBodyMachine(compound+` assign total := 1;`)) + run := pausedDoRun(t, exec) + if total := exec.StateData()["total"]; !valueEqual(total, integerValue(0)) { + t.Fatalf("%s: total = %v after one round; want 0, the assignment after it not yet run", compound, total) + } + exec.SendSignal("Stop", nil) + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("%s: run to completion: %v", compound, err) + } + data := exec.StateData() + if !valueEqual(data["total"], integerValue(1)) || !valueEqual(data["after"], integerValue(1)) { + t.Errorf("%s: total = %v, after = %v; want 1 and 1: the round before the Stop ran the assignment", compound, data["total"], data["after"]) + } + if !run.body.ended || exec.HasPendingDoWork() { + t.Errorf("%s: body ended = %v, pending do work %v; want the body ended with nothing due", compound, run.body.ended, exec.HasPendingDoWork()) + } + } +} + // testDoBodyExitOnAClockWaitAfterALoopLeavesNoTimer: a body whose flow loops in // one node, then waits on the clock at the next — the one round performs the node // and parks the token at the wait — is exited by the Stop while the wait is armed; diff --git a/internal/core/runtime/statements.go b/internal/core/runtime/statements.go index 66190e2f0d..c691fc872a 100644 --- a/internal/core/runtime/statements.go +++ b/internal/core/runtime/statements.go @@ -315,23 +315,11 @@ func (e *stmtEngine) run(stmts []lower.Statement) (stmtFlow, error) { if err != nil || flow == flowReturn { return flow, e.ctx.pausing(f, err) } - if !compound(stmts[f.i]) { - e.ctx.bodyPerformed() - } + e.ctx.bodyPerformed() } return flowNext, nil } -// compound reports a statement whose own statements, iterations or nodes are the -// steps of a body run one at a time, not the statement as a whole. -func compound(stmt lower.Statement) bool { - switch stmt.(type) { - case lower.If, lower.Loop, lower.Block: - return true - } - return false -} - // statement executes one lowered statement, recording it in the trace with the // evaluations and nested statements it produces underneath it; one paused keeps // its trace level and elements open until it is resumed and ends. @@ -469,7 +457,6 @@ func (e *stmtEngine) ifStatement(stmt lower.If) (stmtFlow, error) { return flowNext, err } if !holds && stmt.Else == nil { - e.ctx.bodyPerformed() return flowNext, nil } f = &branchFrame{elseBranch: !holds} @@ -730,11 +717,6 @@ func (e *stmtEngine) loop(stmt lower.Loop) (stmtFlow, error) { } flow, done, err := e.iteration(stmt, f, resumed) resumed = false - // A first iteration ended by the condition is the loop's one step; a later - // one ended so performed nothing since the yield before it. - if done && err == nil && f.iteration == 1 { - e.ctx.bodyPerformed() - } if err != nil || done || flow == flowReturn { return flow, e.ctx.pausing(f, err) }