From c8891457a8f73c8db1d0ab3b4008ac3e872e34bc Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 06:51:51 +0000 Subject: [PATCH 1/3] fix(runtime): interleave executors due at one instant move by move Co-Authored-By: jason.han --- .../explore-executor-turns.fixed.md | 1 + cmd/sysml/check_engine_test.go | 12 +- cmd/sysml/explore_nested_test.go | 16 +- cmd/sysml/explore_turns_test.go | 76 ++++ cmd/sysml/run_test.go | 2 +- docs/project/spec-compliance.md | 4 +- internal/exec/runtime/action_executor.go | 24 +- internal/exec/runtime/advance.go | 109 +++++- internal/exec/runtime/check.go | 107 ++++-- internal/exec/runtime/check_reduce.go | 138 ++----- .../exec/runtime/check_reduce_state_test.go | 11 +- internal/exec/runtime/check_run.go | 34 +- internal/exec/runtime/context.go | 3 + internal/exec/runtime/future_footprint.go | 356 ++++++++++++++++++ internal/exec/runtime/message_dependence.go | 235 ++++++++++++ internal/exec/runtime/model.go | 3 + internal/exec/runtime/scheduler.go | 7 + internal/exec/runtime/state_executor.go | 23 +- .../testdata/check/reduction_expected.txt | 12 +- internal/frontend/repl/checker_state_test.go | 4 +- internal/frontend/repl/explore_test.go | 6 +- internal/ir/lower/footprint.go | 102 ++++- internal/ir/lower/state_footprint.go | 43 ++- internal/ir/lower/state_graph.go | 3 + 24 files changed, 1115 insertions(+), 216 deletions(-) create mode 100644 changes/unreleased/explore-executor-turns.fixed.md create mode 100644 cmd/sysml/explore_turns_test.go create mode 100644 internal/exec/runtime/future_footprint.go create mode 100644 internal/exec/runtime/message_dependence.go diff --git a/changes/unreleased/explore-executor-turns.fixed.md b/changes/unreleased/explore-executor-turns.fixed.md new file mode 100644 index 0000000000..a20169717f --- /dev/null +++ b/changes/unreleased/explore-executor-turns.fixed.md @@ -0,0 +1 @@ +- **Executors due at one instant interleave move by move under `explore`, `check`, `replay` and seeded schedules.** An executor drawn from the due order used to run all its work at the instant before another could move, so two actions reading a shared feature and then writing it never reached the lost update. The executor drawn now makes one move and keeps its turn only while its next move is independent of everything each other due executor may still do at the instant; otherwise the due order is drawn again. Explore runs and check state counts grow on models whose messages cannot be resolved statically. `declared` and `reverse` keep their order. diff --git a/cmd/sysml/check_engine_test.go b/cmd/sysml/check_engine_test.go index ed7c11df81..db420a4b66 100644 --- a/cmd/sysml/check_engine_test.go +++ b/cmd/sysml/check_engine_test.go @@ -302,7 +302,7 @@ func TestEngineCheckBindsWitnessObjectsAcrossRuns(t *testing.T) { got := check(t, binary, model, slices.Concat([]string{"-engine", "check"}, invocation, []string{"-check-diverge", "Plant::spare.level", "-check-witness", dir})...) wantReport(t, got, 1, "divergent: Plant::spare.level ends as 1 or 2", - "Plant::spare.level = 1 (witness "+name(1)+")", "Plant::spare.level = 2 (witness "+name(2)+")", "witness of 3 choices replayed)") + "Plant::spare.level = 1 (witness "+name(1)+")", "Plant::spare.level = 2 (witness "+name(2)+")", "witness of 6 choices replayed)") // The spare's fill runs first, so its step 3 is the first: `b` first leaves level 1, `a` first 2. for _, c := range []struct { n int @@ -314,7 +314,7 @@ func TestEngineCheckBindsWitnessObjectsAcrossRuns(t *testing.T) { t.Fatal(err) } if !strings.HasPrefix(string(content), "object #1 = Plant::tank#1\nobject #2 = Plant::spare#1\n"+ - "t=0.0: action fill of object #2 first of action fill of object #1, action fill of object #2\nstep 3: "+c.took+" first of 2@a, 3@b\n") { + strings.Repeat("t=0.0: action fill of object #2 first of action fill of object #1, action fill of object #2\n", 2)+"step 3: "+c.took+" first of 2@a, 3@b\n") { t.Errorf("witness %d, spare.level = %s:\n%s", c.n, c.level, content) } // The run makes the spare's performance after the tank's: the spare is object #3 here. @@ -505,13 +505,13 @@ func TestEngineCheckSearchesBehaviorsOnOneClock(t *testing.T) { // Named apart, each behavior is its own search; the action's clock runs to its end. wantReport(t, check(t, binary, lampModel, "-engine", "check", "-action", peek, "-state", glow), - 1, "✗ Action Shine::Lamp::peek: divergent (10 states, 9 moves, depth 5)", "divergent: saw ends as false or true", + 1, "✗ Action Shine::Lamp::peek: divergent (9 states, 8 moves, depth 5)", "divergent: saw ends as false or true", "✓ State machine Shine::Lamp::glow: no violation, exhaustive (2 states, 1 moves, depth 1)") // With -advance they are one invocation: the machine's timer and the action's // wait are due together, and the order the search draws decides what peek saw. got := check(t, binary, lampModel, "-engine", "check", "-action", peek, "-state", glow, "-advance", "3") - wantReport(t, got, 1, "✗ Behaviors Shine::Lamp::peek, Shine::Lamp::glow: divergent up to t=3.0 (10 states, 9 moves, depth 5)", + wantReport(t, got, 1, "✗ Behaviors Shine::Lamp::peek, Shine::Lamp::glow: divergent up to t=3.0 (9 states, 8 moves, depth 5)", "divergent: Shine::Lamp::peek.saw ends as false or true", `outcome: Shine::Lamp::glow finalState = "on"; Shine::Lamp::glow visits = "off, on"; Shine::Lamp::peek.saw = false; this.isSolid = true; this.lit = true`, `outcome: Shine::Lamp::glow finalState = "on"; Shine::Lamp::glow visits = "off, on"; Shine::Lamp::peek.saw = true; this.isSolid = true; this.lit = true`) @@ -556,7 +556,7 @@ func TestEngineCheckWitnessOfBehaviorsOnOneClockReplays(t *testing.T) { got := check(t, binary, lampModel, "-engine", "check", "-action", peek, "-state", glow, "-advance", "3", "-check-witness", dir) wantReport(t, got, 1, "divergent: Shine::Lamp::peek.saw ends as false or true", "Shine::Lamp::peek.saw = false (witness "+name(1)+")", "Shine::Lamp::peek.saw = true (witness "+name(2)+")", - "standing: sensitive (witnessed: 10 states, 9 moves searched, witness of 1 choice replayed)") + "standing: sensitive (witnessed: 9 states, 8 moves searched, witness of 2 choices replayed)") for _, c := range []struct { n int @@ -570,7 +570,7 @@ func TestEngineCheckWitnessOfBehaviorsOnOneClockReplays(t *testing.T) { if err != nil { t.Fatal(err) } - if !strings.HasPrefix(string(content), "object #1 = Shine::Lamp#1\nt=3.0: "+c.first+" first of action peek of object #1, state machine glow of object #1\n\n") || + if !strings.HasPrefix(string(content), "object #1 = Shine::Lamp#1\nt=3.0: action peek of object #1 first of action peek of object #1, state machine glow of object #1\nt=3.0: "+c.first+" first of action peek of object #1, state machine glow of object #1\n\n") || !strings.Contains(string(content), "choice at t=3.0: due action peek of object #1, state machine glow of object #1 (unordered; ran "+c.first+" first)") { t.Errorf("witness %d:\n%s", c.n, content) } diff --git a/cmd/sysml/explore_nested_test.go b/cmd/sysml/explore_nested_test.go index 1de097e9c8..cdbce05aa4 100644 --- a/cmd/sysml/explore_nested_test.go +++ b/cmd/sysml/explore_nested_test.go @@ -75,9 +75,9 @@ func TestExploreRunsAMachineOnANestedObject(t *testing.T) { got := check(t, binary, linkedPairModel, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5") wantReport(t, got, 0, "✓ explored Comms::Ground::listen: 2 outcomes", - "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 3 | possible | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", - "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 2 | 1 | possible | t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; events at t=3.0: accept Frame first of time listening 1->quiet, accept Frame; at t=3.0: do listening first of do listening, dispatch time listening 1->quiet", - "complete (4 runs)") + "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 12 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", + "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 2 | 4 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; events at t=3.0: accept Frame first of time listening 1->quiet, accept Frame; at t=3.0: do listening first of do listening, dispatch time listening 1->quiet", + "complete (16 runs)") for _, jobs := range []string{"1", "4"} { again := check(t, binary, linkedPairModel, "-jobs", jobs, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5") if again.output() != got.output() { @@ -89,8 +89,8 @@ func TestExploreRunsAMachineOnANestedObject(t *testing.T) { calm := strings.Replace(linkedPairModel, "accept after 2 [s] then quiet", "accept after 1.5 [s] then quiet", 1) wantReport(t, check(t, binary, calm, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5"), 0, "✓ explored Comms::Ground::listen: 1 outcome", - "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 1 | possible | no choice points", - "complete (1 runs)") + "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 2 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", + "complete (2 runs)") } // TestExploreRunsSiblingsOnOneAssembly checks that two behaviors named on parts of @@ -101,9 +101,9 @@ func TestExploreRunsSiblingsOnOneAssembly(t *testing.T) { binary := buildCLI(t) outcomes := []string{ - "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 1 | 3 | possible | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", - "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 2 | 1 | possible | t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4", - "complete (4 runs)", + "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 1 | 12 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", + "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 2 | 4 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4", + "complete (16 runs)", } byPath := check(t, binary, linkedPairModel, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-state", "Comms::Craft::modes Comms::pair.craft", "-advance", "5") diff --git a/cmd/sysml/explore_turns_test.go b/cmd/sysml/explore_turns_test.go new file mode 100644 index 0000000000..074e162935 --- /dev/null +++ b/cmd/sysml/explore_turns_test.go @@ -0,0 +1,76 @@ +package main + +import ( + "fmt" + "regexp" + "strings" + "testing" +) + +var seenLine = regexp.MustCompile(`seen = \d+`) + +// lostUpdateModel has two actions due at one instant, each reading a shared +// counter in one step and writing it from what it read in the next. +const lostUpdateModel = `package Race { + private import ScalarValues::*; + + part def Counter { attribute count : Integer = 0; } + part counter : Counter; + + action left { + attribute seen : Integer = 0; + first start; + then action wait accept after 1 [SI::s]; + then action read assign seen := counter.count; + then action write assign counter.count := seen + 1; + then done; + } + + action right { + attribute seen : Integer = 0; + first start; + then action wait accept after 1 [SI::s]; + then action read assign seen := counter.count; + then action write assign counter.count := seen + 1; + then done; + } +} +` + +// TestExploreInterleavesExecutorsMoveByMove checks that executors due at one +// instant interleave between their moves: both reads may run before either write, +// so explore, check and a seed reach the lost update, while declared and reverse +// keep running each executor through its turn. +func TestExploreInterleavesExecutorsMoveByMove(t *testing.T) { + binary := buildCLI(t) + invocation := []string{"-instantiate", "Race::counter", "-action", "Race::left", "-action", "Race::right", "-advance", "1"} + lost, leftFirst, rightFirst := "Race::left.seen = 0; Race::right.seen = 0", "Race::left.seen = 0; Race::right.seen = 1", "Race::left.seen = 1; Race::right.seen = 0" + + explored := check(t, binary, lostUpdateModel, append([]string{"-schedule", "explore"}, invocation...)...) + wantReport(t, explored, 0, "✓ explored Race::left, Race::right: 3 outcomes", lost+" |", leftFirst+" |", rightFirst+" |", "complete (") + + checked := check(t, binary, lostUpdateModel, append([]string{"-engine", "check", "-check-diverge", "Race::left.seen"}, invocation...)...) + wantReport(t, checked, 1, "divergent: Race::left.seen ends as 0 or 1", + "outcome: "+lost, "outcome: "+leftFirst, "outcome: "+rightFirst, "witness of 6 choices replayed") + + results := func(policy string) string { + got := check(t, binary, lostUpdateModel, append([]string{"-schedule", policy}, invocation...)...) + wantReport(t, got, 0, "Action completed") + return strings.Join(seenLine.FindAllString(got.output(), -1), ", ") + } + if got := results("declared"); got != "seen = 0, seen = 1" { + t.Errorf("declared runs left through its turn first, want seen = 0, seen = 1, got %s", got) + } + if got := results("reverse"); got != "seen = 1, seen = 0" { + t.Errorf("reverse runs right through its turn first, want seen = 1, seen = 0, got %s", got) + } + seeded := map[string]bool{} + for seed := 1; seed <= 12; seed++ { + seeded[results(fmt.Sprintf("seed:%d", seed))] = true + } + for _, want := range []string{"seen = 0, seen = 0", "seen = 0, seen = 1", "seen = 1, seen = 0"} { + if !seeded[want] { + t.Errorf("no seed of 1..12 reaches %s: %v", want, seeded) + } + } +} diff --git a/cmd/sysml/run_test.go b/cmd/sysml/run_test.go index 558325852e..4faf53868b 100644 --- a/cmd/sysml/run_test.go +++ b/cmd/sysml/run_test.go @@ -1287,7 +1287,7 @@ func TestExploreAdvanceRunsBehaviorsOnOneClock(t *testing.T) { `Due::Beacon::blinking finalState = "shining"; Due::Beacon::blinking visits = "dark, shining"; Due::watcher.sawLit = false; this.isSolid = true; this.lit = true`, `Due::Beacon::blinking finalState = "shining"; Due::Beacon::blinking visits = "dark, shining"; Due::watcher.sawLit = true; this.isSolid = true; this.lit = true`, "possible", - "complete (2 runs)") + "complete (3 runs)") // Advanced short of the instant, neither is due: one outcome, no choice, and // the action that did not complete is the run's error. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 943b049a15..5793e86583 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -708,7 +708,7 @@ checked after the result is bound is not a form the runtime offers, and none is | A guard the executor reads only to report a choice — one after the branch or transition already taken — that fails to evaluate is no alternative and no error: a guard with no result is not true, so its succession is not selected, the run is unchanged, and the failure is an informational `guard-unevaluable` note, while the same failure at the guard the run does take still fails the run | `choice.go` `UnevaluableGuard`, `UnevaluableGuard.Diagnostic` (`SeverityInfo`, code `UnevaluableGuardCode`), `Context.noteUnevaluableGuard`, `Context.UnevaluableGuards`; `action_choice.go` `ActionExecutor.noteUnevaluableGuard`; `action_executor.go` `probeGuard` (a `beginProbe` preview that restores the budget, the trace, every effect and the object identities it took); `state_executor.go` `probeTransition`, `unevaluableTransition`; `state_route.go` `probeBranch` (a choice pseudostate's later branch); `state_change_trigger.go` `probeChangeGuard` | `conformance/action_choice_unevaluable_guard` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_transition` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_branch` + `.expected.json` + `.trace.golden`; `choice_test.go:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestLaterChoiceGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestLaterGuardIsProbedWithoutCost`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteAction_UnevaluableGuardDiagnostics`; `repl/choice_test.go:TestStepReportsUnevaluableGuards`; `robustness_test.go:decision_no_satisfied_guard` (the taken path still fails) | ✅ Faithful (SysML v2 §7.17.3 selects a succession whose guard is true; a guard that cannot be evaluated is not true, and reading it changed nothing) | | A conformance case that admits several outcomes states the whole set: `outcomes` lists every admissible outcome in full — never "anything" — and `admissible` cites the section of `behavior-semantic-oracle.md` that derives the set; a `.trace.order` beside it states the partial order the library does fix as `earlier < later` over trace labels. The harness checks the run's outcome is exactly one listed member, checks the trace against every order constraint, then explores the case and fails on a listed outcome no linearization reached, a reached outcome the list omits, and a hit budget — each naming the outcome and a witness choice sequence | `conformance_test.go` `ExpectedOutcome.Outcomes`/`Admissible`/`ExploreBudget`, `admissibleSchemaProblems` (an `outcomes` list needs two or more full outcomes, an `admissible` title the oracle has, and no single-outcome fields beside it), `matchOutcome`, `runConformanceCase`, `exploreConformanceCase`; `trace_test.go` `checkTraceOrder`, `parseOrderConstraints`, `orderViolations`; `testdata/conformance/README.md` (the schema) | `conformance_test.go:TestAdmissibleOutcomesSchema`, `:TestMatchOutcomeRequiresExactlyOne`, `:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case), `:TestExecutionConformanceUnderPolicies`; `trace_test.go:TestTraceOrderViolationFails`, `:TestExecutionTrace`; `conformance/action_explore_three_writers` (`outcomes` of three, `.trace.order` of six constraints; explored in six runs), `action_choice_shared_message_accept`, `action_choice_fork_token_order` (one outcome, a `.trace.order` admitting the tokens either way), `state_explore_region_order` | ✅ Faithful (a case without `outcomes` is not explored by the harness, so a fixture pinning one linearization of an unobservable openness stays a one-outcome case; the oracle names which fixtures those are) | | Exploration is bounded and distinguishes setup failures from runtime outcomes: the budget is runs (1024 by default) and choice points per run (64), and a budget hit ends the search as `incomplete: budget hit after N runs`, naming `runs` before `depth`; a fresh-context or root-executor creation failure, or a pure structural start-check failure before root behavior runs, means no linearization ran and is returned without outcomes, while a failure during initial model behavior or later is an error outcome. Any runtime-error linearization makes the verdict fail, including an incomplete exploration; only an incomplete search without a witnessed failure is unresolved, and only a complete search without failures proves the outcome set. JSON and the wire include `failedLinearizations` / `failed_linearizations` only when nonzero; standing evidence names the failing count | `runtime/explore.go` `SetupError`, `Exploration.FailedLinearizations`; `runtime/context.go` root action/state setup classification; `runtime/explore_queue.go` `ExploreWith`, `exploreQueue.work`; `runtime/check.go` checker setup failure; `analysis/explore.go` proof strength; `analysis/standing.go` `Result.evidence`; `repl/explore.go` `explorationVerdict`; `cmd/sysml/report.go` `checkExploration`; `grpc/explore.go` `Service.explore` | `runtime/robustness_explore_failures_test.go:TestRuntimeRobustnessExploreFailures`; `analysis/explore_test.go`; `repl/explore_test.go:TestRunActionExploreSetupFailureRunsNoLinearization`, `:TestRunActionExplorePartialFailureFailsTheVerdict`; `cmd/sysml/run_test.go:TestExploreSetupFailureIsNotAnOutcome`, `:TestExplorePartialFailureFailsAndReportsTheFailedRun`, `:TestExploreInitialEntryFailureIsAnOutcome`; `grpc/explore_test.go:TestExploreSetupFailureIsReturnedInTheResponse`, `:TestExploreReportsAFailingRunAsAnOutcome` | ✅ Faithful (setup failures produce no outcome, while a witnessed runtime failure prevents a proof claim) | -| The set of outcomes is also reached by search rather than by enumeration: the explicit-state model checker takes the schedules of an *invocation* — the actions and state machines started on one clock, run to a horizon, and the machines of the objects they materialize — one *move* at a time — one token advancing one node, a body being one move (`stepToken`'s unit, coarser than the interpreter's statement), one event dispatched, one due `do` behavior stepped — enumerating the enabled moves of a state (each token able to act, a join whose tokens have all arrived, a paused token whose wait has ended, a parked `accept` whose message has arrived or whose routing fails under a readiness probe, one move per holding guard of a decision; a machine's dispatch, one per event the library leaves unordered at the instant, and its due do behaviors; among the executors due, the one drawn holds the turn until it has no move at the instant, as `runDue` draws it), snapshotting the run before each choice and restoring it to take the next, so every schedule the library admits is visited and no other. Two moves whose static *footprints* — the features a node's body reads (an outgoing succession's guard and a parked trigger's condition among them) and writes, the channels it sends on and accepts from, the joins and merges it reaches, computed once per node when the action is lowered; for a dispatch the guards and triggers of the transitions the event can select out of the active configuration, their effects and the activity of the states left and entered, for a do step its statements'; one executor's moves pairwise dependent — are independent commute, so only one order of each such pair is searched (persistent sets with a sleep set; a dynamic assignment target or send target depends on everything), and a state already visited — every executor in invocation order: the token multiset by node and frame path, frames root-first with values in the trace recorder's canonical form, a paused body's statement cursor, frames and wait, a machine's configuration, history, values, queue in dispatch order, deferred events, timers and do progress; objects by their materialization path rather than by `Instance.ID`, messages, the clock — is not searched again. What the search finds: a named constraint or requirement `false` at a stable state, a deadlock (`ErrActionDeadlock`, `ErrAcceptDeadlock`) or a typed error a body raises (an unbound parameter, a dangling succession, a division by zero, an `accept` whose `via` port does not resolve, each on the schedule that reaches it) is a *violation*; a feature ending with different final values on different schedules is *divergent*, one witness per value (the features named — `finalState` a machine's resting configuration, `.` and ` finalState` in a joint invocation — else every attribute of the behaviors and their performing object and every machine's `finalState`, an action without an object on its own); a machine resting where nothing wakes it is a complete schedule, not a deadlock, and a wait past the horizon is left unreached, the verdict reading `exhaustive up to t=D`; a bound reached — moves along one schedule (`depth`, 10 000), distinct states (`states`, 1 000 000), the plan's clock (`time`), an executor budget (`actionSteps`, `steps`, `elements`, …) — is named and the verdict is `no violation within bounds`, never `no violation, exhaustive`, the one proof, relative to the atomic move and the properties given. A witness is the `ChoiceTaken` sequence `explore` records for the same steps, written as its choice lines, a blank line and the run's trace, and is *replayed* through the scheduler seam (`replay:`, the policy that follows a witness's choices and refuses where the run departs) before it is reported: the replayed run must reach the state claimed with the same trace, else the witness is *not covered* with the disagreement as the reason. Where an exploration completes, the final states the check reaches are the outcomes it tabled. A body paused mid-statement — a token suspended at a breakpoint or on the clock, a do behavior waiting — is explicit state (`bodyRun`: statement cursor, block, loop and flow-node frames, the nested performance, a `bodyWait` descriptor) a snapshot of the same context captures and restores, so it is searched like any other; a portable `HeldImage` alone refuses it (`ErrSnapshotPausedBody`). Statement-level moves and following a signal to an object whose machine the invocation does not run are later stages'. The search is single-threaded — one executor state per stack frame, one visited set — so `Jobs` divides only the replay of witnesses | `lower/footprint.go` `Footprint`, `Footprints`, `Footprint.Dependent`, `footprintOf` (`Graph.Footprints` beside `Bodies`); `runtime/check.go` `Check`, `checker.search`, `checker.take`, `checker.enter`, `checker.visit`, `checker.stabilize`, `checker.properties`, `checker.final`, `CheckReport`, `CheckVerdict`, `CheckStopped`, `ExecutorBounds`; `runtime/check_reduce.go` `checker.persistent`, `checker.childSleep`, `checker.footprintOf`; `runtime/check_invocation.go` `Invocation`, `Starter`; `runtime/check_run.go` (the executors on one clock, the due order drawn, the horizon); `runtime/check_moves.go` `enabledMove`, `ActionExecutor.enabledMoves`, `ActionExecutor.makeMove`, `StateExecutor.dispatchMoves`, `checkPolicy`; `runtime/check_state.go` `canonicalState`, `stateSpeller`; `runtime/action_body_run.go` `bodyRun`, `bodyWait`; `lower/state_footprint.go` (transition and behavior footprints); `runtime/replay.go` `ParseChoices` (stops at the first blank line), `ReplayPolicy`, `Context.Unfollowed`, `ReplayError`; `runtime/check_replay.go` `Replay`, `Witness.String`, `ReplayDisagreement`; `runtime/action_executor.go` `acceptMatch` (a routing failure kept, not a deadlock); `analysis/check.go` `checkEngine` (below) | `runtime/check_test.go:TestCheckJoinWaitsForSlowestBranch` (`arrived = 3` on every schedule, nothing divergent), `:TestCheckForkBranchesWriteOneFeatureDiverge` (`x` over exactly `{1, 2}`, `leftRan`/`rightRan` agreed), `:TestCheckEvaluatesPropertiesAtCompletion`, `:TestCheckDivergenceOfNamedFeaturesOnly`, `:TestCheckWitnessesReplay`, `:TestCheckReplayDisagreesWithATamperedWitness`, `:TestCheckWitnessesAPerformedActionThroughItsPerformer`, `:TestCheckPropertyOfThePerformerIsWitnessed`, `:TestCheckReportsFailuresAsViolations` (the robustness failures as violations with a witness), `:TestCheckReportsAnUnresolvedViaPortAsTheRoutingError`, `:TestCheckMergeLoopHitsTheDepthBound` (`incomplete`, `depth` named, no hang, no exhaustiveness), `:TestCheckNamesEachExecutorBudget`, `:TestCheckStopsWhenCancelled`, `:TestCheckSettlesTimedBranchesOnTheClock`, `:TestCheckVisitedStatesCloseALoop`; `runtime/check_moves_test.go`; `runtime/check_reduce_test.go:TestCheckReductionIsSound` (reduced and unreduced final-state sets equal over `testdata/check/por_*.sysml`: shared write, guard read, trigger-condition read, send/accept pairing, join convergence, dynamic target), `:TestCheckReductionRatchet` (`testdata/check/reduction_expected.txt`, adjudicated on every movement); `runtime/check_corpus_test.go:TestCheckConformanceOracles` (every action, state and clock case with an admissible set against its `.check.expected.json`, reduced and unreduced — the eight cases whose default run pauses a body and `clock_action_state_due_together` among them), `:TestCheckAgreesWithExploreOverTheConformanceCorpus` (the referee), `:TestCheckWitnessesReplayOverTheConformanceCorpus`; `runtime/check_horizon_test.go` (a re-arming timer bounded by the horizon, a property up to it, an action's wait past it, a machine's failures as violations, the caller's deadline); `runtime/check_reduce_state_test.go` (dispatch and do-step footprints, one executor's moves as a unit); `runtime/action_body_run_test.go` (a body paused at a breakpoint, on the clock and inside a loop resumed, snapshotted and restored); `analysis/check_clock_test.go:TestExploreRefereesCheckOverBehaviorsOnOneClock`, `:TestChecksOfBehaviorsOnOneClockHaveWorkersOfTheirOwn`; `runtime/replay_test.go`; `lower/footprint_test.go`, `lower/state_footprint_test.go` | ✅ Faithful for actions and state machines on one clock (an exhaustive verdict is a proof relative to the atomic move — a body one move, a dispatch one move — and the properties named; statement-level moves and signals to machines off the clock are later stages') | +| The set of outcomes is also reached by search rather than by enumeration: the explicit-state model checker takes the schedules of an *invocation* — the actions and state machines started on one clock, run to a horizon, and the machines of the objects they materialize — one *move* at a time — one token advancing one node, a body being one move (`stepToken`'s unit, coarser than the interpreter's statement), one event dispatched, one due `do` behavior stepped — enumerating the enabled moves of a state (each token able to act, a join whose tokens have all arrived, a paused token whose wait has ended, a parked `accept` whose message has arrived or whose routing fails under a readiness probe, one move per holding guard of a decision; a machine's dispatch, one per event the library leaves unordered at the instant, and its due do behaviors; among the executors due, the one drawn holds the turn after a move only while its next move is independent of everything each other executor due may still do at the instant (`Context.contended`, the same footprints and message dependence as the reduction), and otherwise the due order is drawn again), snapshotting the run before each choice and restoring it to take the next, so every schedule the library admits is visited and no other. Two moves whose static *footprints* — the features a node's body reads (an outgoing succession's guard and a parked trigger's condition among them) and writes, the channels it sends on and accepts from, the joins and merges it reaches, computed once per node when the action is lowered; for a dispatch the guards and triggers of the transitions the event can select out of the active configuration, their effects and the activity of the states left and entered, for a do step its statements'; one executor's moves pairwise dependent — are independent commute, so only one order of each such pair is searched (persistent sets with a sleep set; a dynamic assignment target or send target depends on everything), and a state already visited — every executor in invocation order: the token multiset by node and frame path, frames root-first with values in the trace recorder's canonical form, a paused body's statement cursor, frames and wait, a machine's configuration, history, values, queue in dispatch order, deferred events, timers and do progress; objects by their materialization path rather than by `Instance.ID`, messages, the clock — is not searched again. What the search finds: a named constraint or requirement `false` at a stable state, a deadlock (`ErrActionDeadlock`, `ErrAcceptDeadlock`) or a typed error a body raises (an unbound parameter, a dangling succession, a division by zero, an `accept` whose `via` port does not resolve, each on the schedule that reaches it) is a *violation*; a feature ending with different final values on different schedules is *divergent*, one witness per value (the features named — `finalState` a machine's resting configuration, `.` and ` finalState` in a joint invocation — else every attribute of the behaviors and their performing object and every machine's `finalState`, an action without an object on its own); a machine resting where nothing wakes it is a complete schedule, not a deadlock, and a wait past the horizon is left unreached, the verdict reading `exhaustive up to t=D`; a bound reached — moves along one schedule (`depth`, 10 000), distinct states (`states`, 1 000 000), the plan's clock (`time`), an executor budget (`actionSteps`, `steps`, `elements`, …) — is named and the verdict is `no violation within bounds`, never `no violation, exhaustive`, the one proof, relative to the atomic move and the properties given. A witness is the `ChoiceTaken` sequence `explore` records for the same steps, written as its choice lines, a blank line and the run's trace, and is *replayed* through the scheduler seam (`replay:`, the policy that follows a witness's choices and refuses where the run departs) before it is reported: the replayed run must reach the state claimed with the same trace, else the witness is *not covered* with the disagreement as the reason. Where an exploration completes, the final states the check reaches are the outcomes it tabled. A body paused mid-statement — a token suspended at a breakpoint or on the clock, a do behavior waiting — is explicit state (`bodyRun`: statement cursor, block, loop and flow-node frames, the nested performance, a `bodyWait` descriptor) a snapshot of the same context captures and restores, so it is searched like any other; a portable `HeldImage` alone refuses it (`ErrSnapshotPausedBody`). Statement-level moves and following a signal to an object whose machine the invocation does not run are later stages'. The search is single-threaded — one executor state per stack frame, one visited set — so `Jobs` divides only the replay of witnesses | `lower/footprint.go` `Footprint`, `Footprints`, `Footprint.Dependent`, `footprintOf` (`Graph.Footprints` beside `Bodies`); `runtime/check.go` `Check`, `checker.search`, `checker.take`, `checker.enter`, `checker.visit`, `checker.stabilize`, `checker.properties`, `checker.final`, `CheckReport`, `CheckVerdict`, `CheckStopped`, `ExecutorBounds`; `runtime/check_reduce.go` `checker.persistent`, `checker.childSleep`, `checker.footprintOf`; `runtime/check_invocation.go` `Invocation`, `Starter`; `runtime/check_run.go` (the executors on one clock, the due order drawn, the horizon); `runtime/check_moves.go` `enabledMove`, `ActionExecutor.enabledMoves`, `ActionExecutor.makeMove`, `StateExecutor.dispatchMoves`, `checkPolicy`; `runtime/check_state.go` `canonicalState`, `stateSpeller`; `runtime/action_body_run.go` `bodyRun`, `bodyWait`; `lower/state_footprint.go` (transition and behavior footprints); `runtime/replay.go` `ParseChoices` (stops at the first blank line), `ReplayPolicy`, `Context.Unfollowed`, `ReplayError`; `runtime/check_replay.go` `Replay`, `Witness.String`, `ReplayDisagreement`; `runtime/action_executor.go` `acceptMatch` (a routing failure kept, not a deadlock); `analysis/check.go` `checkEngine` (below) | `runtime/check_test.go:TestCheckJoinWaitsForSlowestBranch` (`arrived = 3` on every schedule, nothing divergent), `:TestCheckForkBranchesWriteOneFeatureDiverge` (`x` over exactly `{1, 2}`, `leftRan`/`rightRan` agreed), `:TestCheckEvaluatesPropertiesAtCompletion`, `:TestCheckDivergenceOfNamedFeaturesOnly`, `:TestCheckWitnessesReplay`, `:TestCheckReplayDisagreesWithATamperedWitness`, `:TestCheckWitnessesAPerformedActionThroughItsPerformer`, `:TestCheckPropertyOfThePerformerIsWitnessed`, `:TestCheckReportsFailuresAsViolations` (the robustness failures as violations with a witness), `:TestCheckReportsAnUnresolvedViaPortAsTheRoutingError`, `:TestCheckMergeLoopHitsTheDepthBound` (`incomplete`, `depth` named, no hang, no exhaustiveness), `:TestCheckNamesEachExecutorBudget`, `:TestCheckStopsWhenCancelled`, `:TestCheckSettlesTimedBranchesOnTheClock`, `:TestCheckVisitedStatesCloseALoop`; `runtime/check_moves_test.go`; `runtime/check_reduce_test.go:TestCheckReductionIsSound` (reduced and unreduced final-state sets equal over `testdata/check/por_*.sysml`: shared write, guard read, trigger-condition read, send/accept pairing, join convergence, dynamic target), `:TestCheckReductionRatchet` (`testdata/check/reduction_expected.txt`, adjudicated on every movement); `runtime/check_corpus_test.go:TestCheckConformanceOracles` (every action, state and clock case with an admissible set against its `.check.expected.json`, reduced and unreduced — the eight cases whose default run pauses a body and `clock_action_state_due_together` among them), `:TestCheckAgreesWithExploreOverTheConformanceCorpus` (the referee), `:TestCheckWitnessesReplayOverTheConformanceCorpus`; `runtime/check_horizon_test.go` (a re-arming timer bounded by the horizon, a property up to it, an action's wait past it, a machine's failures as violations, the caller's deadline); `runtime/check_reduce_state_test.go` (dispatch and do-step footprints, one executor's moves as a unit); `runtime/action_body_run_test.go` (a body paused at a breakpoint, on the clock and inside a loop resumed, snapshotted and restored); `analysis/check_clock_test.go:TestExploreRefereesCheckOverBehaviorsOnOneClock`, `:TestChecksOfBehaviorsOnOneClockHaveWorkersOfTheirOwn`; `runtime/replay_test.go`; `lower/footprint_test.go`, `lower/state_footprint_test.go` | ✅ Faithful for actions and state machines on one clock (an exhaustive verdict is a proof relative to the atomic move — a body one move, a dispatch one move — and the properties named; statement-level moves and signals to machines off the clock are later stages') | | The object an explored run performs a behavior on is one the run builds, never one the session holds: a performer, subject or object named to `explore`, `check`, `smt`, `sweep` or `all` is a *declaration* (a part/item usage or definition) each run instantiates, or a declaration-rooted *path* into what it holds (`Comms::pair.ground`, `Fleet::fleet.rovers[2]`) the run walks inside the object it made, the declaration being instantiated once per run however many behaviors name paths under it, so sibling parts share their assembly and its connectors carry their messages; a declaration `-instantiate` names is given to every run the same way, a machine named alone attaching to the run's one object exhibiting it; the path is checked against the declarations before any run starts (an unknown usage, an index on a single-valued usage, a step through a value) and what only a run can know (a part its recipe left unbuilt, an index past what it built) is that run's error; an id (`#2`, `#2.ground`) or a path from an object the session alone holds is refused as naming no recipe; the wire's `performer_symbol_id` and `subject_symbol_id` spell the same paths, and a witness the checker writes for a behavior on a nested object replays on it | `repl/explore.go` `freshRef` (the longest declaration prefix and the path past it), `checkFreshPath`, `freshPathError`, `planFresh`, `freshPlan.given`, `freshPlan.bind` (one root per declaration per run), `freshObjects.object` (the walk, through `objref.Walker`), `freshObjects.exhibitors`, `freshMachine`, `freshAction`, `freshExhibitorsError`, `UnplannedObjectError`, `ExploredObjectError`; `repl/session.go` `Session.given`, `givenRoots`; `repl/instantiate_report.go` (the CLI's `-instantiate` recorded as a given root); `repl/carryover.go` (a given root dropped with its declaration); `repl/meta.go` `ExhibitorsError.Fresh`; `objref/objref.go` `Ref`, `Segment`, `LooksLikePath`; `objref/walk.go` `Walker.Walk` (the one walk the prompt and the runs share, typed at each refusal); `runtime/context.go` `ExecuteActionPerformedBy`, `ExecuteStatePerformedBy`, `StateOutcomePerformedBy`; `runtime/check_invocation.go` `Invocation.Outcome` (the performers' attributes beside the behaviors'); `grpc/verify.go` `verifyContext.performer`, `subject`, `objectAt`; `grpc/service.go` (`CapabilityPerformer`; `performer_symbol_id` on `ExecuteActionRequest` and `ExecuteStateRequest`); `cmd/sysml/usage.go` (`-instantiate`, `-state`, `-action`); `client/opensysml/execute.go` `PerformedBy`; `client/python/opensysml/connection.py` (`performer=`) | `repl/explore_test.go:TestRunForExploresAMachineOnANestedObject`, `:TestRunForExploresAnActionOnANestedObject`, `:TestRunAnalysisExploresOnANestedSubject`, `:TestRunForExploresSiblingsOnOneRoot` (one root, two machines, the connector between them; the same table under one and four jobs), `:TestExploredRunsAreGivenTheObjectsInstantiated` (a machine alone attaches to the given object, a path reuses it, the prompt's `%instantiate` gives nothing, a given root outlives unrelated submissions and not its declaration's), `:TestExploredPathsAreCheckedAgainstTheDeclarations` (an id, an unknown usage, an index on one value, a step through a value: refused before any run; a part left unbuilt: the run's error); `cmd/sysml/explore_nested_test.go:TestExploreRunsAMachineOnANestedObject` (a connector race tables two outcomes, its no-race variant one, byte for byte under `-jobs 1` and `-jobs 4`), `:TestExploreRunsSiblingsOnOneAssembly`, `:TestExploreRefusesPathsItCannotPlan`, `:TestEngineCheckWitnessesANestedObjectsDivergence` (the witness written, replayed under `-schedule replay:`, and composed under `-engine all`); `runtime/check_test.go:TestCheckWitnessesOfSeveralBehaviorsReplay`, `runtime/replay_test.go:TestReplayFollowsDoActionWitnesses`, `:TestReplayFollowsSiblingDoActionWitnesses`; `grpc/explore_test.go:TestPerformOnANestedObjectOverTheWire`, `grpc/analysis_test.go:TestRunAnalysisOnANestedSubject`, `grpc/capability_test.go` (`performer` advertised); `client/opensysml/performer_test.go`; `client/python/tests/test_performer.py` | ✅ Faithful (the runs' objects are built by the same instantiation and walked by the same `objref.Walker` as the prompt's, so a path means one thing at the prompt and in a run; the session's objects stay out of every run by construction, the plan being made under the session's lock and the objects inside each run) | | Action execution nodes | `action_executor.go:723` stepActionExecutionNode | `action_control_flow.sysml` | ✅ Faithful | | Nested action invocation (`action call : Callee;`, `action call = Callee(3, 4);`, `action call = Callee(a = 3);`, `perform action call : Callee;`) | `runtime/action_frame.go` `bindArguments`, `performInvocation`, `checkInputsBound`; `runtime/state_statements.go` `stateStmtHost.performNode`; `runtime/invoke_action.go` `invocationArguments`, `bindArgumentList`, `Context.actionParametersOf` (over `semantics.Model.BehaviorParametersOf`, so inherited and redefined parameters keep their effective order); `action_executor.go` `stepNestedAction` | `invoke_action_test.go:TestInvokeActionPassesParametersBothWays`, `:TestInvokeActionBindsPositionalArguments`, `:TestInvokeActionBindsNamedArguments`, `:TestInvokeActionRejectsBadArguments`; `conformance/action_node_invocation_positional`, `action_node_invocation_named`, `action_node_typed_body_inputs`, `action_node_inherited_parameters`, `action_node_invocation_empty`, `action_inherited_typed_node_scope`, `action_node_arguments_before_defaults`, `state_block_flow_node_arguments_before_defaults` | ✅ Faithful (arguments bind the callee's inputs by the callee's parameter order and names, never by what the caller happens to name alike; they bind the node's pins before the defaults it declares are evaluated, so a default an argument replaces is never evaluated and one the node keeps reads the argument's value, in an action's flow and in a state's body alike; the callee is resolved where the node was declared, so a node a derived action inherits still finds a callee visible only to the general action; a surplus, missing, unknown or repeated argument is `ErrActionArity`, `ErrUnboundParameter`, `ErrUnknownParameter` or `ErrDuplicateArgument` before the callee runs — a surplus one is also reported statically by `passes/typecheck_expr.go`, so no conformance fixture states it. The row above states the compatibility by-name fallback a bare usage keeps) | @@ -812,7 +812,7 @@ checked after the result is bound is not a form the runtime offers, and none is | Earliest transfer first (`Occurrence::incomingTransferSort` defaults to `earlierFirstIncomingTransferSort`): a completion event is dispatched before a signal due at the same instant. A replayed deferred signal is a new send and is dispatched behind the occurrences already queued — the standard encoding has no way to place it ahead of the pool, where PSSM §8.4 releases a deferred occurrence ahead of every non-completion occurrence | `executor_common.go` eventHeap.Less, isCompletionEvent | `choice_test.go:TestCompletionTransitionChoiceRereadsGuards`, `signal_injection_test.go:TestRunToCompletionTakesAPendingSignalBeforeALaterTimer`; PSSM referee rows *Deferred 001*, *Deferred 005* (`docs/project/pssm-referee.md`) | ⚠️ Approximate — the replay order of different deferred signals against one another and against the pool is not expressible in standard notation | | A transition out of a composite state is enabled while any of its substates is active: matching walks outward from every active leaf through the lowered containment (`StateGraph.ParentState`), the innermost enabled transition wins for the same event (KerML `StatePerformances::StatePerformance::acceptable`, whose `isDispatch` invariant lets an enclosing state performance accept a transfer only when no substate performance in the dispatch scope accepted it), and a false guard does not consume it | `state_executor.go` broadcastEvent, selectTransitions, losesToNestedTransition, nestedIn, activeLeaves, fireFrom, enabledTransitions, acceptsSignal/acceptsSignalFrom (an enclosing state's `accept` takes a signal off the bus) | `conformance/state_composite_outer_transition.sysml`, `:state_composite_inner_priority.sysml`, `state_composite_transition_test.go:TestCompositeStateHandlesEventItsSubstateDoesNot`, `:TestFalseGuardInsideACompositeStateFallsOutward`, `:TestTransitionOutOfAnIntermediateCompositeStateKeepsItsOwnerActive`, `:TestOuterCompositeStateStillHandlesItsEventAfterASubstateMoved`, `robustness_test.go:signal_no_level_of_a_composite_state_accepts` | ✅ Faithful | | Two transitions out of one state enabled by one event: each is a `StateTransitionPerformance` (Kernel Semantic Library `StatePerformances.kerml`) whose `transitionLink` is `HappensBefore[0..1]`, and nothing in the library orders one against another, so which fires is the executor's pick; the innermost-wins rule between a substate's transition and its enclosing state's is SysML v2/KerML order, not a pick | `state_executor.go` `enabledTransitions`, `transitionEnabled`, `probeTransition` (every transition out of the state is matched against the event and its guard and join evaluated — a call trigger's arguments bound for the guard and unbound after — the first enabled fires under the default policy; the ones after it are read in a `beginProbe` preview that restores the budget, the trace, every effect and the object identities the preview took, and one that fails to evaluate is no alternative and no error, recorded as a `guard-unevaluable` note by `unevaluableTransition`), `chooseTransition`, `transitionChoice` (several enabled are a choice point naming the state, the trigger and the transitions by position and target; the pick among them is made only for a candidate that survived conflict resolution); the notes ride on the `dispatchCandidate` into `fireFrom`, and `transitionDecided` records them once the firing transition's guard has been read for the last time — a candidate another region's firing disabled meanwhile reports nothing — after `selectCandidates` has kept one candidate per transition and `losesToNestedTransition` has dropped a composite state's candidate to a nested one (a transition several regions select through their enclosing state is one choice, and ancestor priority is never among the alternatives); `state_change_trigger.go` `observeChangeConditions`, `probeChangeGuard`, `risenChangeTransitions` (every change transition risen by one poll is collected the same way: a state's guards are read live until the first enabled, the ones after it in a `beginProbe` preview, and one that fails to evaluate is no alternative and no error, noted as `guard-unevaluable` and left armed; the first declared fires) | `conformance/state_choice_transition_conflict.sysml` + `.expected.json` (both outcomes listed as admissible) + trace golden; `conformance/state_choice_ancestor_priority_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_shared_ancestor_regions.sysml` + `.expected.json` + trace golden (one `choice` line for two regions); `conformance/state_choice_ancestor_outranked_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_unevaluable_transition.sysml` + `.expected.json` + trace golden; `conformance/state_choice_change_transition_conflict.sysml` + `.expected.json` (both outcomes) + trace golden; `choice_test.go:TestTransitionChoiceNamesStateAndEvent`, `:TestAncestorPriorityIsNotAChoice`, `:TestSharedAncestorChoiceIsReportedOnce`, `:TestAncestorChoiceSuppressedByNestedTransitionIsNotReported`, `:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestNotesOfATransitionBlockedBeforeFiringAreDropped`, `:TestNotesOfATransitionFailingInItsEffectAreKept`, `:TestChangeTransitionChoice`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestChangeTransitionChoiceUnderHierarchyAndRegions`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteState_ChoicePointDiagnostics`; `repl/choice_test.go:TestAdvanceReportsChoicePoints` | ✅ Faithful (declaration order is tool-defined and kept; the pick is reported, and the ordered case is not) | -| Executors due at one instant of the clock are unordered: two performances waiting on the same `TimeInstantValue` (Kernel Semantic Library `Clocks.kerml`) are `HappensBefore`-linked by nothing, so which of an action token and a state transition, of two state machines, or of two actions runs first when their instant comes is the executor's pick | `advance.go` `Context.runDue` (the executors with work due at the current instant, in creation order, are a choice point of kind `ChoiceDueOrder` placed `at t=` and naming each executor — `action `, `state machine of object #n` — and the one run first; the pick is drawn by `scheduler.go` `scheduler.pickDue` under the run's policy — the last created under `reverse`, the default, so a run holding one executor is unchanged; the first created under `declared`; a draw under `seed:`; under `explore`, the exploring run's next slot, `scheduler.describe` giving it the due-order kind and alternatives so the witness names the executor run first and every order of the due executors is a linearization replayed; one executor alone due is no choice and records nothing; within one executor, its work runs in the order it always has; the executors polling a change condition once the definite work at the instant has settled are drawn the same way, so which watcher sees what another's reaction changed is the pick); `choice.go` `ChoiceDueOrder`, `ChoicePoint.String` (`choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first)`) | `conformance/clock_action_state_due_together.sysml` + `.expected.json` (`outcomes`: either may run first) + trace goldens under the default, `declared` and `seed:1`; `conformance/clock_two_machines_share_clock.trace.golden` (two machines due together); `conformance/clock_action_accept_after.trace.golden`, `clock_action_accept_at.trace.golden`, `clock_do_action_while_token_waits.trace.golden` (one executor due: no `choice` line); `scheduler_test.go:TestDueOrderChoice` (the pick under each policy, and none recorded for one executor), `:TestChangeWatchOrderChoice` (two machines polling one condition: the pick under each policy decides which sees the raised value and which what the first left); `repl/runtime_commands_test.go:TestAdvanceMovesActionAndStateDebuggersTogether`; `explore_test.go:TestExploreDueOrder` (three machines due together explore to their six orders, each witnessed by a due-order choice among 3 then among 2, and the driven policies each take one of them), `conformance_test.go:TestExecutionConformance` (`clock_action_state_due_together` explored: both orders reached, no other); `repl/explore.go` `exploreRunFor` (`RunFor` under `explore`: the behaviors named started on one clock in every run, advanced once, their outcomes joined by `Context.JointOutcome` under each behavior's name), `repl/explore_test.go:TestRunForExploresEveryDueOrder`, `cmd/sysml/run_test.go:TestExploreAdvanceRunsBehaviorsOnOneClock` | ✅ Faithful (the default order — the executor started last first — is tool-defined and pinned by the trace golden; the pick is reported, and one executor alone is not; `explore` reaches every order) | +| Executors due at one instant of the clock are unordered: two performances waiting on the same `TimeInstantValue` (Kernel Semantic Library `Clocks.kerml`) are `HappensBefore`-linked by nothing, so which of an action token and a state transition, of two state machines, or of two actions runs first when their instant comes is the executor's pick | `advance.go` `Context.runDue` (the executors with work due at the current instant, in creation order, are a choice point of kind `ChoiceDueOrder` placed `at t=` and naming each executor — `action `, `state machine of object #n` — and the one run first; the pick is drawn by `scheduler.go` `scheduler.pickDue` under the run's policy — the last created under `reverse`, the default, so a run holding one executor is unchanged; the first created under `declared`; a draw under `seed:`; under `explore`, the exploring run's next slot, `scheduler.describe` giving it the due-order kind and alternatives so the witness names the executor run first and every order of the due executors is a linearization replayed; one executor alone due is no choice and records nothing; under `explore`, `check`, `replay` and `seed:` the executor drawn makes one move and keeps its turn only while its next move is independent of what every other executor due may still do before the instant ends — `advance.go` `Context.contended` against `future_footprint.go` `futureFootprints.executorFuture`, which stops an executor's future at a wait on a literal delay past the instant and otherwise takes all it may do, and `message_dependence.go` `Context.channelsMeet`, which separates a send from an accept or two accepts only where both signal types resolve statically and do not conform, and keeps every unresolved type, `via` route, receiver and dispatch-drop dependent — and otherwise the due order is drawn again, so two reads of a shared feature may both run before either write; under `declared` and `reverse` the executor drawn runs its work at the instant through, in the order it always has; the executors polling a change condition once the definite work at the instant has settled are drawn the same way, so which watcher sees what another's reaction changed is the pick); `choice.go` `ChoiceDueOrder`, `ChoicePoint.String` (`choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first)`) | `conformance/clock_action_state_due_together.sysml` + `.expected.json` (`outcomes`: either may run first) + trace goldens under the default, `declared` and `seed:1`; `conformance/clock_two_machines_share_clock.trace.golden` (two machines due together); `conformance/clock_action_accept_after.trace.golden`, `clock_action_accept_at.trace.golden`, `clock_do_action_while_token_waits.trace.golden` (one executor due: no `choice` line); `scheduler_test.go:TestDueOrderChoice` (the pick under each policy, and none recorded for one executor), `:TestChangeWatchOrderChoice` (two machines polling one condition: the pick under each policy decides which sees the raised value and which what the first left); `repl/runtime_commands_test.go:TestAdvanceMovesActionAndStateDebuggersTogether`; `explore_test.go:TestExploreDueOrder` (three machines due together explore to their six orders, each witnessed by a due-order choice among 3 then among 2, and the driven policies each take one of them), `conformance_test.go:TestExecutionConformance` (`clock_action_state_due_together` explored: both orders reached, no other); `repl/explore.go` `exploreRunFor` (`RunFor` under `explore`: the behaviors named started on one clock in every run, advanced once, their outcomes joined by `Context.JointOutcome` under each behavior's name), `repl/explore_test.go:TestRunForExploresEveryDueOrder`, `cmd/sysml/run_test.go:TestExploreAdvanceRunsBehaviorsOnOneClock`, `cmd/sysml/explore_turns_test.go:TestExploreInterleavesExecutorsMoveByMove` (two read-then-write actions due together: explore, check and seeds reach the lost update, `declared` and `reverse` keep their order) | ✅ Faithful (the default order — the executor started last first — is tool-defined and pinned by the trace golden; the pick is reported, and one executor alone is not; `explore` reaches every order) | | Taking a transition out of a composite state exits the states being left innermost-first, then runs the effect, then enters the target; leaving a composite with orthogonal regions exits every active region first | `state_executor.go` transitionToInto (exit to the least common ancestor), exitStates/exitedByAncestorRegion (a state whose region another state being left owns is exited by that state's recursive region teardown, so the chain walk does not exit it a second time), `state_region_transition.go` leaveRegion (which instead clears the region a state is active in, recording its history, before exiting that state, since a region's active state may be nested below it), moveBetweenRegions, exitRegionTo, leaveTopRegions | `conformance/state_composite_exit_order.sysml` + trace golden (two levels of nesting), `:state_composite_orthogonal_exit.sysml` + trace golden, `:state_composite_nested_regions_exit_once.sysml` + trace golden (a region holding a composite with a region of its own: every level exits exactly once), `robustness_test.go:exit_of_nested_regions_with_a_history_pseudostate` | ✅ Faithful | | Every state transition is external — its source is exited, its effect runs, and its target is entered afresh — including when the target is the source itself or one of its substates: KerML orders `transitionLinkSource then effect` and `effect then transitionLink.laterOccurrence` (Kernel Semantic Library `TransitionPerformances.kerml`, `TransitionPerformance`), the source's `exit` is its last step (`StatePerformances.kerml`, `StatePerformance`: `entry then middle`, `middle then exit`) and a state transition orders that exit after its guard (`StateTransitionPerformance`: `guard then transitionLinkSource.exit`). So a simple state transitioning to itself runs exit, effect, entry, and a composite is exited and re-entered around the effect with its regions restarting at their initial states | `state_executor.go` transitionToInto, encloses (the source is the target or contains it); `state_region_transition.go` moveBetweenRegions (the exit boundary is the source's parent where the source `encloses` the target, so a composite self-transitioning inside an orthogonal region is exited too, while its sibling regions stay as they were) | `conformance/state_composite_self_transition.sysml` + trace golden (exit substate, exit composite, effect, re-enter composite and its region), `:state_composite_to_substate.sysml` + trace golden, `:state_composite_self_transition_in_region.sysml` + trace golden, `:w6e_state_simple_self_transition.sysml` + trace golden (exit, effect, entry on a simple state), `parse/w6e_state_self_transition.golden`, `state_composite_transition_test.go:TestOneEventTakesACompositesTransitionOnce`, `w6e_state_self_transition_test.go:TestSimpleSelfTransitionExitsAndReEntersItsState`, `:TestSimpleSelfTransitionInARegionLeavesSiblingRegionsAlone`, `robustness_test.go:composite_self_transition_with_no_substate_to_re_enter`, `w6e_robustness_test.go:TestSimpleSelfTransitionThatNeverSettlesIsBounded`, `:TestSimpleSelfTransitionEffectReadingAnUnknownFeatureIsReported`; `conformance/state_transition_guard_exit_effect_entry_order.sysml` + trace golden (the order made observable through values: the guard reads the pre-exit value, the effect the exit's, the entry the effect's — derived from the same library text in [the semantic oracle](behavior-semantic-oracle.md)) | ✅ Faithful (self-assessed: the pinned reference has no execution surface for state machines, so this row is assessed against the library text cited above and our own goldens, not against another implementation. One residual is tool-defined: a composite state stating no starting substate — no `initial` and no region — is re-entered with no substate active, since nothing names the substate to enter) | | An event reaches only the regions still active when it is dispatched | `state_executor.go` broadcastEvent (each active leaf is re-checked before it is offered the event) | `state_composite_transition_test.go:TestExitedNestedRegionDoesNotReactToTheSameEvent` | ✅ Faithful | diff --git a/internal/exec/runtime/action_executor.go b/internal/exec/runtime/action_executor.go index 6c8cb1f3c1..d91bb250b0 100644 --- a/internal/exec/runtime/action_executor.go +++ b/internal/exec/runtime/action_executor.go @@ -556,6 +556,11 @@ func (e *ActionExecutor) RunToCompletion() error { // run is the RunToCompletion loop, holding the clock where it is when // atCurrentTime is set. func (e *ActionExecutor) run(atCurrentTime bool) error { + return e.runSteps(atCurrentTime, false) +} + +// runSteps is run, stopping after one step where single is set. +func (e *ActionExecutor) runSteps(atCurrentTime, single bool) error { defer e.ctx.beginExecutorRun(&e.driven)() if e.released { @@ -618,6 +623,14 @@ func (e *ActionExecutor) run(atCurrentTime bool) error { e.held = true return err } + if single { + break + } + if !atCurrentTime { + if err := e.ctx.yieldTurn(e, &progress); err != nil { + return err + } + } } if e.state == StateWaiting && !atCurrentTime { e.endPausedBodies() @@ -2724,9 +2737,18 @@ func (e *ActionExecutor) watchesChange() bool { // runDue runs the action to quiescence at the current instant; the steps it takes // count against the drive's budget together with those already taken. func (e *ActionExecutor) runDue(progress *dueProgress) (bool, error) { + return e.runDueSteps(progress, false) +} + +// runMove is runDue stopping after one step. +func (e *ActionExecutor) runMove(progress *dueProgress) (bool, error) { + return e.runDueSteps(progress, true) +} + +func (e *ActionExecutor) runDueSteps(progress *dueProgress, single bool) (bool, error) { before, positions, taken := e.stepCount, e.tokenPositions(), e.dynamicsSteps() e.stepsSpent = progress.steps - err := e.run(true) + err := e.runSteps(true, single) e.stepsSpent = 0 progress.steps += int64(e.stepCount - before) return e.state != StateWaiting || !maps.Equal(positions, e.tokenPositions()) || e.dynamicsSteps() != taken, err diff --git a/internal/exec/runtime/advance.go b/internal/exec/runtime/advance.go index c3bef3a07f..d598d44e56 100644 --- a/internal/exec/runtime/advance.go +++ b/internal/exec/runtime/advance.go @@ -5,6 +5,7 @@ import ( "math" "slices" + "github.com/Open-MBEE/OpenSysML/internal/ir/lower" "github.com/Open-MBEE/OpenSysML/internal/semantic/semantics" ) @@ -25,6 +26,8 @@ type clockWaiter interface { // runDue runs the executor to quiescence at the current instant, counting // against progress, and reports whether it got anywhere. runDue(progress *dueProgress) (bool, error) + // runMove runs one move of the executor's due work, as runDue does. + runMove(progress *dueProgress) (bool, error) // finished reports an executor the clock has nothing left to drive; running a // run of it already on the stack, which drives the clock itself. finished() bool @@ -230,15 +233,115 @@ func (ctx *Context) drawDueOrder(due []clockWaiter) (int, error) { return pick, nil } -// runWaiter runs one executor's due work, recording the run when the executor -// is an object's behavior. +// contended reports whether a move w may make next depends on a move another +// executor may make before it at this instant, under a policy interleaving turns. +func (ctx *Context) contended(w clockWaiter) bool { + if sched := ctx.scheduling(); !sched.interleavesTurns() && !sched.checking() { + return false + } + if ctx.futures == nil { + ctx.futures = newFutureFootprints(ctx) + } + next := nextFootprint(w) + for _, other := range ctx.rivals(w) { + if next.DependentBy(ctx.futures.executorFuture(other), ctx.channelsMeet(executorSelf(w), executorSelf(other))) { + return true + } + } + return false +} + +// rivals are the executors other than w that may move at this instant before w's +// next move: those due or on the stack, and those a rival's moves may wake. +func (ctx *Context) rivals(w clockWaiter) []clockWaiter { + var rivals, idle []clockWaiter + for _, other := range ctx.clock.waiters { + switch { + case other == w || other.finished(): + case other.dueWork() || other.running(): + rivals = append(rivals, other) + default: + idle = append(idle, other) + } + } + for woke := true; woke; { + woke = false + for i, other := range idle { + if other != nil && ctx.wokenBy(other, rivals) { + rivals = append(rivals, other) + idle[i], woke = nil, true + } + } + } + return rivals +} + +// wokenBy reports whether a rival's future may not commute with the idle executor's. +func (ctx *Context) wokenBy(idle clockWaiter, rivals []clockWaiter) bool { + future := ctx.futures.executorFuture(idle) + for _, rival := range rivals { + if ctx.futures.executorFuture(rival).DependentBy(future, ctx.channelsMeet(executorSelf(rival), executorSelf(idle))) { + return true + } + } + return false +} + +// nextFootprint is what any move the executor may make next touches. +func nextFootprint(w clockWaiter) lower.Footprint { + switch exec := w.(type) { + case *ActionExecutor: + var fp lower.Footprint + for _, t := range exec.tokens { + fp = unionFootprints(fp, standing(exec, t)) + } + return fp + case *StateExecutor: + return machineStanding(exec) + } + return lower.Footprint{Dynamic: true} +} + +// runTurn runs the executor's due work, holding its turn only through moves +// independent of every other executor's, so the due order is drawn before each other. +func (ctx *Context) runTurn(w clockWaiter, progress *dueProgress) (bool, error) { + if !ctx.scheduling().interleavesTurns() { + return w.runDue(progress) + } + ran := false + for { + moved, err := w.runMove(progress) + ran = ran || moved + if err != nil || !moved || !w.dueWork() || ctx.contended(w) { + return ran, err + } + } +} + +// yieldTurn draws the due order again before a driver's move contended by another +// executor, running the executors the draw falls on before the driver goes on. +func (ctx *Context) yieldTurn(driver clockWaiter, progress *dueProgress) error { + if ctx.body != nil || !ctx.contended(driver) { + return nil + } + for _, w := range ctx.clock.waiters { + if w != driver && w.running() { + return nil + } + } + _, err := ctx.runDue(driver, progress) + return err +} + +// runWaiter runs one executor's turn of due work, recording the run when the +// executor is an object's behavior. func (ctx *Context) runWaiter(w clockWaiter, progress *dueProgress) (bool, error) { if ctx.trace != nil { if behavior := ctx.behaviorOf(w); behavior != nil { ctx.trace.RecordBehaviorRun(behavior.Kind.String(), behavior.Name, behavior.Object.ID) } } - moved, err := w.runDue(progress) + moved, err := ctx.runTurn(w, progress) if err != nil { if behavior := ctx.behaviorOf(w); behavior != nil { wrapped := fmt.Errorf("%s: %w", behavior.Describe(), err) diff --git a/internal/exec/runtime/check.go b/internal/exec/runtime/check.go index b6db845f8c..de55d5e1c6 100644 --- a/internal/exec/runtime/check.go +++ b/internal/exec/runtime/check.go @@ -244,14 +244,13 @@ func (e *CheckStopped) Unwrap() error { return e.Cause } // resolving them and the search runs from every state a start reaches. func Check(stop context.Context, fresh func() (*Context, error), start Starter, budget CheckBudget, opts CheckOptions, props []CheckProperty) (*CheckReport, error) { c := &checker{ - budget: budget, - opts: opts, - props: props, - visited: make(map[stateKey]*visitedState), - onStack: make(map[stateKey]int), - finals: make(map[string]int), - futures: make(map[futureKey]lower.Footprint), - machineFutures: make(map[*lower.StateGraph]lower.Footprint), + budget: budget, + opts: opts, + props: props, + visited: make(map[stateKey]*visitedState), + onStack: make(map[stateKey]int), + finals: make(map[string]int), + futureFootprints: newFutureFootprints(nil), } starts := [][]int{nil} for i := 0; i < len(starts); i++ { @@ -287,6 +286,7 @@ func (c *checker) searchFrom(stop context.Context, fresh func() (*Context, error ctx.SetTrace(NewTraceRecorder()) } c.ctx, c.budgets = ctx, ctx.Budgets() + c.bind(ctx) run, err := beginInvocation(ctx, start) var setup *SetupError if errors.As(err, &setup) { @@ -339,9 +339,7 @@ type checker struct { // onStack counts the frames on the stack at each state. onStack map[stateKey]int stack []*checkFrame - futures map[futureKey]lower.Footprint - // machineFutures is the footprint of a machine's whole graph, by graph. - machineFutures map[*lower.StateGraph]lower.Footprint + *futureFootprints // budgets are the executors' budgets, each a bound on the moves of its kind // along one schedule. @@ -370,6 +368,14 @@ type visitedState struct { depth int cut bool violated []string + // entry is the mass of the path first reaching the state, on which entryViolated + // were false; below maps each violation to the mass credited under the state. + entry float64 + entryViolated []string + below map[int]float64 + // exact is set once the search under the state left nothing out, so the share + // of a path reaching it again follows from entry and below. + exact bool } // checkFrame is one state on the search stack. @@ -400,6 +406,8 @@ type checkFrame struct { mass float64 units map[checkedExecutor]int violated []string + // inexact is set once a bound, a cycle or a revisit left mass out under the state. + inexact bool } // spending counts the moves of one schedule by the executor budget each draws on. @@ -442,28 +450,64 @@ func (c *checker) hit(bound string) { if !slices.Contains(c.bounds, bound) { c.bounds = append(c.bounds, bound) } + c.inexact() +} + +// inexact marks the state searched from as one whose share of mass is not exact. +func (c *checker) inexact() { + if len(c.stack) > 0 { + c.stack[len(c.stack)-1].inexact = true + } +} + +// spread adds mass to the violation at i and to what every state on the stack holds below it. +func (c *checker) spread(i int, mass float64) { + c.violations[i].Mass += mass + for _, f := range c.stack { + if seen := c.visited[f.key]; seen != nil { + seen.below[i] += mass + } + } +} + +// carry credits a path reaching a searched state again its share of the masses +// below it, reporting false where that share is not exact. +func (c *checker) carry(seen *visitedState, mass float64, violated []string) bool { + if !seen.exact || seen.entry <= 0 || !sameNames(violated, seen.entryViolated) { + return false + } + for i, below := range seen.below { + c.spread(i, mass*below/seen.entry) + } + return true +} + +func sameNames(a, b []string) bool { + return !slices.ContainsFunc(a, func(n string) bool { return !slices.Contains(b, n) }) && + !slices.ContainsFunc(b, func(n string) bool { return !slices.Contains(a, n) }) } // violate records the violation; a property is reported once, by the shortest // schedule found to reach a state where it is false, its mass the sum over the // schedules reaching such a state. func (c *checker) violate(v Violation) { + mass := v.Mass if v.Kind == ViolationProperty { for i, seen := range c.violations { if seen.Kind != ViolationProperty || seen.Name != v.Name { continue } - seen.Mass += v.Mass if v.Depth < seen.Depth { v.Mass = seen.Mass c.violations[i] = v - } else { - c.violations[i].Mass = seen.Mass } + c.spread(i, mass) return } } + v.Mass = 0 c.violations = append(c.violations, v) + c.spread(len(c.violations)-1, mass) } // shareOf is the share of one choice point's alternative: the stated weight's @@ -530,6 +574,11 @@ func (c *checker) search(stop context.Context, mass float64) error { if !f.full && len(f.moves) < len(f.all) { c.leftOut = true } + if f.inexact || f.cut || len(f.moves) < len(f.all) { + c.inexact() + } else if seen := c.visited[f.key]; seen.depth == f.depth { + seen.exact = true + } if f.cut && len(c.stack) > 0 { c.cut(c.stack[len(c.stack)-1]) } @@ -645,9 +694,13 @@ func (c *checker) failed(err error, depth int, mass float64) error { // complete visits the terminal state the invocation reached: a state like any // other, its properties evaluated when new, whose outcome is a final. func (c *checker) complete(depth int, mass float64, violated []string) error { - if _, _, seen, _, err := c.visit(depth, mass, violated); err != nil || seen == nil { + _, _, seen, visited, err := c.visit(depth, mass, violated) + if err != nil || seen == nil { return err } + if !visited { + seen.exact = true + } c.final() return nil } @@ -662,12 +715,16 @@ func (c *checker) visit(depth int, mass float64, violated []string) (form canoni c.hit("states") return form, key, nil, false, nil } - seen = &visitedState{explored: make(map[string]bool), depth: depth} + seen = &visitedState{explored: make(map[string]bool), depth: depth, + entry: mass, entryViolated: slices.Clone(violated), below: make(map[int]float64)} c.visited[key] = seen c.tellHeld() c.properties(depth, mass, violated, seen) } else { - c.revisit = true + if !c.carry(seen, mass, violated) { + c.revisit = true + c.inexact() + } // A path reaching a state where a property is false is credited the first // time it violates it, however the property was found false here before. for _, name := range seen.violated { @@ -690,7 +747,7 @@ func (c *checker) visit(depth int, mass float64, violated []string) (form canoni func (c *checker) credit(name string, mass float64) { for i, v := range c.violations { if v.Kind == ViolationProperty && v.Name == name { - c.violations[i].Mass += mass + c.spread(i, mass) return } } @@ -746,19 +803,17 @@ func (s *visitedState) mark(moves []searchMove) { // footprints, in canonical order. func (c *checker) movesOf(form canonicalForm) []searchMove { enabled := c.run.enabledMoves() - draw := len(owners(enabled)) > 1 moves := make([]searchMove, 0, len(enabled)) for _, m := range enabled { - moves = append(moves, c.named(form, m, draw)) + moves = append(moves, c.named(form, m)) } slices.SortFunc(moves, func(a, b searchMove) int { return strings.Compare(a.name, b.name) }) return moves } // named gives the move its canonical name — its executor's canonical name, its -// token's where it moves one, else its label, and its picks — and its footprint: -// the whole turn's where the move takes the turn, at a state drawing the due order. -func (c *checker) named(form canonicalForm, m enabledMove, draw bool) searchMove { +// token's where it moves one, else its label, and its picks — and its footprint. +func (c *checker) named(form canonicalForm, m enabledMove) searchMove { name := form.names[m.Owner] + ": " if m.Token != 0 { name += form.tokens[tokenKey{m.Owner, m.Token}] @@ -768,11 +823,7 @@ func (c *checker) named(form canonicalForm, m enabledMove, draw bool) searchMove for _, pick := range m.Picks { name = fmt.Sprintf("%s pick %d", name, pick+1) } - footprint := c.footprintOf(m) - if draw { - footprint = c.turnFootprint(m) - } - return searchMove{enabledMove: m, name: name, footprint: footprint} + return searchMove{enabledMove: m, name: name, footprint: c.footprintOf(m)} } // reveal adds, right after the move, the moves taking each other alternative of diff --git a/internal/exec/runtime/check_reduce.go b/internal/exec/runtime/check_reduce.go index 393b3a82ec..8a9b595c0e 100644 --- a/internal/exec/runtime/check_reduce.go +++ b/internal/exec/runtime/check_reduce.go @@ -13,12 +13,6 @@ import ( // equivalent predecessor already explored (bounded-model-checking.md, "The algorithm"). // A unit is what a move advances: an action's token, or a state machine as a whole. -// futureKey identifies what a token may still do: its node in its flow. -type futureKey struct { - graph *lower.ActionGraph - node ast.Node -} - // unit is the unit the move advances: its owner's token, the owner itself for a // state machine's move. func (m enabledMove) unit() tokenKey { @@ -34,7 +28,7 @@ func (c *checker) footprintOf(m enabledMove) lower.Footprint { } switch exec := m.Owner.(type) { case *ActionExecutor: - return c.standing(exec, exec.tokens[exec.tokenIndex(m.Token)]) + return standing(exec, exec.tokens[exec.tokenIndex(m.Token)]) case *StateExecutor: if m.Kind == moveDoStep { return doStepFootprint(exec, m.Node) @@ -46,33 +40,13 @@ func (c *checker) footprintOf(m enabledMove) lower.Footprint { // standing is the footprint of the node the token stands at; a body paused // mid-statement goes on with the rest of that node's, which the node's covers. -func (c *checker) standing(exec *ActionExecutor, t Token) lower.Footprint { +func standing(exec *ActionExecutor, t Token) lower.Footprint { if exec.dynamics != nil { return dynamicsFootprint() } return tokenGraphOf(exec, t).Footprints()[t.Location] } -// turnFootprint is what the move's owner may touch over the turn the move takes: -// the owner keeps the turn until it has no move left at the instant, so it is the -// future of every unit of the owner — each token of an action, the machine whole. -func (c *checker) turnFootprint(m enabledMove) lower.Footprint { - if m.Fails != nil { - return lower.Footprint{Dynamic: true} - } - switch exec := m.Owner.(type) { - case *ActionExecutor: - var turn lower.Footprint - for _, t := range exec.tokens { - turn = unionFootprints(turn, c.tokenFuture(exec, t)) - } - return turn - case *StateExecutor: - return c.machineFuture(exec) - } - return lower.Footprint{Dynamic: true} -} - // machineStanding is what the machine's next unit may touch: a dispatch out of // its configuration, or a step of a do behavior of it. func machineStanding(e *StateExecutor) lower.Footprint { @@ -108,6 +82,14 @@ func dispatchFootprint(e *StateExecutor) lower.Footprint { } } } + return withDrop(e, fp) +} + +// withDrop adds to fp the drop a dispatch of a machine run for an object may make. +func withDrop(e *StateExecutor, fp lower.Footprint) lower.Footprint { + if e.self != nil { + fp.Accepts = append(slices.Clip(fp.Accepts), lower.Channel{Drops: true}) + } return fp } @@ -118,7 +100,7 @@ func triggerChannel(trans *lower.Transition) (lower.Channel, bool) { case *ast.AcceptEvent: channel := lower.Channel{Port: trans.Via} if typed := ast.AsQualifiedName(t.SignalType); typed != nil { - channel.Signal = lower.FeaturePath(typed) + channel.Signal, channel.Type, channel.Scope = lower.FeaturePath(typed), typed, trans.Scope } return channel, true case *ast.CallEvent: @@ -145,85 +127,6 @@ func doStepFootprint(e *StateExecutor, state ast.Node) lower.Footprint { return lower.Footprint{} } -// machineFuture is the footprint of every move the machine may make from any -// configuration: its transitions' and its behaviors', with the messages any -// trigger of it takes; memoized by graph. -func (c *checker) machineFuture(e *StateExecutor) lower.Footprint { - if fp, ok := c.machineFutures[e.graph]; ok { - return fp - } - var future lower.Footprint - for trans, fp := range e.graph.TransitionFootprints() { - future = unionFootprints(future, fp) - if channel, takes := triggerChannel(trans); takes { - future.Accepts = append(future.Accepts, channel) - } - } - for _, fp := range e.graph.BehaviorFootprints() { - future = unionFootprints(future, fp) - } - c.machineFutures[e.graph] = future - return future -} - -// tokenFuture is what the token may still touch: every node reachable from its -// own, the one it stands at included, and from the nodes its frames stand at. -func (c *checker) tokenFuture(exec *ActionExecutor, t Token) lower.Footprint { - if exec.dynamics != nil { - return dynamicsFootprint() - } - future := c.reach(tokenGraphOf(exec, t), t.Location) - for frame := t.frame; frame != nil && frame.node != nil; frame = frame.parent { - flow := frame.flow - if flow == nil && frame.parent != nil { - flow = frame.parent.graph - } - if flow == nil { - flow = exec.graph - } - future = unionFootprints(future, c.reach(flow, frame.node)) - } - return future -} - -func tokenGraphOf(exec *ActionExecutor, t Token) *lower.ActionGraph { - if t.frame != nil && t.frame.graph != nil { - return t.frame.graph - } - return exec.graph -} - -// reach is the union of the footprints of every node reachable from node in -// graph over its successions, the flows those nodes own included; memoized. -func (c *checker) reach(graph *lower.ActionGraph, node ast.Node) lower.Footprint { - key := futureKey{graph: graph, node: node} - if fp, ok := c.futures[key]; ok { - return fp - } - var future lower.Footprint - seen := make(map[ast.Node]bool) - work := []ast.Node{node} - for len(work) > 0 { - n := work[len(work)-1] - work = work[:len(work)-1] - if seen[n] { - continue - } - seen[n] = true - future = unionFootprints(future, graph.Footprints()[n]) - if sub, owns := graph.Subflows[n]; owns && sub != nil && sub.Graph != nil { - for _, start := range sub.Graph.Starts() { - future = unionFootprints(future, c.reach(sub.Graph, start)) - } - } - for _, edge := range graph.Edges[n] { - work = append(work, edge.Target) - } - } - c.futures[key] = future - return future -} - func unionFootprints(f, g lower.Footprint) lower.Footprint { return lower.Footprint{ Reads: append(slices.Clone(f.Reads), g.Reads...), @@ -238,8 +141,13 @@ func unionFootprints(f, g lower.Footprint) lower.Footprint { // dependent reports whether the two moves may not commute: the moves of one // unit never do, and otherwise their footprints decide. -func dependent(a, b searchMove) bool { - return a.unit() == b.unit() || a.footprint.Dependent(b.footprint) +func (c *checker) dependent(a, b searchMove) bool { + return a.unit() == b.unit() || a.footprint.DependentBy(b.footprint, c.meet(a.Owner, b.Owner)) +} + +// meet is which message operations of the two executors may not commute. +func (c *checker) meet(a, b clockWaiter) lower.ChannelsMeet { + return c.ctx.channelsMeet(executorSelf(a), executorSelf(b)) } // persistent selects the moves to explore from a state, less the moves asleep; @@ -309,7 +217,7 @@ func newPersistentClosure(c *checker, all []searchMove) *persistentClosure { for _, t := range e.tokens { u := tokenKey{owner: exec, id: t.ID} p.units = append(p.units, u) - p.standing[u] = c.standing(e, t) + p.standing[u] = standing(e, t) p.future[u] = c.tokenFuture(e, t) } case *StateExecutor: @@ -345,7 +253,7 @@ func (p *persistentClosure) include(u tokenKey) { } standing := p.standing[u] for _, other := range p.units { - if !p.in[other] && p.future[other].Dependent(standing) { + if !p.in[other] && p.future[other].DependentBy(standing, p.c.meet(other.owner, u.owner)) { p.include(other) } } @@ -356,7 +264,7 @@ func (p *persistentClosure) include(u tokenKey) { func (p *persistentClosure) futureDependsOnSet(u tokenKey) bool { future := p.future[u] for _, m := range p.all { - if p.in[m.unit()] && future.Dependent(m.footprint) { + if p.in[m.unit()] && future.DependentBy(m.footprint, p.c.meet(u.owner, m.Owner)) { return true } } @@ -371,12 +279,12 @@ func (c *checker) childSleep(f *checkFrame, m searchMove) []searchMove { } var sleep []searchMove for _, s := range f.sleep { - if !dependent(s, m) { + if !c.dependent(s, m) { sleep = append(sleep, s) } } for _, s := range f.moves[:f.next-1] { - if !dependent(s, m) { + if !c.dependent(s, m) { sleep = append(sleep, s) } } diff --git a/internal/exec/runtime/check_reduce_state_test.go b/internal/exec/runtime/check_reduce_state_test.go index 0124a4a747..6e255f1803 100644 --- a/internal/exec/runtime/check_reduce_state_test.go +++ b/internal/exec/runtime/check_reduce_state_test.go @@ -37,12 +37,11 @@ func startCheckedInvocation(t *testing.T, m *exploreModel, actions, states []str } t.Cleanup(run.inv.Release) c := &checker{ - ctx: ctx, - inv: run.inv, - run: run, - opts: reduced(), - futures: make(map[futureKey]lower.Footprint), - machineFutures: make(map[*lower.StateGraph]lower.Footprint), + ctx: ctx, + inv: run.inv, + run: run, + opts: reduced(), + futureFootprints: newFutureFootprints(ctx), } return &checkedInvocation{run: run, c: c} } diff --git a/internal/exec/runtime/check_run.go b/internal/exec/runtime/check_run.go index 6577502b60..e5bb33b650 100644 --- a/internal/exec/runtime/check_run.go +++ b/internal/exec/runtime/check_run.go @@ -7,10 +7,8 @@ import ( ) // An invocation under check or replay moves one executor one unit at a time. The -// due order is drawn as the clock draws it when it runs what is due: among the -// executors with a move, the one drawn holds the turn until it has no move left -// at the instant, then the order is drawn again. A turn only one executor could -// take is held by none, so a state spells the same however it was reached. +// due order is drawn before every move among the executors with one, so the moves +// of executors due at one instant interleave as the library leaves them free to. // Between moves the run settles: actions park their tokens, and the clock moves // to the earliest wait within the horizon once nothing is left at the instant. @@ -20,8 +18,8 @@ type invocationRun struct { ctx *Context inv *Invocation state *runState - // turn is the executor the due order drew, whose moves alone are enabled while - // it has one and another executor has one too. + // turn is the executor holding the turn: its last move left it a next one no + // other executor's move at the instant may depend on, so its moves alone are enabled. turn checkedExecutor } @@ -84,13 +82,10 @@ func owners(moves []enabledMove) []checkedExecutor { return execs } -// drawOwner resolves which of the executors with a move takes the turn: the only -// one where there is one, else the policy's pick, noted as a due-order choice. +// drawOwner resolves which of the executors with a move makes the next one: the +// only one where there is one, else the policy's pick, noted as a due-order choice. func (r *invocationRun) drawOwner(execs []checkedExecutor) (int, error) { if len(execs) < 2 { - if len(execs) == 1 { - r.turn = execs[0] - } return 0, nil } choice := ChoicePoint{ @@ -105,7 +100,6 @@ func (r *invocationRun) drawOwner(execs []checkedExecutor) (int, error) { } choice.Taken = pick r.ctx.noteChoice(choice) - r.turn = execs[pick] return pick, nil } @@ -201,7 +195,7 @@ func (r *invocationRun) waitsPastHorizon(exec checkedExecutor) bool { } // makeMove makes the move under the `check` policy as one atomic unit: the owner -// drawn as the due order among the executors with a move where no turn is held, +// drawn as the due order among the executors with a move, // the token and picks scripted. It reports the choice points the move drew past its picks. func (r *invocationRun) makeMove(m enabledMove) ([]ChoicePoint, error) { defer r.enter()() @@ -221,13 +215,21 @@ func (r *invocationRun) makeMove(m enabledMove) ([]ChoicePoint, error) { return check.drawn, err } -// step moves one executor one unit: the turn holder, drawn by the policy among -// those with a move where none holds it. +// step moves one executor one unit, drawn by the policy among those with a move, +// and leaves it the turn where the clock would: while no rival contends its next move. func (r *invocationRun) step(execs []checkedExecutor) error { defer r.enter()() pick, err := r.drawOwner(execs) if err != nil { return err } - return execs[pick].stepOne() + owner := execs[pick] + r.turn = nil + if err := owner.stepOne(); err != nil { + return err + } + if owner.dueWork() && !r.ctx.contended(owner) { + r.turn = owner + } + return nil } diff --git a/internal/exec/runtime/context.go b/internal/exec/runtime/context.go index 91920fa77f..9a5ec9d484 100644 --- a/internal/exec/runtime/context.go +++ b/internal/exec/runtime/context.go @@ -271,6 +271,9 @@ type Context struct { // clockRun the run an advance of it draws its due-order choices from. clock Clock clockRun executorRun + // futures memoizes what each executor on the clock may still touch, for + // telling the turns whose moves interleave. + futures *futureFootprints // work counts the changes that can leave an attached behavior holding work; // quiescent is the memo a full scan leaves when it finds them all idle. work uint64 diff --git a/internal/exec/runtime/future_footprint.go b/internal/exec/runtime/future_footprint.go new file mode 100644 index 0000000000..9ac68f7206 --- /dev/null +++ b/internal/exec/runtime/future_footprint.go @@ -0,0 +1,356 @@ +package runtime + +import ( + "github.com/Open-MBEE/OpenSysML/internal/ir/lower" + "github.com/Open-MBEE/OpenSysML/internal/semantic/semantics" + "github.com/Open-MBEE/OpenSysML/internal/semantic/symbols" + "github.com/Open-MBEE/OpenSysML/internal/syntax/ast" +) + +// futureKey identifies what a token may still do at this instant: its node in its flow. +type futureKey struct { + graph *lower.ActionGraph + node ast.Node +} + +// futureFootprints memoizes what executors may still touch at the clock's instant: +// a token's by its node in its flow, a delay by whether it ends the instant; both +// are dropped once the clock moves. A machine's whole graph is kept by graph. +type futureFootprints struct { + ctx *Context + now float64 + nodes map[futureKey]lower.Footprint + ends map[*ast.TimeEvent]bool + machines map[*lower.StateGraph]lower.Footprint +} + +// newFutureFootprints reads the clock of ctx, which bind replaces. +func newFutureFootprints(ctx *Context) *futureFootprints { + return &futureFootprints{ctx: ctx, machines: make(map[*lower.StateGraph]lower.Footprint)} +} + +// bind reads the clock of ctx from now on. +func (f *futureFootprints) bind(ctx *Context) { + f.ctx, f.nodes = ctx, nil +} + +// at drops what was memoized for an instant the clock has left. +func (f *futureFootprints) at() { + if f.nodes != nil && f.now == f.ctx.clock.now { + return + } + f.now = f.ctx.clock.now + f.nodes = make(map[futureKey]lower.Footprint) + f.ends = make(map[*ast.TimeEvent]bool) +} + +// endsInstant reports whether waiting on trigger provably outlasts this instant: +// a literal delay whose wait comes due after now. Anything else may not. +func (f *futureFootprints) endsInstant(trigger ast.Node, scope *symbols.Scope) bool { + t, literal := lower.InstantDelay(trigger) + if !literal { + return false + } + if ends, ok := f.ends[t]; ok { + return ends + } + ends := false + if magnitude, ok := f.ctx.literalDelay(scope, t.Duration); ok { + due, err := f.ctx.dueInstant(t, Value{Kind: ValConst, Const: semantics.Value{Kind: semantics.ValReal, Real: magnitude}}, triggerDescription(t)) + ends = err == nil && due > f.ctx.clock.now + } + f.ends[t] = ends + return ends +} + +// executorFuture is what the executor may still touch at this instant: every +// token's future for an action, the machine's for a state machine, everything +// for any other. +func (f *futureFootprints) executorFuture(w clockWaiter) lower.Footprint { + f.at() + switch exec := w.(type) { + case *ActionExecutor: + return f.actionFuture(exec) + case *StateExecutor: + return f.machineFuture(exec) + } + return lower.Footprint{Dynamic: true} +} + +func (f *futureFootprints) actionFuture(exec *ActionExecutor) lower.Footprint { + var future lower.Footprint + for _, t := range exec.tokens { + future = unionFootprints(future, f.tokenFuture(exec, t)) + } + return future +} + +// tokenFuture is what the token may still touch at this instant: the nodes it can +// reach from its own over successions before a wait ending the instant, the one +// it stands at included, and those reachable from the nodes its frames stand at. +func (f *futureFootprints) tokenFuture(exec *ActionExecutor, t Token) lower.Footprint { + f.at() + if exec.dynamics != nil { + return dynamicsFootprint() + } + graph := tokenGraphOf(exec, t) + var future lower.Footprint + if t.Wait != nil && t.Wait.Timed { + if t.Wait.Due > f.ctx.clock.now { + return standing(exec, t) + } + future = graph.Footprints()[t.Location] + for _, edge := range graph.Edges[t.Location] { + future = unionFootprints(future, f.reach(graph, edge.Target)) + } + } else { + future = f.reach(graph, t.Location) + } + for frame := t.frame; frame != nil && frame.node != nil; frame = frame.parent { + flow := frame.flow + if flow == nil && frame.parent != nil { + flow = frame.parent.graph + } + if flow == nil { + flow = exec.graph + } + future = unionFootprints(future, f.reach(flow, frame.node)) + } + return future +} + +func tokenGraphOf(exec *ActionExecutor, t Token) *lower.ActionGraph { + if t.frame != nil && t.frame.graph != nil { + return t.frame.graph + } + return exec.graph +} + +// reach is the union of the footprints of every node reachable from node in +// graph over its successions, the flows those nodes own included, going on past +// no accept whose delay ends the instant; memoized for the instant. +func (f *futureFootprints) reach(graph *lower.ActionGraph, node ast.Node) lower.Footprint { + key := futureKey{graph: graph, node: node} + if fp, ok := f.nodes[key]; ok { + return fp + } + var future lower.Footprint + seen := make(map[ast.Node]bool) + work := []ast.Node{node} + for len(work) > 0 { + n := work[len(work)-1] + work = work[:len(work)-1] + if seen[n] { + continue + } + seen[n] = true + future = unionFootprints(future, graph.Footprints()[n]) + if sub, owns := graph.Subflows[n]; owns { + if sub == nil || sub.Graph == nil { + future.Dynamic = true + } else { + for _, start := range sub.Graph.Starts() { + future = unionFootprints(future, f.reach(sub.Graph, start)) + } + } + } + if f.waitEndsInstant(graph, n) { + continue + } + for _, edge := range graph.Edges[n] { + work = append(work, edge.Target) + } + } + f.nodes[key] = future + return future +} + +// waitEndsInstant reports whether a token reaching n waits there past this instant. +func (f *futureFootprints) waitEndsInstant(graph *lower.ActionGraph, n ast.Node) bool { + accept, ok := graph.Accepts[n] + if !ok { + return false + } + scope := accept.Scope + if scope == nil { + scope = graph.Scope + } + return f.endsInstant(accept.Trigger, scope) +} + +// machineFuture is what the machine may still touch at this instant: the +// transitions out of its configuration it may fire, on through the states they +// enter, and its do behaviors from where they stand. A machine not yet started, +// holding an entry or running a call may do anything its graph does. +func (f *futureFootprints) machineFuture(e *StateExecutor) lower.Footprint { + f.at() + if e.activeConfig == nil || len(e.held) > 0 || e.pendingCall != nil { + return withDrop(e, f.wholeMachine(e)) + } + timerDue := false + for _, wait := range e.armedWaits() { + if _, timer := wait.what.(transitionWait); timer && wait.Due <= f.ctx.clock.now { + timerDue = true + } + } + var future lower.Footprint + active := make(map[*ast.StateNode]bool) + var work []*ast.StateNode + for _, leaf := range e.activeStates() { + for _, state := range e.getParentChain(leaf) { + if !active[state] { + active[state] = true + work = append(work, state) + } + } + } + for _, act := range e.doActions { + future = unionFootprints(future, f.doFuture(e, act)) + } + steps := e.graph.TransitionSteps() + seen := make(map[*ast.StateNode]bool) + for len(work) > 0 { + state := work[len(work)-1] + work = work[:len(work)-1] + if seen[state] { + continue + } + seen[state] = true + for _, trans := range e.graph.Transitions[state] { + if !(active[state] && timerDue) && f.endsInstant(trans.Trigger, trans.Scope) { + continue + } + step, ok := steps[trans] + if !ok { + return withDrop(e, f.wholeMachine(e)) + } + future = unionFootprints(future, step.Footprint) + if channel, takes := triggerChannel(trans); takes { + future.Accepts = append(future.Accepts, channel) + } + for _, entered := range step.Enters { + future = unionFootprints(future, f.startedDo(e, entered)) + work = append(work, entered) + } + } + } + return withDrop(e, future) +} + +// doFuture is what a do behavior under way or pending may still do at this +// instant: a flow it runs from where its tokens stand, else the whole of it. +func (f *futureFootprints) doFuture(e *StateExecutor, act *doAction) lower.Footprint { + var future lower.Footprint + if run := act.run; run != nil { + behavior := run.host.behavior + if graph, flow := statedFlow(behavior), run.host.flow; graph != nil && flow != nil && flow.graph == graph && run.body.paused.wait.held == nil { + future = f.actionFuture(flow) + } else { + future = e.graph.BehaviorFootprints()[behavior.Node] + } + } + for _, behavior := range act.pending { + future = unionFootprints(future, f.behaviorFuture(e, behavior)) + } + return future +} + +// startedDo is what the do behaviors entering state starts may do at this instant. +func (f *futureFootprints) startedDo(e *StateExecutor, state *ast.StateNode) lower.Footprint { + var future lower.Footprint + if behaviors := e.graph.Behaviors[state]; behaviors != nil { + for _, behavior := range behaviors.Do { + future = unionFootprints(future, f.behaviorFuture(e, behavior)) + } + } + return future +} + +// behaviorFuture is what starting the behavior may do at this instant: a stated +// flow up to the waits ending it, else the whole behavior. +func (f *futureFootprints) behaviorFuture(e *StateExecutor, behavior lower.StateBehavior) lower.Footprint { + graph := statedFlow(behavior) + if graph == nil { + return e.graph.BehaviorFootprints()[behavior.Node] + } + var future lower.Footprint + if behavior.Owner != nil { + future.Reads = []lower.Place{{Name: behavior.Owner.Name, State: behavior.Owner}} + } + for _, start := range graph.Starts() { + future = unionFootprints(future, f.reach(graph, start)) + } + return future +} + +// statedFlow is the flow a behavior whose body is one block stating a flow runs. +func statedFlow(behavior lower.StateBehavior) *lower.ActionGraph { + if len(behavior.Body) != 1 { + return nil + } + if block, ok := behavior.Body[0].(lower.Block); ok { + return block.Graph + } + return nil +} + +// wholeMachine is the footprint of every move the machine may make from any +// configuration: its transitions' and its behaviors', with the messages any +// trigger of it takes; memoized by graph. +func (f *futureFootprints) wholeMachine(e *StateExecutor) lower.Footprint { + if fp, ok := f.machines[e.graph]; ok { + return fp + } + var future lower.Footprint + for trans, fp := range e.graph.TransitionFootprints() { + future = unionFootprints(future, fp) + if channel, takes := triggerChannel(trans); takes { + future.Accepts = append(future.Accepts, channel) + } + } + for _, fp := range e.graph.BehaviorFootprints() { + future = unionFootprints(future, fp) + } + f.machines[e.graph] = future + return future +} + +// literalDelay is the magnitude, in clock units, of a delay written as a number +// with or without a time unit, read without evaluating it. +func (ctx *Context) literalDelay(scope *symbols.Scope, duration ast.Node) (float64, bool) { + var unit ast.Node + if ix, quantity := duration.(*ast.IndexExpr); quantity && ix.Bracket { + duration, unit = ix.Operand, ix.Index + } + var num semantics.Value + switch lit := duration.(type) { + case *ast.LiteralInteger: + val, ok := semantics.ParseInteger(lit.Value) + if !ok { + return 0, false + } + num = val + case *ast.LiteralReal: + val, err := semantics.ParseReal(lit.Value) + if err != nil { + return 0, false + } + num = semantics.Value{Kind: semantics.ValReal, Real: val} + default: + return 0, false + } + if unit == nil { + return num.AsReal(), true + } + term, err := ctx.model.semantics.UnitTermOfExpr(scope, unit) + if err != nil { + return 0, false + } + product, err := ctx.model.semantics.UnitProductOfExpr(scope, unit) + if err != nil { + return 0, false + } + q := &Quantity{Num: num, Unit: Unit{Text: semantics.UnitExprText(unit), Product: product, Term: term}} + magnitude, err := ctx.durationInClockUnits(q, "delay") + return magnitude, err == nil +} diff --git a/internal/exec/runtime/message_dependence.go b/internal/exec/runtime/message_dependence.go new file mode 100644 index 0000000000..1a34c6aee7 --- /dev/null +++ b/internal/exec/runtime/message_dependence.go @@ -0,0 +1,235 @@ +package runtime + +import ( + "strings" + + "github.com/Open-MBEE/OpenSysML/internal/ir/lower" + "github.com/Open-MBEE/OpenSysML/internal/semantic/symbols" + "github.com/Open-MBEE/OpenSysML/internal/syntax/ast" +) + +// signalConformers is what may carry an accept's type: the declarations +// conforming to it and every name or alias naming one; known is false where the +// model cannot be searched for them. +type signalConformers struct { + decls map[ast.Node]bool + names map[string]bool + known bool +} + +// channelsMeet is which message operations of two executors, run by objects a +// and b, may not commute. Two sends always do; a send and a consumer, or two +// consumers, are apart only where each type resolves and no message carries both. +func (ctx *Context) channelsMeet(a, b *Instance) lower.ChannelsMeet { + return func(x lower.Channel, xSends bool, y lower.Channel, ySends bool) bool { + switch { + case xSends && ySends: + return true + case xSends: + return ctx.sendMeets(x, y) + case ySends: + return ctx.sendMeets(y, x) + } + return ctx.consumersMeet(x, a, y, b) + } +} + +// executorSelf is the object an executor runs for, nil for none. +func executorSelf(w clockWaiter) *Instance { + switch exec := w.(type) { + case *ActionExecutor: + return exec.self + case *StateExecutor: + return exec.self + } + return nil +} + +// sendMeets reports whether a send may give or take a message the consumer +// would see: a dispatch may drop a message sent to its object, never one a port carries. +func (ctx *Context) sendMeets(send, consumer lower.Channel) bool { + if consumer.Drops { + return !send.Via + } + sent, want := ctx.sentSignal(send), ctx.channelType(consumer) + if sent == nil || want == nil { + return true + } + return ctx.signalConforms(sent, want) +} + +// consumersMeet reports whether two consumers may compete for one message. One +// object's consumers always do: a machine yields to, or drops for, its siblings. +func (ctx *Context) consumersMeet(x lower.Channel, a *Instance, y lower.Channel, b *Instance) bool { + if objectID(a) == 0 || objectID(b) == 0 || objectID(a) == objectID(b) { + return true + } + if x.Drops || y.Drops { + other, holder := y, b + if y.Drops { + other, holder = x, a + } + // A dispatch drops only portless messages to its object; another's own port takes none of them. + return other.Port != "" && !ctx.ownPort(other, holder) + } + tx, ty := ctx.channelType(x), ctx.channelType(y) + if tx == nil || ty == nil { + return true + } + if ctx.signalConforms(tx, ty) || ctx.signalConforms(ty, tx) { + return true + } + cx, cy := ctx.conformersOf(tx), ctx.conformersOf(ty) + if !cx.known || !cy.known { + return true + } + for decl := range cx.decls { + if cy.decls[decl] { + return true + } + } + // A message no definition types matches by its name, the last segment written. + nx, ny := withName(cx.names, lastWritten(x.Type)), withName(cy.names, lastWritten(y.Type)) + for name := range nx { + if ny[name] { + return true + } + } + return false +} + +// ownPort reports whether a consumer's port statically names a port feature of +// its own object, so the port's holder is that object. +func (ctx *Context) ownPort(c lower.Channel, self *Instance) bool { + if self == nil || c.Port == "" || strings.Contains(c.Port, ".") { + return false + } + sym, ok := ctx.portSymbol(c.Scope, c.Port) + if !ok || sym == nil || sym.Kind != symbols.SymbolPortUsage { + return false + } + if usage, isUsage := sym.Decl.(*ast.Usage); !isUsage || usage.IsReference { + return false + } + for _, of := range ctx.FeaturesOfObject(self) { + if of.Name == c.Port && isPortFeature(of.Feature) && of.Feature.Symbol == sym { + return true + } + } + return false +} + +// withName is names with one more. +func withName(names map[string]bool, name string) map[string]bool { + out := make(map[string]bool, len(names)+1) + for n := range names { + out[n] = true + } + out[name] = true + return out +} + +// lastWritten is the last segment of a type reference as written. +func lastWritten(qn *ast.QualifiedName) string { + if qn == nil || len(qn.Parts) == 0 { + return "" + } + return qn.Parts[len(qn.Parts)-1].Text +} + +// channelType is the definition a consumer's type reference denotes, nil where +// it names none or matching would fall back to names. +func (ctx *Context) channelType(c lower.Channel) *symbols.Symbol { + if c.Drops || c.Type == nil || len(c.Type.Parts) == 0 || c.Scope == nil || ctx.model.semantics == nil { + return nil + } + return ctx.triggerType(c.Scope, c.Type) +} + +// sentSignal is the signal a send's message statically carries, as buildMessage +// types it: a definition named, or the type a constructor names; nil otherwise. +func (ctx *Context) sentSignal(c lower.Channel) *symbols.Symbol { + if c.Scope == nil || ctx.model.resolver == nil || ctx.model.semantics == nil { + return nil + } + if qn := ast.AsQualifiedName(c.Message); qn != nil { + sym, ok := ctx.model.resolver.ResolveQualified(c.Scope, qn) + if ok && isDefinitionSymbol(sym) { + return sym + } + return nil + } + if constructor, ok := c.Message.(*ast.ConstructorExpr); ok && constructor.Type != nil { + sym, ok := ctx.model.resolver.ResolveQualified(c.Scope, constructor.Type) + if !ok || sym == nil { + return nil + } + switch sym.Decl.(type) { + case *ast.Definition, *ast.Usage: + return sym + } + } + return nil +} + +// conformersOf searches the workspace for what conforms to want; a type the +// library declares, which the library may specialize, is not searched. +func (ctx *Context) conformersOf(want *symbols.Symbol) *signalConformers { + if ctx.model.conformers == nil { + ctx.model.conformers = make(map[ast.Node]*signalConformers) + } + if found, ok := ctx.model.conformers[want.Decl]; ok { + return found + } + found := &signalConformers{decls: make(map[ast.Node]bool), names: make(map[string]bool)} + ctx.model.conformers[want.Decl] = found + idx := ctx.model.resolver.Index() + if want.Decl == nil || want.DocName == "" || idx.IsLibraryDocument(want.DocName) { + return found + } + found.known = true + seen := make(map[*symbols.Scope]bool) + var walk func(scope *symbols.Scope) + visit := func(sym *symbols.Symbol) bool { + target := sym + if sym.Kind == symbols.SymbolAlias { + if resolved, ok := ctx.model.resolver.ResolveAliasTarget(sym); ok && resolved != nil { + target = resolved + } else { + return true + } + } + if ctx.signalConforms(target, want) { + if target.Decl == nil { + found.known = false + } + found.decls[target.Decl] = true + found.names[sym.Name] = true + if sym.ShortName != "" { + found.names[sym.ShortName] = true + } + } + if sym.Scope != nil { + walk(sym.Scope) + } + return true + } + walk = func(scope *symbols.Scope) { + if scope == nil || seen[scope] { + return + } + seen[scope] = true + scope.ForEachMember(visit) + scope.ForEachAnonymousMember(visit) + for _, child := range scope.Children() { + walk(child) + } + } + for _, doc := range idx.WorkspaceDocuments() { + walk(idx.DocumentRoot(doc)) + } + for _, scope := range ctx.model.scopes { + walk(scope) + } + return found +} diff --git a/internal/exec/runtime/model.go b/internal/exec/runtime/model.go index 9db942e250..4e407b0bf6 100644 --- a/internal/exec/runtime/model.go +++ b/internal/exec/runtime/model.go @@ -146,6 +146,8 @@ type Model struct { // machine judges every message in flight against every trigger it holds each step. triggerTypes map[triggerTypeKey]*symbols.Symbol signalMatches map[signalMatchKey]bool + // conformers memoizes, by an accept type's declaration, what may carry it. + conformers map[ast.Node]*signalConformers // sources holds the text of the files the model was read from, by name, so an // error about a declaration can say where it was written. A file no caller @@ -277,6 +279,7 @@ func (m *Model) RegisterScope(scope *symbols.Scope) { m.scopes = append(m.scopes, scope) m.declared = nil m.census = nil + m.conformers = nil } // declaredSymbol is the symbol a registered scope tree declares for the diff --git a/internal/exec/runtime/scheduler.go b/internal/exec/runtime/scheduler.go index b409204cd2..e1271c7513 100644 --- a/internal/exec/runtime/scheduler.go +++ b/internal/exec/runtime/scheduler.go @@ -364,6 +364,13 @@ func (s *scheduler) oneMove() bool { return (s.policy.kind == scheduleExplore && s.explore != nil) || s.replay != nil || s.checking() } +// interleavesTurns reports whether the due order is drawn again after each move of +// an executor whose future depends on another's — under explore, a seed and a +// replay — rather than once per turn the executor runs to quiescence. +func (s *scheduler) interleavesTurns() bool { + return (s.policy.kind == scheduleExplore && s.explore != nil) || s.policy.kind == scheduleSeeded || s.replay != nil +} + // checking reports whether the run makes the moves the model checker selects. func (s *scheduler) checking() bool { return s.policy.kind == scheduleCheck && s.check != nil diff --git a/internal/exec/runtime/state_executor.go b/internal/exec/runtime/state_executor.go index 30c28efb84..09d059ee28 100644 --- a/internal/exec/runtime/state_executor.go +++ b/internal/exec/runtime/state_executor.go @@ -3457,10 +3457,10 @@ func (e *StateExecutor) RunToQuiescence() error { // once nothing is due it advances to the earliest wait, running whatever is due there. func (e *StateExecutor) run(atCurrentTime bool) error { var progress dueProgress - return e.runCounting(atCurrentTime, &progress) + return e.runCounting(atCurrentTime, false, &progress) } -func (e *StateExecutor) runCounting(atCurrentTime bool, progress *dueProgress) (err error) { +func (e *StateExecutor) runCounting(atCurrentTime, single bool, progress *dueProgress) (err error) { defer e.ctx.beginExecutorRun(&e.driven)() defer e.completedWhole(&err) wasRunning := e.inRun @@ -3483,6 +3483,14 @@ func (e *StateExecutor) runCounting(atCurrentTime bool, progress *dueProgress) ( if e.callReleased() { return nil } + if single { + return nil + } + if !atCurrentTime { + if err := e.ctx.yieldTurn(e, progress); err != nil { + return err + } + } continue } if atCurrentTime { @@ -3586,8 +3594,17 @@ func (e *StateExecutor) drivable() bool { // runDue runs the machine to quiescence at the current instant. func (e *StateExecutor) runDue(progress *dueProgress) (bool, error) { + return e.runDueUnits(progress, false) +} + +// runMove is runDue stopping after one unit of the run. +func (e *StateExecutor) runMove(progress *dueProgress) (bool, error) { + return e.runDueUnits(progress, true) +} + +func (e *StateExecutor) runDueUnits(progress *dueProgress, single bool) (bool, error) { before := *progress - err := e.runCounting(true, progress) + err := e.runCounting(true, single, progress) return progress.events > before.events || progress.doSteps > before.doSteps, err } diff --git a/internal/exec/runtime/testdata/check/reduction_expected.txt b/internal/exec/runtime/testdata/check/reduction_expected.txt index e73cef18c1..2dcfbf303d 100644 --- a/internal/exec/runtime/testdata/check/reduction_expected.txt +++ b/internal/exec/runtime/testdata/check/reduction_expected.txt @@ -14,10 +14,10 @@ 49 51 58 79 por_streaming_flow 19 21 19 22 por_constructor 13 13 30 38 por_state_independent -17 18 17 18 por_state_effect_write -17 18 17 18 por_state_guard_read -21 22 21 22 por_state_do_write -9 9 9 9 por_state_send_accept -72 72 72 72 por_state_join_exit -26 24 26 24 por_state_join_guard +15 16 17 20 por_state_effect_write +15 16 17 20 por_state_guard_read +27 29 32 38 por_state_do_write +13 13 13 13 por_state_send_accept +96 108 102 120 por_state_join_exit +34 38 36 42 por_state_join_guard 7 6 15 18 por_two_machines diff --git a/internal/frontend/repl/checker_state_test.go b/internal/frontend/repl/checker_state_test.go index 193f93fa79..37a2dc2aff 100644 --- a/internal/frontend/repl/checker_state_test.go +++ b/internal/frontend/repl/checker_state_test.go @@ -32,7 +32,7 @@ func TestEngineCheckSearchesStateMachines(t *testing.T) { if len(verdicts) != 1 { t.Fatalf("verdicts = %+v, want one for the invocation", verdicts) } - wantVerdict(t, verdicts[0], VerdictFails, "✗ Behaviors Shared::Lamp::peek, Shared::Lamp::glow: divergent up to t=3.0 (10 states, 9 moves, depth 5)", + wantVerdict(t, verdicts[0], VerdictFails, "✗ Behaviors Shared::Lamp::peek, Shared::Lamp::glow: divergent up to t=3.0 (9 states, 8 moves, depth 5)", "divergent: Shared::Lamp::peek.saw ends as false or true", `Shared::Lamp::glow finalState = "on"; Shared::Lamp::glow visits = "off, on"; Shared::Lamp::peek.saw = false`, `Shared::Lamp::glow finalState = "on"; Shared::Lamp::glow visits = "off, on"; Shared::Lamp::peek.saw = true`) @@ -82,7 +82,7 @@ func TestReplayStepsBehaviorsOnOneClock(t *testing.T) { run(t, s, "%instantiate Shared::Lamp") wants(t, run(t, s, "%action Shared::Lamp::peek Shared::Lamp"), "Started action executor") wants(t, run(t, s, "%state Shared::Lamp::glow Shared::Lamp"), "Current state: off") - wants(t, run(t, s, "%advance 3"), "Advanced to 3.0", "Current state: on", "Action completed", saw, "1 choice point") + wants(t, run(t, s, "%advance 3"), "Advanced to 3.0", "Current state: on", "Action completed", saw, "2 choice points") } } diff --git a/internal/frontend/repl/explore_test.go b/internal/frontend/repl/explore_test.go index 2c2b6c19f4..b85c2b60a7 100644 --- a/internal/frontend/repl/explore_test.go +++ b/internal/frontend/repl/explore_test.go @@ -459,7 +459,7 @@ func TestRunForExploresAnActionOnANestedObject(t *testing.T) { if v.Status != VerdictHolds { t.Fatalf("status = %v, want holds:\n%s", v.Status, strings.Join(v.Lines, "\n")) } - wantsInOrder(t, strings.Join(v.Lines, "\n"), "✓ explored Comms::Craft::ack: 2 outcomes", "seen = 1", "seen = 2", "complete (") + wantsInOrder(t, strings.Join(v.Lines, "\n"), "✓ explored Comms::Craft::ack: 3 outcomes", "seen = 1", "seen = 1", "seen = 2", "complete (") // The craft instantiated on its own is never pinged, so it sends nothing. v = s.RunAction("Comms::Craft::ack", "Comms::Pair::craft") @@ -501,7 +501,7 @@ func TestRunForExploresSiblingsOnOneRoot(t *testing.T) { wantsInOrder(t, out, "✓ explored Comms::Ground::listen Comms::pair.ground, Comms::Craft::modes Comms::pair.craft: 2 outcomes", "Comms::Craft::modes Comms::pair.craft.emitted = 4", "Comms::Ground::listen Comms::pair.ground.received = 1", "Comms::Craft::modes Comms::pair.craft.emitted = 4", "Comms::Ground::listen Comms::pair.ground.received = 2", - "complete (4 runs)") + "complete (33 runs)") if len(verdicts[0].Outcomes) != 2 { t.Errorf("outcomes = %+v, want two", verdicts[0].Outcomes) } @@ -835,7 +835,7 @@ func TestRunForExploresEveryDueOrder(t *testing.T) { `Shared::Lamp::glow finalState = "on"; Shared::Lamp::glow visits = "off, on"; Shared::Lamp::peek.saw = false; this.isSolid = true; this.lit = true`, `Shared::Lamp::glow finalState = "on"; Shared::Lamp::glow visits = "off, on"; Shared::Lamp::peek.saw = true; this.isSolid = true; this.lit = true`, "possible", - "complete (2 runs)") + "complete (3 runs)") // One behavior explored with a duration is its own outcome, as RunStateMachine tables it. verdicts = s.RunFor(nil, []Behavior{glow}, 3) diff --git a/internal/ir/lower/footprint.go b/internal/ir/lower/footprint.go index 461feb2e9b..a1e4edd89a 100644 --- a/internal/ir/lower/footprint.go +++ b/internal/ir/lower/footprint.go @@ -56,13 +56,20 @@ func (p Place) String() string { } // Channel is one message a move sends or waits for: the signal type as written -// ("" for any) and the port it travels through ("" for none). +// ("" for any) and the port it travels through ("" for none). Type is the accept's +// type reference and Message the send's message, each resolving in Scope; Via marks +// a send routed by connections, Drops a machine's dispatch, which may discard a +// message sent to its object. type Channel struct { - Signal string - Port string + Signal string + Port string + Type *ast.QualifiedName + Message ast.Node + Scope *symbols.Scope + Via bool + Drops bool } -// String renders the channel as `Signal via Port`, dropping what is absent. func (c Channel) String() string { text := c.Signal if text == "" { @@ -92,13 +99,23 @@ type Footprint struct { // two sends ordering it), both queuing a completion, convergence on one join or // merge, or a dynamic target. func (f Footprint) Dependent(g Footprint) bool { + return f.DependentBy(g, nil) +} + +// ChannelsMeet reports whether a message operation of one move may not commute +// with one of another: each channel with whether it sends. +type ChannelsMeet func(a Channel, aSends bool, b Channel, bSends bool) bool + +// DependentBy is Dependent with meet deciding which message operations meet; +// a nil meet has every two meet. +func (f Footprint) DependentBy(g Footprint, meet ChannelsMeet) bool { if f.Dynamic || g.Dynamic { return true } if placesMeet(f.Writes, g.Reads) || placesMeet(f.Writes, g.Writes) || placesMeet(g.Writes, f.Reads) { return true } - if f.messages() && g.messages() { + if f.messagesMeet(g, meet) { return true } if f.Completion && g.Completion { @@ -114,6 +131,30 @@ func (f Footprint) Dependent(g Footprint) bool { return false } +func (f Footprint) messagesMeet(g Footprint, meet ChannelsMeet) bool { + if !f.messages() || !g.messages() { + return false + } + if meet == nil { + return true + } + return channelsMeet(f.Sends, true, g.Sends, true, meet) || + channelsMeet(f.Sends, true, g.Accepts, false, meet) || + channelsMeet(f.Accepts, false, g.Sends, true, meet) || + channelsMeet(f.Accepts, false, g.Accepts, false, meet) +} + +func channelsMeet(as []Channel, aSends bool, bs []Channel, bSends bool, meet ChannelsMeet) bool { + for _, a := range as { + for _, b := range bs { + if meet(a, aSends, b, bSends) { + return true + } + } + } + return false +} + // messages reports whether the move sends or accepts a message. func (f Footprint) messages() bool { return len(f.Sends) > 0 || len(f.Accepts) > 0 @@ -465,7 +506,7 @@ func (b *footprintBuilder) statement(stmt Statement) { // A `via` send is routed by connections at run time. b.footprint.Dynamic = true } - b.footprint.Sends = append(b.footprint.Sends, Channel{Port: viaPortOf(s)}) + b.footprint.Sends = append(b.footprint.Sends, Channel{Port: viaPortOf(s), Message: s.Message, Scope: s.Scope, Via: s.IsVia}) case Declare: b.reads(s.Scope, s.Value) b.write(Place{Name: s.Name}) @@ -512,16 +553,51 @@ func (b *footprintBuilder) block(block Block) { b.statements(block.Statements) return } - for _, node := range block.Graph.Nodes { - nested := block.Graph.Footprints()[node] - if !block.Graph.StatementRuns[node] { - // A nested action or a perform inside a block runs a behavior of its own. - nested.Dynamic = true + b.merge(FlowFootprint(block.Graph)) +} + +// FlowFootprint is what running the flow may touch: every node's footprint and +// those of the flows its nodes own; a node performing an action is dynamic. +func FlowFootprint(graph *ActionGraph) Footprint { + var b footprintBuilder + b.flow(graph, make(map[*ActionGraph]bool)) + return b.footprint +} + +func (b *footprintBuilder) flow(graph *ActionGraph, seen map[*ActionGraph]bool) { + if graph == nil || seen[graph] { + return + } + seen[graph] = true + for _, node := range graph.Nodes { + b.merge(graph.Footprints()[node]) + if sub := graph.Subflows[node]; sub != nil { + if sub.Graph == nil { + b.footprint.Dynamic = true + } + b.flow(sub.Graph, seen) } - b.merge(nested) } } +// InstantDelay is the time event of an accept or transition trigger that may end +// the instant: a relative delay written as a number, with or without a unit. +func InstantDelay(trigger ast.Node) (*ast.TimeEvent, bool) { + t, ok := trigger.(*ast.TimeEvent) + if !ok || t.Absolute { + return nil, false + } + duration := t.Duration + if ix, quantity := duration.(*ast.IndexExpr); quantity && ix.Bracket { + duration = ix.Operand + } + switch duration.(type) { + case *ast.LiteralInteger, *ast.LiteralReal: + return t, true + } + return nil, false +} + func (b *footprintBuilder) merge(other Footprint) { for _, p := range other.Reads { b.read(p) @@ -750,7 +826,7 @@ func (b *footprintBuilder) accept() { if !ok { return } - channel := Channel{Port: accept.ViaPort} + channel := Channel{Port: accept.ViaPort, Type: accept.SignalType, Scope: accept.Scope} if accept.SignalType != nil { channel.Signal = accept.SignalType.Text() } diff --git a/internal/ir/lower/state_footprint.go b/internal/ir/lower/state_footprint.go index fd36248ad7..a639d548c4 100644 --- a/internal/ir/lower/state_footprint.go +++ b/internal/ir/lower/state_footprint.go @@ -74,12 +74,39 @@ func (g *StateGraph) activity(state *ast.StateNode) Place { // transitionFootprint projects the footprint of a transition out of a state. func transitionFootprint(graph *StateGraph, trans *Transition) Footprint { - b := &stateFootprintBuilder{footprintBuilder: &footprintBuilder{}, graph: graph, crossed: make(map[*ast.PseudostateNode]bool)} + return transitionBuilder(graph, trans, false).footprint +} + +// transitionBuilder projects a transition out of a state, without the do +// behaviors of the states it enters when withoutDo is set. +func transitionBuilder(graph *StateGraph, trans *Transition, withoutDo bool) *stateFootprintBuilder { + b := &stateFootprintBuilder{footprintBuilder: &footprintBuilder{}, graph: graph, crossed: make(map[*ast.PseudostateNode]bool), withoutDo: withoutDo} source := trans.Source.(*ast.StateNode) b.read(graph.activity(source)) b.trigger(trans) b.segment(source, trans) - return b.footprint + return b +} + +// TransitionStep is what firing a transition may do short of the do behaviors it +// starts: its Footprint, and every state it may enter, whose do behaviors start. +type TransitionStep struct { + Footprint Footprint + Enters []*ast.StateNode +} + +// TransitionSteps is transition out of a state → its TransitionStep, computed on +// first use as TransitionFootprints is. +func (g *StateGraph) TransitionSteps() map[*Transition]TransitionStep { + g.lowerFootprints() + g.stepsOnce.Do(func() { + g.transitionSteps = make(map[*Transition]TransitionStep) + for trans := range g.transitionFootprints { + b := transitionBuilder(g, trans, true) + g.transitionSteps[trans] = TransitionStep{Footprint: b.footprint, Enters: b.entered} + } + }) + return g.transitionSteps } type stateFootprintBuilder struct { @@ -87,6 +114,9 @@ type stateFootprintBuilder struct { graph *StateGraph // crossed are the pseudostates followed, so a cycle through one ends. crossed map[*ast.PseudostateNode]bool + // withoutDo leaves out the do behaviors of the states entered, listed in entered. + withoutDo bool + entered []*ast.StateNode } // trigger adds what the trigger reads: a change condition or a time duration. An @@ -263,8 +293,15 @@ func (b *stateFootprintBuilder) exits(state *ast.StateNode) { // entry, or the region it completes. func (b *stateFootprintBuilder) enters(state *ast.StateNode) { b.write(b.graph.activity(state)) + if !slices.Contains(b.entered, state) { + b.entered = append(b.entered, state) + } if behaviors := b.graph.Behaviors[state]; behaviors != nil { - for _, behavior := range slices.Concat(behaviors.Entry, behaviors.Do) { + started := behaviors.Do + if b.withoutDo { + started = nil + } + for _, behavior := range slices.Concat(behaviors.Entry, started) { b.merge(b.graph.behaviorFootprints[behavior.Node]) } } diff --git a/internal/ir/lower/state_graph.go b/internal/ir/lower/state_graph.go index 843dd5a7f1..1dd780750d 100644 --- a/internal/ir/lower/state_graph.go +++ b/internal/ir/lower/state_graph.go @@ -117,6 +117,9 @@ type StateGraph struct { transitionFootprints map[*Transition]Footprint behaviorFootprints map[ast.Node]Footprint footprintsOnce sync.Once + // transitionSteps: transition out of a state → its step short of do behaviors. + transitionSteps map[*Transition]TransitionStep + stepsOnce sync.Once // CompositeStates: state → regions CompositeStates map[*ast.StateNode][]*ast.StateRegion From edcb7cbd625eed90f190c5bc011f48502963c0fa Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 18:05:40 +0000 Subject: [PATCH 2/3] fix(runtime): separate executors' moves on distinct objects and contend a move that may end a run Co-Authored-By: jason.han --- cmd/sysml/check_engine_test.go | 4 +- cmd/sysml/explore_nested_test.go | 16 +- docs/project/spec-compliance.md | 4 +- internal/exec/runtime/advance.go | 52 ++++- internal/exec/runtime/check_reduce.go | 48 +++-- internal/exec/runtime/future_footprint.go | 70 ++++++- internal/exec/runtime/message_dependence.go | 80 +++++++- .../testdata/check/reduction_expected.txt | 2 +- internal/frontend/repl/explore_test.go | 2 +- internal/ir/lower/footprint.go | 185 ++++++++++++++---- internal/ir/lower/footprint_test.go | 31 ++- internal/ir/lower/state_footprint.go | 4 +- 12 files changed, 406 insertions(+), 92 deletions(-) diff --git a/cmd/sysml/check_engine_test.go b/cmd/sysml/check_engine_test.go index db420a4b66..260982b199 100644 --- a/cmd/sysml/check_engine_test.go +++ b/cmd/sysml/check_engine_test.go @@ -302,7 +302,7 @@ func TestEngineCheckBindsWitnessObjectsAcrossRuns(t *testing.T) { got := check(t, binary, model, slices.Concat([]string{"-engine", "check"}, invocation, []string{"-check-diverge", "Plant::spare.level", "-check-witness", dir})...) wantReport(t, got, 1, "divergent: Plant::spare.level ends as 1 or 2", - "Plant::spare.level = 1 (witness "+name(1)+")", "Plant::spare.level = 2 (witness "+name(2)+")", "witness of 6 choices replayed)") + "Plant::spare.level = 1 (witness "+name(1)+")", "Plant::spare.level = 2 (witness "+name(2)+")", "witness of 3 choices replayed)") // The spare's fill runs first, so its step 3 is the first: `b` first leaves level 1, `a` first 2. for _, c := range []struct { n int @@ -314,7 +314,7 @@ func TestEngineCheckBindsWitnessObjectsAcrossRuns(t *testing.T) { t.Fatal(err) } if !strings.HasPrefix(string(content), "object #1 = Plant::tank#1\nobject #2 = Plant::spare#1\n"+ - strings.Repeat("t=0.0: action fill of object #2 first of action fill of object #1, action fill of object #2\n", 2)+"step 3: "+c.took+" first of 2@a, 3@b\n") { + "t=0.0: action fill of object #2 first of action fill of object #1, action fill of object #2\nstep 3: "+c.took+" first of 2@a, 3@b\n") { t.Errorf("witness %d, spare.level = %s:\n%s", c.n, c.level, content) } // The run makes the spare's performance after the tank's: the spare is object #3 here. diff --git a/cmd/sysml/explore_nested_test.go b/cmd/sysml/explore_nested_test.go index cdbce05aa4..05fdbc7efe 100644 --- a/cmd/sysml/explore_nested_test.go +++ b/cmd/sysml/explore_nested_test.go @@ -75,9 +75,9 @@ func TestExploreRunsAMachineOnANestedObject(t *testing.T) { got := check(t, binary, linkedPairModel, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5") wantReport(t, got, 0, "✓ explored Comms::Ground::listen: 2 outcomes", - "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 12 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", - "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 2 | 4 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; events at t=3.0: accept Frame first of time listening 1->quiet, accept Frame; at t=3.0: do listening first of do listening, dispatch time listening 1->quiet", - "complete (16 runs)") + "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 4 | possible | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", + "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 2 | 1 | possible | t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; events at t=3.0: accept Frame first of time listening 1->quiet, accept Frame; at t=3.0: do listening first of do listening, dispatch time listening 1->quiet", + "complete (5 runs)") for _, jobs := range []string{"1", "4"} { again := check(t, binary, linkedPairModel, "-jobs", jobs, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5") if again.output() != got.output() { @@ -89,8 +89,8 @@ func TestExploreRunsAMachineOnANestedObject(t *testing.T) { calm := strings.Replace(linkedPairModel, "accept after 2 [s] then quiet", "accept after 1.5 [s] then quiet", 1) wantReport(t, check(t, binary, calm, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5"), 0, "✓ explored Comms::Ground::listen: 1 outcome", - "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 2 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", - "complete (2 runs)") + "finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 1 | possible | no choice points", + "complete (1 runs)") } // TestExploreRunsSiblingsOnOneAssembly checks that two behaviors named on parts of @@ -101,9 +101,9 @@ func TestExploreRunsSiblingsOnOneAssembly(t *testing.T) { binary := buildCLI(t) outcomes := []string{ - "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 1 | 12 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", - "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 2 | 4 | possible | t=2.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4", - "complete (16 runs)", + "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 1 | 4 | possible | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4", + "Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 2 | 1 | possible | t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4", + "complete (5 runs)", } byPath := check(t, binary, linkedPairModel, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-state", "Comms::Craft::modes Comms::pair.craft", "-advance", "5") diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 5793e86583..46e542ac56 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -708,7 +708,7 @@ checked after the result is bound is not a form the runtime offers, and none is | A guard the executor reads only to report a choice — one after the branch or transition already taken — that fails to evaluate is no alternative and no error: a guard with no result is not true, so its succession is not selected, the run is unchanged, and the failure is an informational `guard-unevaluable` note, while the same failure at the guard the run does take still fails the run | `choice.go` `UnevaluableGuard`, `UnevaluableGuard.Diagnostic` (`SeverityInfo`, code `UnevaluableGuardCode`), `Context.noteUnevaluableGuard`, `Context.UnevaluableGuards`; `action_choice.go` `ActionExecutor.noteUnevaluableGuard`; `action_executor.go` `probeGuard` (a `beginProbe` preview that restores the budget, the trace, every effect and the object identities it took); `state_executor.go` `probeTransition`, `unevaluableTransition`; `state_route.go` `probeBranch` (a choice pseudostate's later branch); `state_change_trigger.go` `probeChangeGuard` | `conformance/action_choice_unevaluable_guard` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_transition` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_branch` + `.expected.json` + `.trace.golden`; `choice_test.go:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestLaterChoiceGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestLaterGuardIsProbedWithoutCost`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteAction_UnevaluableGuardDiagnostics`; `repl/choice_test.go:TestStepReportsUnevaluableGuards`; `robustness_test.go:decision_no_satisfied_guard` (the taken path still fails) | ✅ Faithful (SysML v2 §7.17.3 selects a succession whose guard is true; a guard that cannot be evaluated is not true, and reading it changed nothing) | | A conformance case that admits several outcomes states the whole set: `outcomes` lists every admissible outcome in full — never "anything" — and `admissible` cites the section of `behavior-semantic-oracle.md` that derives the set; a `.trace.order` beside it states the partial order the library does fix as `earlier < later` over trace labels. The harness checks the run's outcome is exactly one listed member, checks the trace against every order constraint, then explores the case and fails on a listed outcome no linearization reached, a reached outcome the list omits, and a hit budget — each naming the outcome and a witness choice sequence | `conformance_test.go` `ExpectedOutcome.Outcomes`/`Admissible`/`ExploreBudget`, `admissibleSchemaProblems` (an `outcomes` list needs two or more full outcomes, an `admissible` title the oracle has, and no single-outcome fields beside it), `matchOutcome`, `runConformanceCase`, `exploreConformanceCase`; `trace_test.go` `checkTraceOrder`, `parseOrderConstraints`, `orderViolations`; `testdata/conformance/README.md` (the schema) | `conformance_test.go:TestAdmissibleOutcomesSchema`, `:TestMatchOutcomeRequiresExactlyOne`, `:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case), `:TestExecutionConformanceUnderPolicies`; `trace_test.go:TestTraceOrderViolationFails`, `:TestExecutionTrace`; `conformance/action_explore_three_writers` (`outcomes` of three, `.trace.order` of six constraints; explored in six runs), `action_choice_shared_message_accept`, `action_choice_fork_token_order` (one outcome, a `.trace.order` admitting the tokens either way), `state_explore_region_order` | ✅ Faithful (a case without `outcomes` is not explored by the harness, so a fixture pinning one linearization of an unobservable openness stays a one-outcome case; the oracle names which fixtures those are) | | Exploration is bounded and distinguishes setup failures from runtime outcomes: the budget is runs (1024 by default) and choice points per run (64), and a budget hit ends the search as `incomplete: budget hit after N runs`, naming `runs` before `depth`; a fresh-context or root-executor creation failure, or a pure structural start-check failure before root behavior runs, means no linearization ran and is returned without outcomes, while a failure during initial model behavior or later is an error outcome. Any runtime-error linearization makes the verdict fail, including an incomplete exploration; only an incomplete search without a witnessed failure is unresolved, and only a complete search without failures proves the outcome set. JSON and the wire include `failedLinearizations` / `failed_linearizations` only when nonzero; standing evidence names the failing count | `runtime/explore.go` `SetupError`, `Exploration.FailedLinearizations`; `runtime/context.go` root action/state setup classification; `runtime/explore_queue.go` `ExploreWith`, `exploreQueue.work`; `runtime/check.go` checker setup failure; `analysis/explore.go` proof strength; `analysis/standing.go` `Result.evidence`; `repl/explore.go` `explorationVerdict`; `cmd/sysml/report.go` `checkExploration`; `grpc/explore.go` `Service.explore` | `runtime/robustness_explore_failures_test.go:TestRuntimeRobustnessExploreFailures`; `analysis/explore_test.go`; `repl/explore_test.go:TestRunActionExploreSetupFailureRunsNoLinearization`, `:TestRunActionExplorePartialFailureFailsTheVerdict`; `cmd/sysml/run_test.go:TestExploreSetupFailureIsNotAnOutcome`, `:TestExplorePartialFailureFailsAndReportsTheFailedRun`, `:TestExploreInitialEntryFailureIsAnOutcome`; `grpc/explore_test.go:TestExploreSetupFailureIsReturnedInTheResponse`, `:TestExploreReportsAFailingRunAsAnOutcome` | ✅ Faithful (setup failures produce no outcome, while a witnessed runtime failure prevents a proof claim) | -| The set of outcomes is also reached by search rather than by enumeration: the explicit-state model checker takes the schedules of an *invocation* — the actions and state machines started on one clock, run to a horizon, and the machines of the objects they materialize — one *move* at a time — one token advancing one node, a body being one move (`stepToken`'s unit, coarser than the interpreter's statement), one event dispatched, one due `do` behavior stepped — enumerating the enabled moves of a state (each token able to act, a join whose tokens have all arrived, a paused token whose wait has ended, a parked `accept` whose message has arrived or whose routing fails under a readiness probe, one move per holding guard of a decision; a machine's dispatch, one per event the library leaves unordered at the instant, and its due do behaviors; among the executors due, the one drawn holds the turn after a move only while its next move is independent of everything each other executor due may still do at the instant (`Context.contended`, the same footprints and message dependence as the reduction), and otherwise the due order is drawn again), snapshotting the run before each choice and restoring it to take the next, so every schedule the library admits is visited and no other. Two moves whose static *footprints* — the features a node's body reads (an outgoing succession's guard and a parked trigger's condition among them) and writes, the channels it sends on and accepts from, the joins and merges it reaches, computed once per node when the action is lowered; for a dispatch the guards and triggers of the transitions the event can select out of the active configuration, their effects and the activity of the states left and entered, for a do step its statements'; one executor's moves pairwise dependent — are independent commute, so only one order of each such pair is searched (persistent sets with a sleep set; a dynamic assignment target or send target depends on everything), and a state already visited — every executor in invocation order: the token multiset by node and frame path, frames root-first with values in the trace recorder's canonical form, a paused body's statement cursor, frames and wait, a machine's configuration, history, values, queue in dispatch order, deferred events, timers and do progress; objects by their materialization path rather than by `Instance.ID`, messages, the clock — is not searched again. What the search finds: a named constraint or requirement `false` at a stable state, a deadlock (`ErrActionDeadlock`, `ErrAcceptDeadlock`) or a typed error a body raises (an unbound parameter, a dangling succession, a division by zero, an `accept` whose `via` port does not resolve, each on the schedule that reaches it) is a *violation*; a feature ending with different final values on different schedules is *divergent*, one witness per value (the features named — `finalState` a machine's resting configuration, `.` and ` finalState` in a joint invocation — else every attribute of the behaviors and their performing object and every machine's `finalState`, an action without an object on its own); a machine resting where nothing wakes it is a complete schedule, not a deadlock, and a wait past the horizon is left unreached, the verdict reading `exhaustive up to t=D`; a bound reached — moves along one schedule (`depth`, 10 000), distinct states (`states`, 1 000 000), the plan's clock (`time`), an executor budget (`actionSteps`, `steps`, `elements`, …) — is named and the verdict is `no violation within bounds`, never `no violation, exhaustive`, the one proof, relative to the atomic move and the properties given. A witness is the `ChoiceTaken` sequence `explore` records for the same steps, written as its choice lines, a blank line and the run's trace, and is *replayed* through the scheduler seam (`replay:`, the policy that follows a witness's choices and refuses where the run departs) before it is reported: the replayed run must reach the state claimed with the same trace, else the witness is *not covered* with the disagreement as the reason. Where an exploration completes, the final states the check reaches are the outcomes it tabled. A body paused mid-statement — a token suspended at a breakpoint or on the clock, a do behavior waiting — is explicit state (`bodyRun`: statement cursor, block, loop and flow-node frames, the nested performance, a `bodyWait` descriptor) a snapshot of the same context captures and restores, so it is searched like any other; a portable `HeldImage` alone refuses it (`ErrSnapshotPausedBody`). Statement-level moves and following a signal to an object whose machine the invocation does not run are later stages'. The search is single-threaded — one executor state per stack frame, one visited set — so `Jobs` divides only the replay of witnesses | `lower/footprint.go` `Footprint`, `Footprints`, `Footprint.Dependent`, `footprintOf` (`Graph.Footprints` beside `Bodies`); `runtime/check.go` `Check`, `checker.search`, `checker.take`, `checker.enter`, `checker.visit`, `checker.stabilize`, `checker.properties`, `checker.final`, `CheckReport`, `CheckVerdict`, `CheckStopped`, `ExecutorBounds`; `runtime/check_reduce.go` `checker.persistent`, `checker.childSleep`, `checker.footprintOf`; `runtime/check_invocation.go` `Invocation`, `Starter`; `runtime/check_run.go` (the executors on one clock, the due order drawn, the horizon); `runtime/check_moves.go` `enabledMove`, `ActionExecutor.enabledMoves`, `ActionExecutor.makeMove`, `StateExecutor.dispatchMoves`, `checkPolicy`; `runtime/check_state.go` `canonicalState`, `stateSpeller`; `runtime/action_body_run.go` `bodyRun`, `bodyWait`; `lower/state_footprint.go` (transition and behavior footprints); `runtime/replay.go` `ParseChoices` (stops at the first blank line), `ReplayPolicy`, `Context.Unfollowed`, `ReplayError`; `runtime/check_replay.go` `Replay`, `Witness.String`, `ReplayDisagreement`; `runtime/action_executor.go` `acceptMatch` (a routing failure kept, not a deadlock); `analysis/check.go` `checkEngine` (below) | `runtime/check_test.go:TestCheckJoinWaitsForSlowestBranch` (`arrived = 3` on every schedule, nothing divergent), `:TestCheckForkBranchesWriteOneFeatureDiverge` (`x` over exactly `{1, 2}`, `leftRan`/`rightRan` agreed), `:TestCheckEvaluatesPropertiesAtCompletion`, `:TestCheckDivergenceOfNamedFeaturesOnly`, `:TestCheckWitnessesReplay`, `:TestCheckReplayDisagreesWithATamperedWitness`, `:TestCheckWitnessesAPerformedActionThroughItsPerformer`, `:TestCheckPropertyOfThePerformerIsWitnessed`, `:TestCheckReportsFailuresAsViolations` (the robustness failures as violations with a witness), `:TestCheckReportsAnUnresolvedViaPortAsTheRoutingError`, `:TestCheckMergeLoopHitsTheDepthBound` (`incomplete`, `depth` named, no hang, no exhaustiveness), `:TestCheckNamesEachExecutorBudget`, `:TestCheckStopsWhenCancelled`, `:TestCheckSettlesTimedBranchesOnTheClock`, `:TestCheckVisitedStatesCloseALoop`; `runtime/check_moves_test.go`; `runtime/check_reduce_test.go:TestCheckReductionIsSound` (reduced and unreduced final-state sets equal over `testdata/check/por_*.sysml`: shared write, guard read, trigger-condition read, send/accept pairing, join convergence, dynamic target), `:TestCheckReductionRatchet` (`testdata/check/reduction_expected.txt`, adjudicated on every movement); `runtime/check_corpus_test.go:TestCheckConformanceOracles` (every action, state and clock case with an admissible set against its `.check.expected.json`, reduced and unreduced — the eight cases whose default run pauses a body and `clock_action_state_due_together` among them), `:TestCheckAgreesWithExploreOverTheConformanceCorpus` (the referee), `:TestCheckWitnessesReplayOverTheConformanceCorpus`; `runtime/check_horizon_test.go` (a re-arming timer bounded by the horizon, a property up to it, an action's wait past it, a machine's failures as violations, the caller's deadline); `runtime/check_reduce_state_test.go` (dispatch and do-step footprints, one executor's moves as a unit); `runtime/action_body_run_test.go` (a body paused at a breakpoint, on the clock and inside a loop resumed, snapshotted and restored); `analysis/check_clock_test.go:TestExploreRefereesCheckOverBehaviorsOnOneClock`, `:TestChecksOfBehaviorsOnOneClockHaveWorkersOfTheirOwn`; `runtime/replay_test.go`; `lower/footprint_test.go`, `lower/state_footprint_test.go` | ✅ Faithful for actions and state machines on one clock (an exhaustive verdict is a proof relative to the atomic move — a body one move, a dispatch one move — and the properties named; statement-level moves and signals to machines off the clock are later stages') | +| The set of outcomes is also reached by search rather than by enumeration: the explicit-state model checker takes the schedules of an *invocation* — the actions and state machines started on one clock, run to a horizon, and the machines of the objects they materialize — one *move* at a time — one token advancing one node, a body being one move (`stepToken`'s unit, coarser than the interpreter's statement), one event dispatched, one due `do` behavior stepped — enumerating the enabled moves of a state (each token able to act, a join whose tokens have all arrived, a paused token whose wait has ended, a parked `accept` whose message has arrived or whose routing fails under a readiness probe, one move per holding guard of a decision; a machine's dispatch, one per event the library leaves unordered at the instant, and its due do behaviors; among the executors due, the one drawn holds the turn after a move only while its next move is independent of everything each other executor due may still do at the instant (`Context.contended`, the same footprints and message dependence as the reduction), and otherwise the due order is drawn again), snapshotting the run before each choice and restoring it to take the next, so every schedule the library admits is visited and no other. Two moves whose static *footprints* — the features a node's body reads (an outgoing succession's guard and a parked trigger's condition among them) and writes, the channels it sends on and accepts from, the joins and merges it reaches, computed once per node when the action is lowered; for a dispatch the guards and triggers of the transitions the event can select out of the active configuration, their effects and the activity of the states left and entered, for a do step its statements'; one executor's moves pairwise dependent — are independent commute, so only one order of each such pair is searched (persistent sets with a sleep set; a dynamic assignment target or send target, or a `new` of a type that evaluates or starts anything, depends on everything; a `new` of a plain type depends on another creation and on a read of what objects exist, and a `via` send on a write of anything but an attribute or a state's activity; the moves of two executors run for two objects are apart on their pins, their states' activity and the features each names alone of its own object), and a state already visited — every executor in invocation order: the token multiset by node and frame path, frames root-first with values in the trace recorder's canonical form, a paused body's statement cursor, frames and wait, a machine's configuration, history, values, queue in dispatch order, deferred events, timers and do progress; objects by their materialization path rather than by `Instance.ID`, messages, the clock — is not searched again. What the search finds: a named constraint or requirement `false` at a stable state, a deadlock (`ErrActionDeadlock`, `ErrAcceptDeadlock`) or a typed error a body raises (an unbound parameter, a dangling succession, a division by zero, an `accept` whose `via` port does not resolve, each on the schedule that reaches it) is a *violation*; a feature ending with different final values on different schedules is *divergent*, one witness per value (the features named — `finalState` a machine's resting configuration, `.` and ` finalState` in a joint invocation — else every attribute of the behaviors and their performing object and every machine's `finalState`, an action without an object on its own); a machine resting where nothing wakes it is a complete schedule, not a deadlock, and a wait past the horizon is left unreached, the verdict reading `exhaustive up to t=D`; a bound reached — moves along one schedule (`depth`, 10 000), distinct states (`states`, 1 000 000), the plan's clock (`time`), an executor budget (`actionSteps`, `steps`, `elements`, …) — is named and the verdict is `no violation within bounds`, never `no violation, exhaustive`, the one proof, relative to the atomic move and the properties given. A witness is the `ChoiceTaken` sequence `explore` records for the same steps, written as its choice lines, a blank line and the run's trace, and is *replayed* through the scheduler seam (`replay:`, the policy that follows a witness's choices and refuses where the run departs) before it is reported: the replayed run must reach the state claimed with the same trace, else the witness is *not covered* with the disagreement as the reason. Where an exploration completes, the final states the check reaches are the outcomes it tabled. A body paused mid-statement — a token suspended at a breakpoint or on the clock, a do behavior waiting — is explicit state (`bodyRun`: statement cursor, block, loop and flow-node frames, the nested performance, a `bodyWait` descriptor) a snapshot of the same context captures and restores, so it is searched like any other; a portable `HeldImage` alone refuses it (`ErrSnapshotPausedBody`). Statement-level moves and following a signal to an object whose machine the invocation does not run are later stages'. The search is single-threaded — one executor state per stack frame, one visited set — so `Jobs` divides only the replay of witnesses | `lower/footprint.go` `Footprint`, `Footprints`, `Footprint.Dependent`, `footprintOf` (`Graph.Footprints` beside `Bodies`); `runtime/check.go` `Check`, `checker.search`, `checker.take`, `checker.enter`, `checker.visit`, `checker.stabilize`, `checker.properties`, `checker.final`, `CheckReport`, `CheckVerdict`, `CheckStopped`, `ExecutorBounds`; `runtime/check_reduce.go` `checker.persistent`, `checker.childSleep`, `checker.footprintOf`; `runtime/check_invocation.go` `Invocation`, `Starter`; `runtime/check_run.go` (the executors on one clock, the due order drawn, the horizon); `runtime/check_moves.go` `enabledMove`, `ActionExecutor.enabledMoves`, `ActionExecutor.makeMove`, `StateExecutor.dispatchMoves`, `checkPolicy`; `runtime/check_state.go` `canonicalState`, `stateSpeller`; `runtime/action_body_run.go` `bodyRun`, `bodyWait`; `lower/state_footprint.go` (transition and behavior footprints); `runtime/replay.go` `ParseChoices` (stops at the first blank line), `ReplayPolicy`, `Context.Unfollowed`, `ReplayError`; `runtime/check_replay.go` `Replay`, `Witness.String`, `ReplayDisagreement`; `runtime/action_executor.go` `acceptMatch` (a routing failure kept, not a deadlock); `analysis/check.go` `checkEngine` (below) | `runtime/check_test.go:TestCheckJoinWaitsForSlowestBranch` (`arrived = 3` on every schedule, nothing divergent), `:TestCheckForkBranchesWriteOneFeatureDiverge` (`x` over exactly `{1, 2}`, `leftRan`/`rightRan` agreed), `:TestCheckEvaluatesPropertiesAtCompletion`, `:TestCheckDivergenceOfNamedFeaturesOnly`, `:TestCheckWitnessesReplay`, `:TestCheckReplayDisagreesWithATamperedWitness`, `:TestCheckWitnessesAPerformedActionThroughItsPerformer`, `:TestCheckPropertyOfThePerformerIsWitnessed`, `:TestCheckReportsFailuresAsViolations` (the robustness failures as violations with a witness), `:TestCheckReportsAnUnresolvedViaPortAsTheRoutingError`, `:TestCheckMergeLoopHitsTheDepthBound` (`incomplete`, `depth` named, no hang, no exhaustiveness), `:TestCheckNamesEachExecutorBudget`, `:TestCheckStopsWhenCancelled`, `:TestCheckSettlesTimedBranchesOnTheClock`, `:TestCheckVisitedStatesCloseALoop`; `runtime/check_moves_test.go`; `runtime/check_reduce_test.go:TestCheckReductionIsSound` (reduced and unreduced final-state sets equal over `testdata/check/por_*.sysml`: shared write, guard read, trigger-condition read, send/accept pairing, join convergence, dynamic target), `:TestCheckReductionRatchet` (`testdata/check/reduction_expected.txt`, adjudicated on every movement); `runtime/check_corpus_test.go:TestCheckConformanceOracles` (every action, state and clock case with an admissible set against its `.check.expected.json`, reduced and unreduced — the eight cases whose default run pauses a body and `clock_action_state_due_together` among them), `:TestCheckAgreesWithExploreOverTheConformanceCorpus` (the referee), `:TestCheckWitnessesReplayOverTheConformanceCorpus`; `runtime/check_horizon_test.go` (a re-arming timer bounded by the horizon, a property up to it, an action's wait past it, a machine's failures as violations, the caller's deadline); `runtime/check_reduce_state_test.go` (dispatch and do-step footprints, one executor's moves as a unit); `runtime/action_body_run_test.go` (a body paused at a breakpoint, on the clock and inside a loop resumed, snapshotted and restored); `analysis/check_clock_test.go:TestExploreRefereesCheckOverBehaviorsOnOneClock`, `:TestChecksOfBehaviorsOnOneClockHaveWorkersOfTheirOwn`; `runtime/replay_test.go`; `lower/footprint_test.go`, `lower/state_footprint_test.go` | ✅ Faithful for actions and state machines on one clock (an exhaustive verdict is a proof relative to the atomic move — a body one move, a dispatch one move — and the properties named; statement-level moves and signals to machines off the clock are later stages') | | The object an explored run performs a behavior on is one the run builds, never one the session holds: a performer, subject or object named to `explore`, `check`, `smt`, `sweep` or `all` is a *declaration* (a part/item usage or definition) each run instantiates, or a declaration-rooted *path* into what it holds (`Comms::pair.ground`, `Fleet::fleet.rovers[2]`) the run walks inside the object it made, the declaration being instantiated once per run however many behaviors name paths under it, so sibling parts share their assembly and its connectors carry their messages; a declaration `-instantiate` names is given to every run the same way, a machine named alone attaching to the run's one object exhibiting it; the path is checked against the declarations before any run starts (an unknown usage, an index on a single-valued usage, a step through a value) and what only a run can know (a part its recipe left unbuilt, an index past what it built) is that run's error; an id (`#2`, `#2.ground`) or a path from an object the session alone holds is refused as naming no recipe; the wire's `performer_symbol_id` and `subject_symbol_id` spell the same paths, and a witness the checker writes for a behavior on a nested object replays on it | `repl/explore.go` `freshRef` (the longest declaration prefix and the path past it), `checkFreshPath`, `freshPathError`, `planFresh`, `freshPlan.given`, `freshPlan.bind` (one root per declaration per run), `freshObjects.object` (the walk, through `objref.Walker`), `freshObjects.exhibitors`, `freshMachine`, `freshAction`, `freshExhibitorsError`, `UnplannedObjectError`, `ExploredObjectError`; `repl/session.go` `Session.given`, `givenRoots`; `repl/instantiate_report.go` (the CLI's `-instantiate` recorded as a given root); `repl/carryover.go` (a given root dropped with its declaration); `repl/meta.go` `ExhibitorsError.Fresh`; `objref/objref.go` `Ref`, `Segment`, `LooksLikePath`; `objref/walk.go` `Walker.Walk` (the one walk the prompt and the runs share, typed at each refusal); `runtime/context.go` `ExecuteActionPerformedBy`, `ExecuteStatePerformedBy`, `StateOutcomePerformedBy`; `runtime/check_invocation.go` `Invocation.Outcome` (the performers' attributes beside the behaviors'); `grpc/verify.go` `verifyContext.performer`, `subject`, `objectAt`; `grpc/service.go` (`CapabilityPerformer`; `performer_symbol_id` on `ExecuteActionRequest` and `ExecuteStateRequest`); `cmd/sysml/usage.go` (`-instantiate`, `-state`, `-action`); `client/opensysml/execute.go` `PerformedBy`; `client/python/opensysml/connection.py` (`performer=`) | `repl/explore_test.go:TestRunForExploresAMachineOnANestedObject`, `:TestRunForExploresAnActionOnANestedObject`, `:TestRunAnalysisExploresOnANestedSubject`, `:TestRunForExploresSiblingsOnOneRoot` (one root, two machines, the connector between them; the same table under one and four jobs), `:TestExploredRunsAreGivenTheObjectsInstantiated` (a machine alone attaches to the given object, a path reuses it, the prompt's `%instantiate` gives nothing, a given root outlives unrelated submissions and not its declaration's), `:TestExploredPathsAreCheckedAgainstTheDeclarations` (an id, an unknown usage, an index on one value, a step through a value: refused before any run; a part left unbuilt: the run's error); `cmd/sysml/explore_nested_test.go:TestExploreRunsAMachineOnANestedObject` (a connector race tables two outcomes, its no-race variant one, byte for byte under `-jobs 1` and `-jobs 4`), `:TestExploreRunsSiblingsOnOneAssembly`, `:TestExploreRefusesPathsItCannotPlan`, `:TestEngineCheckWitnessesANestedObjectsDivergence` (the witness written, replayed under `-schedule replay:`, and composed under `-engine all`); `runtime/check_test.go:TestCheckWitnessesOfSeveralBehaviorsReplay`, `runtime/replay_test.go:TestReplayFollowsDoActionWitnesses`, `:TestReplayFollowsSiblingDoActionWitnesses`; `grpc/explore_test.go:TestPerformOnANestedObjectOverTheWire`, `grpc/analysis_test.go:TestRunAnalysisOnANestedSubject`, `grpc/capability_test.go` (`performer` advertised); `client/opensysml/performer_test.go`; `client/python/tests/test_performer.py` | ✅ Faithful (the runs' objects are built by the same instantiation and walked by the same `objref.Walker` as the prompt's, so a path means one thing at the prompt and in a run; the session's objects stay out of every run by construction, the plan being made under the session's lock and the objects inside each run) | | Action execution nodes | `action_executor.go:723` stepActionExecutionNode | `action_control_flow.sysml` | ✅ Faithful | | Nested action invocation (`action call : Callee;`, `action call = Callee(3, 4);`, `action call = Callee(a = 3);`, `perform action call : Callee;`) | `runtime/action_frame.go` `bindArguments`, `performInvocation`, `checkInputsBound`; `runtime/state_statements.go` `stateStmtHost.performNode`; `runtime/invoke_action.go` `invocationArguments`, `bindArgumentList`, `Context.actionParametersOf` (over `semantics.Model.BehaviorParametersOf`, so inherited and redefined parameters keep their effective order); `action_executor.go` `stepNestedAction` | `invoke_action_test.go:TestInvokeActionPassesParametersBothWays`, `:TestInvokeActionBindsPositionalArguments`, `:TestInvokeActionBindsNamedArguments`, `:TestInvokeActionRejectsBadArguments`; `conformance/action_node_invocation_positional`, `action_node_invocation_named`, `action_node_typed_body_inputs`, `action_node_inherited_parameters`, `action_node_invocation_empty`, `action_inherited_typed_node_scope`, `action_node_arguments_before_defaults`, `state_block_flow_node_arguments_before_defaults` | ✅ Faithful (arguments bind the callee's inputs by the callee's parameter order and names, never by what the caller happens to name alike; they bind the node's pins before the defaults it declares are evaluated, so a default an argument replaces is never evaluated and one the node keeps reads the argument's value, in an action's flow and in a state's body alike; the callee is resolved where the node was declared, so a node a derived action inherits still finds a callee visible only to the general action; a surplus, missing, unknown or repeated argument is `ErrActionArity`, `ErrUnboundParameter`, `ErrUnknownParameter` or `ErrDuplicateArgument` before the callee runs — a surplus one is also reported statically by `passes/typecheck_expr.go`, so no conformance fixture states it. The row above states the compatibility by-name fallback a bare usage keeps) | @@ -812,7 +812,7 @@ checked after the result is bound is not a form the runtime offers, and none is | Earliest transfer first (`Occurrence::incomingTransferSort` defaults to `earlierFirstIncomingTransferSort`): a completion event is dispatched before a signal due at the same instant. A replayed deferred signal is a new send and is dispatched behind the occurrences already queued — the standard encoding has no way to place it ahead of the pool, where PSSM §8.4 releases a deferred occurrence ahead of every non-completion occurrence | `executor_common.go` eventHeap.Less, isCompletionEvent | `choice_test.go:TestCompletionTransitionChoiceRereadsGuards`, `signal_injection_test.go:TestRunToCompletionTakesAPendingSignalBeforeALaterTimer`; PSSM referee rows *Deferred 001*, *Deferred 005* (`docs/project/pssm-referee.md`) | ⚠️ Approximate — the replay order of different deferred signals against one another and against the pool is not expressible in standard notation | | A transition out of a composite state is enabled while any of its substates is active: matching walks outward from every active leaf through the lowered containment (`StateGraph.ParentState`), the innermost enabled transition wins for the same event (KerML `StatePerformances::StatePerformance::acceptable`, whose `isDispatch` invariant lets an enclosing state performance accept a transfer only when no substate performance in the dispatch scope accepted it), and a false guard does not consume it | `state_executor.go` broadcastEvent, selectTransitions, losesToNestedTransition, nestedIn, activeLeaves, fireFrom, enabledTransitions, acceptsSignal/acceptsSignalFrom (an enclosing state's `accept` takes a signal off the bus) | `conformance/state_composite_outer_transition.sysml`, `:state_composite_inner_priority.sysml`, `state_composite_transition_test.go:TestCompositeStateHandlesEventItsSubstateDoesNot`, `:TestFalseGuardInsideACompositeStateFallsOutward`, `:TestTransitionOutOfAnIntermediateCompositeStateKeepsItsOwnerActive`, `:TestOuterCompositeStateStillHandlesItsEventAfterASubstateMoved`, `robustness_test.go:signal_no_level_of_a_composite_state_accepts` | ✅ Faithful | | Two transitions out of one state enabled by one event: each is a `StateTransitionPerformance` (Kernel Semantic Library `StatePerformances.kerml`) whose `transitionLink` is `HappensBefore[0..1]`, and nothing in the library orders one against another, so which fires is the executor's pick; the innermost-wins rule between a substate's transition and its enclosing state's is SysML v2/KerML order, not a pick | `state_executor.go` `enabledTransitions`, `transitionEnabled`, `probeTransition` (every transition out of the state is matched against the event and its guard and join evaluated — a call trigger's arguments bound for the guard and unbound after — the first enabled fires under the default policy; the ones after it are read in a `beginProbe` preview that restores the budget, the trace, every effect and the object identities the preview took, and one that fails to evaluate is no alternative and no error, recorded as a `guard-unevaluable` note by `unevaluableTransition`), `chooseTransition`, `transitionChoice` (several enabled are a choice point naming the state, the trigger and the transitions by position and target; the pick among them is made only for a candidate that survived conflict resolution); the notes ride on the `dispatchCandidate` into `fireFrom`, and `transitionDecided` records them once the firing transition's guard has been read for the last time — a candidate another region's firing disabled meanwhile reports nothing — after `selectCandidates` has kept one candidate per transition and `losesToNestedTransition` has dropped a composite state's candidate to a nested one (a transition several regions select through their enclosing state is one choice, and ancestor priority is never among the alternatives); `state_change_trigger.go` `observeChangeConditions`, `probeChangeGuard`, `risenChangeTransitions` (every change transition risen by one poll is collected the same way: a state's guards are read live until the first enabled, the ones after it in a `beginProbe` preview, and one that fails to evaluate is no alternative and no error, noted as `guard-unevaluable` and left armed; the first declared fires) | `conformance/state_choice_transition_conflict.sysml` + `.expected.json` (both outcomes listed as admissible) + trace golden; `conformance/state_choice_ancestor_priority_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_shared_ancestor_regions.sysml` + `.expected.json` + trace golden (one `choice` line for two regions); `conformance/state_choice_ancestor_outranked_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_unevaluable_transition.sysml` + `.expected.json` + trace golden; `conformance/state_choice_change_transition_conflict.sysml` + `.expected.json` (both outcomes) + trace golden; `choice_test.go:TestTransitionChoiceNamesStateAndEvent`, `:TestAncestorPriorityIsNotAChoice`, `:TestSharedAncestorChoiceIsReportedOnce`, `:TestAncestorChoiceSuppressedByNestedTransitionIsNotReported`, `:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestNotesOfATransitionBlockedBeforeFiringAreDropped`, `:TestNotesOfATransitionFailingInItsEffectAreKept`, `:TestChangeTransitionChoice`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestChangeTransitionChoiceUnderHierarchyAndRegions`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteState_ChoicePointDiagnostics`; `repl/choice_test.go:TestAdvanceReportsChoicePoints` | ✅ Faithful (declaration order is tool-defined and kept; the pick is reported, and the ordered case is not) | -| Executors due at one instant of the clock are unordered: two performances waiting on the same `TimeInstantValue` (Kernel Semantic Library `Clocks.kerml`) are `HappensBefore`-linked by nothing, so which of an action token and a state transition, of two state machines, or of two actions runs first when their instant comes is the executor's pick | `advance.go` `Context.runDue` (the executors with work due at the current instant, in creation order, are a choice point of kind `ChoiceDueOrder` placed `at t=` and naming each executor — `action `, `state machine of object #n` — and the one run first; the pick is drawn by `scheduler.go` `scheduler.pickDue` under the run's policy — the last created under `reverse`, the default, so a run holding one executor is unchanged; the first created under `declared`; a draw under `seed:`; under `explore`, the exploring run's next slot, `scheduler.describe` giving it the due-order kind and alternatives so the witness names the executor run first and every order of the due executors is a linearization replayed; one executor alone due is no choice and records nothing; under `explore`, `check`, `replay` and `seed:` the executor drawn makes one move and keeps its turn only while its next move is independent of what every other executor due may still do before the instant ends — `advance.go` `Context.contended` against `future_footprint.go` `futureFootprints.executorFuture`, which stops an executor's future at a wait on a literal delay past the instant and otherwise takes all it may do, and `message_dependence.go` `Context.channelsMeet`, which separates a send from an accept or two accepts only where both signal types resolve statically and do not conform, and keeps every unresolved type, `via` route, receiver and dispatch-drop dependent — and otherwise the due order is drawn again, so two reads of a shared feature may both run before either write; under `declared` and `reverse` the executor drawn runs its work at the instant through, in the order it always has; the executors polling a change condition once the definite work at the instant has settled are drawn the same way, so which watcher sees what another's reaction changed is the pick); `choice.go` `ChoiceDueOrder`, `ChoicePoint.String` (`choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first)`) | `conformance/clock_action_state_due_together.sysml` + `.expected.json` (`outcomes`: either may run first) + trace goldens under the default, `declared` and `seed:1`; `conformance/clock_two_machines_share_clock.trace.golden` (two machines due together); `conformance/clock_action_accept_after.trace.golden`, `clock_action_accept_at.trace.golden`, `clock_do_action_while_token_waits.trace.golden` (one executor due: no `choice` line); `scheduler_test.go:TestDueOrderChoice` (the pick under each policy, and none recorded for one executor), `:TestChangeWatchOrderChoice` (two machines polling one condition: the pick under each policy decides which sees the raised value and which what the first left); `repl/runtime_commands_test.go:TestAdvanceMovesActionAndStateDebuggersTogether`; `explore_test.go:TestExploreDueOrder` (three machines due together explore to their six orders, each witnessed by a due-order choice among 3 then among 2, and the driven policies each take one of them), `conformance_test.go:TestExecutionConformance` (`clock_action_state_due_together` explored: both orders reached, no other); `repl/explore.go` `exploreRunFor` (`RunFor` under `explore`: the behaviors named started on one clock in every run, advanced once, their outcomes joined by `Context.JointOutcome` under each behavior's name), `repl/explore_test.go:TestRunForExploresEveryDueOrder`, `cmd/sysml/run_test.go:TestExploreAdvanceRunsBehaviorsOnOneClock`, `cmd/sysml/explore_turns_test.go:TestExploreInterleavesExecutorsMoveByMove` (two read-then-write actions due together: explore, check and seeds reach the lost update, `declared` and `reverse` keep their order) | ✅ Faithful (the default order — the executor started last first — is tool-defined and pinned by the trace golden; the pick is reported, and one executor alone is not; `explore` reaches every order) | +| Executors due at one instant of the clock are unordered: two performances waiting on the same `TimeInstantValue` (Kernel Semantic Library `Clocks.kerml`) are `HappensBefore`-linked by nothing, so which of an action token and a state transition, of two state machines, or of two actions runs first when their instant comes is the executor's pick | `advance.go` `Context.runDue` (the executors with work due at the current instant, in creation order, are a choice point of kind `ChoiceDueOrder` placed `at t=` and naming each executor — `action `, `state machine of object #n` — and the one run first; the pick is drawn by `scheduler.go` `scheduler.pickDue` under the run's policy — the last created under `reverse`, the default, so a run holding one executor is unchanged; the first created under `declared`; a draw under `seed:`; under `explore`, the exploring run's next slot, `scheduler.describe` giving it the due-order kind and alternatives so the witness names the executor run first and every order of the due executors is a linearization replayed; one executor alone due is no choice and records nothing; under `explore`, `check`, `replay` and `seed:` the executor drawn makes one move and keeps its turn only while its next move is independent of what every other executor due may still do before the instant ends — `advance.go` `Context.contended` against `future_footprint.go` `futureFootprints.executorFuture`, which stops an executor's future at a wait on a literal delay past the instant and otherwise takes all it may do, and `message_dependence.go` `Context.channelsMeet`, which separates a send from an accept or two accepts only where both signal types resolve statically and do not conform, and keeps every unresolved type, `via` route, receiver and dispatch-drop dependent, and in which a send naming no target meets no consumer run for another object; a machine's future there leaves out a transition whose signal no queued message carries and no executor due may send at the instant, unless one may send anything; a move that may end the executor's performance (`advance.go` `Context.endContended`) is contended by any other executor that may still move, since an end observes every place — and otherwise the due order is drawn again, so two reads of a shared feature may both run before either write; under `declared` and `reverse` the executor drawn runs its work at the instant through, in the order it always has; the executors polling a change condition once the definite work at the instant has settled are drawn the same way, so which watcher sees what another's reaction changed is the pick); `choice.go` `ChoiceDueOrder`, `ChoicePoint.String` (`choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first)`) | `conformance/clock_action_state_due_together.sysml` + `.expected.json` (`outcomes`: either may run first) + trace goldens under the default, `declared` and `seed:1`; `conformance/clock_two_machines_share_clock.trace.golden` (two machines due together); `conformance/clock_action_accept_after.trace.golden`, `clock_action_accept_at.trace.golden`, `clock_do_action_while_token_waits.trace.golden` (one executor due: no `choice` line); `scheduler_test.go:TestDueOrderChoice` (the pick under each policy, and none recorded for one executor), `:TestChangeWatchOrderChoice` (two machines polling one condition: the pick under each policy decides which sees the raised value and which what the first left); `repl/runtime_commands_test.go:TestAdvanceMovesActionAndStateDebuggersTogether`; `explore_test.go:TestExploreDueOrder` (three machines due together explore to their six orders, each witnessed by a due-order choice among 3 then among 2, and the driven policies each take one of them), `conformance_test.go:TestExecutionConformance` (`clock_action_state_due_together` explored: both orders reached, no other); `repl/explore.go` `exploreRunFor` (`RunFor` under `explore`: the behaviors named started on one clock in every run, advanced once, their outcomes joined by `Context.JointOutcome` under each behavior's name), `repl/explore_test.go:TestRunForExploresEveryDueOrder`, `cmd/sysml/run_test.go:TestExploreAdvanceRunsBehaviorsOnOneClock`, `cmd/sysml/explore_turns_test.go:TestExploreInterleavesExecutorsMoveByMove` (two read-then-write actions due together: explore, check and seeds reach the lost update, `declared` and `reverse` keep their order) | ✅ Faithful (the default order — the executor started last first — is tool-defined and pinned by the trace golden; the pick is reported, and one executor alone is not; `explore` reaches every order) | | Taking a transition out of a composite state exits the states being left innermost-first, then runs the effect, then enters the target; leaving a composite with orthogonal regions exits every active region first | `state_executor.go` transitionToInto (exit to the least common ancestor), exitStates/exitedByAncestorRegion (a state whose region another state being left owns is exited by that state's recursive region teardown, so the chain walk does not exit it a second time), `state_region_transition.go` leaveRegion (which instead clears the region a state is active in, recording its history, before exiting that state, since a region's active state may be nested below it), moveBetweenRegions, exitRegionTo, leaveTopRegions | `conformance/state_composite_exit_order.sysml` + trace golden (two levels of nesting), `:state_composite_orthogonal_exit.sysml` + trace golden, `:state_composite_nested_regions_exit_once.sysml` + trace golden (a region holding a composite with a region of its own: every level exits exactly once), `robustness_test.go:exit_of_nested_regions_with_a_history_pseudostate` | ✅ Faithful | | Every state transition is external — its source is exited, its effect runs, and its target is entered afresh — including when the target is the source itself or one of its substates: KerML orders `transitionLinkSource then effect` and `effect then transitionLink.laterOccurrence` (Kernel Semantic Library `TransitionPerformances.kerml`, `TransitionPerformance`), the source's `exit` is its last step (`StatePerformances.kerml`, `StatePerformance`: `entry then middle`, `middle then exit`) and a state transition orders that exit after its guard (`StateTransitionPerformance`: `guard then transitionLinkSource.exit`). So a simple state transitioning to itself runs exit, effect, entry, and a composite is exited and re-entered around the effect with its regions restarting at their initial states | `state_executor.go` transitionToInto, encloses (the source is the target or contains it); `state_region_transition.go` moveBetweenRegions (the exit boundary is the source's parent where the source `encloses` the target, so a composite self-transitioning inside an orthogonal region is exited too, while its sibling regions stay as they were) | `conformance/state_composite_self_transition.sysml` + trace golden (exit substate, exit composite, effect, re-enter composite and its region), `:state_composite_to_substate.sysml` + trace golden, `:state_composite_self_transition_in_region.sysml` + trace golden, `:w6e_state_simple_self_transition.sysml` + trace golden (exit, effect, entry on a simple state), `parse/w6e_state_self_transition.golden`, `state_composite_transition_test.go:TestOneEventTakesACompositesTransitionOnce`, `w6e_state_self_transition_test.go:TestSimpleSelfTransitionExitsAndReEntersItsState`, `:TestSimpleSelfTransitionInARegionLeavesSiblingRegionsAlone`, `robustness_test.go:composite_self_transition_with_no_substate_to_re_enter`, `w6e_robustness_test.go:TestSimpleSelfTransitionThatNeverSettlesIsBounded`, `:TestSimpleSelfTransitionEffectReadingAnUnknownFeatureIsReported`; `conformance/state_transition_guard_exit_effect_entry_order.sysml` + trace golden (the order made observable through values: the guard reads the pre-exit value, the effect the exit's, the entry the effect's — derived from the same library text in [the semantic oracle](behavior-semantic-oracle.md)) | ✅ Faithful (self-assessed: the pinned reference has no execution surface for state machines, so this row is assessed against the library text cited above and our own goldens, not against another implementation. One residual is tool-defined: a composite state stating no starting substate — no `initial` and no region — is re-entered with no substate active, since nothing names the substate to enter) | | An event reaches only the regions still active when it is dispatched | `state_executor.go` broadcastEvent (each active leaf is re-checked before it is offered the event) | `state_composite_transition_test.go:TestExitedNestedRegionDoesNotReactToTheSameEvent` | ✅ Faithful | diff --git a/internal/exec/runtime/advance.go b/internal/exec/runtime/advance.go index d598d44e56..db23790041 100644 --- a/internal/exec/runtime/advance.go +++ b/internal/exec/runtime/advance.go @@ -236,21 +236,59 @@ func (ctx *Context) drawDueOrder(due []clockWaiter) (int, error) { // contended reports whether a move w may make next depends on a move another // executor may make before it at this instant, under a policy interleaving turns. func (ctx *Context) contended(w clockWaiter) bool { - if sched := ctx.scheduling(); !sched.interleavesTurns() && !sched.checking() { + if !ctx.gateFutures() { return false } - if ctx.futures == nil { - ctx.futures = newFutureFootprints(ctx) - } next := nextFootprint(w) for _, other := range ctx.rivals(w) { - if next.DependentBy(ctx.futures.executorFuture(other), ctx.channelsMeet(executorSelf(w), executorSelf(other))) { + if next.DependentBy(ctx.futures.executorFuture(other), ctx.relation(w, other)) { return true } } return false } +// gateFutures readies the futures of this instant's executors under a policy +// interleaving turns, reporting whether one does. +func (ctx *Context) gateFutures() bool { + if sched := ctx.scheduling(); !sched.interleavesTurns() && !sched.checking() { + return false + } + if ctx.futures == nil { + ctx.futures = newFutureFootprints(ctx) + } + ctx.futures.gate() + return true +} + +// endContended reports whether the driver's next move may end its run while +// another executor may still move at this instant: an end observes every place. +func (ctx *Context) endContended(driver clockWaiter) bool { + return mayEnd(driver) && ctx.gateFutures() && len(ctx.rivals(driver)) > 0 +} + +// mayEnd reports whether the executor's next move may end its performance: a +// token of an action that may, or a machine that can complete or terminate. +func mayEnd(w clockWaiter) bool { + switch exec := w.(type) { + case *ActionExecutor: + return exec.dynamics != nil || slices.ContainsFunc(exec.tokens, func(t Token) bool { return tokenMayEnd(exec, t) }) + case *StateExecutor: + return len(exec.graph.TopRegions) > 0 || len(exec.graph.Terminates) > 0 || slices.ContainsFunc(exec.graph.States, exec.graph.Completes) + } + return true +} + +// tokenMayEnd reports whether the token's next move may end the performance: a +// move out of a nested frame, past no unguarded succession, or reaching beyond its node. +func tokenMayEnd(exec *ActionExecutor, t Token) bool { + if t.frame != nil && t.frame != exec.root || standing(exec, t).Dynamic { + return true + } + edges := tokenGraphOf(exec, t).Edges[t.Location] + return len(edges) == 0 || slices.ContainsFunc(edges, func(e lower.ActionEdge) bool { return e.Guard != nil }) +} + // rivals are the executors other than w that may move at this instant before w's // next move: those due or on the stack, and those a rival's moves may wake. func (ctx *Context) rivals(w clockWaiter) []clockWaiter { @@ -280,7 +318,7 @@ func (ctx *Context) rivals(w clockWaiter) []clockWaiter { func (ctx *Context) wokenBy(idle clockWaiter, rivals []clockWaiter) bool { future := ctx.futures.executorFuture(idle) for _, rival := range rivals { - if ctx.futures.executorFuture(rival).DependentBy(future, ctx.channelsMeet(executorSelf(rival), executorSelf(idle))) { + if ctx.futures.executorFuture(rival).DependentBy(future, ctx.relation(rival, idle)) { return true } } @@ -321,7 +359,7 @@ func (ctx *Context) runTurn(w clockWaiter, progress *dueProgress) (bool, error) // yieldTurn draws the due order again before a driver's move contended by another // executor, running the executors the draw falls on before the driver goes on. func (ctx *Context) yieldTurn(driver clockWaiter, progress *dueProgress) error { - if ctx.body != nil || !ctx.contended(driver) { + if ctx.body != nil || !ctx.contended(driver) && !ctx.endContended(driver) { return nil } for _, w := range ctx.clock.waiters { diff --git a/internal/exec/runtime/check_reduce.go b/internal/exec/runtime/check_reduce.go index 8a9b595c0e..f62337f326 100644 --- a/internal/exec/runtime/check_reduce.go +++ b/internal/exec/runtime/check_reduce.go @@ -109,15 +109,23 @@ func triggerChannel(trans *lower.Transition) (lower.Channel, bool) { return lower.Channel{}, false } -// doStepFootprint is what one step of the state's do behavior runs: the rest of -// the behavior paused mid-way, covered by that behavior's, or the next one pending. +// doStepFootprint is what one step of the state's do behavior runs: a move of a +// token of the flow it runs, else the rest of the behavior paused mid-way, covered +// by that behavior's, or the next one pending. func doStepFootprint(e *StateExecutor, state ast.Node) lower.Footprint { for _, act := range e.doActions { if act.state != state { continue } - if act.run != nil { - return e.graph.BehaviorFootprints()[act.run.host.behavior.Node] + if run := act.run; run != nil { + if flow := runningFlow(run); flow != nil { + fp := lower.Footprint{Reads: []lower.Place{{Name: run.host.behavior.Owner.Name, State: run.host.behavior.Owner}}} + for _, t := range flow.tokens { + fp = unionFootprints(fp, standing(flow, t)) + } + return fp + } + return e.graph.BehaviorFootprints()[run.host.behavior.Node] } if len(act.pending) == 0 { return lower.Footprint{} @@ -136,18 +144,20 @@ func unionFootprints(f, g lower.Footprint) lower.Footprint { Control: append(slices.Clone(f.Control), g.Control...), Completion: f.Completion || g.Completion, Dynamic: f.Dynamic || g.Dynamic, + Creates: f.Creates || g.Creates, + Routes: f.Routes || g.Routes, } } // dependent reports whether the two moves may not commute: the moves of one // unit never do, and otherwise their footprints decide. func (c *checker) dependent(a, b searchMove) bool { - return a.unit() == b.unit() || a.footprint.DependentBy(b.footprint, c.meet(a.Owner, b.Owner)) + return a.unit() == b.unit() || a.footprint.DependentBy(b.footprint, c.relation(a.Owner, b.Owner)) } -// meet is which message operations of the two executors may not commute. -func (c *checker) meet(a, b clockWaiter) lower.ChannelsMeet { - return c.ctx.channelsMeet(executorSelf(a), executorSelf(b)) +// relation is what is known of the two executors moves belong to. +func (c *checker) relation(a, b clockWaiter) lower.Relation { + return c.ctx.relation(a, b) } // persistent selects the moves to explore from a state, less the moves asleep; @@ -241,19 +251,16 @@ func newPersistentClosure(c *checker, all []searchMove) *persistentClosure { return p } -// include adds a unit: its moves when it has some, else the units whose -// future may let it go on. +// include adds a unit: its moves, and the units whose future may let it go on +// or meet any move it may make next, enabled or not. func (p *persistentClosure) include(u tokenKey) { if p.in[u] { return } p.in[u] = true - if slices.ContainsFunc(p.all, func(m searchMove) bool { return m.unit() == u }) { - return - } standing := p.standing[u] for _, other := range p.units { - if !p.in[other] && p.future[other].DependentBy(standing, p.c.meet(other.owner, u.owner)) { + if !p.in[other] && p.future[other].DependentBy(standing, p.c.relation(other.owner, u.owner)) { p.include(other) } } @@ -264,7 +271,7 @@ func (p *persistentClosure) include(u tokenKey) { func (p *persistentClosure) futureDependsOnSet(u tokenKey) bool { future := p.future[u] for _, m := range p.all { - if p.in[m.unit()] && future.DependentBy(m.footprint, p.c.meet(u.owner, m.Owner)) { + if p.in[m.unit()] && future.DependentBy(m.footprint, p.c.relation(u.owner, m.Owner)) { return true } } @@ -290,3 +297,14 @@ func (c *checker) childSleep(f *checkFrame, m searchMove) []searchMove { } return sleep } + +// runningFlow is the flow a do run steps a token of at a time: that of a behavior +// whose body states one, under way with a token and not held at a wait; nil otherwise. +func runningFlow(run *doRun) *ActionExecutor { + behavior := run.host.behavior + graph, flow := statedFlow(behavior), run.host.flow + if graph == nil || flow == nil || flow.graph != graph || run.body.paused.wait.held != nil || len(flow.tokens) == 0 || behavior.Owner == nil { + return nil + } + return flow +} diff --git a/internal/exec/runtime/future_footprint.go b/internal/exec/runtime/future_footprint.go index 9ac68f7206..1340aa07c9 100644 --- a/internal/exec/runtime/future_footprint.go +++ b/internal/exec/runtime/future_footprint.go @@ -16,12 +16,23 @@ type futureKey struct { // futureFootprints memoizes what executors may still touch at the clock's instant: // a token's by its node in its flow, a delay by whether it ends the instant; both // are dropped once the clock moves. A machine's whole graph is kept by graph. +// Once gated, senders are the sends any executor may make at this instant, and +// anySender marks an executor that may send anything. type futureFootprints struct { - ctx *Context - now float64 - nodes map[futureKey]lower.Footprint - ends map[*ast.TimeEvent]bool - machines map[*lower.StateGraph]lower.Footprint + ctx *Context + now float64 + nodes map[futureKey]lower.Footprint + ends map[*ast.TimeEvent]bool + machines map[*lower.StateGraph]lower.Footprint + gated bool + senders []futureSend + anySender bool +} + +// futureSend is a send an executor run for from may make at this instant. +type futureSend struct { + channel lower.Channel + from *Instance } // newFutureFootprints reads the clock of ctx, which bind replaces. @@ -63,6 +74,53 @@ func (f *futureFootprints) endsInstant(trigger ast.Node, scope *symbols.Scope) b return ends } +// gate gathers what every executor may send at this instant, from its future +// with every message-triggered transition open, so a machine's future leaves out +// a transition no message queued or sendable at this instant can fire. +func (f *futureFootprints) gate() { + f.at() + f.gated, f.senders, f.anySender = false, f.senders[:0], len(f.ctx.pendingBehaviors) > 0 + for _, w := range f.ctx.clock.waiters { + if f.anySender { + break + } + if w.finished() { + continue + } + future := f.executorFuture(w) + f.anySender = future.Dynamic + for _, c := range future.Sends { + f.senders = append(f.senders, futureSend{channel: c, from: executorSelf(w)}) + } + } + f.gated = true +} + +// cannotFire reports whether no message the transition's accept takes is queued +// or may be sent at this instant, once gated: its trigger cannot occur before the clock moves. +func (f *futureFootprints) cannotFire(e *StateExecutor, trans *lower.Transition) bool { + accept, ok := trans.Trigger.(*ast.AcceptEvent) + if !f.gated || f.anySender || !ok { + return false + } + want := ast.AsQualifiedName(accept.SignalType) + if want == nil { + return false + } + for _, m := range f.ctx.messages { + if f.ctx.messageMatches(m, want, trans.Scope) { + return false + } + } + consumer, _ := triggerChannel(trans) + for _, send := range f.senders { + if f.ctx.sendMeets(send.channel, send.from, consumer, e.self) { + return false + } + } + return true +} + // executorFuture is what the executor may still touch at this instant: every // token's future for an action, the machine's for a state machine, everything // for any other. @@ -217,7 +275,7 @@ func (f *futureFootprints) machineFuture(e *StateExecutor) lower.Footprint { } seen[state] = true for _, trans := range e.graph.Transitions[state] { - if !(active[state] && timerDue) && f.endsInstant(trans.Trigger, trans.Scope) { + if !(active[state] && timerDue) && f.endsInstant(trans.Trigger, trans.Scope) || f.cannotFire(e, trans) { continue } step, ok := steps[trans] diff --git a/internal/exec/runtime/message_dependence.go b/internal/exec/runtime/message_dependence.go index 1a34c6aee7..c2f485a751 100644 --- a/internal/exec/runtime/message_dependence.go +++ b/internal/exec/runtime/message_dependence.go @@ -24,16 +24,80 @@ func (ctx *Context) channelsMeet(a, b *Instance) lower.ChannelsMeet { return func(x lower.Channel, xSends bool, y lower.Channel, ySends bool) bool { switch { case xSends && ySends: - return true + return !(x.Own && y.Own && objectsApart(a, b)) case xSends: - return ctx.sendMeets(x, y) + return ctx.sendMeets(x, a, y, b) case ySends: - return ctx.sendMeets(y, x) + return ctx.sendMeets(y, b, x, a) } return ctx.consumersMeet(x, a, y, b) } } +// relation is what is known of executors a and b, which two moves belong to: +// whether they are two, run for two objects, and which message operations meet. +func (ctx *Context) relation(a, b clockWaiter) lower.Relation { + sa, sb := executorSelf(a), executorSelf(b) + rel := lower.Relation{Channels: ctx.channelsMeet(sa, sb), Apart: a != b} + if rel.Apart && objectsApart(sa, sb) { + rel.Objects = true + rel.Held = func(p, q lower.Place) bool { + x, y := ctx.slotHolder(a, p.Sym), ctx.slotHolder(b, q.Sym) + return x != nil && y != nil && x != y + } + } + return rel +} + +// objectsApart reports whether a and b are two objects. +func objectsApart(a, b *Instance) bool { + return objectID(a) != 0 && objectID(b) != 0 && objectID(a) != objectID(b) +} + +// ownsFeature reports whether sym is a feature of the object's own, so a name written +// alone and resolving to it, in a behavior the object runs, names the object's slot. +func (ctx *Context) ownsFeature(inst *Instance, sym *symbols.Symbol) bool { + if sym == nil { + return false + } + for _, of := range ctx.FeaturesOfObject(inst) { + if of.Feature.Symbol == sym { + return true + } + } + return false +} + +// slotHolder is what holds the value a name resolving to sym names in a move of +// w's: the machine's own data or performance for its attribute, the object w runs +// for for that object's feature; nil when neither is known. +func (ctx *Context) slotHolder(w clockWaiter, sym *symbols.Symbol) any { + if sym == nil { + return nil + } + if e, ok := w.(*StateExecutor); ok { + for _, attr := range e.graph.Attributes { + if attr.Node == sym.Decl { + if e.occurrence != nil { + return e.occurrence.ID + } + return e + } + } + for _, attrs := range e.graph.StateAttributes { + for _, attr := range attrs { + if attr.Node == sym.Decl { + return e + } + } + } + } + if self := executorSelf(w); ctx.ownsFeature(self, sym) { + return self.ID + } + return nil +} + // executorSelf is the object an executor runs for, nil for none. func executorSelf(w clockWaiter) *Instance { switch exec := w.(type) { @@ -45,9 +109,13 @@ func executorSelf(w clockWaiter) *Instance { return nil } -// sendMeets reports whether a send may give or take a message the consumer -// would see: a dispatch may drop a message sent to its object, never one a port carries. -func (ctx *Context) sendMeets(send, consumer lower.Channel) bool { +// sendMeets reports whether a send by an executor run for from may give or take +// a message a consumer run for at would see: a message for the sending object +// reaches no other's, and a dispatch may drop one sent to its object, never one a port carries. +func (ctx *Context) sendMeets(send lower.Channel, from *Instance, consumer lower.Channel, at *Instance) bool { + if send.Own && objectsApart(from, at) { + return false + } if consumer.Drops { return !send.Via } diff --git a/internal/exec/runtime/testdata/check/reduction_expected.txt b/internal/exec/runtime/testdata/check/reduction_expected.txt index 2dcfbf303d..048f10952c 100644 --- a/internal/exec/runtime/testdata/check/reduction_expected.txt +++ b/internal/exec/runtime/testdata/check/reduction_expected.txt @@ -12,7 +12,7 @@ 44 78 123 306 por_alias 18 19 19 22 por_address 49 51 58 79 por_streaming_flow -19 21 19 22 por_constructor +18 19 19 22 por_constructor 13 13 30 38 por_state_independent 15 16 17 20 por_state_effect_write 15 16 17 20 por_state_guard_read diff --git a/internal/frontend/repl/explore_test.go b/internal/frontend/repl/explore_test.go index b85c2b60a7..54b67d02c7 100644 --- a/internal/frontend/repl/explore_test.go +++ b/internal/frontend/repl/explore_test.go @@ -501,7 +501,7 @@ func TestRunForExploresSiblingsOnOneRoot(t *testing.T) { wantsInOrder(t, out, "✓ explored Comms::Ground::listen Comms::pair.ground, Comms::Craft::modes Comms::pair.craft: 2 outcomes", "Comms::Craft::modes Comms::pair.craft.emitted = 4", "Comms::Ground::listen Comms::pair.ground.received = 1", "Comms::Craft::modes Comms::pair.craft.emitted = 4", "Comms::Ground::listen Comms::pair.ground.received = 2", - "complete (33 runs)") + "complete (5 runs)") if len(verdicts[0].Outcomes) != 2 { t.Errorf("outcomes = %+v, want two", verdicts[0].Outcomes) } diff --git a/internal/ir/lower/footprint.go b/internal/ir/lower/footprint.go index a1e4edd89a..70e11d62b4 100644 --- a/internal/ir/lower/footprint.go +++ b/internal/ir/lower/footprint.go @@ -18,11 +18,13 @@ import ( // Place is one feature a move reads or writes: the declaration the name resolves to // (nil when unresolved) and the name; Local marks a pin, held per performance. // State marks the activity of a state, which a transition reads and writes. +// Direct marks a name written alone, not reached through a chain or qualified. type Place struct { - Sym *symbols.Symbol - Name string - Local bool - State *ast.StateNode + Sym *symbols.Symbol + Name string + Local bool + State *ast.StateNode + Direct bool } // Conflicts reports whether the two places may name one value: places resolving @@ -59,7 +61,7 @@ func (p Place) String() string { // ("" for any) and the port it travels through ("" for none). Type is the accept's // type reference and Message the send's message, each resolving in Scope; Via marks // a send routed by connections, Drops a machine's dispatch, which may discard a -// message sent to its object. +// message sent to its object. Own marks a send naming no target, for the sending object. type Channel struct { Signal string Port string @@ -68,6 +70,7 @@ type Channel struct { Scope *symbols.Scope Via bool Drops bool + Own bool } func (c Channel) String() string { @@ -84,6 +87,8 @@ func (c Channel) String() string { // Footprint is what one atomic move (one token advancing one node, one transition // firing) may touch. Control lists the joins and merges it arrives at; Completion // marks a move that may queue a completion event; Dynamic an unresolved target. +// Creates marks a move that may create an object starting no behavior; Routes one +// sending through connections, which reads whatever the objects' structure holds. type Footprint struct { Reads []Place Writes []Place @@ -92,35 +97,58 @@ type Footprint struct { Control []ast.Node Completion bool Dynamic bool + Creates bool + Routes bool } // Dependent reports whether the two moves may not commute: a data race, both // touching the bus (a send meeting an accept, two accepts competing for one message, // two sends ordering it), both queuing a completion, convergence on one join or -// merge, or a dynamic target. +// merge, creation meeting creation or an extent, routing meeting a structural +// write, or a dynamic target. func (f Footprint) Dependent(g Footprint) bool { - return f.DependentBy(g, nil) + return f.DependentBy(g, Relation{}) } // ChannelsMeet reports whether a message operation of one move may not commute // with one of another: each channel with whether it sends. type ChannelsMeet func(a Channel, aSends bool, b Channel, bSends bool) bool -// DependentBy is Dependent with meet deciding which message operations meet; -// a nil meet has every two meet. -func (f Footprint) DependentBy(g Footprint, meet ChannelsMeet) bool { +// Relation is what is known of the executors two moves belong to. Channels decides +// which message operations meet, nil having every two meet. Apart marks two +// executors, each converging on control nodes of its own; Objects two run for two +// objects, each holding its own pins and state activity, and Held, where set, reports +// whether a direct place of the first move's and one of the second's are slots of different objects. +type Relation struct { + Channels ChannelsMeet + Apart bool + Objects bool + Held func(p, q Place) bool +} + +// DependentBy is Dependent under what rel knows of the moves' executors. +func (f Footprint) DependentBy(g Footprint, rel Relation) bool { if f.Dynamic || g.Dynamic { return true } - if placesMeet(f.Writes, g.Reads) || placesMeet(f.Writes, g.Writes) || placesMeet(g.Writes, f.Reads) { + if rel.placesMeet(f.Writes, g.Reads) || rel.placesMeet(f.Writes, g.Writes) || rel.placesMeet(f.Reads, g.Writes) { return true } - if f.messagesMeet(g, meet) { + if f.messagesMeet(g, rel.Channels) { return true } if f.Completion && g.Completion { return true } + if f.Creates && (g.Creates || readsExtent(g.Reads)) || g.Creates && readsExtent(f.Reads) { + return true + } + if f.Routes && rel.writesStructure(g.Writes) || g.Routes && rel.writesStructure(f.Writes) { + return true + } + if rel.Apart { + return false + } for _, node := range f.Control { for _, other := range g.Control { if node == other { @@ -131,6 +159,62 @@ func (f Footprint) DependentBy(g Footprint, meet ChannelsMeet) bool { return false } +// placesMeet reports whether a place of the first move's, among as, may name the +// value of one of the second's, among bs. +func (rel Relation) placesMeet(as, bs []Place) bool { + for _, a := range as { + for _, b := range bs { + if a.Conflicts(b) && !rel.held(a, b) { + return true + } + } + } + return false +} + +// held reports whether two conflicting places, the first move's and the +// second's, are nonetheless two values. +func (rel Relation) held(p, q Place) bool { + if !rel.Objects { + return false + } + if p.Local || q.Local || p.State != nil || q.State != nil { + return true + } + return p.Direct && q.Direct && rel.Held != nil && rel.Held(p, q) +} + +// readsExtent reports whether a read may be of what objects exist: of anything +// but a state's activity, a pin or a declared feature. +func readsExtent(reads []Place) bool { + for _, p := range reads { + if p.State == nil && !p.Local && (p.Sym == nil || !isFeatureSymbol(p.Sym)) { + return true + } + } + return false +} + +// writesStructure reports whether a write may change what a connection reaches: +// any but of an attribute or a state's activity, or of another executor's pin. +func (rel Relation) writesStructure(writes []Place) bool { + for _, p := range writes { + if p.State != nil || p.Local && rel.Objects { + continue + } + if p.Sym == nil || p.Sym.Kind != symbols.SymbolAttributeUsage { + return true + } + } + return false +} + +// isFeatureSymbol reports whether the symbol is a usage, which holds values rather than classifying them. +func isFeatureSymbol(sym *symbols.Symbol) bool { + _, usage := sym.Decl.(*ast.Usage) + return usage +} + func (f Footprint) messagesMeet(g Footprint, meet ChannelsMeet) bool { if !f.messages() || !g.messages() { return false @@ -160,17 +244,6 @@ func (f Footprint) messages() bool { return len(f.Sends) > 0 || len(f.Accepts) > 0 } -func placesMeet(as, bs []Place) bool { - for _, a := range as { - for _, b := range bs { - if a.Conflicts(b) { - return true - } - } - } - return false -} - // String renders the footprint one clause per line, names sorted, for tests and // the checker's report. func (f Footprint) String() string { @@ -212,6 +285,12 @@ func (f Footprint) String() string { if f.Completion { b.WriteString("completion\n") } + if f.Creates { + b.WriteString("creates\n") + } + if f.Routes { + b.WriteString("routes\n") + } if f.Dynamic { b.WriteString("dynamic\n") } @@ -253,7 +332,7 @@ func declaredFeatures(graph *ActionGraph) map[ast.Node]bool { // footprintOf projects the footprint of one node from the graph's side tables; // declared is declaredFeatures(graph). func footprintOf(graph *ActionGraph, node ast.Node, declared map[ast.Node]bool) Footprint { - b := &footprintBuilder{graph: graph, node: node, scope: nodeScopeOf(graph, node), declared: declared} + b := &footprintBuilder{resolver: graph.resolver, graph: graph, node: node, scope: nodeScopeOf(graph, node), declared: declared} if nodePerformsAction(node) { // The performed action runs in an executor of its own; what it touches is its. b.footprint.Dynamic = true @@ -291,6 +370,8 @@ func nodeScopeOf(graph *ActionGraph, node ast.Node) *symbols.Scope { } type footprintBuilder struct { + // resolver reads a name the scope tree alone does not reach, nil for none. + resolver *resolve.Resolver graph *ActionGraph node ast.Node scope *symbols.Scope @@ -327,14 +408,15 @@ func (b *footprintBuilder) place(scope *symbols.Scope, segments []string, each f name := segments[len(segments)-1] sym, _ := resolve.FeatureSymbolInScope(scope, segments) local := sym != nil && b.declaredByNode(sym) - each(Place{Sym: sym, Name: name, Local: local}) + direct := len(segments) == 1 + each(Place{Sym: sym, Name: name, Local: local, Direct: direct}) if sym == nil { return } if usage, ok := sym.Decl.(*ast.Usage); ok { for _, redefined := range redefinedNames(usage) { if redefined != name { - each(Place{Sym: sym, Name: redefined, Local: local}) + each(Place{Sym: sym, Name: redefined, Local: local, Direct: direct}) } } } @@ -404,8 +486,12 @@ func (b *footprintBuilder) reads(scope *symbols.Scope, expr ast.Node) { b.reads(scope, e.Operand) b.reads(scope, e.Body) case *ast.ConstructorExpr: - // Constructing an object extends its type's extent and starts classifier behaviors. - b.footprint.Dynamic = true + // Constructing an object extends its type's extent and may start classifier behaviors. + if plainType(scope, e.Type) { + b.footprint.Creates = true + } else { + b.footprint.Dynamic = true + } for _, arg := range e.Args { b.reads(scope, arg) } @@ -445,10 +531,19 @@ func (b *footprintBuilder) readName(scope *symbols.Scope, qn *ast.QualifiedName) return } if len(qn.Parts) == 1 { - b.place(scope, []string{qn.Parts[0].Text}, b.read) - return + if _, found := resolve.FeatureSymbolInScope(scope, []string{qn.Parts[0].Text}); found || b.resolver == nil { + b.place(scope, []string{qn.Parts[0].Text}, b.read) + return + } } - b.read(Place{Name: qn.Parts[len(qn.Parts)-1].Text}) + name := qn.Parts[len(qn.Parts)-1].Text + if b.resolver != nil { + if sym, ok := b.resolver.ReadQualified(scope, qn).Symbol(); ok && sym != nil { + b.read(Place{Sym: sym, Name: name, Local: b.declaredByNode(sym), Direct: len(qn.Parts) == 1}) + return + } + } + b.read(Place{Name: name}) } // invokesDeclaredBehavior reports whether an invocation names a calc or action the @@ -503,10 +598,11 @@ func (b *footprintBuilder) statement(stmt Statement) { b.footprint.Dynamic = true } if s.IsVia { - // A `via` send is routed by connections at run time. - b.footprint.Dynamic = true + // A `via` send is routed by connections at run time, materializing the ports it reaches. + b.footprint.Routes, b.footprint.Creates = true, true } - b.footprint.Sends = append(b.footprint.Sends, Channel{Port: viaPortOf(s), Message: s.Message, Scope: s.Scope, Via: s.IsVia}) + own := s.Target == "" && s.TargetExpr == nil && s.Receiver == "" && s.ReceiverExpr == nil && !s.IsVia + b.footprint.Sends = append(b.footprint.Sends, Channel{Port: viaPortOf(s), Message: s.Message, Scope: s.Scope, Via: s.IsVia, Own: own}) case Declare: b.reads(s.Scope, s.Value) b.write(Place{Name: s.Name}) @@ -610,6 +706,27 @@ func (b *footprintBuilder) merge(other Footprint) { b.footprint.Control = append(b.footprint.Control, other.Control...) b.footprint.Completion = b.footprint.Completion || other.Completion b.footprint.Dynamic = b.footprint.Dynamic || other.Dynamic + b.footprint.Creates = b.footprint.Creates || other.Creates + b.footprint.Routes = b.footprint.Routes || other.Routes +} + +// plainType reports whether constructing the named type creates an object that +// starts no behavior and evaluates nothing: a non-abstract item, attribute, part or +// port definition declaring no member and specializing nothing explicitly. +func plainType(scope *symbols.Scope, qn *ast.QualifiedName) bool { + if scope == nil || qn == nil { + return false + } + decl, _, ok := resolve.TypeDeclInScope(scope, qn) + def, isDef := decl.(*ast.Definition) + if !ok || !isDef || def.IsAbstract || len(def.Members) > 0 || len(def.Relationships) > 0 || len(def.Prefixes) > 0 { + return false + } + switch def.Kind { + case ast.DefItem, ast.DefAttribute, ast.DefPart, ast.DefPort: + return true + } + return false } func viaPortOf(s Send) string { diff --git a/internal/ir/lower/footprint_test.go b/internal/ir/lower/footprint_test.go index 21e7a38b45..c3c76ea262 100644 --- a/internal/ir/lower/footprint_test.go +++ b/internal/ir/lower/footprint_test.go @@ -305,11 +305,13 @@ func TestFootprintPinsAndBindings(t *testing.T) { } } -// A `via` send, a chain from a computed base, a nested performance and a -// constructor are dynamic targets, dependent on every other move. +// A chain from a computed base, a nested performance and a constructor of a type +// that evaluates or starts anything are dynamic targets, dependent on every other +// move; a plain constructor creates and a `via` send routes and creates. func TestFootprintDynamicTargets(t *testing.T) { graph := scopedActionGraph(t, ` item def Ping; + item def Busy { attribute a : Integer = 1; } action def Dynamic { attribute x : Integer = 0; attribute made : Ping; @@ -326,6 +328,7 @@ func TestFootprintDynamicTargets(t *testing.T) { } action construct { assign made := new Ping(); } action sendNew { send new Ping() to p; } + action constructBusy { assign made := new Busy(); } join sync; done; succession first start then split; @@ -335,12 +338,14 @@ func TestFootprintDynamicTargets(t *testing.T) { succession first split then nested; succession first split then construct; succession first split then sendNew; + succession first split then constructBusy; succession first viaSend then sync; succession first writeX then sync; succession first typed then sync; succession first nested then sync; succession first construct then sync; succession first sendNew then sync; + succession first constructBusy then sync; succession first sync then done; } action def Add { in a : Integer; out r : Integer; } @@ -350,21 +355,31 @@ func TestFootprintDynamicTargets(t *testing.T) { t.Errorf("a node performing an action is not dynamic:\n%s", typed) } for _, name := range []string{"construct", "sendNew"} { - if fp := footprintNamed(t, graph, name); !fp.Dynamic { - t.Errorf("%s materializes an object yet is not dynamic:\n%s", name, fp) + if fp := footprintNamed(t, graph, name); fp.Dynamic || !fp.Creates { + t.Errorf("%s creates a plain object: want it creating, not dynamic:\n%s", name, fp) } } + if busy := footprintNamed(t, graph, "constructBusy"); !busy.Dynamic { + t.Errorf("constructing a type that evaluates a default is not dynamic:\n%s", busy) + } + construct, sendNew := footprintNamed(t, graph, "construct"), footprintNamed(t, graph, "sendNew") + if !construct.Dependent(sendNew) || !sendNew.Dependent(construct) { + t.Error("two creations commute") + } viaSend := footprintNamed(t, graph, "viaSend") - if !viaSend.Dynamic { - t.Errorf("via send footprint:\n%s\nwant dynamic", viaSend) + if viaSend.Dynamic || !viaSend.Routes || !viaSend.Creates { + t.Errorf("via send footprint:\n%s\nwant routing and creating, not dynamic", viaSend) } if len(viaSend.Sends) != 1 || viaSend.Sends[0].Port != "p" { t.Errorf("via send channels = %v, want [via p]", viaSend.Sends) } + if !viaSend.Dependent(construct) || !construct.Dependent(viaSend) { + t.Error("a via send commutes with a creation") + } writeX := footprintNamed(t, graph, "writeX") - if !viaSend.Dependent(writeX) || !writeX.Dependent(viaSend) { - t.Error("a dynamic move is independent of a write") + if apart := (Relation{Apart: true}); viaSend.DependentBy(writeX, apart) || writeX.DependentBy(viaSend, apart) { + t.Error("another executor's via send depends on a write of an attribute routing reads none of") } nested := footprintNamed(t, graph, "nested") if nested.Dynamic { diff --git a/internal/ir/lower/state_footprint.go b/internal/ir/lower/state_footprint.go index a639d548c4..973e74b1f7 100644 --- a/internal/ir/lower/state_footprint.go +++ b/internal/ir/lower/state_footprint.go @@ -59,7 +59,7 @@ func (g *StateGraph) lowerFootprints() { // behaviorFootprint is what running the behavior's statements touches, and the // activity of the state it belongs to, which stopping it writes. func behaviorFootprint(graph *StateGraph, behavior StateBehavior) Footprint { - b := &footprintBuilder{} + b := &footprintBuilder{resolver: graph.resolver} b.statements(behavior.Body) if behavior.Owner != nil { b.read(graph.activity(behavior.Owner)) @@ -80,7 +80,7 @@ func transitionFootprint(graph *StateGraph, trans *Transition) Footprint { // transitionBuilder projects a transition out of a state, without the do // behaviors of the states it enters when withoutDo is set. func transitionBuilder(graph *StateGraph, trans *Transition, withoutDo bool) *stateFootprintBuilder { - b := &stateFootprintBuilder{footprintBuilder: &footprintBuilder{}, graph: graph, crossed: make(map[*ast.PseudostateNode]bool), withoutDo: withoutDo} + b := &stateFootprintBuilder{footprintBuilder: &footprintBuilder{resolver: graph.resolver}, graph: graph, crossed: make(map[*ast.PseudostateNode]bool), withoutDo: withoutDo} source := trans.Source.(*ast.StateNode) b.read(graph.activity(source)) b.trigger(trans) From efa037c27b5b99c18ebe48020ad1caf4a24ae91a Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 23:01:10 +0000 Subject: [PATCH 3/3] fix(runtime): count a machine's held entry as its move when turns interleave Co-Authored-By: jason.han --- cmd/sysml/explore_turns_test.go | 55 +++++++++++++++++++++++++ internal/exec/runtime/state_executor.go | 27 +++++++----- 2 files changed, 71 insertions(+), 11 deletions(-) diff --git a/cmd/sysml/explore_turns_test.go b/cmd/sysml/explore_turns_test.go index 074e162935..167452c66c 100644 --- a/cmd/sysml/explore_turns_test.go +++ b/cmd/sysml/explore_turns_test.go @@ -74,3 +74,58 @@ func TestExploreInterleavesExecutorsMoveByMove(t *testing.T) { } } } + +// heldEntryModel has a machine whose timer transition holds work's entry cascade +// while the Go it sends is still to be dispatched, and an action due at the same +// instant that reads what the cascade writes. +const heldEntryModel = `package Held { + private import ScalarValues::*; + item def Go; + part def P { + attribute order : Integer = 0; + attribute seen : Integer = 0; + state m parallel { + state left { + entry; then prep; + state prep; + state work { + ref :>> runToCompletionScope = self; + state inner { entry action { assign order := order * 10 + 1; } } + entry action { send new Go() to m; } then inner; + } + transition first prep accept after 1 [SI::s] then work; + } + state right { + entry; then a; + state a; + state b { entry action { assign order := order * 10 + 2; } } + transition first a accept Go then b; + } + } + action peek { + first start; + then action wait accept after 1 [SI::s]; + then action read assign seen := order; + then done; + } + } + part p : P; +} +` + +// TestExploreRunsAHeldEntryAsAMove checks that resuming a held entry counts as the +// machine's move, so the Go queued behind it is still dispatched at the instant. +func TestExploreRunsAHeldEntryAsAMove(t *testing.T) { + binary := buildCLI(t) + invocation := []string{"-instantiate", "Held::p", "-state", "Held::P::m Held::p", "-action", "Held::P::peek Held::p", "-advance", "1"} + + explored := check(t, binary, heldEntryModel, append([]string{"-schedule", "explore"}, invocation...)...) + wantReport(t, explored, 0, "✓ explored Held::P::peek, Held::P::m: 10 outcomes", "this.order = 12; this.seen = 1", "complete (") + if strings.Contains(explored.output(), `finalState = "inner+a"`) { + t.Errorf("an explored run left Go undispatched at the instant it was sent:\n%s", explored.output()) + } + for seed := 1; seed <= 8; seed++ { + got := check(t, binary, heldEntryModel, append([]string{"-schedule", fmt.Sprintf("seed:%d", seed)}, invocation...)...) + wantReport(t, got, 0, "Current state: inner | b") + } +} diff --git a/internal/exec/runtime/state_executor.go b/internal/exec/runtime/state_executor.go index 09d059ee28..074169e01e 100644 --- a/internal/exec/runtime/state_executor.go +++ b/internal/exec/runtime/state_executor.go @@ -3457,10 +3457,11 @@ func (e *StateExecutor) RunToQuiescence() error { // once nothing is due it advances to the earliest wait, running whatever is due there. func (e *StateExecutor) run(atCurrentTime bool) error { var progress dueProgress - return e.runCounting(atCurrentTime, false, &progress) + _, err := e.runCounting(atCurrentTime, false, &progress) + return err } -func (e *StateExecutor) runCounting(atCurrentTime, single bool, progress *dueProgress) (err error) { +func (e *StateExecutor) runCounting(atCurrentTime, single bool, progress *dueProgress) (moved bool, err error) { defer e.ctx.beginExecutorRun(&e.driven)() defer e.completedWhole(&err) wasRunning := e.inRun @@ -3476,26 +3477,27 @@ func (e *StateExecutor) runCounting(atCurrentTime, single bool, progress *duePro for e.state == StateRunning { stepped, err := e.runUnit(progress) if err != nil { - return err + return moved, err } if stepped { + moved = true progress.unsettle() if e.callReleased() { - return nil + return moved, nil } if single { - return nil + return moved, nil } if !atCurrentTime { if err := e.ctx.yieldTurn(e, progress); err != nil { - return err + return moved, err } } continue } if atCurrentTime { e.state = StateSuspended - return nil + return moved, nil } // Nothing left at this instant: the others due run, then the clock moves to the // earliest wait. Only a machine with a timer of its own running moves the clock. @@ -3503,7 +3505,7 @@ func (e *StateExecutor) runCounting(atCurrentTime, single bool, progress *duePro for { picked, err := e.ctx.runDue(e, progress) if err != nil { - return err + return moved, err } // Its turn: work is due, or a change condition it watches is to be polled. if picked || e.dueWork() { @@ -3511,11 +3513,11 @@ func (e *StateExecutor) runCounting(atCurrentTime, single bool, progress *duePro } if _, waiting := e.NextWait(); !waiting || !e.ctx.advanceToNextDue(progress) { e.state = StateSuspended - return nil + return moved, nil } } } - return nil + return moved, nil } // dueLabel names the machine in a due-order choice. @@ -3604,7 +3606,10 @@ func (e *StateExecutor) runMove(progress *dueProgress) (bool, error) { func (e *StateExecutor) runDueUnits(progress *dueProgress, single bool) (bool, error) { before := *progress - err := e.runCounting(true, single, progress) + stepped, err := e.runCounting(true, single, progress) + if single { + return stepped, err + } return progress.events > before.events || progress.doSteps > before.doSteps, err }