feat(runtime): report execution choice points

[devin-ai-integration]

What and why

The Kernel Semantic Library defines only a partial order over performances. Wherever the executors pick among alternatives that order leaves open, they now record a choice point — a trace event and an informational diagnostic — without changing what they do. Default scheduling (reverse token-index order, first holding guard, first enabled transition) is untouched; every existing .expected.json passes unchanged.

Four kinds are recorded (internal/core/runtime/choice.go):

Kind	Where recorded	Rendering
ChoiceTokenOrder — ≥2 tokens advanced in one step	action_executor.go:Step, action_subflow.go (nested flows)	choice step 2: tokens 2@left, 3@right (unordered; took 3@right first)
ChoiceDecisionBranch — decision node with ≥2 holding guards	action_executor.go:stepDecisionNode, probeGuard (guards are read in order until one holds, which is taken; the ones after it are read inside a probe the context undoes, see below)	choice step 3: branches 1->left, 2->right (unordered; took 1->left)
ChoiceWriteOrder — several tokens write one destination in one step (whatever the values: the order is a pick either way)	action_choice.go:noteWrite collects, stepWriteLedger.noteChoices reports once the step is over, reached from the frame write boundary (action_frame.go:setFrameFeature), the performer write (classifier_behavior.go:assignPerformerFeature) and the chained write (assign_chain.go:writeThroughChain); a destination is the object and the shared *FeatureValue written, so a.b.x and c.x reaching one object, or a feature and one redefining it under another name, are one conflict, rendered x of object #3 := …; one choice per destination lists every token's last write and the one that stood	choice step 3: writes x := 1 by token 2, x := 2 by token 3, x := 3 by token 4 (unordered; x := 1 by token 2 stood)
ChoiceTransition — ≥2 transitions enabled from one state for one event or one change	state_executor.go:enabledTransition, probeTransition (the first enabled is taken; the ones after it are read inside a probe) and state_change_trigger.go:observeChangeConditions, probeChangeGuard, risenChangeTransition (a state's change guards are read live until the first enabled, the ones after it inside a probe; the first declared is taken); the notes ride on the dispatchCandidate into fireFrom and transitionDecided records them once the firing transition's guard has been read for the last time, so several regions selecting through their enclosing state make one choice, a composite state's transitions outranked by a nested one report nothing, and a candidate another region's firing disabled meanwhile reports nothing either (one whose effect then fails was the run's choice and is reported)	choice state Idle on accept Go: transitions 1->A, 2->B (unordered; took 1->A) / choice state watching on change: transitions 1->cool, 2->hot (unordered; took 1->cool)

Alternatives are rendered sorted (token id / declaration position) so the line is canonical. Ancestor-priority transition selection is ordered by UML/SysML and is deliberately not reported (state_choice_ancestor_priority_not_reported fixture and TestAncestorPriorityIsNotAChoice).

Tokens excluded from a token-order choice: ones created during the step, ones held at an unready join, ones that did not actually advance (e.g. still waiting at an accept nothing in flight answers). An accept a message in flight at the step's start would have answered is an alternative even if another token took the message first (beginStepOrder scans the queue under a probe, so a port it materializes leaves no trace): one message two parked accepts match is a tokens choice naming both and the recipient (action_choice_shared_message_accept, TestSharedMessageAcceptIsAChoice). A step that fails after a token already went still records the order it took, the failing token included, beside the error. Probe/preview runs discard their choices since they are rolled back.

Later guards are probed, and one with no result is reported, not raised

Reporting a decision or transition choice means reading guards first-match never reached. Those reads happen inside Context.beginProbe(), which restores the step budget, feature writes, trace, created objects (and the identity sequence they drew from, so long as the context still allocates from the same sequence and no live object or set-aside connector holds an identity the probe took: idSequence.release, holdsIdentityFrom), attached behaviors, messages, variant selections and the step write ledger when it returns, and suppresses any note recorded meanwhile — so a later guard that invokes a behavior or spends budget leaves the run exactly as first-match did (TestLaterGuardIsProbedWithoutCost: a cheap and a recursive cost(40) later guard leave the same ctx.steps).

A probed guard that cannot be evaluated is not an alternative and not an error. KerML DecisionPerformance selects exactly one outgoing succession and each guard is a TPCGuardConstraint with inv { allTrue(constrainedGuard()) }: an expression with no result is not true, so its succession is simply not selected, and the library defines no evaluation failure. To make the tool's reading visible it is recorded as a second RunNote kind, UnevaluableGuard (choice.go), on every surface the choices use:

Surface	Rendering
Trace	unevaluable guard step 2: decision select branch 2->alarm: division by zero (not selected) / unevaluable guard state idle on accept Go: transition 2->high: eval guard of transition idle -> high: division by zero (not selected)
Diagnostic	SeverityInfo, Code: guard-unevaluable, Source: runtime, message guard not evaluable: …, span at the guard; on the wire severity: "info" (message prefix distinguishes it from choice point:)
REPL	1 choice point; 1 guard not evaluable; %trace on to see them
Context API	Context.Notes(), UnevaluableGuards(), beside Choices()

Change polling follows the same rule: observeChangeConditions still observes every condition once per poll (the rising edge needs every reading), but a state's guards are read live only until its first enabled transition; the ones after it are read by probeChangeGuard inside a probe, and one that fails to evaluate is noted, not enabled, and left armed for the next poll. Before this change every risen guard was read live and any one failing failed the poll, so a model whose later change guard errors now fires its first enabled transition with a guard-unevaluable note instead of failing.

The first guard or transition read is the run's own, not a probe, and its failure still fails the run as before (TestLaterGuardErrorIsNotAChoiceNorAFailure, TestFirstTransitionFailureStillFailsTheRun, TestExecuteAction_UnevaluableGuardDiagnostics).

Surfaces:

• Trace (-trace, REPL %trace on): TraceRecorder.RecordNote emits the choice … / unevaluable guard … line before the step line.
• gRPC/Connect: ExecuteActionResponse, ExecuteStateResponse, RunAnalysisResponse (both plain analyses and verification cases) carry each choice as an info Diagnostic whose message starts with choice point: (the in-process passes.Diagnostic also carries Code: choice-point, Source: runtime; the wire Diagnostic message stays severity/message/span), on success and on execution-error responses (internal/grpc/convert.go:RunNoteDiagnosticsToProto), unevaluable guards alongside.
• REPL: %step / %continue / %advance (including breakpoint pauses, and after a run that ends in an error) append N choice points; M guards not evaluable; %trace on to see them (each part only when non-zero); with tracing on the hint is dropped since the lines are already visible.
• Context API: Context.Notes(), Choices(), UnevaluableGuards(), reset at each run boundary.

Severity: SeverityInfo, not SeverityHint. A choice point is a true statement about the run that a caller may want to act on (re-run under another schedule, widen an admissible set) — information about the execution, not a stylistic suggestion about the model. Hint in this codebase is reserved for editor-level nudges. Never warning/error: a choice point is not a defect.

Intentional trace golden changes

Every existing golden that changed did so only by gaining choice lines. Probing later guards keeps their evaluation out of the trace, so no golden gains or loses an eval line. No .expected.json changed (ten new ones added).

Six goldens of this branch move a choice / unevaluable guard line without any other change: a write choice is now recorded once the step is over rather than at the second write, so it follows the step's last statement and precedes the token-order line (action_choice_same_step_write_conflict, action_fork_branches_write_one_feature, w7d_send_via_port_to_receiver), and a transition's notes follow its guard's final reading rather than its selection (state_choice_transition_conflict, state_choice_unevaluable_transition, state_choice_shared_ancestor_regions).

Fork concurrency (gained choice step N: tokens … lines; three also gain writes … lines because both branches assign the same feature in one step):
action_accept_suspends_until_message, action_accept_two_waiters, action_block_flow_if_branch_own_flow, action_explicit_succession_fork_join, action_fork_branches_share_features, action_fork_branches_write_one_feature (+writes), action_join_one_token_per_incoming_succession, action_join_same_succession_twice, action_join_three_two_arrive_together (+writes), action_join_waits_for_slowest_branch, action_merge_fork_branch_and_loop, action_nested_flow_in_fork_join, action_nested_node_two_successions_per_performance, action_node_concurrent_nested_bindings, action_node_concurrent_performances, action_node_with_two_incoming_successions_runs_once, f63_merge_body_runs_on_traversal, w7d_send_via_port_to_receiver (+writes).

Decision with overlapping guards: no existing golden has two guards that hold at once; covered by the new action_choice_decision_overlapping_guards fixture.

Transition conflict: no existing golden has two transitions enabled for one event from one state; covered by the new state_choice_transition_conflict fixture.

Unevaluable guard / transition and write through performer / chain: no existing golden exercises them; covered by the new action_choice_unevaluable_guard, state_choice_unevaluable_transition, action_choice_performer_write_conflict and action_choice_chained_write_conflict fixtures.

Specification basis

KerML 1.0 §8.4.4 (Performances / HappensBefore partial order) and SysML v2 1.0 §7.16–7.17 (action succession, decision nodes; transition selection and state hierarchy priority). Moves these rows in docs/project/spec-compliance.md from ⚠️ approximate to ✅ faithful: unordered concurrent performances, conflicting writes within one step, decision node with several holding guards, several enabled transitions on one state. Ancestor-priority transition selection stays as it was (ordered by the spec, not a choice).

How it was verified

New tests:

• Conformance + trace goldens: action_choice_fork_token_order (with .trace.order, two admissible outcomes), action_choice_shared_message_accept, action_choice_decision_overlapping_guards, action_choice_same_step_write_conflict, action_choice_chained_write_conflict (two outcomes), action_choice_performer_write_conflict, action_choice_unevaluable_guard, state_choice_transition_conflict, state_choice_unevaluable_transition, state_choice_ancestor_priority_not_reported, state_choice_shared_ancestor_regions (one choice line for two regions), state_choice_ancestor_outranked_not_reported (no choice line), state_choice_change_transition_conflict (two outcomes, choice … on change).
• Robustness: TestRuntimeRobustness/decision_all_guards_false still returns ErrNoEnabledSuccession and records no choice.
• internal/core/runtime/choice_test.go: TestChoicePointRendering, TestChoicesResetPerRun, TestSharedMessageAcceptIsAChoice, TestTransitionChoiceNamesStateAndEvent, TestLaterGuardErrorIsNotAChoiceNorAFailure (a later guard/transition that divides by zero neither fails the run nor counts as an alternative and is recorded as one guard-unevaluable info note with the guard's span; a first guard that does still fails as before with no note), TestLaterGuardIsProbedWithoutCost, TestFirstTransitionFailureStillFailsTheRun, TestAncestorPriorityIsNotAChoice, TestSharedAncestorChoiceIsReportedOnce, TestAncestorChoiceSuppressedByNestedTransitionIsNotReported, TestTokenOrderIsReportedWhenALaterTokenFails, TestWriteConflictChoice, TestWriteConflictOnOneObjectThroughTwoChains, TestThreeWritersAreOneChoice, TestRepeatedWritesByOneTokenListItsLast (a token's earlier write is no alternative), TestAliasWritesAreOneDestination (performer and chain), TestProbedGuardLeavesObjectIdentitiesUntouched (the same InstanceIDs() whether or not a probed guard made an object), TestNotesOfATransitionBlockedBeforeFiringAreDropped, TestNotesOfATransitionFailingInItsEffectAreKept, TestChangeTransitionChoice, TestLaterChangeGuardErrorIsNotAChoiceNorAFailure (a later change guard that fails to evaluate is a guard-unevaluable note and stays armed, the first enabled transition fires; a first change guard that fails still fails the run), TestChangeTransitionChoiceUnderHierarchyAndRegions (nested change transitions win over the composite's and two regions each fire; only the state with two enabled reports).
• internal/grpc/choice_test.go: TestExecuteAction_ChoicePointDiagnostics, TestExecuteState_ChoicePointDiagnostics, TestRunAnalysis_ChoicePointDiagnostics, TestExecuteAction_UnevaluableGuardDiagnostics, TestExecuteAction_ChoicePointDiagnosticsOnFailure.
• internal/repl/choice_test.go: TestStepReportsChoicePoints, TestStepChoiceSummaryWithTraceOn, TestContinueReportsChoicePoints, TestContinueReportsChoicePointsBeforeFailure, TestAdvanceReportsChoicePoints, TestStepReportsUnevaluableGuards.

End-to-end against the built sysml, sysml-grpc (gRPC and Connect) binaries, compared with a build of the base commit: the three action fixtures' -trace output and the two state fixtures' REPL traces match their goldens; REPL summaries, no-choice models, all-false guards, ancestor priority and error-path wire diagnostics behave as documented; every compared model reaches the same outcome as on the base commit.

Gates (on the branch head):

$ gofmt -l .
$ go build ./...
$ go vet ./...
$ go test ./...                       # all packages ok
$ make lint                           # ✓ Lint passed (staticcheck, gosec)
$ ./scripts/download-training-examples.sh && ./scripts/download-pilot-corpora.sh
$ OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 \
    go test -count=1 ./internal/core/model -run 'TestTrainingExamples|TestPilotCorpora'
ok  	github.com/Open-MBEE/OpenSysML/internal/core/model	13.243s
$ make docs-check                     # OK
$ python3 scripts/changelog.py check  # ok

internal/core/model/testdata/training_examples_expected.txt and the pilot-corpus ratchets are untouched.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (docs/guide/06-behavior.md, docs/reference/cli.md, docs/reference/repl-commands.md, docs/reference/wire-contract.md, docs/project/behavior-semantic-oracle.md, docs/project/spec-compliance.md)
• Changelog entry added as changes/unreleased/execution-choice-points.added.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

[devin-ai-integration]

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

• Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
• Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

On the review flag that the wire Diagnostic carries no stable code, so a client must tell choice-point from guard-unevaluable by message text: the proto Diagnostic (api/proto/sysml.proto) has only severity, message and span, so this is a pre-existing gap for every diagnostic on the wire, not one this PR introduces. Adding code to the message, regenerating, and updating the client libraries and the wire-contract reference is tracked as a follow-up PR and deliberately kept out of this one.