diff --git a/changes/unreleased/entry-transition-effects.added.md b/changes/unreleased/entry-transition-effects.added.md new file mode 100644 index 0000000000..7d256ead57 --- /dev/null +++ b/changes/unreleased/entry-transition-effects.added.md @@ -0,0 +1 @@ +- **Transitions out of a named entry action run effects and routes.** `entry action boot; transition boot do { … } then s;` runs its effect after the entry action and before `s` is entered, and may target a junction or choice of the same body, whose route is resolved after the entry action; availability checks only the incoming transition's own route, and a dead nested default-entry junction fails with a typed run error when its separate entry transition is taken. In a region of a parallel state the effect, like a compound transition's segment effect inside the region it enters, interleaves with the sibling regions' entries, and `-schedule explore` reaches every order. A trigger on such a transition, or an effect on the shorthand `entry; then s;`, is still rejected. diff --git a/changes/unreleased/state-change-trigger-writes.fixed.md b/changes/unreleased/state-change-trigger-writes.fixed.md new file mode 100644 index 0000000000..e0726d709f --- /dev/null +++ b/changes/unreleased/state-change-trigger-writes.fixed.md @@ -0,0 +1 @@ +- **Change triggers observe every completed write.** A state machine's `accept when ` is re-evaluated after each completed feature write that touches a feature the condition reads, and every false-to-true rise queues one change signal, so a condition that becomes true and false again within one run-to-completion step still fires; a value one assignment writes and replaces before it completes raises no rise. Snapshots, held images, replay and `-schedule explore` carry the observed and pending rises. diff --git a/docs/internals/design/precise-semantics-alignment.md b/docs/internals/design/precise-semantics-alignment.md index 9382f62f53..28de185d26 100644 --- a/docs/internals/design/precise-semantics-alignment.md +++ b/docs/internals/design/precise-semantics-alignment.md @@ -106,7 +106,7 @@ in the runtime package. File paths are relative to `internal/exec/runtime/` unle ### State machines (PSSM) -Rows are numbered SM1–SM45 so the count at the end of the map can be checked against them. +Rows are numbered SM1–SM46 so the count at the end of the map can be checked against them. #### The event pool and the run-to-completion step @@ -218,11 +218,12 @@ end, i.e. ahead of later arrivals. *Runtime:* `recallDeferredEvents` re-stamps a occurrence with the current clock time but keeps its arrival ID, so `eventHeap.Less` places it behind completion events at that instant and ahead of every later arrival, in its original order. `TestRecalledEventPrecedesLaterArrivals`, `TestDeferredEventsKeepTheirArrivalOrder`. **agrees.** -*Since removed:* with the extension gone, a kept occurrence is re-sent to `self` as the state is +The removed extension agreed with PSSM. *Since removed:* with it gone, a kept occurrence is +re-sent to `self` as the state is left, an ordinary send that lands behind every occurrence already pooled — the ones that arrived meanwhile and the ones the state's own exit behavior sent — and the kept occurrences of one signal replay in their arrival order but different signals in the order the flush names them, -not in one pooled order. **differs, v2 differs**: the standard encoding has no way to place a +not in one pooled order. **differs because v2 differs**: the standard encoding has no way to place a re-sent occurrence ahead of the pool, and this project no longer has a rule of its own to put there. *Deferred 001* and *Deferred 005* report on this row (`docs/project/pssm-referee.md`). @@ -730,7 +731,8 @@ it followed from the two functions and the comment. *Differs, v2 silent* as firs assessed — and a *Finding*, since the project's own design note says otherwise. *Decided:* PSSM's rule, and the project's own note. A route is resolved before firing only up to the first *choice*: junctions along it are resolved statically as before (SM29), as part -of whether the transition is enabled at all (SM32). Firing then exits the states every branch of the choice leaves (`travel` → +of whether that transition's own route is enabled (SM32); a nested default entry is a separate +transition whose junction is read when it is taken (SM46). Firing then exits the states every branch of the choice leaves (`travel` → `certainExits` over the targets `reachable` past it), runs the segments' effects up to the choice, and only then reads the choice's guards against the data as it now stands; one enabled branch is taken — several enabled is the existing transition choice point, recorded as @@ -745,28 +747,29 @@ seen` reaches `seen`), `state_choice_dynamic_conflict`, `state_pseudostate_chain `state_pseudostate_chain_choice_junction`, `state_pseudostate_chain_choice_choice`, `TestExploreDynamicChoiceBranches` and `robustness_test.go:state_choice_without_an_enabled_branch`; `state_choice_pseudostate` and the other `state_choice_*` cases keep their outcomes. **agrees** -since the decision. The two vertices no longer share one rule: a junction's guards are read -before the step and decide whether the transition is enabled (SM29, SM32), a choice's on arrival, +since the decision. The two vertices no longer share one rule: a junction's guards on the +transition's own route are read before the step and decide whether it is enabled (SM29, SM32); +a choice's are read on arrival, with none enabled the typed error (SM31). **SM31. Choice with no guard true.** PSSM requirement *Choice 003* (§9.4.10): "the model is considered ill formed". *Runtime:* `state_route.go:resolveChoice` fails the run at the instant the choice is reached, after the incoming segment's effect, with the typed `ErrChoiceWithoutBranch` naming the choice (`robustness_test.go:state_choice_without_an_enabled_branch`); a junction with no guard true -fails nothing, since the transition through it is not enabled (SM32, -`region_pseudostate_without_satisfied_guard`). **agrees.** - -**SM32. Junction or join with no path through.** PSSM requirement *Junction 002* (§9.4.11): when no outgoing guard holds, "the -entire compound transition is disabled even though its Triggers are enabled" — the incoming -transition is not selected, and the occurrence is deferred or lost like any other unhandled one. +fails nothing when it lies on the transition's own route, since that transition is not enabled +(SM32, `region_pseudostate_without_satisfied_guard`). A dead nested default-entry junction fails +when its separate entry transition is taken (SM46). **agrees.** + +**SM32. Junction or join with no path through.** PSSM §8.5.6 evaluates a junction on the +transition's route before selection; when no outgoing guard holds, "the entire compound +transition is disabled even though its Triggers are enabled" — the incoming transition is not +selected, and the occurrence is deferred or lost like any other unhandled one. *Runtime, before the decision:* the incoming transition was selected on its own trigger and guard; the failure to route surfaced as a "no guard evaluated to true" run failure when the route was resolved, not as a disabled transition (`region_pseudostate_without_satisfied_guard` used a -junction). *Junction 004* (§9.4.11) puts the junction with no way through on the default entry -of a sibling region: the transition targets a junction inside one region of an orthogonal state, -and the other region's initial transition leads to a junction both of whose guards are false; -PSSM's static evaluation takes the default entry in and disables the whole transition — the state -is never entered, its `entry` never logged, and the next occurrence fires from the source. +junction). A nested default-entry junction is a separate transition and is read when that +transition is taken (SM46); *Junction 004*'s separate explicit target-route behavior remains in +this row. *Join 003* (§9.4.12) puts it at a join's way out: the join's only outgoing transition is guarded false, so PSSM fires the first completion transition into the join on its own (a segment may end at a join, whose completion is waited for) and disables the second, whose entering the join would @@ -776,7 +779,9 @@ of the join. *Differs, v2 silent* as first assessed, the project keeping its rul and junction then shared one static reading. *Decided:* PSSM's rule. Once SM30 made the choice dynamic the two vertices no longer share a rule, and the junction's static reading is the one UML gives it, under which the guards beyond a -junction decide whether the compound transition is enabled at all. Wherever enabledness is +junction decide whether the compound transition is enabled at all. The route checked is the +transition's own: a nested default entry's route belongs to a separate transition out of the +composite's entry action, taken after it (SM46). Wherever enabledness is decided — a signal, call or event dispatch and its preview (`Decide`, `probeTransition`), a completion, a timer, a change poll — `state_route.go:routeAvailable` resolves the route in a preview with the trigger's arguments bound, as firing would. `followOut` marks a junction, or a @@ -800,8 +805,9 @@ firing. Only that sentinel disables: a cycle between pseudostates, a guard that and a binding failure still fail the run as the transition fires. The route is checked only as far as its first choice, whose guards are read on arrival (SM30), so a junction with no way through beyond a choice is the run's error when the choice is resolved. A region's default entry -cannot reach a junction in v2 (an entry transition targets a state, §7.18.3), so *Junction 004*'s -case arises only through the referee's translation. `state_junction_no_way_through_unmatched`, +is a separate entry transition in v2, so a junction there is read after the composite's entry +(SM46), not while evaluating the incoming transition's route; *Junction 004*'s separate explicit +target-route behavior remains on SM32. `state_junction_no_way_through_unmatched`, `state_junction_no_way_through_other_transition_fires`, `state_junction_no_way_through_deferred`, `state_junction_dead_branch_not_drawn`, `state_completion_no_way_through_dropped`, `state_history_default_no_way_through`, @@ -811,13 +817,12 @@ case arises only through the referee's translation. `state_junction_no_way_throu `robustness_test.go:region_pseudostate_without_satisfied_guard` (the source stays active), `robustness_junction_exit_route_test.go`, and `robustness_junction_join_test.go` (`junction_after_choice_keeps_runtime_error`, `junction_cycle_keeps_runtime_error`, -`junction_unevaluable_guard_keeps_runtime_error`). **agrees** since the decision. *Join 003* -passes; *Junction 002* and *Junction 004* stay `fail` in the referee because their junction lies -after the start state the translation needs (`emit.go:startTarget`), so the transition the -runtime disables is that state's completion, not the compound transition PSSM disables (finding -11, open decision 8). *Choice 005* traces the same reach -from the other side — its junction on the composite's default entry is read before `T2(effect)` -and the composite's entry — and is refused on its acting guards before the order is reached; see +`junction_unevaluable_guard_keeps_runtime_error`). **agrees** since the decision, for the +transition's own route. *Join 003* passes; *Junction 004*'s separate explicit target route also +remains within SM32, while its nested default-entry junction is SM46. *Choice 005* traces the +same reach from the other side — its junction on the composite's default entry is read before +`T2(effect)` and the composite's entry — and is refused on its acting guards before the order is +reached; see [A guard whose behavior acts on the model](#a-guard-whose-behavior-acts-on-the-model). #### Fork and join @@ -1035,11 +1040,14 @@ duration` when the state is entered (a composite's timer counts from entering th (`state_time_trigger_restarts_on_re_entry`); units are converted to seconds (`state_time_trigger_test.go`). **agrees** (by exclusion). -**SM40. Change triggers.** *v2/KerML:* §7.18.3 `accept when `, a `ChangeSignal` -accepted when its condition becomes true; the project takes a rising edge. *Runtime:* -`state_change_trigger.go` polls the conditions of the active configuration's transitions once -per `runStep`, after the do round and before the queued occurrence, firing on a false-to-true -edge through the same `dispatchInOrder` as a signal (`state_change_trigger_rising_edge`, +**SM40. Change triggers.** *v2/KerML:* §7.18.3 `accept when `, `Triggers.kerml` +`TriggerWhen`: a `ChangeSignal` sent when its condition changes from false to true, observed by +`ObserveChange` after each completed feature write (`FeatureWritePerformance` assigns when its +performance ends). *Runtime:* `feature_write_watch.go` re-evaluates, after every completed +outermost write, the conditions of the active configuration's transitions whose read set the +write touched, and `state_change_trigger.go` queues each rise and dispatches it once per +`runStep`, after the do round and before the queued occurrence, through the same +`dispatchInOrder` as a signal (`state_change_trigger_transient_rise`, `state_change_trigger_atomic_write`, (`state_change_trigger_rising_edge`, `state_change_trigger_event_order`, `state_change_trigger_autonomous`). **agrees** (by exclusion). **SM41. The shared clock: quiescence before time moves.** PSSM §2.3: a tool "may be limited to a @@ -1128,6 +1136,14 @@ ends the object's portions and refuses later reads once it goes ahead a destroyed end is refused (`TestBindingRefusesADestroyedEnd`). fUML aborts the behaviors and destroys; the runtime refuses the destruction. **differs, v2 silent.** +**SM46. A junction on a nested default entry.** PSSM requirements *Junction 002* and *Junction 004* (§9.4.11) put a junction with no way through on the initial transition of a region that the incoming transition enters by default, and read its guards when the incoming transition is selected: the static evaluation of §8.5.6 reaches through the composite's default entry, and the incoming transition is not enabled. *v2/KerML:* the default entry is not part of the incoming transition. SysML v2 §7.18.3 makes it a transition out of the composite's `entry` action (`EntryTransitionMember`), a `TransitionUsage` of its own whose performance is a `NonStateTransitionPerformance` (`TransitionPerformances.kerml`). There, `succession [1] transitionLinkSource then [1] Performance::self` orders the whole performance, including its guard and the route it takes, after its source: the `entry` action, which `States.sysml` (`StateAction`, entry before the middle subperformances) performs once the composite has been entered. The guards beyond that transition's junction are therefore read when that transition is taken, after the incoming transition's effect and the composite's entry, and cannot decide whether the incoming transition was enabled. *Runtime:* `state_route.go:routeAvailable` resolves only the incoming transition's own route (SM32); `state_executor.go:startIn` resolves the default entry's route when the entry action has completed, and a junction there with no outgoing guard true fails the run with a no-way-through error naming the junction (`state_entry_transition_junction_no_way_fails`). **differs because v2 differs.** + +The discriminating conformance case `state_entry_transition_junction_reads_outer_effect` starts +`x` at 0 and has only the `x > 0` branch; the incoming effect sets `x` to 1, so a junction read +at the incoming transition's selection would leave `Go` unmatched, while the runtime reads it +when the entry transition is taken and reaches `a`. The typed no-way-through failure is covered by +`state_entry_transition_junction_no_way_fails`. + ### Actions (fUML) fUML's activity semantics (formal/21-03-01 §8.9 and §8.10) are the ground PSSM's behaviors @@ -1566,22 +1582,24 @@ as a connector object of its own. Nothing in PSCS would supply that object; it i ## The count -Seventy rows: 45 for state machines, 15 for actions, 10 for composite structures. Each +Seventy-one rows: 46 for state machines, 15 for actions, 10 for composite structures. Each carries one verdict. | Verdict | Rows | |---|---:| -| **agrees** | 54 | -| **differs because v2 differs** | 7 | +| **agrees** | 53 | +| **differs because v2 differs** | 9 | | **differs, v2 silent** | 6 | | **gap** | 3 | -| **Total** | **70** | - -The seven **differs because v2 differs** rows are SM15 (a do activity and the machine competing -for one occurrence), SM36 (local transitions), SM37 (internal transitions), A12 (accept event: -a message no accepter takes stays in flight), A15 (one firing per token: fUML re-fires an -action for every token on a multiplicity-1 pin, the runtime performs the node once with every -delivery), C6 (behavior ports) and C9 (interface-typed ports and name-based dispatch). On each, SysML v2 or the Kernel Semantic Library states the rule the +| **Total** | **71** | + +The nine **differs because v2 differs** rows are SM6 (the standard deferred-event encoding +cannot replay a kept occurrence ahead of events already pooled), SM15 (a do activity and the +machine competing for one occurrence), SM36 (local transitions), SM37 (internal transitions), +SM46 (a junction on a nested default entry), A12 (accept event: a message no accepter takes +stays in flight), A15 (one firing per token: fUML re-fires an action for every token on a +multiplicity-1 pin, the runtime performs the node once with every delivery), C6 (behavior ports) +and C9 (interface-typed ports and name-based dispatch). On each, SysML v2 or the Kernel Semantic Library states the rule the runtime follows, quoted in the row; adopting PSSM, fUML or PSCS there would move the runtime away from the specification it implements, so none of them is a candidate for a port. @@ -1610,8 +1628,9 @@ Four rows first assessed *differs, v2 silent* now **agree**, each decided for PS implemented, the first assessment and the *Decided:* sentence kept in the row: **SM11** (a composite state's completion fires its own completion transition), **SM28** (an empty history with no default transition performs the owner's default entry), **SM30** (a choice's guards are -read on arrival) and **SM32** (a junction or a join's way out with no path through disables the -compound transition, and the occurrence is handled as any unmatched one). +read on arrival) and **SM32** (a junction or a join's way out with no path through on the +transition's own route disables the compound transition, and the occurrence is handled as any +unmatched one). The three **gap** rows: @@ -1991,7 +2010,7 @@ one admitted trace has seven segments — `T1.2(guard)::T1.3(guard)::T2(effect)` composite's entry, `T1.4(guard)::T1.5(guard)`, the first substate's entry (the trace is quoted in [the referee record](../../project/pssm-referee.md)): the junction's two guards read at `T2`'s selection, before its effect and the composite's entry — the static evaluation of §8.5.6 -reaching through the composite's default entry, the same reach SM32 records for *Junction 004* +reaching through the composite's default entry, the same reach SM46 records for *Junction 004* — and the choice's two read on arrival, after the composite's entry, the dynamic evaluation of §8.5.7. The suite observes *when each guard is read*, and the calls are its only means of observing it. Whether the referee can observe the same without giving a v2 guard a @@ -2015,9 +2034,9 @@ and "guard expressions with side effects are ill formed". | Candidate | What it would do | Result against the admitted trace | |---|---|---| -| Guard reads as the referee's observable: the emitter spells the four guards as the pure `true`/`false` they return, the runtime records each guard evaluation as a trace event naming the transition, and the run maps the events to `T1.n(guard)` in `log` | the guard stays a Boolean expression and the model is never mutated; the observable is the runtime's, not the model's | **refused.** Run under the shape the emitter produces (an initial into a junction is spelled as a helper start state whose completion transition reaches the junction, `emit.go`, `TestEmitInitialIntoPseudostate`), the runtime's execution trace reads the junction's guards *after* the composite's `enter` line and the helper state's entry, as the completion transition out of it is selected (`state_route.go:resolveRoute` → `followOut`, SM29: static for *that* transition, whose source is inside the composite), and the choice's after the helper state's exit — `T2(effect)`, the composite's entry, then `T1.2(guard)::T1.3(guard)::T1.4(guard)::T1.5(guard)` and the first substate's entry at best, which the suite does not admit; its one trace needs the junction read at `T2`'s selection, before `T2(effect)`, a reach through the default entry that SM32 recorded as *differs, v2 silent* and the library's `entry then middle` places the other way. The channel is also short of the suite's reads: `enabledBranches` reads the first guard of a vertex in the open and every further one under `beginProbe`, which restores `ctx.trace` — so of the four reads the execution trace holds two `eval` lines, `T1.2`'s and `T1.4`'s, and `T1.3`'s and `T1.5`'s are rolled back with the probe; a choice branch past the first is read once probed and once more when drawn (`resolveChoice`), a read the suite never traces. Exposing every read as an event would need a rule for probe reads, repeated reads and their identity that no test of the suite fixes and this one contradicts on its first two entries. Reached against admitted: 0 of 1, with one trace the suite refuses. Nothing else moves — no other expressible test has an acting guard (`TestClassifyGuardSideEffect`), and the runtime is unchanged | +| Guard reads as the referee's observable: the emitter spells the four guards as the pure `true`/`false` they return, the runtime records each guard evaluation as a trace event naming the transition, and the run maps the events to `T1.n(guard)` in `log` | the guard stays a Boolean expression and the model is never mutated; the observable is the runtime's, not the model's | **refused.** Run under the shape the emitter produces (an initial into a junction is spelled as a helper start state whose completion transition reaches the junction, `emit.go`, `TestEmitInitialIntoPseudostate`), the runtime's execution trace reads the junction's guards *after* the composite's `enter` line and the helper state's entry, as the completion transition out of it is selected (`state_route.go:resolveRoute` → `followOut`, SM29: static for *that* transition, whose source is inside the composite), and the choice's after the helper state's exit — `T2(effect)`, the composite's entry, then `T1.2(guard)::T1.3(guard)::T1.4(guard)::T1.5(guard)` and the first substate's entry at best, which the suite does not admit; its one trace needs the junction read at `T2`'s selection, before `T2(effect)`, a reach through the default entry that SM46 records as *differs because v2 differs* and the library's `entry then middle` places the other way. The channel is also short of the suite's reads: `enabledBranches` reads the first guard of a vertex in the open and every further one under `beginProbe`, which restores `ctx.trace` — so of the four reads the execution trace holds two `eval` lines, `T1.2`'s and `T1.4`'s, and `T1.3`'s and `T1.5`'s are rolled back with the probe; a choice branch past the first is read once probed and once more when drawn (`resolveChoice`), a read the suite never traces. Exposing every read as an event would need a rule for probe reads, repeated reads and their identity that no test of the suite fixes and this one contradicts on its first two entries. Reached against admitted: 0 of 1, with one trace the suite refuses. Nothing else moves — no other expressible test has an acting guard (`TestClassifyGuardSideEffect`), and the runtime is unchanged | | A `calc def` or an expression with a side effect: spell each guard as a calculation that appends to `log` and returns its literal | the trace would be reached | **refused.** A v2 expression is pure — a `calc def` is a `Function` and a `calc` usage an `Expression` (SysML v2 §7.17), an `Evaluation` that computes a result and performs no action; a transition's guard is an `Expression` (§7.18.3, `validateTransitionFeatureMembershipGuardExpression`), so `bool guard[*]` is an `Evaluation`, not a `step`, and no `assign`, `send` or `perform` may stand in one. What acts is `step effect[*]`, ordered after the guard. UML 2.5.1 §14.5.11 calls the guard with the side effect ill formed, so the spelling would encode a construct the source specification declares malformed to observe an order the target library places differently. Not spelled | -| A `differs-by-design` row: adjudicate the test as differing because v2 orders the default entry after the composite's entry (SM32) | the test would run with pure guards and its `fail` on the missing four segments would be attributed to the tool choice | **refused.** `differs-by-design` names a *differs because v2 differs* row a test reaches (`rows.go:TestRows`); SM32 was then *differs, v2 silent* and now **agrees**, so the bucket does not apply, and the test does not run at all: with pure guards it reaches `T2(effect)`, the composite's entry and the first substate's entry, three segments where seven are admitted, and the difference is the construct's, not the order's alone. The classifier's refusal stands; SM31 (choice with no guard true) and SM32 (junction with no path through) were unchanged by it, and *Junction 002*, *Junction 004* and *Join 003* kept their buckets and reasons | +| A `differs-by-design` row: adjudicate the test as differing because v2 orders the default entry after the composite's entry (SM46) | the test would run with pure guards and its `fail` on the missing four segments would be attributed to the tool choice | **refused.** SM46 now classifies the nested default-entry timing, but this case remains refused: with pure guards it reaches `T2(effect)`, the composite's entry and the first substate's entry, three segments where seven are admitted, and the difference is not attributable to that ordering alone. Its acting guards are not faithfully spellable or observable in v2; the classifier's refusal stands. SM31 and SM32 are unchanged; *Junction 002* and *Junction 004* now report on SM46, and *Join 003* remains on SM32 | The classification is the settled one: *guard side effect* is a construct with no translation and no faithful observable, `not-expressible` with the reason naming the four transitions, @@ -2107,10 +2126,12 @@ whose guard changes between the completion and its dispatch step; and a join who the suite places before the last segment's effect — are the ones that would report on a tool choice; those landing on SM11, SM28, SM30 and SM32 (a composite owning a completion transition, a history entered with nothing recorded and no default, a choice whose guard reads what the -incoming effect wrote, a junction or join with no way through) report on rules decided for PSSM's +incoming effect wrote, a junction on the transition's own route or a join with no way through) +report on rules decided for PSSM's reading, and so check that the runtime does what it was decided to do; and the 37 tests -with no spelling or translation, together with any test that reaches SM15, SM36 or SM37, would fail for reasons -that are v2's, and a harness would have to exclude them by classification rather than report + with no spelling or translation, together with any test that reaches SM6, SM15, SM36, SM37 + or SM46, would fail for reasons that are v2's, and a harness would have to exclude them by + classification rather than report them as failures. Used that way, the suite is a second opinion on the tool choices and a regression oracle for the rows that agree; it is never a conformance statement about SysML v2. @@ -2130,9 +2151,10 @@ Track E of the roadmap, on its acceptance gate, and on what a user would see. ineffective whenever any other region reacted, which defeated its purpose; the extension and the decision have since been removed together, see the row) and SM28 (an empty history with no default falls back to the region's initial transition — a refusal serves no v2 rule, - and UML is the extension's reference); **keep ours, and say so** on SM30 and SM32 (the - runtime's static evaluation of choice and junction guards is one rule for both vertices and is - what makes `pseudostates.md`'s reading of a junction hold; a change would split them), on SM9 +and UML is the extension's reference); **keep ours, and say so** on SM30 (choice guards are read +on arrival, after the incoming effect) and SM32 (junction guards on the transition's own route +are read statically before it fires; a nested default-entry junction is separately adjudicated +under SM46), on SM9 (a guard read once at completion is the simpler rule, and a completion-occurrence pool would be a second event kind for the one case the row names), on SM45 and C8 (a refused destroy and a failed send are typed errors a modeler sees, where fUML/PSCS @@ -2193,7 +2215,8 @@ Track E of the roadmap, on its acceptance gate, and on what a user would see. ### (c) A user-selectable PSSM-conformant execution mode - **Scope.** A `-semantics pssm` (or `%semantics`) switch under which the state executor follows - PSSM on every row where it differs: SM7, SM11, SM15, SM28, SM30, SM32, SM34, SM36, SM37, SM45, + PSSM on every row where it differs: SM6, SM7, SM11, SM15, SM28, SM30, SM32, SM34, SM36, SM37, + SM45, SM46, plus the local and internal transition kinds themselves, which need new notation and lowering (`transition local first …`), a completion-event pool (SM9 exactly rather than equivalently), @@ -2235,18 +2258,19 @@ Track E of the roadmap, on its acceptance gate, and on what a user would see. ## Recommendation **Option (a), with (b) as a follow-on once (a)'s two changes have landed.** The map shows no case -for porting the precise-semantics family: 50 of 70 rows agree already, 7 differ because SysML v2 +for porting the precise-semantics family: 53 of 71 rows agree already, 9 differ because SysML v2 says otherwise and must stay as they are, and the 3 gaps are v2 gaps Track E already owns. What remains is nine tool choices, and on two of them — SM7 and SM28 — PSSM's rule is the reference this project's own extensions name (UML) applied consistently, while ours is an accident of implementation order; on the other seven the runtime's rule is deliberate and better for a modeler -(typed errors over silent drops, one guard-evaluation rule for both pseudostates, one reading of -a completion guard, the library's connector model), and the row records why. Option (b) is worth having *after* that, as an +(typed errors over silent drops, static junction routing on a transition's own route and dynamic +choice routing, one reading of a completion guard, the library's connector model), and the row +records why. Option (b) is worth having *after* that, as an advisory oracle in the established `cmd/pilot-*` shape and with its meaning stated in its own words: an advisory PSSM comparison tests reproduction of UML behavior unless the model and semantics have a defensible SysML v2 mapping, and it is never proof of SysML v2 conformance. Option (c) is rejected: two normative interpreters break the analysis framework's rule, double -stage 3 of the model checker, and make the runtime disagree with the v2 text on six rows for +stage 3 of the model checker, and make the runtime disagree with the v2 text on nine rows for users who select the mode. Option (d) is rejected because SM7 and SM28 are findings this note has now made and leaving them stands the extensions on UML for their syntax and on nothing for their semantics. @@ -2256,10 +2280,10 @@ recommended, SM11 as leaned and as the library's own `done`/`endShot` binding re the project's own `pseudostates.md` already promised, so the "keep ours" position above holds for SM9, SM45, C8 and C3 only. Each of the four rows carries its *Decided:* sentence with the functions and fixtures; option (b) remains the follow-on it was. -SM32 was decided for PSSM's rule afterwards: the "keep ours" argument for it — one static rule for -choice and junction — went with SM30's decision, which made the choice dynamic, and the junction's -static reading is then the one UML gives it, which decides enabledness (SM32's *Decided:* -sentence). SM34's segment firing was decided with it; where the owner is left stays the runtime's. +SM32 was decided for PSSM's rule afterwards: once SM30 made choices dynamic, the earlier argument +for keeping ours — one static rule for choice and junction — no longer applied; the junction's +static reading nevertheless matches UML for a transition's own route (SM32's *Decided:* sentence). +SM34's segment firing was decided with it; where the owner is left stays the runtime's. Nothing here changes the architecture's position. SysML v2 and the Kernel Semantic Library govern; UML 2.5.1 — and now, on the state-body extensions, PSSM's reading of UML — is the @@ -2556,7 +2580,12 @@ sites of the runtime's fixed, the pool's order and the do step drawn on the entr apart by the source performing nothing, which neither v2 nor PSSM does. The three stay `fail`, their reasons citing the language difference. Whether that difference takes a *differs because v2 differs* row — moving the three to `differs-by-design` through - `tools/referee/pssm/rows.go:TestRows` — is open decision 8. + `tools/referee/pssm/rows.go:TestRows` — was open decision 8. *Withdrawn*: the reading + that v2 cannot place the effect holds for the shorthand `EntryTransitionMember` only. A + transition out of a named entry action is a `TransitionUsage` performed as a + `NonStateTransitionPerformance`, its effect after the entry action and before the + target's entry, within the entry; the emitter spells the initial transition that way and + the three pass (see the referee record). - *History 001-C*'s first half is about the **pool's order** (SM10): PSSM generates a completion event as its source is entered and dispatches in generation order (§8.5.9), so the entry draw decides the pool's order, which `scheduleTransitionEvents` @@ -2666,4 +2695,6 @@ Addressed to the maintainers; each gives the options and the lean. construct both languages have, and the runtime implements the v2 side; this one would name a construct v2 lacks, and a `differs-by-design` count that grows by three on a translation limit reads as conformance gained. The three reasons are precise and stable, and the bucket can be moved in a - change of its own if the maintainers read it otherwise. + change of its own if the maintainers read it otherwise. *Withdrawn*: the premise was the + shorthand's. A transition out of a named entry action carries an effect within the entry + (`TransitionPerformances.kerml` `NonStateTransitionPerformance`), and the three pass. diff --git a/docs/internals/design/pseudostates.md b/docs/internals/design/pseudostates.md index 4abfce3bde..4fd78793ec 100644 --- a/docs/internals/design/pseudostates.md +++ b/docs/internals/design/pseudostates.md @@ -24,7 +24,10 @@ Pseudostates are transient vertices in state machines that enable complex contro - Used to merge multiple incoming transitions or split paths - Several enabled branches are a transition choice point (`ChoiceTaken` at the junction, enumerated by `explore`); an unguarded branch is the else branch -- No enabled branch disables the compound transition (PSSM *Junction 002*) +- No enabled branch on the transition's own route disables it; a junction on a composite's + nested default entry belongs to a separate transition out of `entry`, is read after the outer + effect and composite entry, and fails at run time with a typed no-way-through error if no + branch is enabled (SM46; PSSM *Junction 002* differs by design) ### Semantics @@ -134,11 +137,14 @@ choice point at the junction the schedule policy draws and records only as the t candidate another region's reaction disarms draws nothing; the unguarded segments are the default when no guard holds — and goes on until the route reaches a state or a choice. The guards read the data as it stands before the incoming transition's effect. If no static -branch is available, only `errNoWayThrough` leaves the compound transition unenabled before -selection; the occurrence remains available to another enabled transition, deferral, or unmatched -discard. A completion with no path is dropped. A history default route is checked this way only -when the source is outside the history owner, because leaving the owner may record the history -before its default route is read (see the precise-semantics alignment note, SM29 and SM32). +branch is available on the transition's own route, only `errNoWayThrough` leaves that transition +unenabled before selection; the occurrence remains available to another enabled transition, +deferral, or unmatched discard. A completion with no path is dropped. A junction on a composite's +nested default entry is read when its separate entry transition is taken, after the outer effect +and composite entry; if no branch is enabled, the run fails with a typed no-way-through error +(SM46). A history default route is checked this way only when the source is outside the history +owner, because leaving the owner may record the history before its default route is read (see the +precise-semantics alignment note, SM29, SM32 and SM46). **Choice evaluation** is dynamic. `followOut` leaves the route open at a choice. Firing (`travel`) then exits the states every branch of the open choice leaves — the source's ancestors @@ -256,9 +262,10 @@ package JunctionTest { 2. **Junction:** - Guards read before the incoming transition fires, in definition order; several holding is a recorded choice point, as at a choice - - No way through leaves the compound transition unenabled before selection, so the occurrence - is handled as unmatched: another enabled transition may take it, it may be deferred, or it - may be discarded; a completion with no way through is dropped + - No way through on the transition's own route leaves it unenabled before selection, so the + occurrence is handled as unmatched: another enabled transition may take it, it may be + deferred, or it may be discarded; a completion with no way through is dropped. A dead + junction on a nested default entry instead fails when that entry transition is taken (SM46) - Only `errNoWayThrough` disables; route cycles, unevaluable guards and binding failures remain run errors, and static route checking stops at the first choice diff --git a/docs/internals/design/region-order-scheduling.md b/docs/internals/design/region-order-scheduling.md index 2a1eae07c1..7db0993ebc 100644 --- a/docs/internals/design/region-order-scheduling.md +++ b/docs/internals/design/region-order-scheduling.md @@ -655,6 +655,14 @@ an empty `StatePerformance` and a completion like any other) and PSSM contradict event is dispatched after the step whatever the source performs). That is a special case of the translation's shape, not a semantics. +*Since resolved for these three.* The spelling argument above holds for the shorthand +`EntryTransitionMember` only. A transition out of a named entry action is a `TransitionUsage` +whose source is an action, a `NonStateTransitionPerformance` (`TransitionPerformances.kerml`): +it follows the entry action within the entry and runs its effect before the target's entry, +which is the entry-unit row exactly. The emitter now writes the initial transition that way, the +effect is a unit of its region's queue on the entry front, and *Entering 010*, *Entering 011* and +*Junction 005* pass with no runtime rule about completions. + **The first halves of the History tests are about the pool's order.** Both regions enter a silent state whose completion is enabled at once. PSSM's pool holds the two completion events in the order they were generated — §8.5.9, "a new `CompletionEventOccurrence` is placed into the diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md index 8f59273eac..1e23320a83 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -1730,6 +1730,36 @@ which is drawn against the branches' remaining target entries, six outcomes. `state_do_step_machine_before_top_entries` is the same shape at the machine, whose do behavior begins before its top regions are entered: six outcomes. +### Effects on the way into the regions of a parallel state: each precedes its own target's entry, the regions interleave + +Fixtures: `state_entry_transition_effect_regions` (golden, explored, checked), +`state_junction_inside_orthogonal_region` (golden, explored, checked). + +A transition out of a named entry action, `entry action boot; transition boot do { … } then s;`, +is a `TransitionUsage` whose source is an action rather than a state, so its performance is a +`NonStateTransitionPerformance` (`TransitionPerformances.kerml`; `Actions.sysml` +`DecisionTransitionAction`, `Action::decisionTransitions`): `transitionLinkSource then effect` +and `effect then transitionLink.laterOccurrence` place the effect after the entry action and +before the target's `StatePerformance` begins, and `succession transitionLinkSource then +Performance::self` makes the transition part of the entry, not a step dispatched after it. It +has no trigger: an accepter needs a state source (the pilot's +`validateTransitionUsageTriggerActions`). The shorthand `entry; then s;` (§7.18.3 +`EntryTransitionMember`, a `GuardedTargetSuccession`) still carries a guard at most. A segment +of a compound transition that continues inside a region of the parallel state it enters is the +same shape one level down: its effect is a `TransitionPerformance` step between the +pseudostate's predecessor and its target's entry. + +The regions of a parallel state are `middle` steps of its `StatePerformance` +(`StatePerformances.kerml` `succession entry then middle`), concurrent with each other, and +nothing in either library orders one region's transition performance against another +region's. So the parallel state's own entry comes first, each region's effect precedes its own +target's entry, and the regions' chains interleave in every way: for a region whose chain is an +effect then an entry beside one whose chain is a single entry, three orders. PSSM's *Entering +010*, *Entering 011* and *Junction 005* admit exactly these linearizations. The executor +offers each effect as a unit of its region's queue on the entry front +(`state_unit_front.go` `entryTransitionEffectHead`, `state_region_entry.go` `enterRegion`), so +`-schedule explore` reaches each order. + ### A succession outside a behavior body orders the performances it relates, wherever they run Fixtures: `namespace_succession_chain_ends` (golden), `type_succession_performed_actions` diff --git a/docs/project/pssm-referee-baseline.json b/docs/project/pssm-referee-baseline.json index 34b96e43ef..35c5dc49a9 100644 --- a/docs/project/pssm-referee-baseline.json +++ b/docs/project/pssm-referee-baseline.json @@ -6,14 +6,14 @@ "url": "https://www.omg.org/spec/PSSM/20181101/PSSM_TestSuite.xmi", "suiteDigest": "c355b249c356774377a46b60345019d827af1ce417bde88e533aa5f39206ae07", "tests": 103, - "recorded": "2026-10-01", - "develop": "deca2b0389f796b02fa1c30a387617d0613a034c" + "recorded": "2026-10-03", + "develop": "3d45ca6fb200339461594cd086004e461633e6d1" }, "buckets": { - "differs-by-design": 5, - "fail": 11, + "differs-by-design": 7, + "fail": 6, "not-expressible": 34, - "pass": 53 + "pass": 56 }, "tests": [ { @@ -630,32 +630,24 @@ "name": "Entering 010", "area": "Entering", "class": "standard", - "bucket": "fail", - "reasons": [ - "admitted trace not reached: S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)", - "admitted trace not reached: S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)" - ], + "bucket": "pass", "expected": [ "S1(entry)::S1.1(entry)::T2.1(effect)::S2.1(entry)", "S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)", "S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)" ], "reached": [ - "S1(entry)::S1.1(entry)::T2.1(effect)::S2.1(entry)" + "S1(entry)::S1.1(entry)::T2.1(effect)::S2.1(entry)", + "S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)", + "S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)" ], - "runs": 4 + "runs": 20 }, { "name": "Entering 011", "area": "Entering", "class": "standard", - "bucket": "fail", - "reasons": [ - "admitted trace not reached: S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)", - "admitted trace not reached: S1(entry)::T1.1(effect)::T2.1(effect)::S1.2(entry)::S1.1(entry)", - "admitted trace not reached: S1(entry)::T2.1(effect)::T1.1(effect)::S1.1(entry)::S1.2(entry)", - "admitted trace not reached: S1(entry)::T2.1(effect)::T1.1(effect)::S1.2(entry)::S1.1(entry)" - ], + "bucket": "pass", "expected": [ "S1(entry)::T1.1(effect)::S1.1(entry)::T2.1(effect)::S1.2(entry)", "S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)", @@ -666,9 +658,13 @@ ], "reached": [ "S1(entry)::T1.1(effect)::S1.1(entry)::T2.1(effect)::S1.2(entry)", - "S1(entry)::T2.1(effect)::S1.2(entry)::T1.1(effect)::S1.1(entry)" + "S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)", + "S1(entry)::T1.1(effect)::T2.1(effect)::S1.2(entry)::S1.1(entry)", + "S1(entry)::T2.1(effect)::S1.2(entry)::T1.1(effect)::S1.1(entry)", + "S1(entry)::T2.1(effect)::T1.1(effect)::S1.1(entry)::S1.2(entry)", + "S1(entry)::T2.1(effect)::T1.1(effect)::S1.2(entry)::S1.1(entry)" ], - "runs": 4 + "runs": 40 }, { "name": "Exiting 001", @@ -1438,20 +1434,17 @@ "name": "Junction 002", "area": "Junction", "class": "extension", - "row": "SM32", - "rowKind": "agrees", - "bucket": "fail", + "row": "SM46", + "rowKind": "differs because v2 differs", + "bucket": "differs-by-design", "reasons": [ - "reached a trace the suite does not admit: S1(entry)", + "run error: process event: fire transition out of wait: entry transition through junction S1_Junction1: no way through: junction S1_Junction1: no guard evaluated to true", "admitted trace not reached: T3(effect)", - "reports on SM32 (Junction or join with no path through): agrees" + "reports on SM46 (Junction on a nested default entry): differs because v2 differs" ], "expected": [ "T3(effect)" ], - "reached": [ - "S1(entry)" - ], "runs": 1 }, { @@ -1473,40 +1466,35 @@ "name": "Junction 004", "area": "Junction", "class": "extension", - "row": "SM32", - "rowKind": "agrees", - "bucket": "fail", + "row": "SM46", + "rowKind": "differs because v2 differs", + "bucket": "differs-by-design", "reasons": [ - "reached a trace the suite does not admit: S1(entry)::T1.3(effect)::S1.2(exit)", + "run error: process event: fire transition out of wait: enter state: enter starting state in region S1/Region2: entry transition through junction S1_Junction1_2: no way through: junction S1_Junction1_2: no guard evaluated to true", "admitted trace not reached: T3(effect)", - "reports on SM32 (Junction or join with no path through): agrees" + "reports on SM46 (Junction on a nested default entry): differs because v2 differs" ], "expected": [ "T3(effect)" ], - "reached": [ - "S1(entry)::T1.3(effect)::S1.2(exit)" - ], - "runs": 2 + "runs": 6 }, { "name": "Junction 005", "area": "Junction", "class": "extension", - "bucket": "fail", - "reasons": [ - "admitted trace not reached: S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)", - "admitted trace not reached: S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)" - ], + "bucket": "pass", "expected": [ "S1(entry)::T1.3(effect)::T2.1(effect)::S2.1(entry)::S1.2(exit)::S1(exit)", "S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)", "S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)" ], "reached": [ - "S1(entry)::T1.3(effect)::T2.1(effect)::S2.1(entry)::S1.2(exit)::S1(exit)" + "S1(entry)::T1.3(effect)::T2.1(effect)::S2.1(entry)::S1.2(exit)::S1(exit)", + "S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)", + "S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)" ], - "runs": 4 + "runs": 20 }, { "name": "Junction 006", diff --git a/docs/project/pssm-referee.md b/docs/project/pssm-referee.md index bf2d0cde37..1f20610934 100644 --- a/docs/project/pssm-referee.md +++ b/docs/project/pssm-referee.md @@ -218,13 +218,13 @@ for. `differs-by-design` is never inferred from a failure: the table is written by hand from the note, names the row, and is reviewed with every change to it. A test the table maps to a *differs, v2 silent* row stays a `fail` when it fails and cites the row either way, so the bucket -lists say which failures are second opinions on a tool choice. Of the six *differs because v2 -differs* rows, only SM15 (a do activity and the machine competing for one occurrence) is -reached by an expressible test; SM36 and SM37 (local and internal transitions) have no -spelling and their tests are not expressible, and A12, C6 and C9 are action and composite-structure -rows no state-machine test exercises. SM11, SM28, SM30 and SM32 are now `agrees` rows: their -PSSM decisions are implemented. Junction 002 and Junction 004 still fail while citing SM32, -because an `agrees` citation does not change a trace mismatch's bucket. SM34 remains +lists say which failures are second opinions on a tool choice. Of the nine *differs because v2 +differs* rows, SM15 (a do activity and the machine competing for one occurrence) and SM46 (the +nested default-entry junctions in Junction 002 and Junction 004) are reached by expressible tests; +SM36 and SM37 (local and internal transitions) have no spelling and their tests are not expressible, +and A12, C6 and C9 are action and composite-structure rows no state-machine test exercises. SM11, +SM28, SM30 and SM32 remain `agrees` rows: Join003 and Junction 004's separate explicit target +route report on SM32, while the nested default-entry cases report on SM46. SM34 remains *differs, v2 silent*, narrowed to when the join owner is left and cited by Join001. SM9 (when a completion guard is read) no failing test reaches, and SM45 (destroying a performing object), C3 (multi-valued connector ends) and C8 (a send with no receiver) are not state-machine rows @@ -232,7 +232,7 @@ and no test in the suite reaches them. ## Baseline -Recorded **2026-10-01** on develop commit **`deca2b0389f796b02fa1c30a387617d0613a034c`** with deferred signals written in the +Recorded **2026-10-03** on develop commit **`3d45ca6fb200339461594cd086004e461633e6d1`** with deferred signals written in the standard buffer / accept-loop / exit-flush encoding the migrator writes (the `defer` state member, an OpenSysML extension, and the runtime's deferral machinery are removed), with entry, do and effect behaviors bound to the triggering event's data, exit behaviors to the leaving transition's payload, the @@ -240,7 +240,8 @@ behaviors returning the call's outputs, the tester's calls and traces driven in the tester's order and standalone machines read as targets, with completion events queued in the order their sources are entered and a due do step of an entered state drawn against the sibling regions' remaining entry units (the pool's order following the entry draw and the do step on the -entry front, finding 11's two runtime parts), the order of orthogonal +entry front, finding 11's two runtime parts), a region's initial transition spelled as a transition +out of its named entry action whose effect and route are units of the region's entry front, the order of orthogonal regions drawn as choice points at finding 9's four sites (region entry, region exit, the units of the firings one occurrence selects, a due do step against the dispatch, drawn per token move of the do flow), `terminate` executing @@ -255,25 +256,70 @@ The regenerated JSON and the bucket figures below are the current baseline. | Bucket | Tests | |---|---:| -| `pass` | 53 | -| `fail` | 11 | +| `pass` | 56 | +| `fail` | 6 | | `not-expressible` | 34 | -| `differs-by-design` | 5 | +| `differs-by-design` | 7 | | **Total** | **103** | ### Movements since the previous baseline -The current baseline records **53 `pass`**, **11 `fail`**, **34 `not-expressible`** and **5 +The previous baseline was **58 `pass`**, **6 `fail`**, **34 `not-expressible`** and **5 +`differs-by-design`**. Two tests moved from `pass` to `differs-by-design`; no other test's +bucket, reasons or reached set changed. For both, the nested default-entry transition is taken +after the incoming transition's effect and the composite's entry, while PSSM reads that +junction at outer selection. + +| Test | Row | Movement | Cause and adjudication | +|---|---|---|---| +| Junction 002 | SM46 | `pass` → `differs-by-design` | Design difference. The entry transition's junction is read after the outer effect and composite entry; PSSM reads it at outer selection. Reached: `run error: process event: fire transition out of wait: entry transition through junction S1_Junction1: no way through: junction S1_Junction1: no guard evaluated to true`. Admitted trace not reached: `T3(effect)` | +| Junction 004 | SM46 | `pass` → `differs-by-design` | Design difference. The nested entry transition's junction is read after the outer effect and composite entry; PSSM reads it at outer selection. Reached: `run error: process event: fire transition out of wait: enter state: enter starting state in region S1/Region2: entry transition through junction S1_Junction1_2: no way through: junction S1_Junction1_2: no guard evaluated to true`. Admitted trace not reached: `T3(effect)` | + +### Earlier entry-transition changes + +The earlier entry-transition changes moved five tests from the older baseline of **53 `pass`**, +**11 `fail`**, **34 `not-expressible`** and **5 `differs-by-design`**: *Entering 010*, +*Entering 011* and *Junction 005* remain `fail` → `pass`; *Junction 002* and *Junction 004* +now finish `fail` → `differs-by-design`. These cases turn on how a region's initial transition +is spelled. The emitter used to translate it, when it had an effect or ended +at a pseudostate, as the completion of a behavior-less helper start state, on the reading that an +entry transition carries a guard at most (§7.18.3 `EntryTransitionMember`). That holds for the +shorthand only: a transition out of a *named* entry action, `entry action 'R.initial'; transition +'R.initial' do { … } then s;`, is a `TransitionUsage` whose source is an action, performed as a +`NonStateTransitionPerformance` that follows the entry action within the entry, its effect before +the target's entry (`TransitionPerformances.kerml`; the pinned pilot accepts the shape). The +emitter now writes that (`emit.go:startEntry`, `writeEntry`), the runtime executes such a +transition's effect and junction or choice route as part of entering the body +(`state_executor.go:startIn`), and in a region of a parallel state the effect is a unit of the +region's entry queue ([the derivation](behavior-semantic-oracle.md#effects-on-the-way-into-the-regions-of-a-parallel-state-each-precedes-its-own-targets-entry-the-regions-interleave)). Finding 11's +language difference and open decision 8 are withdrawn with it. + +| Test | Cause | Movement | Adjudication | +|---|---|---|---| +| Entering 010 | translation limitation, finding 11 (withdrawn) | `fail` → `pass`, 4 → 20 runs | Expected. `T2.1(effect)` is a unit of region 2's entry queue, so it falls before, between or after region 1's explicit entry of `S1.1`; the three admitted orders are reached and nothing else | +| Entering 011 | translation limitation, finding 11 (withdrawn) | `fail` → `pass`, 4 → 40 runs | Expected. Each region's initial effect precedes its own target's entry and interleaves with the other region's two units: all six admitted orders, nothing else | +| Junction 002 | design difference, SM46 | `fail` → `differs-by-design` | The incoming transition enters `S1`; its nested entry transition reads `S1_Junction1` after the outer effect and composite entry, then fails with `process event: fire transition out of wait: entry transition through junction S1_Junction1: no way through: junction S1_Junction1: no guard evaluated to true`. PSSM reads the junction at outer selection, so admitted `T3(effect)` is not reached | +| Junction 004 | design difference, SM46 | `fail` → `differs-by-design` | The incoming transition enters `S1`; the nested entry transition reads `S1_Junction1_2` after the outer effect and composite entry, then fails with `process event: fire transition out of wait: enter state: enter starting state in region S1/Region2: entry transition through junction S1_Junction1_2: no way through: junction S1_Junction1_2: no guard evaluated to true`. PSSM reads the junction at outer selection, so admitted `T3(effect)` is not reached | +| Junction 005 | translation limitation, finding 11 (withdrawn); runtime gap | `fail` → `pass`, 4 → 20 runs | Expected. Region 2's `T2.1(effect)` is a unit of its entry queue, and `T1.3(effect)`, the segment out of the region-1 junction the entering transition targets, is now a unit of region 1's queue after `S1(entry)` (`state_region_entry.go:enterRegion`) rather than run before either region is entered; the three admitted orders are reached, `S2.1`'s real completion still dispatched after the front | + +The six that remain `fail` are each adjudicated below: *Transition 017*, *Exiting 002*, +*History 001-C* and *History 002-B* on suite defects recorded in `omg-issues.md`, *Join001* on +SM34 (*differs, v2 silent*) and the suite's malformed trace, and *Transition 019* on the order +of silent target entries against the `T*.3` effects, where v2 orders the completion pool by +entry and the suite by effect. + +### Movements before that + +The baseline before that recorded **53 `pass`**, **11 `fail`**, **34 `not-expressible`** and **5 `differs-by-design`** tests, from 52 / 12 / 34 / 5. The count change is *Join003*, which moved from `fail` to `pass`: its first completion segment now arrives on its own occurrence, and the second is not enabled because the join's only way out is guarded false. -*Junction 002* and *Junction 004* no longer fail at runtime with “no guard evaluated to true”. -Both junctions lie after the helper start state emitted by `emit.go:startTarget`. Under SysML v2 -§7.18.3 an entry transition has no effect and targets a state, so the transition disabled by the -runtime is that state's completion, not the compound transition whose target PSSM evaluates -statically. They remain `fail` with reached-but-not-admitted traces and cite SM32 as `agrees`; -the helper-state shape is finding 11 and open decision 8. +*Junction 002* and *Junction 004* are now `differs-by-design` on SM46. The incoming transition +checks only its own route; its nested default-entry transition is taken after the outer effect +and composite entry, where a dead junction fails with a typed run error. PSSM reads those +junctions at outer selection, so the admitted `T3(effect)` traces are not reached. *Junction +004*'s separate explicit target-route behavior remains under SM32, as does *Join003*. *Join001* remains `fail`: its reasons include the difference over when the join owner is left (SM34) and the suite's malformed second registered trace ([the suite defect](omg-issues.md#pssm-join-001-admits-a-malformed-trace)). @@ -283,9 +329,9 @@ state entry order and the `T*.3` effects differ: the completion pool follows the `T*.2` effects. *Junction 005* is unchanged; it remains `fail` on admitted orders it does not reach, attributed to finding 11. -SM11, SM28, SM30 and SM32 are now `agrees` rows because their PSSM decisions are implemented. -A failure that cites an `agrees` row remains in `fail`; *Junction 002* and *Junction 004* are -examples. +SM11, SM28, SM30 and SM32 are `agrees` rows because their PSSM decisions are implemented. +SM32 applies to a transition's own route; *Join003* remains a passing example, and *Junction +004*'s separate explicit target route remains within that row. ### Movements before that @@ -487,7 +533,6 @@ table — and no bucket moves. | Test | Finding | Movement | Adjudication | |---|---|---|---| | Transition 017 | 11 (the pool's order, fixed), suite defect | `fail` → `fail`, reason changed | Expected. The three admitted traces that dispatch `T3.1.2(effect)`, the completion of `S3.1`'s region, before `T2.2(effect)`, the completion of `S1`'s other region — `T2(effect)::S1(entry)::T3.1.2(effect)::T2.2(effect)::S3.1(doActivity)::T3.2(effect)`, `…::T3.1.2(effect)::S3.1(doActivity)::T2.2(effect)::…` and `…::S3.1(doActivity)::T3.1.2(effect)::T2.2(effect)::…` — are reached: region 3 drawn first at `entering S1` puts `S3.1.1`'s completion into the pool ahead of `S2.1`'s, and the do step falls before, between or after the two dispatches as before. Six of the eight admitted traces are reached; the two still missing fire `T3.2`, `S3.1`'s own completion transition, before `T3.1.2`, the completion out of its region, the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-transition-017-admits-a-parents-completion-before-its-regions). `fail` citing the defect alone; finding 11's part of the reason is closed | -| Entering 011 | 11 (an initial transition's effect, a completion effect in v2) | `fail` → `fail`, reason changed | Expected (the enumeration's `2 of 6`). Both regions' initial transitions have an effect, spelled as a completion out of a start state; the two start states' completions now dispatch in the order the entry draw entered them, so `S1(entry)::T1.1(effect)::S1.1(entry)::T2.1(effect)::S1.2(entry)` is reached beside `S1(entry)::T2.1(effect)::S1.2(entry)::T1.1(effect)::S1.1(entry)`. The four still missing interleave one region's effect with the other's entry, UML's initial-transition effect as an entry unit, which no v2 completion gives (finding 11, the alignment note's open decision 8); the reason stands on them | | History 001-C | 11 (the pool's order, fixed; the suite's defect) | `fail` → `fail`, reason changed | Expected (the enumeration's `2 of 2` for the first half). The first entry of `S1` now dispatches `S2.1`'s completion before `S1.1`'s when region 2 is drawn first, so `S1(entry)::S2.2(entry)::S1.1(exit)::S1.2(entry)::…` is reached beside the trace the PSSM text prints. The ten still missing fire `S1.1(exit)::S1.2(entry)` inside the step that restores region 2, the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-history-001-c-and-002-b-admit-a-completion-inside-the-restore-and-contradict-each-other); the reason stands on them | | History 002-B | 11 (the pool's order, fixed; the suite's defect) | `fail` → `fail`, reason changed | Expected (the enumeration's `1 of 2, 1 extra / 2 of 3`). After the restore, region 1's default entry of `S1.1` and region 2's restored `S2.2` with its initial `S2.2.1` each generate a completion, dispatched now in the order the entry draw entered them, so `…::T3(effect)::S1(entry)::S2.2(entry)::S2.2.1(exit)::T2.2.2(effect)::S2.2.2(entry)::S1.1(exit)::S1.2(entry)::S1(exit)`, the order the specification's own text gives, is reached beside the one reached before. The first entry of `S1` likewise dispatches `S2.1`'s completion first when region 2 is drawn first, `S1(entry)::S2.1(exit)::S2.2(entry)::S1.1(exit)::S1.2(entry)::…`, the order §8.5.9 gives and *History 001-C* admits for the identical half — two traces, one per restore order, which this test does not register. Two of the six admitted are reached and two unregistered ones; the four still missing — three that dispatch `S2.2.1`'s completion, generated a step later, before `S1.1`'s, and one that fires `T1.2` inside the restore — are the suite's defect, recorded in `omg-issues.md` as above; the reason stands on them and on the two unregistered traces | @@ -593,8 +638,8 @@ on what remains missing. No count moved between the baseline of develop `bcc6b13e0` (with the junction branch-choice fix, 2026-09-15) and the one that followed it (develop `46828f14f`, 2026-09-16). The baseline file changed all the same: the adjudication of -the fourteen failures it left unattributed ([below](#fail-11)) added four tests to the -committed table — *Junction 004* and *Join003* on SM32, *Join001* and *Transition 019* on +the fourteen failures it left unattributed ([below](#fail-6)) added four tests to the +committed table — *Junction 004*'s explicit target route and *Join003* on SM32, *Join001* and *Transition 019* on SM34, both *differs, v2 silent* rows — so their rows now carry the row and its verdict, and their reasons the *reports on* line. All four stay `fail`, as a test mapped to a tool-choice row does; none was inferred from the run, each was read against its requirement, and the @@ -698,7 +743,7 @@ initial transition enters, `emit_test.go:TestEmitInitialWithEffect`). Five tests The emitter fix also altered the recorded reason, without moving the bucket, of *Entering 010*, *Entering 011*, *Junction 004* and *Junction 005* (the repeated `T1.1(effect)` / `T2.1(effect)` of a region's initial transition is gone; *Junction 004* now reaches no trace at all — a run -error at the junction whose guards are all false, SM32's case — where it reached an inadmissible +error at the junction whose guards are all false, now adjudicated on SM46 — where it reached an inadmissible one), and finding 7 the reason of *History 001-C* and *History 002-B* (the restore is now the admitted one; what remains missing are the other interleavings of the two regions' entries and exits). A later translation fix — the values a test's constructor writes on the new instance are @@ -740,18 +785,18 @@ short trace to a budget exhaustion: with SM11 its `S1` now completes and fires ` history, and the history-record timing of finding 7 makes that re-enter `S1.1` without end. The remaining failures' reasons are byte-identical to the previous baseline's. -### `pass` (53) +### `pass` (56) Behavior 001, Behavior 002, Behavior 003 A, Behavior 003 B, Transition 001, Transition 007, Transition 011 C, Transition 015, Transition 016, Transition 020, Transition 022, Event 001, Event 002, Event 008, Event 009, Event 010, Event 015, Event 016 A (reports on SM11), Event 016 B, Event 017 A, Event 017 B, Event 018, Event 019 A, Event 019 B, Event 019 C, Event 019 D, Event 019 E, Entering 004, -Entering 005, Exiting 001, Exiting 003, Exiting 005, Fork 002, Choice 001 and Choice 002 (report on SM30), Choice 003, +Entering 005, Entering 010, Entering 011, Exiting 001, Exiting 003, Exiting 005, Fork 002, Choice 001 and Choice 002 (report on SM30), Choice 003, Choice 004, Final001 (reports on SM11), Deferred 002, History 001-A, History 001-B, -History 001-D, History 002-A, History 002-C (reports on SM28), History 002-D, Join002, Join003, Junction 001, -Junction 003, Standalone 003, Terminate 001, Terminate 002. +History 001-D, History 002-A, History 002-C (reports on SM28), History 002-D, Join002, Join003 (reports on SM32), Junction 001, +Junction 003, Junction 005, Standalone 003, Terminate 001, Terminate 002. -### `differs-by-design` (5) +### `differs-by-design` (7) | Test | Row | Admitted trace not reached | |---|---|---| @@ -760,10 +805,12 @@ Junction 003, Standalone 003, Terminate 001, Terminate 002. | Deferred 003 | SM7 | `S1.1.1(exit)::T1.1.2(effect)::S1.1(exit)::T1.2(effect)::S1.2(exit)::T1.3(effect)` — the machine's transition out of `S1` on `AnotherSignal` fires while `S1.1` keeps the signal; PSSM lets the deferring substate hold it | | Deferred 004 A | SM7 | `S1.1(exit)::T1.2(effect)::S2.1(exit)::T2.2(effect)::S1(exit)::T4(effect)` — the sibling region's `T2.2` fires on `Continue` at once; PSSM holds it until `S1.1` releases the occurrence | | Deferred 004 B | SM7 | `S1.1.1(exit)::T1.1.2(effect)::S1.1(exit)::S2.1(exit)::T2.2(effect)::S1(exit)` — the same with the deferring state nested one level deeper than the sibling's transition | +| Junction 002 | SM46 | `T3(effect)` — the runtime instead reaches a typed no-way-through error when the nested entry transition is taken after the outer effect and composite entry; PSSM reads the junction at outer selection | +| Junction 004 | SM46 | `T3(effect)` — the runtime instead reaches a typed no-way-through error when the nested entry transition is taken after the outer effect and composite entry; PSSM reads the junction at outer selection | -### `fail` (11) +### `fail` (6) -Every failure is accounted for. Three cite a note row, six cite a finding recorded +Every failure is accounted for. One cites a note row, three cite a finding recorded [below](#findings-about-our-own-conformance), and two additional failures are described after those tables: *Transition 019* (silent target-state entry order versus effect order) and *Exiting 002* (a suite defect). The failures citing a note row or finding are second opinions on @@ -771,15 +818,13 @@ the referenced rule or finding; those citations do not themselves determine the a translation defect: each translated model was read against the test's UML, and every construct the test uses reaches the run. -#### Citing a note row (3) +#### Citing a note row (1) | Test | Row | What the run shows | |---|---|---| -| Junction 002 | SM32 | Reaches `S1(entry)` while PSSM admits `T3(effect)`. The junction is after the helper start state, so the disabled transition is that state's completion (finding 11, open decision 8). The trace mismatch remains `fail` although SM32 is now `agrees` | -| Junction 004 | SM32 | Reaches `S1(entry)::T1.3(effect)::S1.2(exit)` while PSSM admits `T3(effect)`. As in *Junction 002*, the junction is after the helper start state, so the disabled transition is that state's completion (finding 11, open decision 8); the SM32 citation is `agrees`, but the trace mismatch remains `fail` | | Join001 | SM34 | The run leaves `S1` after the last incoming effect, where PSSM leaves it before that effect. Its second registered trace is malformed: it names nonexistent `S1.2`, repeats `T2.4` and omits `T2.3` ([suite defect](omg-issues.md#pssm-join-001-admits-a-malformed-trace)) | -#### Citing a finding (6) +#### Citing a finding (3) One line per test, from the baseline's `reasons`: what the run reached that the suite does not admit (`—` when every reached trace is admitted and the failure is only a missing one), and @@ -789,11 +834,8 @@ quoted and the number given. The full sets are in the baseline file. | Test | Finding | Reached, not admitted | Admitted, not reached | |---|---|---|---| | Transition 017 | suite defect (finding 11's part, the pool's order, fixed) | — | `T2(effect)::S1(entry)::T2.2(effect)::T3.2(effect)::S3.1(doActivity)::T3.1.2(effect)` and `T2(effect)::S1(entry)::T2.2(effect)::T3.2(effect)::T3.1.2(effect)::S3.1(doActivity)` (six of the eight admitted orders are reached: the do activity's segment before, between and after the two completions' dispatches, the completions `T2.2` and `T3.1.2` in either order — PSSM's pool holds them in the order their sources were entered (§8.5.9), which the entry draw at `entering S1` decides, and the runtime queues each as its source's entry unit is performed). The two missing fire `T3.2`, `S3.1`'s completion transition, before `T3.1.2`, the completion out of its own region, and run the do activity's segment after `S3.1` was left; they contradict the test's expected sequence and `StatePerformances.kerml` alike and are the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-transition-017-admits-a-parents-completion-before-its-regions) — no runtime reaches them, so the test stays `fail` on them | -| Entering 010 | 11 (an initial transition's effect, a completion effect in v2) | — | `S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)` and `S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)` (the third admitted order is reached; both run `T2.1(effect)`, the second region's initial transition's effect, before the first region's explicit target `S1.1` is entered. UML runs that effect as part of the region's default entry, so PSSM admits it anywhere against the sibling's entry units; SysML v2 has no place for an effect on an entry transition, so the referee spells it as the effect of a completion transition out of a start state, which the runtime dispatches as a step of its own after the entry, as it does every v2 completion. Folding the effect into the target's entry action instead is refused by this very test: region 1's initial transition `T1.1` has an effect too, and its target `S1.1` is the one the tester enters explicitly, so the fold runs `T1.1(effect)` on an entry that bypasses the initial transition — a trace in none of the three admitted; the design note's candidate table has the enumeration) | -| Entering 011 | 11 (an initial transition's effect, a completion effect in v2) | — | `S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)` and 3 more orders of the two regions' initial effects and entries (two of the six admitted orders are reached, each region's initial effect and entry whole, in the order the entry draw entered the two start states; as *Entering 010*, with an initial effect in each region. The four missing interleave one region's effect with the other's entry. The fold into the target's entry action reaches the same two and no refused trace, and no more: one entry action is one unit, so `T1.1(effect)` cannot be split from `S1.1(entry)` around the sibling's units as the other four admitted orders split it) | | History 001-C | 11 (the suite's defect; the pool's order, fixed) | — | `S1(entry)::S1.1(exit)::S1.2(entry)::S2.2(entry)::S2.2.1(exit)::S2.2.2(entry)::S1(exit)::S1(entry)::S1.1(exit)::S1.2(entry)::S2.2(entry)::S2.2.2(entry)::S1(exit)` and 9 more orders of the two regions' entries and exits (two of the twelve admitted orders are reached, the one the PSSM text prints and the one that dispatches `S2.1`'s completion before `S1.1`'s after the first entry of `S1` — the pool in the order the regions were entered, which the runtime's queue follows). The ten missing fire `S1.1(exit)::S1.2(entry)`, a completion the default entry of region 1 enables, *inside* the step that restores region 2, before or between `S2.2(entry)::S2.2.2(entry)`; the test's own note ends the restoring step first ("This completes the step started by the firing of `T4`. When dispatched, the completion event occurrence generated by `S1.1` triggers `T1.2`"), and six of the ten split the firing around a restored entry, which *History 002-B* forbids — the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-history-001-c-and-002-b-admit-a-completion-inside-the-restore-and-contradict-each-other) | | History 002-B | 11 (the suite's defect; the pool's order, fixed) | `S1(entry)::S2.1(exit)::S2.2(entry)::S1.1(exit)::S1.2(entry)::…` (two traces, one per order of the restore's two completions) | `…::S1(exit)::T3(effect)::S1(entry)::S1.1(exit)::S1.2(entry)::S2.2(entry)::S2.2.1(exit)::T2.2.2(effect)::S2.2.2(entry)::S1(exit)` and 3 more orders of the two regions' entries and exits (two of the six admitted orders are reached, the one the PSSM text prints and the one that dispatches region 2's restored completion first after the restore, `S2.2(entry)::S2.2.1(exit)::T2.2.2(effect)::S2.2.2(entry)::S1.1(exit)::S1.2(entry)`, which the specification's text gives). The two reached and not admitted dispatch `S2.1`'s completion before `S1.1`'s after the first entry of `S1`, the order §8.5.9's pool gives when region 2 is entered first and the one *History 001-C* admits for the identical half. Three of the missing dispatch `S2.2.1`'s completion, generated by `T2.2`'s firing in the second step, before `S1.1`'s, generated by the first step's entry, which §8.5.9's pool cannot do in any entry order; one more fires `S1.1(exit)::S1.2(entry)` inside the step that restores region 2, which the test's own note ends first ("At the end of the RTC step … the state machine is in configuration `S1[S1.1, S2.2[S2.2.1]]`. The next step consists in the firing of `T1.2`"). The suite's defect, recorded in [`omg-issues.md`](omg-issues.md#pssm-history-001-c-and-002-b-admit-a-completion-inside-the-restore-and-contradict-each-other) | -| Junction 005 | 11 (an initial transition's effect, a completion effect in v2) | — | `S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)` and `S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)` (the third admitted order, `T1.3(effect)` first after `S1(entry)`, is reached: the second region's initial effect `T2.1` and its target's entry are admitted before or around the junction segment's effect, as *Entering 010*'s. `S2.1`'s completion out of `S1`, a real one, is admitted only after `T1.3(effect)` in all three, where the runtime dispatches it. The fold into the target's entry action has no target here: `T2.1` ends at a junction, whose way out a guard decides, so the effect has no one state's entry to join) | Every reason in full — each extra trace, each missing trace, each error — is in the baseline file's `reasons`. @@ -984,8 +1026,11 @@ the runtime; a `fail` cites a tool choice, a translation limit or the suite's de ends at a junction). *Junction 005* shows the class is right — `S2.1`'s real completion is admitted only after the sibling's remaining entry unit — so no runtime rule reaches the three without telling a start state's completion from a real one, which neither v2 nor PSSM does. - Whether the difference takes a *differs because v2 differs* row is the alignment note's open - decision 8; the three stay `fail` citing it. *History 001-C*'s first half wants the **pool's** + Whether the difference takes a *differs because v2 differs* row was the alignment note's open + decision 8; the three stayed `fail` citing it. **Withdrawn**: the premise was the shorthand's. + A transition out of a named entry action carries an effect and is performed within the entry, + so the emitter spells the initial transition that way and the three pass (the movements since + the previous baseline). *History 001-C*'s first half wants the **pool's** **order** to follow the entry draw (§8.5.9: completion events dispatch in the order generated, which the order the regions were entered decides), where the runtime queued them after the move in declaration order (`scheduleTransitionEvents`) — one of the two parts of the finding that @@ -1055,16 +1100,16 @@ detail. By root cause: | A transition into an active ancestor re-entered it | runtime defect, SM35 (fixed) | Transition 011 C | `pass` | | Several completion transitions out of one state were not one choice | runtime defect, SM19 (fixed) | Event 015 | `pass` | | A guard whose behavior acts on the model | translation defect, the classifier (a construct with no translation) | Choice 005 | `not-expressible` | -| A junction or join with no way through | formerly missing alignment text; SM32 is now decided and implemented (`agrees`) | Junction 004, Join003 | Join003 `pass`; Junction 004 remains `fail` on the translated helper-state trace mismatch while citing SM32 as `agrees` | +| A junction on a transition's own route, or a join with no way through | SM32 is decided and implemented (`agrees`) for the transition's own route | Join003; Junction 004's separate explicit target route | Join003 remains `pass` on SM32; Junction 004's separate target-route behavior remains SM32, while its nested default-entry junction is `differs-by-design` on SM46 | | When the join owner is left | SM34 remains *differs, v2 silent*: PSSM leaves it before the final segment effect, the runtime after | Join001; Transition 019 (its remaining ordering mismatch is not SM34) | Join001 remains `fail`, citing SM34; Transition 019 remains `fail` on silent target-entry/effect ordering without an SM34 citation | | Region entry, exit and firing-unit order is not a recorded choice | runtime gap, finding 9 (fixed at these sites) | Exiting 001, Exiting 003 | `pass` | | A do step against the dispatch at the head of the pool is not a recorded choice | runtime gap, finding 9 (fixed at this site, at do-action granularity) | Behavior 003 A | `pass` | | A do activity's first segment registered as always before the next dispatch | suite defect (the suite admits both orders elsewhere) | Exiting 002 | `fail`, citing the defect | -| An initial transition's effect is a completion effect in v2 | language difference, finding 11 (adjudicated; the row is open decision 8 of the alignment note) | Entering 010, Entering 011 | `fail`, citing finding 11 | +| An initial transition's effect is a completion effect in v2 | translation limitation, finding 11 (withdrawn: a transition out of a named entry action carries the effect within the entry) | Entering 010, Entering 011 | `pass` | | The pool's order does not follow the entry draw | runtime gap, finding 11 (fixed: completions queued as their sources are entered) | History 001-C (one trace, reached), Transition 017 (three, reached) | `fail`, citing the suite's defects for the rest | | A completion dispatched inside the step that restores the sibling region | suite defect, finding 11 (recorded in `omg-issues.md`) | History 001-C, History 002-B | `fail`, citing finding 11 | | A do step against a sibling's entry unit is not a recorded choice | runtime gap, finding 11 (fixed: a due do step is a unit of its region's queue on the entry front) | Terminate 002 | `pass` | -| A junction segment's effect before its owner's entry | runtime defect, finding 10 (fixed) | Junction 005 | `fail`, citing finding 11 for the initial transition's effect, admitted before or around the segment's effect once the segment's effect follows `S1(entry)` | +| A junction segment's effect before its owner's entry | runtime defect, finding 10 (fixed) | Junction 005 | `pass`, once the segment's effect and the sibling's initial effect are units of their regions' entry queues | *Fork 002* and *Join001*, which finding 6's fix brought out of `not-expressible` after that baseline, are attributed with them: *Fork 002* to finding 9 (region entry order, now `pass`) diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 729331a858..b7d71421c0 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -848,7 +848,7 @@ nothing above. | A succession out of a state body's own entry subaction names the state it starts in (`entry; then off;`), which is how a machine designates where it starts | `lower/entry_transition.go` `addEntryTransition`, `UnconditionalStart`; `lower/state_graph.go` collectTransitions SuccessionEdge case + `isEntrySubaction` | `lower/state_notation_test.go:TestToStateGraph_EntrySuccessionNamesInitialState`, `lower/transition_source_test.go:TestToStateGraph_UnguardedEntryTransitionIsInitial`, `state_entry_succession_initial.sysml` conformance, `tests/parser/testdata/parse/behavior_exhibit_state_body.golden` | ✅ Faithful | | A state body's two-ended `first a then b;` is the `SuccessionAsUsage` a -> b that `succession first a then b;` spells with its keyword (SysML.xtext `SuccessionAsUsage` under `StateBodyItem`), so it lowers to the same completion (trigger-less) transition, resolving nested, qualified, chained (`c.c1`), region-local and pseudostate endpoints as a `succession` does, and designates no initial state; a machine whose only edges are such successions and no entry marker has no initial state, reported as an exhibited machine with none is. A succession end written as a feature chain names the nested vertex the qualified spelling names — `c.c1` and `c::c1` are one endpoint, as source or target, in either spelling, and the chain's first segment reaches a vertex nested anywhere in the machine (`c1.deep` for `c::c1::deep`) as a qualified end's does — and one whose member, or whose operand, is not a vertex is reported as a qualified end naming none is | `parser/behavior.go` (state-body `first` dispatch: a guarded `first a if g then b;` is a transition, a two-ended `first a then b;` a `SuccessionAsUsage`, and only a one-ended `first a;` an `InitialNode`); `parser/parser.go` `bodyContext.carriesActions` (a state body carries vertices, not a token flow); `parser/succession.go` `atTwoEndedFirst`, `atChainedFirstSuccession`; `resolve/references.go` `connectorEnd` (state-machine succession ends are endpoints, a chained end its operand then its member); `resolve/transition.go` `ResolveEndpointRef`, `resolveEndpointChain`, `lookupEndpointChain`, `VertexInScope` (over `endpointParts`); `lower/endpoints.go` `EndpointRef`, `EndpointResolver.Endpoint` (a name or a feature chain); `lower/state_graph.go` `collectUsageTransitions` → `addCompletion`, `vertexFor` (over `endpointPrefix`); `passes/state_transition.go` `checkEndpoint`, `endpointName` | `parse/state_body_first_succession.golden` (state definition, state usage, nested state, exhibited state, qualified ends, inherited `start`, guarded `first … if … then`, an action body's `first` kept as an initial node), `lower/state_graph_nested_test.go:TestKeywordlessSuccessionLowersLikeTheSuccessionKeyword`, `lower/state_notation_test.go:TestToStateGraph_InitialDesignationIsRecordedOnTheGraph`, `passes/state_transition_test.go:TestStateBodyFirstIsASuccession`, `passes/succession_endpoint_test.go:TestEndpointNamingNoMemberIsReported` (an unresolved end of either spelling), `:TestStateSuccessionEndpointSpellingsAcceptVertices`, `:TestStateSuccessionChainedEndpointsAcceptNestedVertices`, `:TestResolvedStateEndpointNotVertexIsReported` (`outer.mode`), `lower/state_graph_nested_test.go:TestSuccessionChainedEndpointsNameNestedVertices`, `resolve/references_test.go`, `export/behavior_test.go` (a `sysml:SuccessionAsUsage`, no `sysx:InitialNode`), conformance `state_first_succession_chain.sysml` (`entry; then a;` with `first a then b; first b then c; first c then done;` completes with the log `"a b c "`), `state_first_succession_without_entry.sysml` (`first b then c;` alone: no initial state), `state_first_succession_chained_endpoint.sysml` (`b.b1`, `b::b2`, `c1.deep`, `c.c1.deep` as source and target of both spellings), `robustness_test.go:object_exhibited_machine_whose_only_edge_is_a_first_succession` | ✅ Faithful (previously the two-ended form parsed as an `InitialNode` with a successor and lowered as an entry transition into `b`, so the machine started in `b` without an entry marker and, beside `entry; then a;`, never left `a`; the pinned pilot accepts the keyword-less spelling without diagnostics) | | A one-ended `first a;` in a state body orders nothing: a state body has no token flow for an initial node to start | `passes/state_transition.go` `CodeFirstNamesNoTarget` (constraint tier, an error in every mode), beside the notation tier's `nonstandard-notation` warning that the production exists in an action body alone; `lower/transition_source.go` `IsStateSource` (an `InitialNode` is not a state source) | `passes/state_transition_test.go:TestOneEndedFirstInAStateBodyIsReported`, `:TestTransitionToFirstMarkerIsIllegal`, `passes/nonstandard_notation_test.go:TestOneEndedFirstOutsideAnActionBodyIsAnExtension`, `robustness_test.go:state_transition_endpoint_naming_a_first_marker` | ✅ Faithful (reported, never a silent no-op: the lowering has no vertex for it and a transition naming it as an endpoint is refused) | -| Guarded entry transitions — SysML v2 §7.18.3 `EntryTransitionMember` (`entry; if cold then heating; if not cold then idle;`, `entry assign x := …; if c then s;`, `entry action boot { } if c then s;`, `transition boot if c then s;`): the transitions out of a body's entry action choose the state the body starts in. They are tried in declaration order each time the body is entered — at machine start and whenever a transition enters the composite state, orthogonal region or exhibited state whose body they belong to — after the entry action itself has run, and the first whose guard holds is entered; an unguarded `then s;` among them is taken when reached; when alternatives are written and none holds the machine has nowhere to start. A typed or specializing state that writes entry transitions of its own starts by them alone, the inherited ones being replaced as its own entry behavior replaces the inherited one; one writing none keeps the inherited start. An entry transition carries a guard at most: a trigger, an effect, or a target that is not a state is ill-formed | `lower/entry_transition.go` `EntryTransition`, `StateGraph.EntryTransitions` (keyed by the body's owner, kept in declaration order), `withOwnEntryTransitions` (a body's own alternatives replace the inherited ones, from `lower/state_graph.go` `collectGroupTransitions`), `StateGraph.StartOf`, `lowerEntryTransition` (typed `EntryTransitionShapeError` for a trigger or effect, `EntryTransitionTargetError` for a non-state target); `lower/state_graph.go` `machineState` (the machine's own entry behavior runs before its alternatives are tried); `runtime/state_executor.go` `startIn`, `entryGuardHolds`, `enterStartOf` (from `initialize`, `transitionToInto`, `enterRegionsInto`, which enters a region of a parallel state through the substate standing for it, so its entry behavior has run and its guards read that substate's own attributes; the state it descends to is the one the active configuration records for its region, the one events are scheduled from, and the one checked for completion, so an alternative into `done` completes the machine as it starts), `completeIfDone` (judges a composite state complete once its every region started in `done`), `runtime/state_region_transition.go` `moveBetweenRegions`, `enterOutside`; `runtime/errors.go` `ErrNoEntryTransitionHolds`; `passes/state_transition.go` `checkEntryTransition` (`CodeEntryTransitionShape`, `CodeEntryTransitionTarget`); `view/behavior.go` `stateMachineNode` (the state rendering draws each body's entry transitions as edges out of its `start`, in declaration order and carrying the guard as transition edges do, and marks only `StateGraph.UnconditionalStart` `initial`), `view/mermaid.go` `writeStateNode` (`[*] --> s : [guard]` inside the body) | `lower/transition_source_test.go:TestToStateGraph_GuardedEntryTransitionsKeepDeclarationOrder`, `:TestToStateGraph_EntryTransitionShape` (trigger, effect, trigger after an unguarded start, pseudostate target), `passes/state_transition_test.go:TestGuardedEntryTransitionIsLegal`, `:TestEntryTransitionShapeIsReported`, `:TestTransitionOutOfEntryActionIsLegal`, `:TestTriggeredTransitionOutOfEntryActionIsNotAVertex`, `:TestEntryActionTransitionIntoPseudostateIsNotAVertex`, `view/render_test.go:TestStateRenderingDrawsGuardedEntryTransitions` (+ goldens `state-entry.text.golden`, `state-entry.mermaid.golden`: machine, composite-state and orthogonal-region alternatives), conformance `state_entry_transition_guard_first.sysml`, `state_entry_transition_guard_second.sysml`, `state_entry_transition_default.sysml` (unguarded alternative), `state_entry_action_transition_guarded.sysml` (named entry action, `transition boot if c then s;`), `state_entry_transition_nested_regions.sysml` (+ trace golden: machine, composite-state and orthogonal-region alternatives, the machine's `entry assign` read by its guards), `state_entry_transition_reentry.sysml` (+ trace golden: a composite state's alternatives re-tried on each entry, `state_usages_independent.sysml` starting each typed usage by its inherited entry transition), `state_entry_transition_region_composite.sysml` (+ trace golden: a region's transition into a composite state whose alternative chooses a nested state, which then answers the next signal), `state_entry_transition_done.sysml` (an alternative into `done` completes the machine as it starts, after its exit behavior), `state_entry_transition_nested_done.sysml` (a transition into a parallel state whose every region starts in `done` completes the machine), goldens `state_entry_transition_guarded.sysml` (guarded and unguarded alternatives after `entry;`, an entry assignment and a named entry action, in a composite state, an orthogonal region and an exhibited state; accepted clean by the pinned pilot), `state_target_transition_placements.sysml` (`entry; then s;` at each depth), `robustness_test.go:no_entry_transition_guard_holds`, `:entry_transition_target_is_not_a_state`, `:entry_transition_carries_a_trigger`, `:entry_transition_into_done_completes_at_initialize`, `:named_entry_action_transition_into_done_completes_at_initialize` (`transition begin then done;` and `succession first begin then done;` out of a named entry action complete the same way, a declared state `done` being entered instead), `:own_entry_transitions_replace_inherited_ones` (a specializing machine, a typed usage, a guarded typed usage and a typed orthogonal region start where their own alternatives say; a usage redeclaring only the entry behavior keeps the inherited start), `:region_entry_transitions_into_done_complete_at_initialize`, `:nested_regions_into_done_complete_at_initialize`, `:transition_into_nested_regions_in_done_completes`, `:region_start_descends_through_entry_transitions`, `:region_entry_guards_read_the_region_state_attributes`, `:leaving_regions_descends_through_entry_transitions` | ✅ Faithful (every accepted shape, the trigger and effect rejections and the attribute-target rejection were refereed against the pinned pilot both ways, see `pilot-differential.md`; a pseudostate target cannot be refereed, the pilot having no `choice`/`junction` grammar, and an action-usage target the pilot accepts is reported here by the endpoint rule every transition is held to) | +| Guarded entry transitions — SysML v2 §7.18.3 `EntryTransitionMember` (`entry; if cold then heating; if not cold then idle;`, `entry assign x := …; if c then s;`, `entry action boot { } if c then s;`, `transition boot if c then s;`): the transitions out of a body's entry action choose the state the body starts in. They are tried in declaration order each time the body is entered — at machine start and whenever a transition enters the composite state, orthogonal region or exhibited state whose body they belong to — after the entry action itself has run, and the first whose guard holds is entered; an unguarded `then s;` among them is taken when reached; when alternatives are written and none holds the machine has nowhere to start. A typed or specializing state that writes entry transitions of its own starts by them alone, the inherited ones being replaced as its own entry behavior replaces the inherited one; one writing none keeps the inherited start. The shorthand carries a guard at most (`GuardedTargetSuccession`); a transition out of a named entry action, `entry action boot; transition boot do { … } then s;`, is a `TransitionUsage` whose source is an action, a `NonStateTransitionPerformance` (`TransitionPerformances.kerml`, `Actions.sysml` `DecisionTransitionAction`), so it may carry an effect, run after the entry action and before its target's entry as part of entering the body, and may target a junction or choice of the same body; the junction of an entry transition is resolved before that transition's effect, while a choice stays open and its guards are read after the effect, as covered by `state_entry_transition_effect_junction_static` and `state_entry_transition_effect_opens_choice`. In a region of a parallel state the effect is a unit of that region's entry queue, interleaving with the sibling regions' ([the derivation](behavior-semantic-oracle.md#effects-on-the-way-into-the-regions-of-a-parallel-state-each-precedes-its-own-targets-entry-the-regions-interleave)). A trigger needs a state source (the pilot's `validateTransitionUsageTriggerActions`), and a shorthand effect, a fork or join target, or a pseudostate of another body are ill-formed. Availability checks only the incoming transition's own route (SM32); a nested default entry is a separate transition out of the composite's `entry` action and its junction is read when that transition is taken, after the incoming effect and composite entry. If the junction has no way through, the run fails with a typed error naming the junction (SM46), as covered by `state_entry_transition_junction_no_way_fails.sysml` and `state_entry_transition_junction_reads_outer_effect.sysml` | `lower/entry_transition.go` `EntryTransition`, `StateGraph.EntryTransitions` (keyed by the body's owner, kept in declaration order), `withOwnEntryTransitions` (a body's own alternatives replace the inherited ones, from `lower/state_graph.go` `collectGroupTransitions`), `StateGraph.StartOf`, `lowerEntryTransition`, `addEntryTransitionTarget` (`EntryTransition.Effect`, `.Via`; typed `EntryTransitionShapeError` for a trigger or shorthand effect, `EntryTransitionTargetError` for any other target), `UnconditionalStart`; `lower/state_graph.go` `machineState` (the machine's own entry behavior runs before its alternatives are tried); `runtime/state_executor.go` `startIn`, `runEntryEffect`, `resolveEntryRoute`, `continueEntryRoute`, `entryGuardHolds`, `enterStartOf`; `runtime/state_unit_front.go` `entryTransitionEffectHead`, `runtime/state_region_entry.go` `startHead`, `enterRegion`; `runtime/state_route.go` `routeAvailable` (checks only the incoming transition's own route), `completeIfDone` (judges a composite state complete once its every region started in `done`), `runtime/state_region_transition.go` `moveBetweenRegions`, `enterOutside`; `runtime/errors.go` `ErrNoEntryTransitionHolds`; `passes/state_transition.go` `checkEntryTransition` (`CodeEntryTransitionShape`, `CodeEntryTransitionTarget`; a trigger on a transition out of a named entry action is reported by `checkAccepterSource` at the trigger, `CodeAccepterSourceNotState`); `view/behavior.go` `stateMachineNode` (the state rendering draws each body's entry transitions as edges out of its `start`, in declaration order and carrying the guard as transition edges do, and marks only `StateGraph.UnconditionalStart` `initial`), `view/mermaid.go` `writeStateNode` (`[*] --> s : [guard]` inside the body) | `lower/transition_source_test.go:TestToStateGraph_GuardedEntryTransitionsKeepDeclarationOrder`, `:TestToStateGraph_EntryTransitionShape` (trigger, effect, trigger after an unguarded start, pseudostate target), `:TestToStateGraph_EntryTransitionEffectAndRoute`, `:TestToStateGraph_EntryTransitionCannotTargetAnotherBodiesRoute`, `passes/state_transition_test.go:TestGuardedEntryTransitionIsLegal`, `:TestEntryTransitionShapeIsReported`, `:TestTransitionOutOfEntryActionIsLegal`, `:TestTriggeredTransitionOutOfEntryActionIsRejected`, `:TestEntryActionTransitionIntoJunctionIsClean`, `:TestEntryActionTransitionIntoChoiceIsClean`, `:TestEntryActionTransitionIntoJunctionInAnotherBodyIsReported`, conformance `state_entry_transition_effect.sysml`, `state_entry_transition_effect_regions.sysml` (explored: three orders), `state_entry_transition_junction.sysml`, `state_entry_transition_choice.sysml`, `state_entry_transition_guarded_effect_not_taken.sysml`, `state_entry_transition_explicit_inner.sysml`, `state_entry_transition_history_restore.sysml`, `state_entry_transition_junction_no_way_fails.sysml` (trace golden), `state_entry_transition_effect_opens_choice.sysml`, `state_entry_transition_effect_junction_static.sysml`, `state_entry_transition_junction_reads_outer_effect.sysml` (trace golden), golden `state_entry_transition_effect.sysml`, `robustness_entry_transition_effect_test.go:TestRuntimeRobustnessEntryTransitionEffect`, `view/render_test.go:TestStateRenderingDrawsGuardedEntryTransitions` (+ goldens `state-entry.text.golden`, `state-entry.mermaid.golden`: machine, composite-state and orthogonal-region alternatives), conformance `state_entry_transition_guard_first.sysml`, `state_entry_transition_guard_second.sysml`, `state_entry_transition_default.sysml` (unguarded alternative), `state_entry_action_transition_guarded.sysml` (named entry action, `transition boot if c then s;`), `state_entry_transition_nested_regions.sysml` (+ trace golden: machine, composite-state and orthogonal-region alternatives, the machine's `entry assign` read by its guards), `state_entry_transition_reentry.sysml` (+ trace golden: a composite state's alternatives re-tried on each entry, `state_usages_independent.sysml` starting each typed usage by its inherited entry transition), `state_entry_transition_region_composite.sysml` (+ trace golden: a region's transition into a composite state whose alternative chooses a nested state, which then answers the next signal), `state_entry_transition_done.sysml` (an alternative into `done` completes the machine as it starts, after its exit behavior), `state_entry_transition_nested_done.sysml` (a transition into a parallel state whose every region starts in `done` completes the machine), goldens `state_entry_transition_guarded.sysml` (guarded and unguarded alternatives after `entry;`, an entry assignment and a named entry action, in a composite state, an orthogonal region and an exhibited state; accepted clean by the pinned pilot), `state_target_transition_placements.sysml` (`entry; then s;` at each depth), `robustness_test.go:no_entry_transition_guard_holds`, `:entry_transition_target_is_not_a_state`, `:entry_transition_carries_a_trigger`, `:entry_transition_into_done_completes_at_initialize`, `:named_entry_action_transition_into_done_completes_at_initialize` (`transition begin then done;` and `succession first begin then done;` out of a named entry action complete the same way, a declared state `done` being entered instead), `:own_entry_transitions_replace_inherited_ones` (a specializing machine, a typed usage, a guarded typed usage and a typed orthogonal region start where their own alternatives say; a usage redeclaring only the entry behavior keeps the inherited start), `:region_entry_transitions_into_done_complete_at_initialize`, `:nested_regions_into_done_completes_at_initialize`, `:transition_into_nested_regions_in_done_completes`, `:region_start_descends_through_entry_transitions`, `:region_entry_guards_read_the_region_state_attributes`, `:leaving_regions_descends_through_entry_transitions` | ✅ Faithful (every accepted shape, the trigger and shorthand-effect rejections and the attribute-target rejection were refereed against the pinned pilot both ways, see `pilot-differential.md`, and the pilot accepts a named entry action's transition with an effect; a pseudostate target cannot be refereed, the pilot having no `choice`/`junction` grammar, and an action-usage target the pilot accepts is reported here by the endpoint rule every transition is held to) | | A transition out of a state body's own entry action names the state it starts in (`entry action initial { } transition initial then off;`), the entry action standing in for a start pseudostate (SysML v2 §7.19.3) | `ast/state_entry.go` `EntryActions`/`StateEntryActions`/`IsEntryAction`; `resolve/transition.go` `startAction`; `passes/state_transition.go` `machine.startActions`; `lower/state_graph.go` `startsAt` | `resolve/transition_test.go`, `passes/state_transition_test.go:TestTransitionOutOfEntryActionIsLegal`, `lower/state_notation_test.go`, `state_entry_action_transition_initial.sysml` conformance | ✅ Faithful (an ordinary action named as an endpoint is still reported) | | Termination when a transition reaches `done` | `state_executor.go` completeIfDone (see the completion rule below) | `state_simple.sysml` | ✅ Faithful | | State entry actions | `state_executor.go:749` enterState | `state_do_behavior.sysml` | ✅ Faithful | @@ -900,7 +900,7 @@ nothing above. | CallEvent triggers (`accept op(param)` notation, operation and argument matching, arguments bound for guard/effect) | `parser/behavior.go` parseTriggerEvent/parseCallEvent; `symbols/bodyscopes.go` triggerParameterDefiner (parameters are members of the transition, reachable from its own guard/effect); `state_executor.go` matchesEvent EventCall case, bindTriggerArguments, InvokeOperation; `perform.go` `callPayload` (a queued call carries the declaration its arguments select among the owner's same-named operations, `Call.Declared`), `callTriggerOperations` (a trigger names the declarations with an input for each of its parameters, those with exactly its parameters when any has — all of several differing in their parameters' types alone, since the notation writes no types — so a call of a declared operation fires only the triggers naming its declaration, as a UML `CallEvent` names one operation) | `tests/parser/testdata/parse/state_call_trigger.golden`, `lower/trigger_test.go:TestTriggerClassification_CallTrigger`, `model/behavior_body_resolve_test.go` call-trigger parameter cases, `state_call_trigger{,_guard,_nested,_regions}.sysml` conformance, `signal_test.go:TestCallEventMatchesOperationName`, `:TestRejectedCallLeavesNoArgumentsBehind`, `robustness_test.go:call_of_unhandled_operation`, `:call_argument_of_wrong_type`, `robustness_call_results_test.go:TestRuntimeRobustnessCallResults/overload_fires_the_trigger_naming_its_declaration` | ✅ Faithful (a call trigger on an enclosing composite state sees the invocation while a substate is active) | | A synchronous call of an operation a call trigger accepts returns to the caller once the run-to-completion step the call event triggers is done, with the values the behaviors that step fires — the transition's effect, an entry or an exit — returned or assigned to the operation's `out`/result parameters, by name, the last write winning — the parameters the operation declares as a member of the machine's owner (or of the machine itself when it stands alone) when it declares one, among several so named the one the call's arguments select as a call in the model would (`ErrAmbiguousInvocation` before the call is queued when they select none), the arguments checked against that declaration's inputs as an invocation's are (`ErrUnboundParameter` before the call is queued for an unbound or unknown one, `ErrTypeMismatch` for one of the wrong type, an omitted input carrying its default), the call event carrying that declaration so it fires only the triggers naming it — an `inout` the step writes nothing to going back as the caller passed it, since its parameter value is the argument until a behavior writes it (PSSM §8.5.9 `CallEventExecution`) — every output the step returned when the trigger names no declared operation; a call a state defers holds its caller through the machine's later steps until it is recalled and dispatched; a call the run leaves queued or deferred has not returned, and one no transition accepts is discarded and returns nothing (PSSM §8.5.9 `CallEventOccurrence`; the caller is released only after the step) | `runtime/perform.go` `StateExecutor.Call` (queues the call event with `InvokeOperation`, runs the machine at the current instant until that event has been dispatched — `callReleased` stops the run loop after the unit dispatching it, so events the step queued and timers it armed stay for the machine's later runs, while a deferred call keeps the run going through the steps until it is recalled — and reports a held call as `ErrCallNotReturned` through `eventDisposition`), `pendingCall` (captured by `snapshot.go` `capture` and `held_image_behavior.go` `imagedState`, so an undone step or a materialized image restores the call as it stood), `callPayload` (the declaration through `invoke_operation.go` `memberCalled`, the selection `InvokeOperation` makes, its inputs through `operationInputs`, the check `InvokeOperation` makes, and each input's value or default checked against its parameter as an assignment is, `callInputs`), `newPendingCall`, `callTaken` and `recordCallOutput` (outputs kept only from a behavior the pending call's own event fires, not from nested behavior another occurrence runs, and only under the names the declared operation returns, so a helper's other `inout`/`out` stays the object's own; a declared `inout` argument fills in under a transition that fired on the call and no behavior wrote to, so a discarded call still returns nothing); `action_frame.go` `performanceOwner.returnAround` and `assignEnclosingBy` route a nested action's `return` or output assignment to the enclosing behavior's parameter of that name (`action_executor.go`, `calc_statements.go`, `state_statements.go` hosts) | `conformance/state_call_trigger_results.sysml` (`.expected.json`, trace golden: `compute` doubled by the effect, negated by the entry), `robustness_call_results_test.go:TestRuntimeRobustnessCallResults` (held, recalled, untaken, empty, repeated and erroring calls; the caller released before the completion step its call queued and before a timer it armed, a signal queued ahead dispatched first, a declared operation returning its own parameters alone, an `inout` argument returned as passed, as written and not at all when nothing takes the call; an overloaded operation returning the outputs of the declaration the arguments select, firing the trigger naming that declaration, and refused as ambiguous when they select none; a call leaving a declared input unbound or naming none, or carrying a wrong-typed one, refused before it is queued; an omitted input carrying its default; a calc and a constraint returning their result alone; a rolled-back step restoring the call), `call_capture_test.go:TestStateCaptureTakesThePendingCall`, `:TestHeldImageCarriesThePendingCall` | ✅ Faithful | | Sourceless transitions (`accept … then`, `if … then`, `then`, `transition if … then`, `transition then`) — SysML v2 §7.18.3 `TargetTransitionUsage`: a transition usage written without a source part, whose source "is taken to be the closest lexically previous state usage" in the body that declares it, so it is a member of the body that declares the state it leaves, written after that state, at any depth (a state def body, an exhibited or performed state usage body, a composite state's body, an orthogonal region's body); the pilot's `UsageUtil.getPreviousFeature` derives it the same way, looking back over the other transitions chained off that state. A pseudostate declared before the shorthand is not that state usage: a `choice`, `junction`, `join` or `fork` is left by `transition first … then …;` only | `ast/transition_source.go` `ImplicitTransitionSource` (the previous-member rule over the complete ordered body, looking past the sourceless transitions chained off the same state and the succession `then state s;` lists after `s`); `lower/transition_source.go` `ImplicitSource`, `IsEntryTransition`, `IsStateSource` (a `PseudostateNode`, `InitialNode` or `FinalNode` is not a state source), the typed `ErrNoTransitionSource` and `TransitionSourceError` (`TransitionSourceNotVertexFormat`, `TransitionSourceRegionFormat`, `TransitionSourcePseudostateFormat`, `TransitionSourceMarkerFormat`); `lower/state_graph.go` `lowerTransitionMember` lowers the shorthand from the vertex the rule names, over the inherited and own members `lower/state_inheritance.go` materialises with their owner and scope; `passes/state_transition.go` `(*transitionChecker).checkImplicitSource` reports the same rule at the constraint tier (`CodeNoTransitionSource`, `CodeTransitionSourceNotVertex`) | `parser/behavior_test.go` `TestParseStateBody_SourcelessTransitionForms`, goldens `state_target_transition_guard.sysml` and `state_target_transition_placements.sysml` (top-level, composite, orthogonal-region placements with trigger, guard, effect and dotted targets, each `source=""`; both accepted clean by the pinned pilot), `lower/transition_source_test.go` (`TestToStateGraph_SourcelessTransitionLeavesThePrecedingState`, `:…InheritedSourcelessTransitionLeavesEachMaterialization`, `:…SourcelessTransitionWithNothingBefore`, `:…SourcelessTransitionAfterANonVertex` — start marker, explicit transition, succession usage, triggered and guarded shorthand after a `choice`, triggered shorthand after a `join`, `:…SourcelessTransitionAfterARegion`), `passes/state_transition_test.go:TestSourcelessAcceptTransitionIsLegal`, `:TestSourcelessTransitionChainAndSuccessionAreLegal`, `:TestSourcelessTransitionWithNothingBeforeIsReported`, `:TestSourcelessTransitionAfterANonVertexIsReported` (a pseudostate before the shorthand among them, and the explicit `transition first pick …` form it names staying legal), `:TestSourcelessTransitionAfterARegionIsReported`, conformance `accept_then_transition.sysml`, `state_target_transition_top_level_timed.sysml` (+ trace golden), `state_target_transition_nested_timed.sysml` (+ trace golden: one firing, one entry action, no self-loop), `state_target_transition_guard.sysml`, `state_target_transition_after_do_action.sysml`, `robustness_test.go:sourceless_transition_with_nothing_before`, `:sourceless_transition_after_a_non_state` (a `do` action, an attribute, a `choice` pseudostate) | ✅ Faithful (the earlier reading — the shorthand written *inside* the state it leaves, with that containing state as its source, and refused at the machine's top level — was wrong: the pinned pilot rejects the nested placement with parse errors (`no viable alternative at input 'accept'`), and accepts the flat placement this implementation now lowers, so `accept_then_transition.sysml` was rewritten into the flat form. A shorthand written first in its body, or after a member that is not a state of this machine — a `do` action, an attribute, an `in` parameter, a written succession, documentation, a pseudostate, a region of a parallel state — is reported by the constraint tier with the member named, and the lowering keeps the same typed errors as a backstop; the pilot rejects each of those placements it can parse too, by its grammar or by `A transition with an accepter must have a state as its source`, and has no grammar for `choice`/`junction` to referee the pseudostate placement against) | -| ChangeEvent triggers (when expr) | `state_executor.go` matchesEvent, RunToCompletion (polls after each micro-step and again at quiescence); `state_change_trigger.go` pollChangeEvents, SuspendReason | `state_executor_test.go:TestStateChangeEvent`, `state_change_trigger_test.go:TestChangeTriggerRunsWithoutAnExternalPoll`, `:TestChangeTriggerFiresOnRiseFromDoBehavior`, `:TestChangeTriggerDoesNotRefireUnchangedCondition`, `:TestChangeTriggerFalseConditionIsReported`, `conformance/state_change_trigger_autonomous.sysml`, `:state_change_trigger_rising_edge.sysml`, `:state_change_trigger_event_order.sysml` + trace golden | ⚠️ Approximate (driven by the run itself and fired on the condition rising; KerML has no clock, so re-testing once per micro-step is a tool-defined cadence — see the known limitation) | +| ChangeEvent triggers (when expr) — `Triggers.kerml` `TriggerWhen` returns a `ChangeSignal`, "a signal to be sent when the Boolean result of its changeCondition Expression changes from false to true" (`Observation.kerml`), and `ObserveChange` waits while the condition is false and sends the signal once it is true, then waits again. The condition's result can change only when a feature it reads is written, and a write is seen only once complete: a `FeatureWritePerformance` assigns its replacement values "at time its performance ends", and a `FeatureMonitorPerformance` compares a before time slice with an after snapshot that must differ (`FeatureReferencingPerformances.kerml`). So the conditions of the active configuration's transitions are re-evaluated after every completed outermost write that changes a feature they read, and each false-to-true rise queues one change signal, consumed by the next dispatch; a rise followed by a fall within one run-to-completion step still fires, while a value one assignment writes and replaces before it completes is never observed. KerML has no clock, so the library's own granularity is the completed write. A machine that cannot progress reports which condition it waits on | `feature_write_watch.go` `beginFeatureWrite`/`endFeatureWrite` (nested writes coalesced into the outermost one, compared before/after), `noteStateDataWrite`, `beginChangeRead`; `instance.go` `storeFeatureValue`; `binding.go`, `classifier_behavior.go` (bound and occurrence writes inside the same bracket); `dependents.go` `noteRead` (the condition's read set); `state_change_trigger.go` `changeConditionHolds`, `observeFeatureWrite`, `observeStateDataWrite`, `observeChangedValue`, `pollChangeEvents`, `SuspendReason`; `state_executor.go` `matchesEvent`, `RunToCompletion`; `snapshot.go`, `held_image_behavior.go`, `check_state.go` (observed, pending and read-set state carried by snapshots, held images and check-state keys) | `state_executor_test.go:TestStateChangeEvent`, `state_change_trigger_test.go:TestChangeTriggerRunsWithoutAnExternalPoll`, `:TestChangeTriggerFiresOnRiseFromDoBehavior`, `:TestChangeTriggerDoesNotRefireUnchangedCondition`, `:TestChangeTriggerFalseConditionIsReported`, `conformance/state_change_trigger_autonomous.sysml`, `:state_change_trigger_rising_edge.sysml`, `:state_change_trigger_event_order.sysml` + trace golden, `:TestChangeTriggerKeepsOutsideWriteRiseUntilPoll` (a rise and fall between polls fires), `:TestChangeTriggerIgnoresRiseInsideOneWrite` (a rise and fall inside one outermost write does not), conformance `state_change_trigger_transient_rise.sysml` (+ trace golden: a condition true and false again inside one step fires), `state_change_trigger_atomic_write.sysml` (+ trace golden: a write whose bound feature follows it raises no rise), golden `state_change_trigger_transient_rise.sysml`, `robustness_change_trigger_writes_test.go:TestRuntimeRobustnessChangeTriggerWrites` | ✅ Faithful | | TimeEvent triggers (`accept after ` relative, `accept at