fix(runtime): write-granular change triggers, unordered composite entry, entry-action transition effects

[devin-ai-integration]

What and why

Three state-machine execution changes, each derived from the vendored Kernel Semantic and Systems libraries, plus adjudication of the PSSM referee failures.

1. Change triggers are observed at every completed write, not once per micro-step. Before, a when <expr> condition that became true and false again inside one step was missed.
2. Composite entry admits every order the libraries admit. A composite state's own do step and its substates' entry work are unordered, so both are scheduler choice points under -schedule explore. Before, there was one fixed order.
3. 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. It may target a junction or choice in the same body. In a region of a parallel state, that effect is a unit of the region's entry front, as is a compound-transition segment's effect inside the region it enters. This closes five PSSM failures; the other six are adjudicated as suite defects or design differences.

Specification basis

Change triggers. Triggers.kerml TriggerWhen builds a ChangeSignal, "a signal to be sent when the Boolean result of its changeCondition Expression changes from false to true" (Observation.kerml). ObserveChange waits while the condition is false, then sends the signal. A condition's result can change only when a feature it reads is written. A write is seen only once it completes: FeatureWritePerformance assigns its values "at time its performance ends", and FeatureMonitorPerformance needs a before time slice and an after snapshot that differ (FeatureReferencingPerformances.kerml). KerML has no clock, so the granularity the library supports is the completed write.

So, after each completed outermost feature write, the runtime re-evaluates the conditions whose recorded read set the write touched. Each false-to-true rise queues one change signal, which the next dispatch consumes. A value that one assignment writes and replaces before it completes is never observed:

beginFeatureWrite(fv)                  // nested writes coalesce
  … writes, bindings, invalidations …  // noteFeatureWrite records the before-value once
endFeatureWrite()                      // outermost only: for each fv whose value changed,
                                       //   each executor re-evaluates conditions reading fv;
                                       //   rise ⇒ changePending[t] = true
pollChangeEvents: fires if holds || pending

Probe and preview evaluation are excluded. Observed, pending and read-set state is carried by snapshots, held images and check-state keys. Executors whose graph has no change trigger return early. spec-compliance.md: the ChangeEvent row moves to ✅ Faithful and its known limitation is removed.

Composite entry. StatePerformances.kerml: entry then middle, middle then exit, and do is a middle step. The substates' entry work is also within the state's middle, and the libraries do not order it against the composite's own do. That is now a choice point rather than a fixed order (state_anonymous_action_body: both interleavings, with goldens). The known limitation is removed.

Entry-action transitions. §7.18.3 EntryTransitionMember (the shorthand entry; then s;) is a GuardedTargetSuccession, so it still carries a guard at most. A transition whose source is a named entry action is a TransitionUsage with an action source, performed as a NonStateTransitionPerformance (TransitionPerformances.kerml; Actions.sysml DecisionTransitionAction):

• transitionLinkSource then effect and effect then transitionLink.laterOccurrence put the effect after the entry action and before the target's entry, within the entry.
• The regions of a parallel state are concurrent middle steps, and nothing orders one region's transition performance against another's. So each effect precedes its own target's entry, and the regions interleave in every way.

The pinned pilot accepts the shape, and still rejects a trigger on it ("A transition with an accepter must have a state as its source", validateTransitionUsageTriggerActions). The full derivation is in behavior-semantic-oracle.md § "Effects on the way into the regions of a parallel state: each precedes its own target's entry, the regions interleave". The spec-compliance.md guarded-entry-transition row is updated, and a new row covers route effects inside a parallel state's regions.

What now executes

• accept when c fires on every admitted rise, including a rise followed by a fall within one run-to-completion step.
• A composite state's do and its substates' entries interleave, and explore reaches each order.
• An effect on a transition out of a named entry action, and a junction or choice target in the same body. A route with no way through disables the transition that would enter that body, checked for the explicit target and for the sibling regions' default entries.
• Effects on segments that continue inside an entered parallel state's region run on that region's entry front.
• The junction of an entry transition is resolved before that transition's effect (static, as for any junction). A choice in it stays open, and its guards are read after the effect. A nested default entry's junction is read when that entry transition is taken, not when the incoming transition is selected, so it reads what the incoming effect wrote; with no guard true the run fails with a typed no-way-through error (state_entry_transition_effect_junction_static, state_entry_transition_effect_opens_choice, state_entry_route_dead_alternative, state_entry_transition_junction_reads_outer_effect, state_entry_transition_junction_no_way_fails).

What is still refused, and why

• A trigger on a transition out of an entry action. An accepter needs a state source (pilot validateTransitionUsageTriggerActions).
• An effect on the shorthand entry; then s;. GuardedTargetSuccession has no effect. The diagnostic suggests the named entry-action spelling.
• A fork or join target, or a pseudostate of another body, for an entry transition. Typed EntryTransitionTargetError.

PSSM referee: 53/11/34/5 → 56/6/34/7

Three tests moved fail → pass and two fail → differs-by-design; no other bucket, reason or reached set moved. Each movement is adjudicated in pssm-referee.md § "Movements since the previous baseline":

Test	Class	Adjudication
Entering 010, Entering 011	translation limitation (resolved)	Initial-transition effects are now spelled as transitions out of the region's named entry action, so each is a unit of its region's entry queue. Exactly the admitted 3 / 6 orders are reached. The alignment note's open decision on recording these as a language difference is withdrawn: its premise held for the shorthand only.
Junction 002, Junction 004	design difference, new alignment-note row "A junction on a nested default entry"	The junction is now the body's own entry route rather than lying after a helper start state. PSSM reads it when the incoming transition is selected and disables that transition. In SysML v2 the default entry is a separate transition out of the composite's entry action (§7.18.3 EntryTransitionMember; NonStateTransitionPerformance: succession transitionLinkSource then self), so its junction is read when that entry transition is taken, after the incoming effect and the composite's entry; with no guard true the run fails with a typed no-way-through error naming the junction. routeAvailable checks only the incoming transition's own route.
Junction 005	translation limitation + runtime gap (resolved)	T1.3(effect) (the junction segment inside region 1) and T2.1(effect) are each units of their region's entry front after S1(entry). All three admitted orders are reached.

The six that remain fail, each with evidence on file:

Test	Class	Where
Transition 017	suite defect: two anomalous admitted traces	omg-issues.md
Exiting 002	suite defect: registers one of two orders it admits elsewhere	omg-issues.md
History 001-C, History 002-B	suite defect: a completion dispatched inside the restoring step, and the two tests contradict each other on identical halves	omg-issues.md
Join001	design difference (v2 is silent on when the join owner is left) + malformed expected trace	pssm-referee.md, omg-issues.md
Transition 019	design difference: v2 orders the completion pool by entry, the suite by effect	pssm-referee.md

The baseline was regenerated only after these adjudications. -check -jobs 8 reproduces it, and the -json reports for -jobs 1 and -jobs 8 are byte-identical.

How it was verified

• go build ./..., go vet ./...: clean. gofmt -l .: empty.
• go test ./... and go test -C tools ./...: pass.
• go test -race ./internal/exec/runtime/ ./internal/ir/lower/... ./internal/check/passes/behavior/...: pass.
• make docs-check: pass (0 broken links; IDs and figures OK). python3 scripts/changelog.py check: pass.
• Corpora fetched with download-training-examples.sh, download-pilot-corpora.sh, download-pilot-library-xmi.sh and download-pssm-suite.sh. OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_PILOT_LIBRARY_XMI=1 OPENSYSML_REQUIRE_PSSM_SUITE=1 go test -count=1 ./tests/corpus/... ./tests/identity/...: pass. training_examples_expected.txt is untouched, and the pilot-differential digest did not drift.
• PSSM referee: as above.
• Pilot Xpect -check: 1,293 agree / 33 disagree, identical to develop. A triggered transition out of an entry action keeps the accepter-source diagnostic at the trigger (TransitionUsage_invalid.sysml.xt:54).
• New tests:
  • Conformance and trace goldens: state_change_trigger_transient_rise, state_change_trigger_atomic_write, state_anonymous_action_body (both orders), and state_entry_transition_{effect,effect_regions,junction,choice,guarded_effect_not_taken,explicit_inner,history_restore,junction_no_way_disables}. state_junction_inside_orthogonal_region now has three outcomes.
  • Unit tests: TestChangeTriggerKeepsOutsideWriteRiseUntilPoll (a rise and fall between polls fires) and TestChangeTriggerIgnoresRiseInsideOneWrite (inside one outermost write it does not; verified load-bearing by removing the bracket).
  • Robustness: TestRuntimeRobustnessChangeTriggerWrites and TestRuntimeRobustnessEntryTransitionEffect.
  • Parser goldens for the transient-rise and entry-transition-effect shapes, plus lowering, checker and emitter unit tests.
• Not run: the fUML referee's -check. Its suite download failed with HTTP 429 from Maven Central. No fUML-relevant code changed.

Checklist

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

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/394b8e09b1374a4bb4d92ad8d1f5b7e1
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/394b8e09b1374a4bb4d92ad8d1f5b7e1?variant=devin
Requested by: @HuiJun

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

This branch now conflicts with develop. Conflicting files, and the merged PRs that changed them:

• internal/exec/runtime/state_change_trigger.go (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)
• internal/exec/runtime/state_executor.go (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)
• tools/referee/pssm/emit.go (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)

To resolve: merge current develop into this branch with an ordinary merge commit (no rebase or force-push).
Reconcile the code conflicts with #864's statement-order scheduling (calc, constraint and case-step bodies) rather than taking one side; a conflict that needs a design decision should be raised on this PR, not guessed.

Planned merge order for the execution PRs: #844 → #850 → #838 → (#851 → #853 → #857) → #830 → #833 → #842 → #837 → #834 → #816.

Re-run the full gate (go build ./..., go vet ./..., gofmt -l ., make lint, make docs-check, go test ./...) and wait for green CI before marking ready.

[devin-ai-integration]

Hold on pushes: please don't push to this branch, including develop merges or empty commits to retrigger CI, until a maintainer says the CI runners are free. Prepare the conflict resolution locally and push it then.