diff --git a/changes/unreleased/execution-choice-points.added.md b/changes/unreleased/execution-choice-points.added.md
new file mode 100644
index 000000000..225bfe1f9
--- /dev/null
+++ b/changes/unreleased/execution-choice-points.added.md
@@ -0,0 +1,18 @@
+- **The executors report every choice point: a pick among alternatives the library leaves
+  unordered.** Several steppable tokens in one action step, several holding guards at a decision
+  node, several enabled transitions out of one state for one event or one change, and several
+  tokens writing one feature in one step are each recorded as a `choice` trace line naming the alternatives and the
+  one taken (`choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)`), as an
+  informational diagnostic on `ExecuteAction`, `ExecuteState` and `RunAnalysis` responses, and as
+  one summary line after `%step`, `%continue` and `%advance` (`2 choice points; %trace on to see
+  them`). What the executor does is unchanged — reverse token order, first holding guard, first
+  declared transition — so every existing result and trace is the same: the guards and
+  transitions after the first that holds are read in a preview that is undone, and one that
+  cannot be evaluated there is not an alternative and not an error but an informational
+  `guard-unevaluable` diagnostic, an `unevaluable guard` trace line and a count in the summary
+  (`1 guard not evaluable`). Writes to the performing part and through a feature chain count as
+  the object's, so two chains reaching one object in one step are one conflict, as are a feature
+  and one redefining it; a step's writes to one feature are one choice listing every token's last
+  write, recorded once the step is complete. The
+  innermost-transition-wins rule between a substate and the state enclosing it is spec-defined
+  order and is not reported.
diff --git a/docs/guide/06-behavior.md b/docs/guide/06-behavior.md
index 55e791bbb..e929fa9df 100644
--- a/docs/guide/06-behavior.md
+++ b/docs/guide/06-behavior.md
@@ -187,6 +187,27 @@ the state or the data a guard reads changes between the send and the dispatch, t
 - `%advance <time>` — Advance simulation time by `<time>` units, processing every event due
 - `%stop` — Stop debugging
 
+**Choice points.** The library orders some things and leaves others open: a succession says
+which step comes first, but nothing says which of two fork branches steps first, which of two
+waiting accepts takes the one message both answer to, which of two holding guards a decision
+follows, which of two transitions out of one state fires on the same event, or whose write
+stands when several branches assign one feature in one step. Where the
+executor has to pick, it follows one fixed rule — reverse token order, first holding guard, first
+declared transition, so a run replays exactly — and records a *choice point* rather than passing
+the pick off as the only outcome. `%step`, `%continue` and `%advance` end with a count of the
+choices they made (`2 choice points; %trace on to see them`), `%trace on` shows each as a
+`choice` line naming the alternatives and the one taken (`choice step 3: tokens 2@left, 3@right
+(unordered; took 3@right first)`), and the gRPC responses carry each as an informational
+diagnostic. A run with no choice points has the one outcome the model states; one with choice
+points has the outcome this executor's rule produces, and the lines say where another rule would
+diverge. The innermost-transition-wins rule between a substate and the state enclosing it is
+spec-defined order, not a choice, and is not reported. Reporting never changes the run: once a
+guard or transition holds, the ones after it are read in a preview that is undone, and one that
+cannot be evaluated there — a division by zero, say — is not an alternative and not an error (a
+guard with no result is not true, so its branch is not taken); it is counted beside the choices
+(`1 guard not evaluable`) and shown in the trace as an `unevaluable guard` line. The first guard
+read is the run's own, and its failure fails the run as it always has.
+
 For complete workflows, see
 [examples/action-executor-demo.sysml](../../examples/action-executor-demo.sysml),
 [examples/orthogonal-regions-demo.sysml](../../examples/orthogonal-regions-demo.sysml) and
diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md
index 3a282b71e..31950251a 100644
--- a/docs/project/behavior-semantic-oracle.md
+++ b/docs/project/behavior-semantic-oracle.md
@@ -50,6 +50,11 @@ scheduling detail the library says nothing about:
 - A state machine records a transition's guard evaluation, exit, effect and entry as they run, and
   evaluates a guard once to select the transition and once again to fire it; the second
   evaluation is a tool detail with no observable effect, since a guard is an expression.
+- A `choice` line marks a point where the executor picked among alternatives the library leaves
+  unordered — several steppable tokens in one step, several holding decision guards, several
+  enabled transitions out of one state for one event, or two tokens writing one feature in one
+  step — and names the alternative it took. Everything after a `choice` line is one linearization
+  among the ones that line admits.
 
 When a golden is reviewed against this record, the question is whether the golden's
 linearization is *one of* the linearizations the derivation admits and whether every outcome the
@@ -209,9 +214,110 @@ against — a run must match exactly one member. The partial order the library d
 as `.trace.order` constraints (`split < left`, `split < right`, `left < sync`, `right < sync`) the
 trace must satisfy. The exact trace golden stays: it records the executor's scheduling (`right`
 is the branch declared last, so its token is stepped first and `left` writes last, giving
-`x = 1`) and exists only so a change in that scheduling is noticed. The compliance row stays
-approximate because the runtime still picks an order the specification does not, and reports no
-conflict.
+`x = 1`) and exists only so a change in that scheduling is noticed. The executor reports the
+conflict as a choice point (`choice step 3: writes x := 1 by token 2, x := 2 by token 3
+(unordered; x := 1 by token 2 stood)`), so the trace and the diagnostics name the value that
+stood as a tool decision rather than passing it off as the model's answer. Companion fixtures:
+`action_choice_same_step_write_conflict` (golden), the same shape over a `String` feature;
+`action_choice_chained_write_conflict` (golden), the same shape writing one object's feature
+through a feature chain (`s.reading`) from both branches; and
+`action_choice_performer_write_conflict` (golden), a performed action's branches both writing
+the part performing it. A destination is the object written and the feature written, whatever
+name reached it, so two chains reaching one object are one conflict
+(`TestWriteConflictOnOneObjectThroughTwoChains`), a feature and one redefining it are one
+destination under either name (`TestAliasWritesAreOneDestination`), and two writes of equal
+value are still one: the library orders the writes no more when they agree. The choice is
+recorded once the step is complete, one per destination, listing the last write of every token
+that wrote it and the one that stood: three branches are one choice of three
+(`TestThreeWritersAreOneChoice`), and a token writing twice contributes only its last write, the
+one that would stand had it gone last (`TestRepeatedWritesByOneTokenListItsLast`).
+
+### A decision with several holding guards: exactly one branch follows, which one is open
+
+Fixture: `action_choice_decision_overlapping_guards` (golden).
+
+```
+start → select ─ if level > 50 → warn  { handler := 1 } → done
+               ─ if level > 70 → alarm { handler := 2 } → done
+```
+
+Derived constraints:
+
+- `select` is followed by a performance of exactly one target (DecisionPerformance: "the
+  outgoingHBLink is an instance of exactly one of the Successions"), so `handler` ends `1` or
+  `2`, never `0`.
+- Each guard is a `TPCGuardConstraint` on its own link; a false guard leaves that link out. With
+  `level = 75` both guards are true, so neither link is excluded by its guard.
+
+Open: which of the two admissible links the decision performance takes. The library says only
+that it is exactly one of them; nothing ranks `warn` against `alarm`.
+
+Pinned outcome: the admissible set `{handler = 1, handler = 2}`, stated as `outcomes` citing this
+section. The executor evaluates every guard, takes the first declared, and records the choice
+(`choice step 2: decision select branches 1->warn, 2->alarm hold (unordered; took 1->warn)`);
+the golden pins that linearization. Reporting never changes the run: the guards after the first
+holding one are read in a preview that is undone — what evaluating them costs, writes or starts
+is restored, and nothing they do is traced — so the run spends and does what first-match did
+(`TestLaterGuardIsProbedWithoutCost`). A guard read that way that cannot be evaluated is not an
+alternative and not an error: the library's `TPCGuardConstraint` is `inv { allTrue(constrainedGuard()) }`,
+an expression with no result is not true, so the link it guards is simply not selected, and the
+library defines no failure for it. The executor records the guard as an informational
+`guard-unevaluable` note (`unevaluable guard step 2: decision select branch 2->alarm: division by
+zero (not selected)`) so the tool's reading is visible without changing the run
+(`TestLaterGuardErrorIsNotAChoiceNorAFailure`; fixture `action_choice_unevaluable_guard`, golden).
+The first guard read is the run's own, not a preview, and its failure fails the run as it always
+has. A decision whose guards are all false remains an execution error
+(`TestRuntimeRobustness/decision_all_guards_false`), as the library then admits no outgoing link.
+
+### Two transitions out of one state enabled by one event: exactly one fires, which one is open
+
+Fixture: `state_choice_transition_conflict` (golden).
+
+```
+idle ─ accept Go if level > 5 → low  { route := 1 }
+     ─ accept Go if level > 7 → high { route := 2 }
+```
+
+Derived constraints:
+
+- A `StateTransitionPerformance` follows its trigger and its guard, and its
+  `transitionLinkSource.exit` follows the guard (`StatePerformances.kerml`); the source performance
+  `idle` ends once, so at most one transition out of it fires for one Go.
+- Both guards hold for `level = 8`, so both transitions are enabled by the one event; the
+  machine ends in `low` or `high`, never still in `idle`.
+
+Open: which enabled transition fires. UML orders a transition on a descendant state before one
+on its ancestor (the case `state_choice_ancestor_priority_not_reported` pins that rule, and the
+executor does not report it as a choice); between two transitions on the *same* state nothing
+in the library or the specification ranks them. The choice is the firing transition's: the
+regions of a parallel state that select the same transition out of it make one choice, reported
+once (`state_choice_shared_ancestor_regions`), and a composite state's transitions that lose to a
+nested one were never chosen among, so nothing about them is reported
+(`state_choice_ancestor_outranked_not_reported`).
+
+Pinned outcome: the admissible set `{route = 1 in low, route = 2 in high}`, stated as `outcomes`
+citing this section. The executor examines every transition out of the state for the event,
+fires the first declared, and records the choice (`choice state idle on accept Go: transitions
+1->low, 2->high (unordered; took 1->low)`); the golden pins that linearization. As for a decision,
+the transitions after the first enabled one are read in a preview that is undone, and one whose
+guard cannot be evaluated is not an alternative and does not fail the dispatch: it is recorded as
+an informational `guard-unevaluable` note naming the state, the event and the transition
+(`TestLaterGuardErrorIsNotAChoiceNorAFailure`; fixture `state_choice_unevaluable_transition`,
+golden). The first transition read is the run's own, and its failure fails the dispatch as it
+always has (`TestFirstTransitionFailureStillFailsTheRun`).
+
+The choice is recorded when the transition fires, not when it is selected: a transition selected
+on the event reads its guard once more as it fires, and one another region's reaction has
+meanwhile disabled does not fire and reports nothing
+(`TestNotesOfATransitionBlockedBeforeFiringAreDropped`), while one whose effect then fails was
+the run's choice all the same (`TestNotesOfATransitionFailingInItsEffectAreKept`). A change
+occurrence is an event like a signal: two `accept when` transitions out of one state whose
+conditions rise on one write are enabled by one occurrence, and the same rule applies — the
+first declared fires, the rise is consumed for the others, and the choice is recorded
+(`choice state watching on change: transitions 1->cool, 2->hot (unordered; took 1->cool)`;
+fixture `state_choice_change_transition_conflict`, golden; `TestChangeTransitionChoice`,
+`TestChangeTransitionChoiceUnderHierarchyAndRegions` for the nested-wins and parallel-region
+shapes).
 
 ### A merge is re-entered on every traversal of a loop
 
diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md
index 7eebecded..3005bfddd 100644
--- a/docs/project/spec-compliance.md
+++ b/docs/project/spec-compliance.md
@@ -485,11 +485,12 @@ by name is refused naming what is missing rather than approximated.
 | Final node termination | `action_executor.go:512` stepFinalNode | `action_control_flow.sysml` | ✅ Faithful |
 | One feature space per performance: a succession is a `HappensBefore` link (Kernel Semantic Library `Occurrences.kerml`) that orders occurrences and carries no values, so the steps of an action — concurrent ones included — read and write the features of the one action they belong to; and each nested action node is a performance of its own (`Actions::Action :> Performance`, `subactions :> subperformances`), holding the parameters and attributes it declares and those of the action it performs in a frame of its own, so same-named pins on two nodes do not collide, `node.pin` reads and `bind`/`flow` ends address that frame (two bindings at one input pin must agree, else `ErrBindingConflict`; a binding at an undirected attribute of a node is kept at both ends: the node reads the other end as it begins and carries back what it changed as it ends; an end that chains through an object, `bind add.sum = holder.inner.mark`, writes the feature of the object the chain reaches, typed as an assignment through it is), a body-local `in a = 3;` on a typed node and the positional or named arguments of `action n = Callee(3, 4)` seed the callee's inputs by the callee's own parameter order and names, and an untyped `n` read as a value is the callee's `result`; a typed or invoked node's subactions are those of the action it performed, so `call.inner.v` reads through it; a pin holding an object is chained through like any feature, so `pick.target.mark` reads a member of the object at the pin; a read of `p.v` in a branch is of that branch's `p` where the other branch declares one too; a feature a node declares with a sibling node's name shadows that node, so `pick.mark` in the node reads its own object-valued `pick`; a nested body still resolves the enclosing action's features lexically and writes them in place | `runtime/action_frame.go` `actionFrame`, `beginPerformance`, `seedDeclaredValues`, `performInvocation`/`adopt`, `nodesNamed`/`subaction`, `bindInputPins`/`bindOutputPins`, `deliver`, `collect`; `runtime/action_executor.go` `ActionExecutor.root`, `stepNestedAction`, `Results`/`Data`; `runtime/eval.go` `lookupSubaction`/`evalSubactionPath`; `runtime/invoke_action.go` `bindArgumentList`; `lower/action_graph.go` `ActionGraph.Features`/`Scopes`/`Bindings`, `Feature`, `PinBinding`, `lowerFeatures`, `lowerPinBindings`, `lowerInheritedPinConnections` (over `resolve.ActionGeneralBodies`); `runtime/action_executor.go` `deliverFlow` | `conformance/action_fork_branches_share_features.sysml` + trace golden, `action_executor_test.go:TestActionExecutor_ForkNode_SharedFeatureSpace`; `conformance/action_node_pins_isolated` + trace golden, `action_node_pins_two_levels` + trace golden, `action_node_typed_body_inputs`, `action_node_invocation_positional`, `action_node_invocation_named`, `action_node_dependent_default`, `action_node_bind_input`, `action_node_bind_input_agreeing`, `action_node_bind_overrides_default`, `action_node_arguments_read_caller`, `action_node_default_reads_calc_per_performance`, `action_node_bind_output`, `action_node_bind_undirected_attribute`, `action_node_bind_output_through_chain`, `action_node_bind_undirected_through_chain`, `action_node_body_writes_enclosing`, `action_flow_between_same_named_pins`, `action_node_concurrent_performances` + trace golden, `action_node_bind_nested_to_enclosing`, `action_node_concurrent_nested_bindings` + trace golden, `action_node_pin_read_before_performed` (`ErrNodeNotPerformed`), `action_block_flow_sibling_pins` + trace golden, `action_block_flow_loop_node_frames`, `action_block_flow_nested_pins`, `action_block_flow_if_branch` + trace golden, `action_block_flow_nested_action` + trace golden, `action_block_flow_if_branch_bindings`, `action_block_flow_loop_bindings` + trace golden, `action_node_typed_nested_pins`, `action_block_flow_else_branch_same_name`, `action_block_flow_alternating_branch_nodes`, `action_node_pin_object_member`, `action_node_feature_shadows_sibling_node`, `action_inherited_node_bindings`; `lower/action_node_frame_test.go`, `lower/block_graph_test.go`, `lower/action_inherited_test.go:TestToActionGraphInheritedPinConnections`; `robustness_test.go:node_pin_of_a_node_not_yet_performed`, `:node_pin_the_node_does_not_declare`, `:block_node_pin_of_a_node_not_yet_performed`, `:block_node_pin_the_node_does_not_declare`, `:else_branch_node_read_before_it_performs` (`ErrNodeNotPerformed`), `:typed_node_pin_of_a_node_the_callee_does_not_declare`, `:node_read_as_a_value_without_a_result` (`ErrNodePin`), `:node_pin_member_through_a_scalar_pin`, `:node_invocation_too_many_arguments`, `:node_invocation_too_few_arguments` (`ErrActionArity`, `ErrUnboundParameter`), `:node_invocation_unknown_named_argument` (`ErrUnknownParameter`), `:node_binding_to_a_non_parameter`, `:node_binding_output_to_an_unknown_feature`, `:node_binding_output_through_a_scalar_chain`, `:node_binding_output_through_a_chain_violates_target_type` (`ErrBindingEnd`), `:node_undirected_binding_carried_to_a_non_parameter` (`ErrNodePin`), `:node_pin_bound_to_unequal_values` (`ErrBindingConflict`), `:node_output_bound_to_a_nested_node_that_never_runs` (`ErrBindingEnd`), `:block_node_binding_to_a_non_parameter` (`ErrBindingEnd`), `:block_node_binding_names_a_node_without_a_pin`, `:inherited_binding_names_a_node_without_a_pin`, `:block_node_pin_bound_where_nodes_are_not_performed`, `:node_flow_into_a_pin_the_target_does_not_declare` (`ErrNodePin`), `:performed_action_input_bound_by_nothing`, `:state_entry_action_input_bound_by_nothing` (`ErrUnboundParameter`) | ⚠️ Approximate (self-assessed: the pinned OMG pilot implementation executes no actions. A node's frame is a runtime frame, not a materialized occurrence, so it has no identity a `send` could address and `Results()` reports it as `p.v`, the latest performance of the node standing for it; a node reached from two fork branches is one performance that follows both, holding at each of its pins the one delivery the flow into that pin carried and sending its outputs on once (`action_node_concurrent_performances`; two `flow`s into one `[1]` pin of one performance are a model conflict the runtime does not yet refuse — it keeps the earliest delivery, a limitation, not a rule); a pin holds, in order of precedence, what a flow delivered, what a `bind` at it gives, then the value the node's own declaration states, and a declared value written in terms of another pin reads what that pin holds. A pin of an untyped `action n = Callee(args)` is read as `n` — the callee's `result` — while `n.pin` on it is refused by name resolution, which does not type `n` by the invocation; write it as a typed usage `action n : Callee` to read `n.pin`. An action declared in an `if` branch or a loop body is a node of that block's own flow (`lower/block_graph.go` `lowerNestedNode`, `ActionGraph.BlockNodes`) and a performance of its own like any other node, begun by the statement engine (`runtime/action_statements.go` `performNode`) with the block's locals — a loop variable — in reach, so a sibling in the branch reads its pins as `p.v` and `Results()` reports them under its path, and a `bind` or `flow` written in the block at one of its nodes' pins is lowered into the block's own flow (`lower/block_graph.go` `lowerBlockConnector`) and applied per performance, so `bind dbl.a = i` in a loop body seeds each iteration's node from that iteration's variable; a loop performs the node once per iteration and the latest performance stands for it; a debugger breakpoint on such a node pauses the run before each performance of it (`runtime/action_body_run.go` `runPausable`/`pauseAt`, `ActionExecutor.NodeNames` over `lower.BlockFlows`; `debug_api_test.go:TestBreakpointPausesBeforeABranchNode`, `:TestBreakpointPausesOnEachLoopIteration`, `:TestBreakpointPausesInsideABlockNodesOwnFlow`, `repl/runtime_commands_test.go:TestBreakpointOnABlockNodePausesEachIteration`). A binding end naming a pin two levels down, `bind leg.inner.w = x`, carries the whole path (`PinBinding.Path`), so it addresses `inner`'s pin and not one of `leg`; and a binding between a nested pin and a pin of the node around it, or of another node under that node — `bind leg.inner.v = leg.v`, `bind leg.inner.v = leg.rest.n` — holds within the one performance of `leg` the nested node runs in, the performance that follows both fork branches feeding `leg`'s pins, so an inner's output is never queued for a performance yet to come (`runtime/action_frame.go` `otherEnd`; `action_node_bind_nested_to_enclosing`, `action_node_concurrent_nested_bindings`) (`action_node_bind_nested_pin_path`, `lower/action_node_frame_test.go:TestActionBindingAtANestedNodePin`, `:TestActionBindingAtANodePinThroughAChain`, `robustness_test.go:nested_pin_binding_into_a_node_performing_another_action`, `:nested_pin_binding_at_an_undeclared_pin` (`ErrBindingEnd`), `:flow_reaching_into_a_nodes_own_flow`; a binding reaching into a node that performs an action of its own, and a `flow` end reaching past one node into its own flow — a flow joins pins of the nodes of one flow — are refused when the graph is lowered). A `bind` or `flow` a general action states at a pin of a node the derived action inherits applies to that node's performance too, evaluated in the general action's scope and once per declaring action however many generalization paths reach it, while one at a node the derived action does not sequence lowers to nothing. Such a connector follows its node's declaration, not its name: where the derived action declares a node of its own under the inherited node's name, the general's connector lowers to nothing rather than attaching to the replacement's same-named pin, while one redefining the inherited node (`action add :>> add`, directly or through another redefinition) takes it; a binding between two of the general's nodes holds at both ends or at neither, so one whose other end names a node the derived action replaced lowers to nothing rather than reading the replacement's pin by name (`lower/action_graph.go` `inheritedNodeLookup` over `resolve.ActionNodeOfBody`/`RedefinesActionNode`, `bindsReplacedNode`; `action_inherited_node_masked.sysml`, `action_inherited_node_redefined.sysml`, `action_inherited_node_binding_other_end_replaced.sysml`, `lower/action_inherited_test.go:TestToActionGraphInheritedPinConnectionsFollowDeclarationIdentity`, `robustness_test.go:inherited_binding_does_not_reach_a_masking_node`, `inherited_binding_does_not_reach_through_a_replaced_other_end`). A `perform` in statement form and a state's entry/do/exit action are invocations too (`runtime/invoke_action.go` `invokeAction`): an `in` without a default that no argument or same-named caller value binds is refused before the callee runs (`ErrUnboundParameter`). For compatibility with the flat feature space this replaces, a bare typed usage `action call : Callee;` with no binding at a pin still reads an unbound `in` from the same-named enclosing feature — an invocation `Callee()` passes nothing and lets the callee's defaults apply, which are evaluated in declaration order after the supplied inputs are bound, so a default may read an earlier input — and every invocation form still returns its `out` values into same-named enclosing features that exist once the node's own body has run, so a body that rewrites an output returns what it wrote (`action_invoked_node_body_writes_output`) — a `bind` or `flow` at the pin is the spelled form) |
 | Fork node (1→N parallelism): SysML v2 §7.17.3 rule 4 requires target multiplicity 1..1 on every outgoing succession; `Actions::ForkAction` has no inherent behavior and duplicates control, not values | `action_executor.go:654` `stepForkNode` | `conformance/action_fork_branches_share_features.sysml` + `.expected.json` + trace golden; `robustness_test.go:fork_without_a_successor` (`ErrInvalidActionFlow`) | ✅ Faithful |
+| Concurrent performances are unordered: `HappensBefore` links (Kernel Semantic Library `Occurrences.kerml`) order only the occurrences a succession joins, so two tokens steppable in one step are ordered by nothing in the library | `action_executor.go` `Step` (tokens step in reverse index order, the executor's own rule); `action_choice.go` `beginStepOrder`, `offeredMessage`, `stepTokenNoting`, `tokenActed`, `noteTokenOrder` (the tokens that acted in one step — moved, retired, forked, joined, resumed, took a message or failed — and every accept a message in flight at the step's start would have answered had another token not taken it first are a choice point naming each as `id@node` and the one stepped first; not one held at an accept nothing in flight answers or an unready join, nor one the step itself created; a step that fails still records the order it took before failing); `action_subflow.go` (a nested flow's step records its own) | `conformance/action_choice_fork_token_order.sysml` + `.expected.json` (one outcome; `.trace.order` admits the tokens either way) + trace golden; `conformance/action_choice_shared_message_accept.sysml` + `.expected.json` + trace golden (one message two parked accepts answer to: the choice names the accept left waiting as well as the recipient); `choice_test.go:TestSharedMessageAcceptIsAChoice`; every fork/join trace golden carries the `choice step N: tokens …` lines its concurrency implies (`action_explicit_succession_fork_join`, `action_join_waits_for_slowest_branch`, `action_nested_flow_in_fork_join`, …); `choice_test.go:TestTokenOrderIsReportedWhenALaterTokenFails`; `repl/choice_test.go:TestStepReportsChoicePoints`, `:TestContinueReportsChoicePointsBeforeFailure`; `grpc/choice_test.go:TestExecuteAction_ChoicePointDiagnostics`, `:TestExecuteAction_ChoicePointDiagnosticsOnFailure` | ✅ Faithful (the order is tool-defined and stable — deterministic replay is kept — and every step that had one to make says so in the trace, on the response's diagnostics and in the debugger's summary line) |
 | Join node (N→1 synchronization): SysML v2 §7.17.3 rule 3 requires source multiplicity 1..1 on every incoming succession; `Actions::JoinAction` (Systems Library `Actions.sysml`: "Join behavior results from requiring that the source multiplicity of all incoming succession connectors be 1..1") synchronizes control and merges no values; each incoming succession is a `HappensBefore` link (Kernel Semantic Library `Occurrences.kerml`; `TransitionPerformances.kerml` `TransitionPerformance` `transitionLink: HappensBefore[0..1]`) whose later occurrence is the one join performance, so the join follows exactly one performance of every source — one per succession, not one per token | `lower/action_graph.go` `ActionEdge` (`Source`, `Target`, `Guard`, `Decl` — a comparable identity for every succession, implicit block-flow edges included); `runtime/executor_common.go` `Token.Via` (the edge a token travelled, zero for a token no succession delivered), `Token.travel`; `runtime/action_executor.go` `synchronize` (from `stepToken`, before the node kind is dispatched), `arrival`, `awaitedSuccessions`, `Awaiting`, `stepJoinNode` (passes the one token on) | `conformance/action_fork_branches_share_features.sysml` + `.expected.json` + trace golden; `conformance/action_join_waits_for_slowest_branch.sysml`, `action_join_one_token_per_incoming_succession.sysml`, `action_join_same_succession_twice.sysml`, `action_join_three_two_arrive_together.sysml`, each + trace golden and derived from the library text in [the semantic oracle](behavior-semantic-oracle.md); `action_explicit_succession_fork_join`, `action_nested_flow_in_fork_join`, `state_fork_join_pseudostate` + trace goldens; `robustness_test.go:deadlock_join_starvation`, `:deadlock_join_same_succession_twice` (`ErrActionDeadlock`); `repl/runtime_commands_test.go:TestTokensShowHeldJoinArrivals`; `debug_api_test.go:TestBreakpointPausesOncePerSynchronizedPerformance`, `:TestBreakpointOnALoopedNodePausesEachPass`, `:TestBreakpointOnANestedFirstNodePausesWhileOthersSynchronize`, `repl/runtime_commands_test.go:TestBreakpointOnAConvergingNodePausesOnce` (a breakpoint on a join or a plain node several successions reach pauses once per performance, with every arrival in) | ✅ Faithful (a token records the succession it travelled, and a join fires when one token has arrived over each of its incoming successions: the earliest token per succession collapse into one fresh token that performs the join, and a second token over an already-delivered succession stays held for the join's next firing rather than standing in for another succession — `action_join_one_token_per_incoming_succession` completes with `log = 12`, `action_join_same_succession_twice` with `log = 1212`. A held token is progress-neutral like an accept-parked one, so a join one of whose successions no token can travel deadlocks the run (`ErrActionDeadlock`) rather than firing on a token count; the REPL's `%tokens` says which succession a held token arrived over and which it awaits. A step moves each token at most once — `ActionExecutor.Step` numbers its sweep, and a token that sweep moved, created or sent into a nested flow (`enterSubflow`) takes its next step once it ends — so the last arrival's step leaves the held tokens at the node and the next performs it, and a debugger breakpoint on the node stops there once, before the performance, not once per arriving token) |
-| Concurrent branches assigning the same feature | `action_executor.go:529` stepForkNode (branches write the shared space in step order) | `conformance/action_fork_branches_write_one_feature.sysml` + `.expected.json` + trace golden ([the semantic oracle](behavior-semantic-oracle.md) derives that both branches run and both writes precede the join, and pins the runtime's pick of `x = 1` as tool-defined); `robustness_test.go:fork_branches_assigning_the_same_feature` | ⚠️ Approximate (branches out of a fork are unordered by the spec, so a same-feature write from each leaves the value unspecified; the runtime steps tokens in a fixed order and the last write in *that* order stands — step order, not the order the branches are written in — deterministic per model, but not a spec-mandated outcome, and no conflict is reported; the golden locks that order against regression, it does not make it a derived outcome) |
+| Concurrent branches assigning the same feature | `action_executor.go` stepForkNode (branches write the shared space in step order); `action_choice.go` `noteWrite`, `stepWriteLedger.noteChoices` (several tokens writing one destination — the object and the shared `FeatureValue` written, so a feature and one redefining it are one destination, whether the action's own feature, the performer's via `assignPerformerFeature`, or a chained object's via `writeThroughChain` — in one step are recorded once the step is complete as one choice point naming the feature, every token's last write and the one that stood) | `conformance/action_fork_branches_write_one_feature.sysml` + `.expected.json` + trace golden ([the semantic oracle](behavior-semantic-oracle.md) derives that both branches run and both writes precede the join, and pins the runtime's pick of `x = 1` as tool-defined); `conformance/action_choice_same_step_write_conflict.sysml` + `.expected.json` (both outcomes listed as admissible) + trace golden; `conformance/action_choice_chained_write_conflict.sysml` + `.expected.json` (both outcomes) + trace golden; `conformance/action_choice_performer_write_conflict.sysml` + `.expected.json` + trace golden; `choice_test.go:TestWriteConflictChoice`, `:TestWriteConflictOnOneObjectThroughTwoChains`, `:TestAliasWritesAreOneDestination`, `:TestThreeWritersAreOneChoice`, `:TestRepeatedWritesByOneTokenListItsLast`; `robustness_test.go:fork_branches_assigning_the_same_feature` | ✅ Faithful (branches out of a fork are unordered by the spec, so a same-feature write from each leaves the value open between the two; the runtime steps tokens in a fixed order and the last write in *that* order stands, and it reports the pick as a `choice` trace line and an informational diagnostic — `writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 1 by token 2 stood)` — so the outcome is one of the admissible ones and is labelled as a tool-defined order rather than passed off as the derived one) |
 | Merge node (N→1 non-blocking): SysML v2 §7.17.3 rule 1 gives incoming successions source multiplicity 0..1; `Actions::MergeAction` (Systems Library `Actions.sysml`: "a MergePerformance that selects exactly one incoming HappensBeforeLink. Incoming succession connectors to a MergeAction must have source multiplicity 0..1 and subset the incomingHBLink feature inherited from MergePerformance") is a `MergePerformance` (Kernel Semantic Library `ControlPerformances.kerml`: `incomingHBLink: HappensBefore[1]` — "For each instance of MergePerformance, the incomingHBLink is an instance of exactly one of the Successions, ordering the MergePerformance as happening after an instance of the source of that Succession"), so every arrival is its own merge performance following its own one source — a loop re-enters the merge on every pass, and each of a fork's branches traverses it — where a join (`JoinAction`, source multiplicity 1..1 on every incoming succession) or a plain node follows one performance per succession; the loop's exit is the `DecisionPerformance`'s (`outgoingHBLink` "is an instance of exactly one of the Successions") and its termination the guard's; a guarded succession out of the merge is a `DecisionTransitionAction` (Systems Library `Actions.sysml`: "the base type of TransitionUsages used as conditional successions in action models"), a `NonStateTransitionPerformance` (Kernel Semantic Library `TransitionPerformances.kerml`: `in feature transitionLinkSource: Performance[1]`, `binding transitionLink.earlierOccurrence = transitionLinkSource`, `succession [1] transitionLinkSource then [1] Performance::self`) whose guard constrains the `HappensBefore` link through `TPCGuardConstraint` (`constrainedHBLink` / `constrainedGuard`, `inv { allTrue(constrainedGuard()) }`) — so the merge performance, body included, is complete before its guard is read, and a false guard drops the link to the successor, not the merge's performance | `runtime/action_executor.go` `stepMergeNode` (checks the one outgoing succession, runs the merge's body, then evaluates the succession's guard and forwards the token or retires it — per arrival, no per-run traversal record), `synchronizes` (exempts `MergeNode` from the multi-incoming synchronization `stepToken` applies to every other node kind); `chargeActionStep` (`ErrActionStepLimitExceeded`) bounds an unguarded loop | `conformance/action_decision_merge_guarded_branch.sysml` + `.expected.json` + trace golden; `conformance/action_merge_loop_reenters.sysml` + trace golden (the specification's `ChargeBattery` loop: `monitor` reads `level` at 0, 50 and 100, the third `decide` takes `endCharging`, `level = 100`, `passes = 3`), `action_merge_loop_three_passes.sysml` + trace golden (`count = 3`, `merged = 3`: one merge body run per pass), `action_merge_fork_branch_and_loop.sysml` + trace golden (a merge reached directly from a fork, through the fork's other branch and twice more through a guarded loop: `merged = 4`, `worked = 4`, `passes = 4`), `f63_merge_body_runs_on_traversal.sysml` + trace golden (a fork's direct arrival performs the merge with the guard false and is retired, the second arrival performs it again and passes: `mergeRuns = 2`, `passed = 2`), `action_merge_body_flips_own_guard.sysml` + trace golden (the merge body's own increment is what its outgoing guard reads: `arrivals = 3`, `continued = 2`), all derived from the library text in [the semantic oracle](behavior-semantic-oracle.md); `action_executor_test.go:TestActionExecutor_MergeNode`, `:TestActionExecutor_MergeNode_ControlOnly` (two fork branches into one merge yield two downstream tokens), `:TestActionExecutor_GuardedSuccession_PrunedMergeStaysOpen`; `robustness_test.go:merge_without_a_successor` (`ErrInvalidActionFlow`), `:unguarded_loop_through_a_merge` (`start → m → a → m` with no exit: `RunToCompletion` returns `ErrActionStepLimitExceeded`, and direct `Step` calls keep the one token circling until `RunToCompletion` reports the same); `repl/runtime_commands_test.go:TestActionDebuggerStepsAnUnguardedMergeLoop` (`%step` walks the loop, `%continue` reports the step budget) | ✅ Faithful (a merge passes each arriving token, runs its body once per arrival before its outgoing guard is read, and never blocks; two arrivals from a fork are two merge performances and two downstream tokens — collapsing them is a join's job, not a merge's) |
 | An action node reached over several successions is one performance that follows all of them: a step with no declared multiplicity holds one value (KerML 1.0 §7.4.5), and each succession into it is a `HappensBefore` link (Kernel Semantic Library `Occurrences.kerml`) whose later occurrence is that performance | `runtime/action_executor.go` `synchronize` — the join row's one gate, applied from `stepToken` to every node kind but a merge (`synchronizes`; `Actions::MergeAction` passes each arrival on) — with `awaitedSuccessions`, `reachableFrom` and `leaves` deciding which successions a plain node awaits; `runtime/action_subflow.go` `Token.positionIn` (a token in a nested flow stands at the node performing it) | `conformance/action_node_with_two_incoming_successions_runs_once.sysml` + trace golden, `action_nested_node_two_successions_per_performance.sysml` + trace golden (two performances of an action holding such a node each perform it once), `action_node_concurrent_performances` + trace golden and `action_node_concurrent_nested_bindings` + trace golden (a flow-owning node reached from two fork branches performs once, each flow at its own pin), all derived in [the semantic oracle](behavior-semantic-oracle.md); `action_node_converges_after_decision` + trace golden (a plain node behind a decision's two branches performs once for the branch taken, no deadlock) and `action_node_loop_back_reperforms` + trace golden (a plain node a loop re-enters performs once per pass), with `action_decision_else_done`, `action_guard_reads_calc_usage`, `action_succession_guard_fork_branch_pruned` and `f63_control_node_body` pinning the same at final nodes and under fork guards; `robustness_test.go:deadlock_join_starvation`, `:deadlock_join_same_succession_twice` pin that a join, unlike a plain node, awaits an unreachable source (`ErrActionDeadlock`) | ✅ Faithful (`hits = 1`: the tokens arriving over the node's successions collapse into one performance, per performance of the owning action. A join awaits every incoming succession, its sources being 1..1; a plain node awaits a succession only once it has delivered or while some token of the activation, other than one held at the node, can still reach its source without passing through the node or through a join that node must feed — a decision branch whose guard did not hold, or a succession back from a node downstream of this one, orders no performance before this one, so a loop through a plain node re-performs it once per iteration rather than deadlocking) |
-| Decision node (guarded branching): SysML v2 §7.17.3 rule 2 gives outgoing successions target multiplicity 0..1; `Actions::DecisionAction` selects exactly one outgoing `HappensBeforeLink` | `action_executor.go:829` `stepDecisionNode` | `conformance/action_decision_merge_guarded_branch.sysml` + `.expected.json` + trace golden; `robustness_test.go:decision_no_satisfied_guard` (`ErrNoEnabledSuccession`) | ✅ Faithful |
+| Decision node (guarded branching): SysML v2 §7.17.3 rule 2 gives outgoing successions target multiplicity 0..1; `Actions::DecisionAction` selects exactly one outgoing `HappensBeforeLink` | `action_executor.go` `stepDecisionNode`, `probeGuard` (guards are evaluated in order until one holds, as `enabledSuccessions` evaluates them out of any other node; the ones after it are read in a `beginProbe` preview that restores the budget, the trace, every effect and the object identities the preview took; the first that holds is taken, an unguarded succession is the fallback when none holds; a previewed guard that fails to evaluate is no alternative and no error, recorded as a `guard-unevaluable` note by `noteUnevaluableGuard`), `action_choice.go` `noteDecisionBranches` (several holding guards are a choice point naming the branches by position and target) | `conformance/action_decision_merge_guarded_branch.sysml` + `.expected.json` + trace golden; `conformance/action_choice_decision_overlapping_guards.sysml` + `.expected.json` (both outcomes listed as admissible) + trace golden; `conformance/action_choice_unevaluable_guard.sysml` + `.expected.json` + trace golden; `choice_test.go:TestChoicesResetPerRun`, `:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestLaterGuardIsProbedWithoutCost`; `grpc/choice_test.go:TestExecuteAction_UnevaluableGuardDiagnostics`; `repl/choice_test.go:TestStepReportsUnevaluableGuards`; `robustness_test.go:decision_no_satisfied_guard`, `:decision_all_guards_false` (`ErrNoEnabledSuccession`) | ✅ Faithful (the library selects exactly one link but does not say which when several guards hold, so the pick is the executor's and is reported as one) |
 | Action execution nodes | `action_executor.go:723` stepActionExecutionNode | `action_control_flow.sysml` | ✅ Faithful |
 | Nested action invocation (`action call : Callee;`, `action call = Callee(3, 4);`, `action call = Callee(a = 3);`, `perform action call : Callee;`) | `runtime/action_frame.go` `bindArguments`, `performInvocation`, `checkInputsBound`; `runtime/state_statements.go` `stateStmtHost.performNode`; `runtime/invoke_action.go` `invocationArguments`, `bindArgumentList`, `Context.actionParametersOf` (over `semantics.Model.BehaviorParametersOf`, so inherited and redefined parameters keep their effective order); `action_executor.go` `stepNestedAction` | `invoke_action_test.go:TestInvokeActionPassesParametersBothWays`, `:TestInvokeActionBindsPositionalArguments`, `:TestInvokeActionBindsNamedArguments`, `:TestInvokeActionRejectsBadArguments`; `conformance/action_node_invocation_positional`, `action_node_invocation_named`, `action_node_typed_body_inputs`, `action_node_inherited_parameters`, `action_node_invocation_empty`, `action_inherited_typed_node_scope`, `action_node_arguments_before_defaults`, `state_block_flow_node_arguments_before_defaults` | ✅ Faithful (arguments bind the callee's inputs by the callee's parameter order and names, never by what the caller happens to name alike; they bind the node's pins before the defaults it declares are evaluated, so a default an argument replaces is never evaluated and one the node keeps reads the argument's value, in an action's flow and in a state's body alike; the callee is resolved where the node was declared, so a node a derived action inherits still finds a callee visible only to the general action; a surplus, missing, unknown or repeated argument is `ErrActionArity`, `ErrUnboundParameter`, `ErrUnknownParameter` or `ErrDuplicateArgument` before the callee runs — a surplus one is also reported statically by `passes/typecheck_expr.go`, so no conformance fixture states it. The row above states the compatibility by-name fallback a bare usage keeps) |
 | Assignment statement in a body (`assign x := <expr>`) | `lower/action_graph.go` lowerStatement Assign; `runtime/action_statements.go` execStatement | `action_send_accept.sysml`, `lower/action_body_test.go:TestActionBodyLowering` | ✅ Faithful |
@@ -570,6 +571,7 @@ by name is refused naming what is missing rather than approximated.
 | Deferred events retained while a deferring state is active, delivered afterwards in arrival order — a message on the bus addressed to the machine that its active configuration defers, accepting it nowhere, is the machine's to take and hold, as one it accepts is | `parser/behavior.go` parseDeferMember (`defer <event>[, <event>]*;`); `lower/state_graph.go` stateNodeFromUsage, collectDeferred; `state_executor.go` defersEvent, recallDeferredEvents, acceptableMessage, defersMessage | `parser/testdata/parse/state_defer.golden`, `parser/state_notation_test.go:TestDeferMemberParsing`, `lower/state_notation_test.go:TestToStateGraph_DeferNotation`, `state_deferred_event.sysml` + `state_undeferred_event.sysml` conformance, `state_deferred_test.go`, `signal_injection_test.go:TestPostedMessageTheActiveStateDefersIsHeld`, `repl/send_test.go:TestSendDefersWhatTheActiveStateDefers` | ✅ Faithful |
 | Earliest transfer first (`Occurrence::incomingTransferSort` defaults to `earlierFirstIncomingTransferSort`): a recalled event is dispatched before the events that arrived while it was deferred, and a completion event before either | `executor_common.go` eventHeap.Less, isCompletionEvent; `state_executor.go` recallDeferredEvents | `state_deferred_test.go:TestRecalledEventPrecedesLaterArrivals` | ✅ Faithful |
 | A transition out of a composite state is enabled while any of its substates is active: matching walks outward from every active leaf through the lowered containment (`StateGraph.ParentState`), the innermost enabled transition wins for the same event, and a false guard does not consume it | `state_executor.go` broadcastEvent, selectTransitions, losesToNestedTransition, nestedIn, activeLeaves, fireFrom, enabledTransition, acceptsSignal/acceptsSignalFrom (an enclosing state's `accept` takes a signal off the bus) | `conformance/state_composite_outer_transition.sysml`, `:state_composite_inner_priority.sysml`, `state_composite_transition_test.go:TestCompositeStateHandlesEventItsSubstateDoesNot`, `:TestFalseGuardInsideACompositeStateFallsOutward`, `:TestTransitionOutOfAnIntermediateCompositeStateKeepsItsOwnerActive`, `:TestOuterCompositeStateStillHandlesItsEventAfterASubstateMoved`, `robustness_test.go:signal_no_level_of_a_composite_state_accepts` | ✅ Faithful |
+| Two transitions out of one state enabled by one event: each is a `StateTransitionPerformance` (Kernel Semantic Library `StatePerformances.kerml`) whose `transitionLink` is `HappensBefore[0..1]`, and nothing in the library orders one against another, so which fires is the executor's pick; the innermost-wins rule between a substate's transition and its enclosing state's is UML/SysML order, not a pick | `state_executor.go` `enabledTransition`, `transitionEnabled`, `probeTransition` (every transition out of the state is matched against the event and its guard and join evaluated — a call trigger's arguments bound for the guard and unbound after — the first enabled fires; the ones after it are read in a `beginProbe` preview that restores the budget, the trace, every effect and the object identities the preview took, and one that fails to evaluate is no alternative and no error, recorded as a `guard-unevaluable` note by `unevaluableTransition`), `transitionChoice` (several enabled are a choice point naming the state, the trigger and the transitions by position and target); the notes ride on the `dispatchCandidate` into `fireFrom`, and `transitionDecided` records them once the firing transition's guard has been read for the last time — a candidate another region's firing disabled meanwhile reports nothing — after `selectCandidates` has kept one candidate per transition and `losesToNestedTransition` has dropped a composite state's candidate to a nested one (a transition several regions select through their enclosing state is one choice, and ancestor priority is never among the alternatives); `state_change_trigger.go` `observeChangeConditions`, `probeChangeGuard`, `risenChangeTransition` (every change transition risen by one poll is collected the same way: a state's guards are read live until the first enabled, the ones after it in a `beginProbe` preview, and one that fails to evaluate is no alternative and no error, noted as `guard-unevaluable` and left armed; the first declared fires) | `conformance/state_choice_transition_conflict.sysml` + `.expected.json` (both outcomes listed as admissible) + trace golden; `conformance/state_choice_ancestor_priority_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_shared_ancestor_regions.sysml` + `.expected.json` + trace golden (one `choice` line for two regions); `conformance/state_choice_ancestor_outranked_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_unevaluable_transition.sysml` + `.expected.json` + trace golden; `conformance/state_choice_change_transition_conflict.sysml` + `.expected.json` (both outcomes) + trace golden; `choice_test.go:TestTransitionChoiceNamesStateAndEvent`, `:TestAncestorPriorityIsNotAChoice`, `:TestSharedAncestorChoiceIsReportedOnce`, `:TestAncestorChoiceSuppressedByNestedTransitionIsNotReported`, `:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestNotesOfATransitionBlockedBeforeFiringAreDropped`, `:TestNotesOfATransitionFailingInItsEffectAreKept`, `:TestChangeTransitionChoice`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestChangeTransitionChoiceUnderHierarchyAndRegions`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteState_ChoicePointDiagnostics`; `repl/choice_test.go:TestAdvanceReportsChoicePoints` | ✅ Faithful (declaration order is tool-defined and kept; the pick is reported, and the ordered case is not) |
 | Taking a transition out of a composite state exits the states being left innermost-first, then runs the effect, then enters the target; leaving a composite with orthogonal regions exits every active region first | `state_executor.go` transitionToInto (exit to the least common ancestor), exitStates/exitedByAncestorRegion (a state whose region another state being left owns is exited by that state's recursive region teardown, so the chain walk does not exit it a second time), `state_region_transition.go` leaveRegion (which instead clears the region a state is active in, recording its history, before exiting that state, since a region's active state may be nested below it), moveBetweenRegions, exitRegionTo, leaveTopRegions | `conformance/state_composite_exit_order.sysml` + trace golden (two levels of nesting), `:state_composite_orthogonal_exit.sysml` + trace golden, `:state_composite_nested_regions_exit_once.sysml` + trace golden (a region holding a composite with a region of its own: every level exits exactly once), `robustness_test.go:exit_of_nested_regions_with_a_history_pseudostate` | ✅ Faithful |
 | Every state transition is external — its source is exited, its effect runs, and its target is entered afresh — including when the target is the source itself or one of its substates: KerML orders `transitionLinkSource then effect` and `effect then transitionLink.laterOccurrence` (Kernel Semantic Library `TransitionPerformances.kerml`, `TransitionPerformance`), the source's `exit` is its last step (`StatePerformances.kerml`, `StatePerformance`: `entry then middle`, `middle then exit`) and a state transition orders that exit after its guard (`StateTransitionPerformance`: `guard then transitionLinkSource.exit`). So a simple state transitioning to itself runs exit, effect, entry, and a composite is exited and re-entered around the effect with its regions restarting at their initial states | `state_executor.go` transitionToInto, encloses (the source is the target or contains it); `state_region_transition.go` moveBetweenRegions (the exit boundary is the source's parent where the source `encloses` the target, so a composite self-transitioning inside an orthogonal region is exited too, while its sibling regions stay as they were) | `conformance/state_composite_self_transition.sysml` + trace golden (exit substate, exit composite, effect, re-enter composite and its region), `:state_composite_to_substate.sysml` + trace golden, `:state_composite_self_transition_in_region.sysml` + trace golden, `:w6e_state_simple_self_transition.sysml` + trace golden (exit, effect, entry on a simple state), `parse/w6e_state_self_transition.golden`, `state_composite_transition_test.go:TestOneEventTakesACompositesTransitionOnce`, `w6e_state_self_transition_test.go:TestSimpleSelfTransitionExitsAndReEntersItsState`, `:TestSimpleSelfTransitionInARegionLeavesSiblingRegionsAlone`, `robustness_test.go:composite_self_transition_with_no_substate_to_re_enter`, `w6e_robustness_test.go:TestSimpleSelfTransitionThatNeverSettlesIsBounded`, `:TestSimpleSelfTransitionEffectReadingAnUnknownFeatureIsReported`; `conformance/state_transition_guard_exit_effect_entry_order.sysml` + trace golden (the order made observable through values: the guard reads the pre-exit value, the effect the exit's, the entry the effect's — derived from the same library text in [the semantic oracle](behavior-semantic-oracle.md)) | ✅ Faithful (self-assessed: the pinned reference has no execution surface for state machines, so this row is assessed against the library text cited above and our own goldens, not against another implementation. One residual is tool-defined: a composite state stating no starting substate — no `initial` and no region — is re-entered with no substate active, since nothing names the substate to enter) |
 | An event reaches only the regions still active when it is dispatched | `state_executor.go` broadcastEvent (each active leaf is re-checked before it is offered the event) | `state_deferred_test.go:TestExitedNestedRegionDoesNotReactToTheSameEvent` | ✅ Faithful |
diff --git a/docs/reference/cli.md b/docs/reference/cli.md
index bdf95f87b..70c990abf 100644
--- a/docs/reference/cli.md
+++ b/docs/reference/cli.md
@@ -160,7 +160,7 @@ reported, so a script that reads it takes the output from the first `{`.
 | `--debug` | | Report every diagnostic over the whole session buffer, with the pass that produced it |
 | `--quiet` | | Report errors only, suppressing warnings |
 | `--strict` | | Judge the model as conforming SysML v2: notation no pinned production admits is an error, not a warning (see [Strict conformance](../guide/03-command-line.md#strict-conformance)) |
-| `--trace` | | Report each execution step: expression evaluation, calc invocation, action tokens, state transitions |
+| `--trace` | | Report each execution step: expression evaluation, calc invocation, action tokens, state transitions, each `choice` the executor made among alternatives the library leaves unordered, naming the alternatives and the one taken, and each `unevaluable guard` it read only to report one and could not evaluate ([Choice points](../guide/06-behavior.md)) |
 | `--convert <format>` | | Convert the model instead of running it: `sysml`, `kerml`, `ttl`, `turtle` or `rdf`. RDF is [experimental](rdf-mapping.md#status-experimental) and every run that converts it says so on stderr (see [the RDF mapping](rdf-mapping.md)) |
 | `--from <format>` | | Input format for `--convert`: the `--convert` formats, or `xmi`/`mdzip` for a SysML v1 model to migrate (default: from the input's extension; `.xmi` and `.mdzip` are recognized) — see [SysML v1 migration](sysml-v1-migration.md) |
 | `--migration-report <file>` | | With `--convert` from `xmi`: write the element-by-element migration report to this file, JSON when it ends in `.json`, text otherwise. Without it the one-line summary goes to stderr |
diff --git a/docs/reference/repl-commands.md b/docs/reference/repl-commands.md
index bfe8e6f26..92b3b77e9 100644
--- a/docs/reference/repl-commands.md
+++ b/docs/reference/repl-commands.md
@@ -23,7 +23,7 @@ into the parts it holds (`car.fl.hub`, `#3.fl`, `car.wheels[2]`).
 | `%save <file>` | Write the session model to a file: `.sysml` notation (comments preserved) or `.ttl` RDF, which is [experimental](rdf-mapping.md#status-experimental) and reported as such on each save |
 | `%query <oslc-query>` | Identify model elements using OSLC Query text |
 | `%verbosity [level]` | Show or set output level: `quiet` (errors only), `normal`, `debug` (every diagnostic over the whole buffer) |
-| `%trace [on\|off]` | Show or set execution tracing: each evaluation, calc invocation, action step and state transition |
+| `%trace [on\|off]` | Show or set execution tracing: each evaluation, calc invocation, action step and state transition, and each `choice` the executor made among alternatives the library leaves unordered — several steppable tokens, several holding decision guards, several enabled transitions out of one state for one event, two tokens writing one feature in one step — naming the alternatives and the one taken, and each `unevaluable guard` it read only to report one and could not evaluate ([Choice points](../guide/06-behavior.md)). `%step`, `%continue` and `%advance` end with a count of the choices they made and of the guards they could not evaluate (`1 choice point; 1 guard not evaluable`) whether or not tracing is on |
 | `%strict [on\|off]` | Show or set strict conformance: report notation no SysML v2 production admits as an error, and reprint the session's diagnostics under the new mode ([Strict conformance](../guide/03-command-line.md#strict-conformance)) |
 | `%budget` | Show the five bounds one run may spend, each with the variable that raises it |
 | **Library Discovery** | |
diff --git a/docs/reference/wire-contract.md b/docs/reference/wire-contract.md
index 96d298204..6fe0a62d9 100644
--- a/docs/reference/wire-contract.md
+++ b/docs/reference/wire-contract.md
@@ -710,7 +710,41 @@ $ … /ExecuteAction -d '{"modelHash":"b4e0…ded9","actionSymbolId":"Test::noSt
 
 An action with no outputs answers `{}` (captured for `action nop { first start; done;
 succession first start then done; }`). The response carries no step trace; ordering-sensitive
-behavior is pinned by the engine's golden traces, not exposed on this call.
+behavior is pinned by the engine's golden traces, not exposed on this call. What it does carry
+is every *choice point* the run made — a step in which the executor picked among alternatives
+the library leaves unordered (several steppable tokens, several holding decision guards, two
+tokens writing one feature in one step; see [Choice points](../guide/06-behavior.md)) — as an
+`"info"` diagnostic located at the action, present beside `outputs` on success and beside
+`error` when the run failed after making one (captured for `action tally { attribute leftCount :
+Integer = 0; attribute rightCount : Integer = 0; first start; fork split; action left { assign
+leftCount := leftCount + 1; } action right { assign rightCount := rightCount + 10; } join sync;
+done; … }` with a succession from `split` to each branch and from each to `sync`, in `tally.sysml`):
+
+```console
+$ … /ExecuteAction -d '{"modelHash":"81b1…73fc","actionSymbolId":"Test::tally"}'
+{"outputs":{"leftCount":{"intValue":"1"},"rightCount":{"intValue":"10"}},"diagnostics":[{"severity":"info","message":"choice point: step 3: tokens 2@left, 3@right (unordered; took 3@right first)","span":{"file":"tally.sysml","startLine":2,"startCol":2,"endLine":20,"endCol":2}}]}
+```
+
+A run with no `diagnostics` had exactly one order to take. The order taken is the engine's fixed
+rule, the same on every call, so the outputs are reproducible; the diagnostics say where another
+rule would have been equally valid.
+
+To report a decision's choice the engine reads the guards after the first holding one in a
+preview it undoes, so reading them costs and changes nothing. One it cannot evaluate there is
+not an alternative and not an error — a guard with no result is not true, so its branch is not
+selected — and is reported as a second kind of `"info"` diagnostic, `guard not evaluable: …`,
+naming the step, the decision, the branch by position and target, and the failure, located at
+the guard (for `action route { attribute level : Integer = 75; … then decide select; if level > 50
+then warn; if 1 / (level - 75) > 0 then alarm; … }`):
+
+```console
+$ … /ExecuteAction -d '{"modelHash":"81b1…73fc","actionSymbolId":"Test::route"}'
+{"outputs":{"level":{"intValue":"75"},"handler":{"intValue":"1"}},"diagnostics":[{"severity":"info","message":"guard not evaluable: step 2: decision select branch 2->alarm: division by zero (not selected)","span":{"file":"tally.sysml","startLine":31,"startCol":10,"endLine":31,"endCol":30}}]}
+```
+
+The first guard read is the run's own, not a preview: when it cannot be evaluated the run fails
+with `error` as it always has, and no `guard not evaluable` diagnostic is added. The two kinds are
+told apart by message prefix, `choice point: ` and `guard not evaluable: `; both are `"info"`.
 
 ### `ExecuteState`
 
@@ -738,7 +772,21 @@ $ … /ExecuteState -d '{"modelHash":"b4e0…ded9","stateMachineSymbolId":"Test:
 ```
 
 `finalContext` is absent when the machine has no variables; `statesVisited` lists a state each
-time it is entered, so a state entered twice appears twice.
+time it is entered, so a state entered twice appears twice. `diagnostics` carries an `"info"`
+entry for each event that enabled several transitions out of one state, located at the
+transition taken, as `ExecuteAction`'s does for its steps, and a `guard not evaluable: <state> on
+<trigger>: transition <n>-><target>: <failure> (not selected)` entry for a transition after the
+first enabled one whose guard it could not evaluate in its preview. Both belong to the transition
+that fires: a transition out of a parallel state that several of its regions select is one entry,
+and a transition on a substate beating one on the state enclosing it is spec-defined order, so
+nothing about the beaten state's transitions is reported. For `state def Hub { entry;
+then Idle; state Idle; state A; state B; transition first Idle accept Go then A; transition first
+Idle accept Go then B; }` in the same document:
+
+```console
+$ … /ExecuteState -d '{"modelHash":"81b1…73fc","stateMachineSymbolId":"Test::Hub","events":["Go"]}'
+{"statesVisited":["Idle","A"],"diagnostics":[{"severity":"info","message":"choice point: state Idle on accept Go: transitions 1->A, 2->B (unordered; took 1->A)","span":{"file":"tally.sysml","startLine":25,"startCol":3,"endLine":26,"endCol":3}}]}
+```
 
 ### `EvaluateCalc`
 
@@ -850,7 +898,8 @@ $ … /VerifyRequirement -d '{"modelHash":"96c9…994d","symbolId":"Ver::touchdo
 
 A step that fails, a body that deadlocks or exhausts its step budget and a case that runs itself are
 `FAILURE_REASON_EVALUATION` failures naming the case. Structured and complex arguments are
-capability-gated as `EvaluateCalc`'s are.
+capability-gated as `EvaluateCalc`'s are. The choice points the case's steps made are its
+`diagnostics`, shaped as `ExecuteAction`'s.
 
 ### `RunSweep`
 
diff --git a/internal/core/runtime/action_choice.go b/internal/core/runtime/action_choice.go
new file mode 100644
index 000000000..d976f671a
--- /dev/null
+++ b/internal/core/runtime/action_choice.go
@@ -0,0 +1,320 @@
+package runtime
+
+import (
+	"fmt"
+	"slices"
+	"sort"
+
+	"github.com/Open-MBEE/OpenSysML/internal/core/ast"
+	"github.com/Open-MBEE/OpenSysML/internal/core/lower"
+	"github.com/Open-MBEE/OpenSysML/internal/core/source"
+	"github.com/Open-MBEE/OpenSysML/internal/core/symbols"
+)
+
+// The choice points an action run makes; recording one never alters what the
+// executor does (reverse token order, first holding guard, later write stands).
+
+// writeDest identifies a feature a write reaches: one a performance holds under
+// its canonical name, or one an object holds under any of its names (FeatureValue).
+type writeDest struct {
+	holder  *actionFrame
+	object  *Instance
+	feature *FeatureValue
+	name    string
+}
+
+// stepWrite is one write a step made: by which token, and what it wrote.
+type stepWrite struct {
+	token int64
+	value Value
+}
+
+// destWrites is what one step wrote to one destination: each token's last write,
+// in the order the tokens first wrote, and the write that stands.
+type destWrites struct {
+	label string // the destination as a trace names it: `x`, or `x of object #3`
+	file  string
+	span  source.Span
+	last  []stepWrite
+	stood stepWrite
+}
+
+// stepWriteLedger is what the action step under way wrote so far, by destination.
+type stepWriteLedger struct {
+	step   int
+	writer int64 // the token whose step is running, 0 between tokens
+	writes map[writeDest]*destWrites
+	order  []writeDest // destinations in the order first written
+}
+
+// beginStepWrites opens the ledger of the writes one step makes, numbered step;
+// the closer returned records its choices and restores the ledger it shadowed.
+func (e *performances) beginStepWrites(step int) func() {
+	saved := e.ctx.stepWrites
+	ledger := &stepWriteLedger{step: step, writes: make(map[writeDest]*destWrites)}
+	e.ctx.stepWrites = ledger
+	return func() {
+		ledger.noteChoices(e.ctx)
+		e.ctx.stepWrites = saved
+	}
+}
+
+// beginTokenStep marks the token whose step is running, returning what to
+// restore once its step is over.
+func (e *performances) beginTokenStep(id int64) func() {
+	ledger := e.ctx.stepWrites
+	if ledger == nil {
+		return func() {}
+	}
+	saved := ledger.writer
+	ledger.writer = id
+	return func() { ledger.writer = saved }
+}
+
+// noteFrameWrite records a write the running token made to a feature f holds.
+func (e *performances) noteFrameWrite(f *actionFrame, name string, value Value) {
+	file, span := e.ctx.featureLocation(f.scope, name)
+	key := f.key(name)
+	e.ctx.noteWrite(writeDest{holder: f, name: key}, key, value, file, span)
+}
+
+// noteObjectWrite records a write the running token made to a feature obj holds,
+// under whichever of its names the write spelled.
+func (ctx *Context) noteObjectWrite(obj *Instance, name string, value Value) {
+	dest := writeDest{object: obj, name: name}
+	var file string
+	var span source.Span
+	if fv := obj.FeatureValues[name]; fv != nil {
+		dest = writeDest{object: obj, feature: fv}
+		if fv.Feature != nil && fv.Feature.Symbol != nil {
+			file, span = fv.Feature.Symbol.DocName, fv.Feature.Symbol.DeclSpan
+		}
+	}
+	ctx.noteWrite(dest, fmt.Sprintf("%s of object #%d", name, obj.ID), value, file, span)
+}
+
+// noteWrite records a write the running token made to dest, labelled as a trace
+// names it; destinations several tokens wrote are reported once the step ends.
+func (ctx *Context) noteWrite(dest writeDest, label string, value Value, file string, span source.Span) {
+	ledger := ctx.stepWrites
+	if ledger == nil || ledger.writer == 0 {
+		return
+	}
+	w := stepWrite{token: ledger.writer, value: value}
+	d := ledger.writes[dest]
+	if d == nil {
+		d = &destWrites{label: label, file: file, span: span}
+		ledger.writes[dest] = d
+		ledger.order = append(ledger.order, dest)
+	}
+	d.stood = w
+	if i := slices.IndexFunc(d.last, func(prev stepWrite) bool { return prev.token == w.token }); i >= 0 {
+		d.last[i] = w
+		return
+	}
+	d.last = append(d.last, w)
+}
+
+// noteChoices records each destination two or more tokens wrote within the step
+// as a choice point, whatever they wrote: another order lets another write stand.
+func (l *stepWriteLedger) noteChoices(ctx *Context) {
+	for _, dest := range l.order {
+		d := l.writes[dest]
+		if len(d.last) < 2 {
+			continue
+		}
+		writes := slices.Clone(d.last)
+		sort.Slice(writes, func(i, j int) bool { return writes[i].token < writes[j].token })
+		alts := make([]string, len(writes))
+		taken := 0
+		for i, w := range writes {
+			alts[i] = fmt.Sprintf("%s := %s by token %d", d.label, FormatTraceValue(w.value), w.token)
+			if w.token == d.stood.token {
+				taken = i
+			}
+		}
+		ctx.noteChoice(ChoicePoint{
+			Kind:         ChoiceWriteOrder,
+			Step:         l.step,
+			Alternatives: alts,
+			Taken:        taken,
+			File:         d.file,
+			Span:         d.span,
+		})
+	}
+}
+
+// featureLocation locates the declaration of the feature name resolves to in
+// scope, for a diagnostic about a write to it; "" when none resolves.
+func (ctx *Context) featureLocation(scope *symbols.Scope, name string) (string, source.Span) {
+	if ctx.resolver == nil || scope == nil {
+		return "", source.Span{}
+	}
+	sym, ok := ctx.resolver.LookupName(scope, name)
+	if !ok || sym == nil {
+		return "", source.Span{}
+	}
+	return sym.DocName, sym.DeclSpan
+}
+
+// stepOrder collects the tokens of one step that could have gone first, in the
+// order the step reached them: the ones it advanced, and an accept a message in
+// flight would have answered had another not taken it first.
+type stepOrder struct {
+	firstNew int64          // tokens from this ID on were created by the step itself
+	unready  map[int64]bool // held at a join whose branches had not all arrived
+	offered  map[int64]bool // at an accept a message in flight answers
+	acted    []Token
+}
+
+// beginStepOrder opens the order of a step about to run.
+func (e *ActionExecutor) beginStepOrder() stepOrder {
+	order := stepOrder{firstNew: e.nextTokenID, unready: make(map[int64]bool), offered: make(map[int64]bool)}
+	for _, t := range e.tokens {
+		if consumed, held := e.arrivals(t); held && consumed == nil {
+			order.unready[t.ID] = true
+		}
+	}
+	if pending := e.ctx.PendingMessages(); len(pending) > 0 {
+		// Matching may materialize a port; as a probe, the scan leaves the run as it was.
+		defer e.ctx.beginProbe()()
+		for _, t := range e.tokens {
+			if e.offeredMessage(t, pending) {
+				order.offered[t.ID] = true
+			}
+		}
+	}
+	return order
+}
+
+// offeredMessage reports whether one of the messages in flight answers the accept
+// the token sits at, so that stepping it first would have taken the message.
+func (e *ActionExecutor) offeredMessage(t Token, pending []Message) bool {
+	usage, ok := t.Location.(*ast.Usage)
+	if !ok || t.body != nil {
+		return false
+	}
+	accept, isAccept := e.graphOf(t.frame).Accepts[usage]
+	if !isAccept || accept.Trigger != nil {
+		return false
+	}
+	matches, _ := e.acceptMatch(t.frame, accept, usage)
+	return slices.ContainsFunc(pending, matches)
+}
+
+// stepTokenNoting steps the token at index i and notes it in order when it did
+// something it could have done first (not parked, and not enabled by this step),
+// or was offered a message another token took first. A step that fails was still
+// the token's turn, so the order taken is complete.
+func (e *ActionExecutor) stepTokenNoting(i int, order *stepOrder) error {
+	before := e.tokens[i]
+	count := len(e.tokens)
+	err := e.stepToken(i)
+	if order.eligible(before) && (err != nil || order.offered[before.ID] || e.tokenActed(before, count)) {
+		order.acted = append(order.acted, before)
+	}
+	return err
+}
+
+// eligible reports whether the token could have gone first in the step and is
+// not yet noted.
+func (o *stepOrder) eligible(t Token) bool {
+	if t.ID >= o.firstNew || o.unready[t.ID] {
+		return false
+	}
+	for _, a := range o.acted {
+		if a.ID == t.ID {
+			return false
+		}
+	}
+	return true
+}
+
+// tokenActed reports whether the step of the token snapshotted as before moved,
+// consumed, retired, resumed, forked or joined it, or took its awaited message.
+func (e *ActionExecutor) tokenActed(before Token, count int) bool {
+	if before.body != nil || len(e.tokens) != count {
+		return true
+	}
+	i := e.tokenIndex(before.ID)
+	if i < 0 {
+		return true
+	}
+	after := e.tokens[i]
+	return after.moved != before.moved || (before.Wait != nil && after.Wait == nil)
+}
+
+// noteTokenOrder records the tokens a step advanced as a choice point when there
+// are at least two; which went first is the executor's rule, not the library's.
+func (e *ActionExecutor) noteTokenOrder(step int, order stepOrder) {
+	if len(order.acted) < 2 {
+		return
+	}
+	first := order.acted[0].ID
+	tokens := make([]Token, len(order.acted))
+	copy(tokens, order.acted)
+	sort.Slice(tokens, func(i, j int) bool { return tokens[i].ID < tokens[j].ID })
+	alts := make([]string, len(tokens))
+	taken := 0
+	for i, t := range tokens {
+		alts[i] = fmt.Sprintf("%d@%s", t.ID, nodeIdentifier(t.Location))
+		if t.ID == first {
+			taken = i
+		}
+	}
+	e.ctx.noteChoice(ChoicePoint{
+		Kind:         ChoiceTokenOrder,
+		Step:         step,
+		Alternatives: alts,
+		Taken:        taken,
+		File:         e.action.DocName,
+		Span:         e.action.DeclSpan,
+	})
+}
+
+// noteDecisionBranches records the holding guarded successions of a decision node,
+// at their declared positions, as a choice point when there are at least two.
+func (e *ActionExecutor) noteDecisionBranches(frame *actionFrame, node *ast.DecisionNode, successors []lower.ActionEdge, holding []int) {
+	if len(holding) < 2 {
+		return
+	}
+	alts := make([]string, len(holding))
+	for i, pos := range holding {
+		alts[i] = branchName(successors, pos)
+	}
+	e.ctx.noteChoice(ChoicePoint{
+		Kind:         ChoiceDecisionBranch,
+		Step:         e.stepCount + 1,
+		Where:        "decision " + nodeIdentifier(node),
+		Alternatives: alts,
+		Taken:        0,
+		File:         e.decisionFile(frame),
+		Span:         node.Span(),
+	})
+}
+
+// noteUnevaluableGuard records the guard of the succession at position pos out of
+// a decision node, probed once the branch was decided, as one with no result.
+func (e *ActionExecutor) noteUnevaluableGuard(frame *actionFrame, node *ast.DecisionNode, successors []lower.ActionEdge, pos int, err error) {
+	e.ctx.noteUnevaluableGuard(UnevaluableGuard{
+		Step:        e.stepCount + 1,
+		Where:       "decision " + nodeIdentifier(node),
+		Alternative: branchName(successors, pos),
+		Reason:      err.Error(),
+		File:        e.decisionFile(frame),
+		Span:        successors[pos].Guard.Span(),
+	})
+}
+
+// branchName names a decision's succession by declared position and target.
+func branchName(successors []lower.ActionEdge, pos int) string {
+	return fmt.Sprintf("%d->%s", pos+1, nodeIdentifier(successors[pos].Target))
+}
+
+// decisionFile is the file the flow frame performs was declared in.
+func (e *ActionExecutor) decisionFile(frame *actionFrame) string {
+	if scope := e.graphOf(frame).Scope; scope != nil && scope.DocName() != "" {
+		return scope.DocName()
+	}
+	return e.action.DocName
+}
diff --git a/internal/core/runtime/action_executor.go b/internal/core/runtime/action_executor.go
index 7b5440242..8224ecff1 100644
--- a/internal/core/runtime/action_executor.go
+++ b/internal/core/runtime/action_executor.go
@@ -242,42 +242,24 @@ func (e *ActionExecutor) Step() error {
 		tokenLocationsBefore[i] = t.Location
 	}
 
-	// Collect token indices to step (snapshot before iteration)
-	tokenIndices := make([]int, len(e.tokens))
-	for i := range e.tokens {
-		tokenIndices[i] = i
-	}
-
 	// The tokens a breakpoint left paused resume last, the longest paused first,
 	// once every other token has had its step: one pausing again and again does
 	// not hold the rest back.
 	paused := e.pausedTokens()
 	defer e.beginSweep()()
 
-	// Step tokens in reverse order to handle removal safely
-	// (removing token at higher index doesn't affect lower indices)
-	for i := len(tokenIndices) - 1; i >= 0 && e.state != StateSuspended; i-- {
-		// Check if token still exists (may have been removed by join/final)
-		if i >= len(e.tokens) || e.moving(e.tokens[i]) ||
-			e.tokens[i].drivenByBody() || e.tokens[i].body != nil {
-			continue
-		}
+	// Several tokens advanced in one step are a choice point the library leaves open.
+	order := e.beginStepOrder()
+	endWrites := e.beginStepWrites(e.stepCount + 1)
 
-		if err := e.stepToken(i); err != nil {
-			e.endPausedBodies()
-			return err
-		}
-	}
-	for _, id := range paused {
-		if e.state == StateSuspended {
-			break
-		}
-		if i := e.tokenIndex(id); i >= 0 {
-			if err := e.stepToken(i); err != nil {
-				e.endPausedBodies()
-				return err
-			}
-		}
+	err := e.stepTokens(len(e.tokens), paused, &order)
+	// What the tokens wrote and the order they took are facts of the step whether
+	// or not it failed.
+	endWrites()
+	e.noteTokenOrder(e.stepCount+1, order)
+	if err != nil {
+		e.endPausedBodies()
+		return err
 	}
 
 	// A step a breakpoint ends leaves every other token where it was, yet the run
@@ -848,6 +830,7 @@ func (e *ActionExecutor) stepToken(tokenIdx int) error {
 	if tokenIdx < 0 || tokenIdx >= len(e.tokens) {
 		return fmt.Errorf("invalid token index %d", tokenIdx)
 	}
+	defer e.beginTokenStep(e.tokens[tokenIdx].ID)()
 
 	if e.tokens[tokenIdx].body != nil {
 		return e.resumeBody(tokenIdx)
@@ -1076,20 +1059,73 @@ func (e *ActionExecutor) enabledSuccessions(frame *actionFrame, node ast.Node) (
 // guardHolds evaluates the guard a succession out of node carries; a succession
 // carrying none is unconditional.
 func (e *ActionExecutor) guardHolds(ec *EvalContext, node, guard ast.Node) (bool, error) {
-	if guard == nil {
-		return true, nil
-	}
-	result, err := ec.Eval(guard)
+	result, err := guardResult(ec, guard)
 	if err != nil {
 		return false, fmt.Errorf("eval guard of %s: %w", nodeDescription(node), err)
 	}
-	if result.Kind != ValConst || result.Const.Kind != semantics.ValBool {
+	if !result.isBool() {
 		return false, fmt.Errorf("%w: %s: guard must evaluate to boolean, got %v",
 			ErrTypeMismatch, nodeDescription(node), result.Kind)
 	}
 	return result.Const.Bool, nil
 }
 
+// guardResult is what a guard evaluates to; no guard is true.
+func guardResult(ec *EvalContext, guard ast.Node) (Value, error) {
+	if guard == nil {
+		return boolValue(true), nil
+	}
+	return ec.Eval(guard)
+}
+
+// probeGuard reads the guard of the succession at position i out of a decision
+// node whose branch is already decided, as a probe the context undoes whole: the
+// read reports a choice and leaves the run as it was. A guard with no result is
+// noted and not selected.
+func (e *ActionExecutor) probeGuard(frame *actionFrame, node *ast.DecisionNode, successors []lower.ActionEdge, i int) bool {
+	result, err := func() (Value, error) {
+		defer e.ctx.beginProbe()()
+		ec := e.evalContextFor(frame, e.graphOf(frame).Scope)
+		defer ec.beginStep()()
+		return guardResult(ec, successors[i].Guard)
+	}()
+	if err == nil && !result.isBool() {
+		err = fmt.Errorf("%w: guard must evaluate to boolean, got %v", ErrTypeMismatch, result.Kind)
+	}
+	if err != nil {
+		e.noteUnevaluableGuard(frame, node, successors, i, err)
+		return false
+	}
+	return result.Const.Bool
+}
+
+// stepTokens gives each of the first count tokens its step, highest index first
+// so a removal leaves the lower indices in place, then the tokens a breakpoint
+// left paused; a breakpoint reached on the way ends the sweep.
+func (e *ActionExecutor) stepTokens(count int, paused []int64, order *stepOrder) error {
+	for i := count - 1; i >= 0 && e.state != StateSuspended; i-- {
+		// The token may have been removed by a join or final node.
+		if i >= len(e.tokens) || e.moving(e.tokens[i]) ||
+			e.tokens[i].drivenByBody() || e.tokens[i].body != nil {
+			continue
+		}
+		if err := e.stepTokenNoting(i, order); err != nil {
+			return err
+		}
+	}
+	for _, id := range paused {
+		if e.state == StateSuspended {
+			break
+		}
+		if i := e.tokenIndex(id); i >= 0 {
+			if err := e.stepTokenNoting(i, order); err != nil {
+				return err
+			}
+		}
+	}
+	return nil
+}
+
 // stepInitialNode advances token from initial node to successors.
 func (e *ActionExecutor) stepInitialNode(tokenIdx int) error {
 	token := &e.tokens[tokenIdx]
@@ -1294,12 +1330,14 @@ func (e *ActionExecutor) stepDecisionNode(tokenIdx int) error {
 	defer ec.beginStep()()
 
 	// Two-pass evaluation:
-	// 1. Evaluate all guarded edges first
-	// 2. If none match, use unguarded edge as fallback (else branch)
+	// 1. Evaluate all guarded edges; take the first that holds (several: a choice point)
+	// 2. If none holds, use unguarded edge as fallback (else branch)
 
 	var unguardedEdge *lower.ActionEdge
+	var holding []int
 
-	// Pass 1: Check guarded edges
+	// Pass 1: Check guarded edges. Once one holds the branch is decided; the rest
+	// are probed only to report the choice, which leaves the run as it was.
 	for i := range successors {
 		edge := &successors[i]
 		// No guard = remember for fallback
@@ -1308,15 +1346,24 @@ func (e *ActionExecutor) stepDecisionNode(tokenIdx int) error {
 			continue
 		}
 
-		holds, err := e.guardHolds(ec, decisionNode, edge.Guard)
-		if err != nil {
-			return err
+		var holds bool
+		if len(holding) > 0 {
+			holds = e.probeGuard(token.frame, decisionNode, successors, i)
+		} else {
+			var err error
+			if holds, err = e.guardHolds(ec, decisionNode, edge.Guard); err != nil {
+				return err
+			}
 		}
 		if holds {
-			token.travel(*edge, e.sweep)
-			return nil
+			holding = append(holding, i)
 		}
 	}
+	if len(holding) > 0 {
+		e.noteDecisionBranches(token.frame, decisionNode, successors, holding)
+		token.travel(successors[holding[0]], e.sweep)
+		return nil
+	}
 
 	// Pass 2: Use unguarded edge as fallback
 	if unguardedEdge != nil {
diff --git a/internal/core/runtime/action_frame.go b/internal/core/runtime/action_frame.go
index d44f4a8d9..f2be50d27 100644
--- a/internal/core/runtime/action_frame.go
+++ b/internal/core/runtime/action_frame.go
@@ -615,12 +615,17 @@ func (e *performances) takeDeliveries(f *actionFrame, node ast.Node, perf *actio
 // performance occurrence for the action's own features.
 func (e *performances) setFrameFeature(f *actionFrame, name string, value Value) error {
 	if f == e.root {
-		return e.owner.setFeature(name, value)
+		if err := e.owner.setFeature(name, value); err != nil {
+			return err
+		}
+		e.noteFrameWrite(f, name, value)
+		return nil
 	}
 	if err := e.ctx.checkNamedWrite(f.scope, f.describe(), name, value); err != nil {
 		return err
 	}
 	f.data[f.key(name)] = value
+	e.noteFrameWrite(f, name, value)
 	return nil
 }
 
diff --git a/internal/core/runtime/action_subflow.go b/internal/core/runtime/action_subflow.go
index 58b71922a..7444b27ba 100644
--- a/internal/core/runtime/action_subflow.go
+++ b/internal/core/runtime/action_subflow.go
@@ -100,13 +100,19 @@ func (e *ActionExecutor) runSubflow(perf *actionFrame) error {
 func (e *ActionExecutor) stepSubflow(perf *actionFrame) (bool, error) {
 	before := e.subflowLocations(perf)
 	defer e.beginSweep()()
-	for i := len(e.tokens) - 1; i >= 0; i-- {
+	order := e.beginStepOrder()
+	endWrites := e.beginStepWrites(e.stepCount + 1)
+	var err error
+	for i := len(e.tokens) - 1; i >= 0 && err == nil; i-- {
 		if i >= len(e.tokens) || e.moving(e.tokens[i]) || !e.tokens[i].inFlowOf(perf) {
 			continue
 		}
-		if err := e.stepToken(i); err != nil {
-			return false, err
-		}
+		err = e.stepTokenNoting(i, &order)
+	}
+	endWrites()
+	e.noteTokenOrder(e.stepCount+1, order)
+	if err != nil {
+		return false, err
 	}
 	after := e.subflowLocations(perf)
 	if len(after) != len(before) {
diff --git a/internal/core/runtime/assign_chain.go b/internal/core/runtime/assign_chain.go
index 231b4c7e6..2f93847f7 100644
--- a/internal/core/runtime/assign_chain.go
+++ b/internal/core/runtime/assign_chain.go
@@ -32,7 +32,11 @@ func writeThroughChain(ec *EvalContext, chain *lower.AssignTarget, feature strin
 	}
 	// Written through the object itself, so the value is multiplicity-checked and
 	// seen by every feature reaching that object, as a direct write is.
-	return target.SetFeatureValue(ec.ctx, feature, value)
+	if err := target.SetFeatureValue(ec.ctx, feature, value); err != nil {
+		return err
+	}
+	ec.ctx.noteObjectWrite(target, feature, value)
+	return nil
 }
 
 // chainCarrier walks a chained target's steps to the object whose feature the
diff --git a/internal/core/runtime/choice.go b/internal/core/runtime/choice.go
new file mode 100644
index 000000000..9d8ca9e7e
--- /dev/null
+++ b/internal/core/runtime/choice.go
@@ -0,0 +1,236 @@
+package runtime
+
+import (
+	"fmt"
+	"strings"
+
+	"github.com/Open-MBEE/OpenSysML/internal/core/passes"
+	"github.com/Open-MBEE/OpenSysML/internal/core/source"
+)
+
+// ChoiceKind names what an executor chose among at a choice point.
+type ChoiceKind int
+
+const (
+	// ChoiceTokenOrder: several tokens were steppable in one step, and the step
+	// advanced them in an order the library does not fix.
+	ChoiceTokenOrder ChoiceKind = iota
+	// ChoiceDecisionBranch: several guards of one decision node held.
+	ChoiceDecisionBranch
+	// ChoiceWriteOrder: two tokens wrote one feature within one step, so which
+	// value the feature holds afterwards is the order the writes were applied in.
+	ChoiceWriteOrder
+	// ChoiceTransition: several transitions out of one state were enabled for
+	// one event.
+	ChoiceTransition
+)
+
+// String is the kind as a trace or diagnostic names it.
+func (k ChoiceKind) String() string {
+	switch k {
+	case ChoiceTokenOrder:
+		return "token order"
+	case ChoiceDecisionBranch:
+		return "decision branch"
+	case ChoiceWriteOrder:
+		return "write order"
+	case ChoiceTransition:
+		return "transition"
+	}
+	return fmt.Sprintf("ChoiceKind(%d)", int(k))
+}
+
+// ChoiceDiagnosticCode is the code every choice-point diagnostic carries.
+const ChoiceDiagnosticCode = "choice-point"
+
+// UnevaluableGuardCode is the code a diagnostic about a guard the run could not
+// evaluate carries.
+const UnevaluableGuardCode = "guard-unevaluable"
+
+// RunNote is a finding a run records about itself without changing it: a choice
+// point it made, or a guard it read only to report one and could not evaluate.
+type RunNote interface {
+	// Describe renders the note for a diagnostic; String is its trace line.
+	Describe() string
+	String() string
+	// Diagnostic is the note as an informational finding about the run.
+	Diagnostic() passes.Diagnostic
+	// Location is the file and span of the declaration the note is about; file is
+	// "" when the runtime could not name one.
+	Location() (file string, span source.Span)
+}
+
+// ChoicePoint is one point where an executor had several enabled alternatives the
+// Kernel Semantic Library leaves unordered and took one by its own scheduling rule.
+type ChoicePoint struct {
+	Kind ChoiceKind
+	// Step is the action step the choice was made in, 0 for a state machine.
+	Step int
+	// Where names the decision node or the state and event; empty for a token order.
+	Where string
+	// Alternatives are canonical: tokens by ID, branches and transitions by
+	// declaration position, writes by writing token. Taken indexes the one taken.
+	Alternatives []string
+	Taken        int
+	// File and Span locate the declaration the choice was made at; File is ""
+	// when the runtime could not name one.
+	File string
+	Span source.Span
+}
+
+// Describe renders the choice for a diagnostic: the alternatives in canonical
+// order and which one the executor took.
+func (c ChoicePoint) Describe() string {
+	alts := strings.Join(c.Alternatives, ", ")
+	taken := ""
+	if c.Taken >= 0 && c.Taken < len(c.Alternatives) {
+		taken = c.Alternatives[c.Taken]
+	}
+	switch c.Kind {
+	case ChoiceTokenOrder:
+		return fmt.Sprintf("step %d: tokens %s (unordered; took %s first)", c.Step, alts, taken)
+	case ChoiceDecisionBranch:
+		return fmt.Sprintf("step %d: %s branches %s hold (unordered; took %s)", c.Step, c.Where, alts, taken)
+	case ChoiceWriteOrder:
+		return fmt.Sprintf("step %d: writes %s (unordered; %s stood)", c.Step, alts, taken)
+	case ChoiceTransition:
+		return fmt.Sprintf("%s: transitions %s (unordered; took %s)", c.Where, alts, taken)
+	}
+	return fmt.Sprintf("%s: %s (unordered; took %s)", c.Kind, alts, taken)
+}
+
+// String is the trace line the choice is recorded as.
+func (c ChoicePoint) String() string {
+	return "choice " + c.Describe()
+}
+
+// Location is where the choice was made.
+func (c ChoicePoint) Location() (string, source.Span) {
+	return c.File, c.Span
+}
+
+// Diagnostic is the choice as a finding about the run: informational, since a
+// model is not wrong for admitting several orders and the run took one of them.
+func (c ChoicePoint) Diagnostic() passes.Diagnostic {
+	return passes.Diagnostic{
+		Severity: passes.SeverityInfo,
+		Span:     c.Span,
+		Message:  "choice point: " + c.Describe(),
+		Code:     ChoiceDiagnosticCode,
+		Source:   "runtime",
+	}
+}
+
+// UnevaluableGuard is a guard an executor read only to report a choice, once a
+// branch or transition already held, and could not evaluate. A guard with no
+// result is not true, so its succession is not selected; the run is unchanged.
+type UnevaluableGuard struct {
+	// Step is the action step the guard was read in, 0 for a state machine.
+	Step int
+	// Where names the decision node or the state and event, as a ChoicePoint does.
+	Where string
+	// Alternative is the branch or transition by declaration position, as a
+	// ChoicePoint lists it.
+	Alternative string
+	// Reason is the evaluation error.
+	Reason string
+	File   string
+	Span   source.Span
+}
+
+// Describe renders the guard for a diagnostic: where it was read, which
+// alternative it guards and why it has no result.
+func (g UnevaluableGuard) Describe() string {
+	if g.Step > 0 {
+		return fmt.Sprintf("step %d: %s branch %s: %s (not selected)", g.Step, g.Where, g.Alternative, g.Reason)
+	}
+	return fmt.Sprintf("%s: transition %s: %s (not selected)", g.Where, g.Alternative, g.Reason)
+}
+
+// String is the trace line the guard is recorded as.
+func (g UnevaluableGuard) String() string {
+	return "unevaluable guard " + g.Describe()
+}
+
+// Location is where the guard was declared.
+func (g UnevaluableGuard) Location() (string, source.Span) {
+	return g.File, g.Span
+}
+
+// Diagnostic is the guard as a finding about the run: informational, since the
+// library selects no succession whose guard is not true and defines no failure.
+func (g UnevaluableGuard) Diagnostic() passes.Diagnostic {
+	return passes.Diagnostic{
+		Severity: passes.SeverityInfo,
+		Span:     g.Span,
+		Message:  "guard not evaluable: " + g.Describe(),
+		Code:     UnevaluableGuardCode,
+		Source:   "runtime",
+	}
+}
+
+// noteChoice keeps a choice point for the run's diagnostics and, when tracing,
+// writes it to the trace where it was made.
+func (ctx *Context) noteChoice(c ChoicePoint) {
+	ctx.note(c)
+}
+
+// noteUnevaluableGuard keeps a guard the run could not evaluate, as noteChoice does.
+func (ctx *Context) noteUnevaluableGuard(g UnevaluableGuard) {
+	ctx.note(g)
+}
+
+// noteAll records notes in order.
+func (ctx *Context) noteAll(notes []RunNote) {
+	for _, n := range notes {
+		ctx.note(n)
+	}
+}
+
+// note keeps n for the run's diagnostics and, when tracing, writes it to the
+// trace where it was made. A probe's preview is not a run.
+func (ctx *Context) note(n RunNote) {
+	if ctx.probes > 0 {
+		return
+	}
+	ctx.notes = append(ctx.notes, n)
+	if ctx.trace != nil {
+		ctx.trace.RecordNote(n)
+	}
+}
+
+// Notes returns what the latest run noted about itself, in order: its choice
+// points and the guards it could not evaluate.
+func (ctx *Context) Notes() []RunNote {
+	out := make([]RunNote, len(ctx.notes))
+	copy(out, ctx.notes)
+	return out
+}
+
+// NoteCount is how many notes the latest run has made so far, so a caller
+// stepping an executor can tell what one of its steps noted.
+func (ctx *Context) NoteCount() int {
+	return len(ctx.notes)
+}
+
+// Choices returns the choice points made since the latest run began, in order.
+func (ctx *Context) Choices() []ChoicePoint {
+	var out []ChoicePoint
+	for _, n := range ctx.notes {
+		if c, ok := n.(ChoicePoint); ok {
+			out = append(out, c)
+		}
+	}
+	return out
+}
+
+// UnevaluableGuards returns the guards the latest run could not evaluate, in order.
+func (ctx *Context) UnevaluableGuards() []UnevaluableGuard {
+	var out []UnevaluableGuard
+	for _, n := range ctx.notes {
+		if g, ok := n.(UnevaluableGuard); ok {
+			out = append(out, g)
+		}
+	}
+	return out
+}
diff --git a/internal/core/runtime/choice_test.go b/internal/core/runtime/choice_test.go
new file mode 100644
index 000000000..c283811a5
--- /dev/null
+++ b/internal/core/runtime/choice_test.go
@@ -0,0 +1,1059 @@
+package runtime
+
+import (
+	"fmt"
+	"strings"
+	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/core/ast"
+	"github.com/Open-MBEE/OpenSysML/internal/core/passes"
+	"github.com/Open-MBEE/OpenSysML/internal/core/semantics"
+)
+
+// A choice point renders one canonical line per kind, and its diagnostic is
+// informational: the model is not wrong for admitting several orders.
+func TestChoicePointRendering(t *testing.T) {
+	cases := []struct {
+		choice ChoicePoint
+		want   string
+	}{
+		{ChoicePoint{Kind: ChoiceTokenOrder, Step: 2, Alternatives: []string{"2@left", "3@right"}, Taken: 1},
+			"choice step 2: tokens 2@left, 3@right (unordered; took 3@right first)"},
+		{ChoicePoint{Kind: ChoiceDecisionBranch, Step: 3, Where: "decision pick", Alternatives: []string{"1->a", "2->b"}, Taken: 0},
+			"choice step 3: decision pick branches 1->a, 2->b hold (unordered; took 1->a)"},
+		{ChoicePoint{Kind: ChoiceWriteOrder, Step: 4, Alternatives: []string{"x := 1 by token 2", "x := 2 by token 3"}, Taken: 0},
+			"choice step 4: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 1 by token 2 stood)"},
+		{ChoicePoint{Kind: ChoiceTransition, Where: "state idle on accept Go", Alternatives: []string{"1->low", "2->high"}, Taken: 0},
+			"choice state idle on accept Go: transitions 1->low, 2->high (unordered; took 1->low)"},
+	}
+	for _, c := range cases {
+		if got := c.choice.String(); got != c.want {
+			t.Errorf("String() = %q, want %q", got, c.want)
+		}
+		d := c.choice.Diagnostic()
+		if d.Severity != passes.SeverityInfo {
+			t.Errorf("%s: severity = %v, want info", c.want, d.Severity)
+		}
+		if d.Code != ChoiceDiagnosticCode || d.Source != "runtime" {
+			t.Errorf("%s: code/source = %q/%q", c.want, d.Code, d.Source)
+		}
+		if d.Message != "choice point: "+strings.TrimPrefix(c.want, "choice ") {
+			t.Errorf("%s: message = %q", c.want, d.Message)
+		}
+	}
+}
+
+// Each run starts its own list of choice points; the ones of a run ending in an
+// error are still reported, since they explain how the run got there.
+func TestChoicesResetPerRun(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		action route {
+			attribute level : Integer = 75;
+			attribute handler : Integer = 0;
+			first start;
+			then decide select;
+				if level > 50 then warn;
+				if level > 70 then alarm;
+			action warn { assign handler := 1; }
+			then done;
+			action alarm { assign handler := 2; }
+			then done;
+		}
+		action plain {
+			attribute n : Integer = 0;
+			first start;
+			then action one { assign n := 1; }
+			then done;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	route := findSymbolByName(idx.DocumentRoot("<test>"), "route", ast.DefAction)
+	plain := findSymbolByName(idx.DocumentRoot("<test>"), "plain", ast.DefAction)
+	if route == nil || plain == nil {
+		t.Fatal("actions not found")
+	}
+
+	if _, err := ctx.ExecuteAction(route); err != nil {
+		t.Fatalf("route: %v", err)
+	}
+	choices := ctx.Choices()
+	if len(choices) != 1 || choices[0].Kind != ChoiceDecisionBranch {
+		t.Fatalf("route choices = %v, want one decision branch", choices)
+	}
+	if choices[0].File != "<test>" || choices[0].Span.Len == 0 {
+		t.Errorf("decision choice is not located: file %q span %+v", choices[0].File, choices[0].Span)
+	}
+
+	if _, err := ctx.ExecuteAction(plain); err != nil {
+		t.Fatalf("plain: %v", err)
+	}
+	if got := ctx.Choices(); len(got) != 0 {
+		t.Fatalf("plain inherited choices from the earlier run: %v", got)
+	}
+}
+
+// Two transitions out of one state enabled by one event are a choice point
+// naming the state, the event and both transitions; the first still fires.
+func TestTransitionChoiceNamesStateAndEvent(t *testing.T) {
+	src := `package test {
+		state Dispatcher {
+			attribute level : Integer = 8;
+			entry; then idle;
+			state idle;
+			state low;
+			state high;
+			transition first idle accept Go if level > 5 then low;
+			transition first idle accept Go if level > 7 then high;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Dispatcher", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, []string{"Go"})
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if strings.Join(visited, ",") != "idle,low" {
+		t.Fatalf("visited %v, want idle then low: the first enabled transition still fires", visited)
+	}
+	choices := ctx.Choices()
+	if len(choices) != 1 || choices[0].Kind != ChoiceTransition {
+		t.Fatalf("choices = %v, want one transition choice", choices)
+	}
+	want := "choice state idle on accept Go: transitions 1->low, 2->high (unordered; took 1->low)"
+	if got := choices[0].String(); got != want {
+		t.Errorf("choice = %q, want %q", got, want)
+	}
+}
+
+// Reporting a choice never changes the run: a guard after the first holding one
+// that cannot be evaluated is no alternative, not an error the run never had;
+// before any guard holds it still fails the run as it always did.
+func TestLaterGuardErrorIsNotAChoiceNorAFailure(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		action route {
+			attribute level : Integer = 75;
+			attribute handler : Integer = 0;
+			first start;
+			then decide select;
+				if level > 50 then warn;
+				if 1 / (level - 75) > 0 then alarm;
+			action warn { assign handler := 1; }
+			then done;
+			action alarm { assign handler := 2; }
+			then done;
+		}
+		action broken {
+			attribute level : Integer = 75;
+			first start;
+			then decide select;
+				if 1 / (level - 75) > 0 then alarm;
+				if level > 50 then warn;
+			action warn;
+			then done;
+			action alarm;
+			then done;
+		}
+		state Dispatcher {
+			attribute level : Integer = 8;
+			entry; then idle;
+			state idle;
+			state low;
+			state high;
+			transition first idle accept Go if level > 5 then low;
+			transition first idle accept Go if 1 / (level - 8) > 0 then high;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	root := idx.DocumentRoot("<test>")
+	route := findSymbolByName(root, "route", ast.DefAction)
+	broken := findSymbolByName(root, "broken", ast.DefAction)
+	dispatcher := findSymbolByName(root, "Dispatcher", ast.DefState)
+	if route == nil || broken == nil || dispatcher == nil {
+		t.Fatal("behaviors not found")
+	}
+
+	values, err := ctx.ExecuteAction(route)
+	if err != nil {
+		t.Fatalf("route: %v", err)
+	}
+	if got := FormatTraceValue(values["handler"]); got != "1" {
+		t.Fatalf("handler = %s, want the first holding guard's branch", got)
+	}
+	if got := ctx.Choices(); len(got) != 0 {
+		t.Fatalf("an unevaluable guard was reported as a choice: %v", got)
+	}
+	want := "unevaluable guard step 2: decision select branch 2->alarm: division by zero (not selected)"
+	if got := ctx.UnevaluableGuards(); len(got) != 1 || got[0].String() != want {
+		t.Fatalf("unevaluable guards = %v, want [%s]", got, want)
+	}
+	diag := ctx.UnevaluableGuards()[0].Diagnostic()
+	if diag.Severity != passes.SeverityInfo || diag.Code != UnevaluableGuardCode || diag.Source != "runtime" {
+		t.Errorf("diagnostic = %+v, want an informational %s from the runtime", diag, UnevaluableGuardCode)
+	}
+	if !strings.HasPrefix(diag.Message, "guard not evaluable: ") {
+		t.Errorf("message = %q, want it to say the guard is not evaluable", diag.Message)
+	}
+	if file, span := ctx.UnevaluableGuards()[0].Location(); file != "<test>" || span.Len == 0 {
+		t.Errorf("location = %q %v, want the guard's span in the test file", file, span)
+	}
+
+	if _, err := ctx.ExecuteAction(broken); err == nil || !strings.Contains(err.Error(), "division by zero") {
+		t.Fatalf("broken: err = %v, want the first guard's evaluation error", err)
+	}
+	if got := ctx.UnevaluableGuards(); len(got) != 0 {
+		t.Fatalf("the first guard's failure was noted rather than raised: %v", got)
+	}
+
+	_, visited, err := ctx.ExecuteStateWithEvents(dispatcher, []string{"Go"})
+	if err != nil {
+		t.Fatalf("dispatcher: %v", err)
+	}
+	if strings.Join(visited, ",") != "idle,low" {
+		t.Fatalf("visited %v, want idle then low", visited)
+	}
+	if got := ctx.Choices(); len(got) != 0 {
+		t.Fatalf("an unevaluable transition guard was reported as a choice: %v", got)
+	}
+	got := ctx.UnevaluableGuards()
+	if len(got) != 1 || got[0].Where != "state idle on accept Go" || got[0].Alternative != "2->high" ||
+		!strings.Contains(got[0].Reason, "division by zero") || got[0].Step != 0 {
+		t.Fatalf("unevaluable guards = %+v, want the second transition out of idle on Go", got)
+	}
+	if !strings.HasPrefix(got[0].Describe(), "state idle on accept Go: transition 2->high: ") {
+		t.Errorf("description = %q, want the state, event and transition first", got[0].Describe())
+	}
+}
+
+// A guard read only to report a choice is previewed: what evaluating it costs
+// and does is undone, so the run spends and traces exactly what first-match did.
+func TestLaterGuardIsProbedWithoutCost(t *testing.T) {
+	route := func(second string) string {
+		return `package test {
+			private import ScalarValues::*;
+			calc def cost { in n : Integer; return : Integer = if n > 0 ? cost(n - 1) + 1 else 0; }
+			action route {
+				attribute level : Integer = 75;
+				attribute handler : Integer = 0;
+				first start;
+				then decide select;
+					if level > 50 then warn;
+					if ` + second + ` then alarm;
+				action warn { assign handler := 1; }
+				then done;
+				action alarm { assign handler := 2; }
+				then done;
+			}
+		}`
+	}
+	spent := func(t *testing.T, second string) int64 {
+		idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, route(second)))
+		sym := findSymbolByName(idx.DocumentRoot("<test>"), "route", ast.DefAction)
+		if sym == nil {
+			t.Fatal("action not found")
+		}
+		values, err := ctx.ExecuteAction(sym)
+		if err != nil {
+			t.Fatalf("route with guard %s: %v", second, err)
+		}
+		if got := FormatTraceValue(values["handler"]); got != "1" {
+			t.Fatalf("handler = %s with guard %s, want the first holding guard's branch", got, second)
+		}
+		if len(ctx.Choices()) != 1 || len(ctx.UnevaluableGuards()) != 0 {
+			t.Fatalf("notes with guard %s = %v, want the one branch choice", second, ctx.Notes())
+		}
+		return ctx.steps
+	}
+	cheap := spent(t, "level > 70")
+	dear := spent(t, "cost(40) > 0")
+	if cheap != dear {
+		t.Errorf("steps spent = %d with a cheap later guard, %d with a dear one; want the same", cheap, dear)
+	}
+}
+
+// The first transition read is the run's, not a preview: its failure fails the
+// run as it always has.
+func TestFirstTransitionFailureStillFailsTheRun(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		state Dispatcher {
+			attribute level : Integer = 8;
+			entry; then idle;
+			state idle;
+			state low;
+			state high;
+			transition first idle accept Go if 1 / (level - 8) > 0 then high;
+			transition first idle accept Go if level > 5 then low;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Dispatcher", ast.DefState)
+	if sym == nil {
+		t.Fatal("state not found")
+	}
+	_, _, err := ctx.ExecuteStateWithEvents(sym, []string{"Go"})
+	if err == nil || !strings.Contains(err.Error(), "division by zero") {
+		t.Fatalf("err = %v, want the first transition's evaluation error", err)
+	}
+	if got := ctx.UnevaluableGuards(); len(got) != 0 {
+		t.Fatalf("the first transition's failure was noted rather than raised: %v", got)
+	}
+}
+
+// Writes to one object through different features are writes to one destination:
+// a step writing `cell.mark` and `twin.mark` of the same cell is one conflict.
+func TestWriteConflictOnOneObjectThroughTwoChains(t *testing.T) {
+	src := `
+	package test {
+		private import ScalarValues::*;
+		part def Cell {
+			attribute mark : Integer = 0;
+		}
+		part def Rig {
+			part cell : Cell;
+			ref part twin : Cell = cell;
+			perform action marking {
+				first start;
+				fork split;
+				action viaCell { assign cell.mark := 1; }
+				action viaTwin { assign twin.mark := 2; }
+				join sync;
+				done;
+				succession first start then split;
+				succession first split then viaCell;
+				succession first split then viaTwin;
+				succession first viaCell then sync;
+				succession first viaTwin then sync;
+				succession first sync then done;
+			}
+		}
+	}`
+	ctx, _, err := instantiateWithLibraries(t, src, "test::Rig")
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	var writes []string
+	for _, c := range ctx.Choices() {
+		if c.Kind == ChoiceWriteOrder {
+			writes = append(writes, c.String())
+		}
+	}
+	if len(writes) != 1 || !strings.Contains(writes[0], "writes mark of object #") ||
+		!strings.Contains(writes[0], ":= 1 by token 2,") || !strings.Contains(writes[0], ":= 2 by token 3") {
+		t.Fatalf("write choices = %q, want one conflict on the cell's mark", writes)
+	}
+}
+
+// A transition on a substate and one on its enclosing state enabled by the same
+// event are ordered by UML (the substate's fires), so they are no choice point.
+func TestAncestorPriorityIsNotAChoice(t *testing.T) {
+	src := `package test {
+		state Monitor {
+			attribute temp : Integer = 30;
+			entry; then running;
+			state running {
+				entry; then fine;
+				state fine;
+				state warm;
+				transition first fine accept Tick if temp > 20 then warm;
+			}
+			state halted;
+			transition first running accept Tick if temp > 10 then halted;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Monitor", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, []string{"Tick"})
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if strings.Join(visited, ",") != "running,fine,warm" {
+		t.Fatalf("visited %v, want the substate's transition to fire", visited)
+	}
+	if got := ctx.Choices(); len(got) != 0 {
+		t.Fatalf("ancestor priority reported as a choice: %v", got)
+	}
+}
+
+// Leaves in sibling regions select the same transition out of the composite
+// state enclosing them, which fires once: so does the choice among the
+// transitions out of it.
+func TestSharedAncestorChoiceIsReportedOnce(t *testing.T) {
+	src := `package test {
+		state Machine {
+			attribute level : Integer = 8;
+			entry; then work;
+			state work parallel {
+				state a { entry; then a1; state a1; }
+				state b { entry; then b1; state b1; }
+			}
+			state low;
+			state high;
+			transition first work accept Go if level > 5 then low;
+			transition first work accept Go if level > 7 then high;
+			transition first work accept Go if 1 / (level - 8) > 0 then high;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Machine", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, []string{"Go"})
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if strings.Join(visited, ",") != "work,a1,b1,low" {
+		t.Fatalf("visited %v, want both regions entered, then the first transition out of work", visited)
+	}
+	want := "choice state work on accept Go: transitions 1->low, 2->high (unordered; took 1->low)"
+	if got := ctx.Choices(); len(got) != 1 || got[0].String() != want {
+		t.Fatalf("choices = %v, want exactly [%s]", got, want)
+	}
+	if got := ctx.UnevaluableGuards(); len(got) != 1 || got[0].Alternative != "3->high" {
+		t.Fatalf("unevaluable guards = %v, want the third transition out of work, once", got)
+	}
+}
+
+// A transition out of a composite state loses to one a nested state takes on the
+// same event, so the alternatives found out of the composite state were never
+// the run's to choose among: nothing about them is reported.
+func TestAncestorChoiceSuppressedByNestedTransitionIsNotReported(t *testing.T) {
+	src := `package test {
+		state Machine {
+			attribute level : Integer = 8;
+			entry; then work;
+			state work parallel {
+				state a {
+					entry; then a1;
+					state a1;
+					state a2;
+					transition first a1 accept Go then a2;
+				}
+				state b { entry; then b1; state b1; }
+			}
+			state low;
+			state high;
+			transition first work accept Go if level > 5 then low;
+			transition first work accept Go if level > 7 then high;
+			transition first work accept Go if 1 / (level - 8) > 0 then high;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Machine", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, []string{"Go"})
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if strings.Join(visited, ",") != "work,a1,b1,a2" {
+		t.Fatalf("visited %v, want the nested transition to fire and work to stay active", visited)
+	}
+	if got := ctx.Notes(); len(got) != 0 {
+		t.Fatalf("the outranked transitions out of work were reported: %v", got)
+	}
+}
+
+// A step that fails after one token already went still made an ordering choice:
+// the failing token could have gone first, and the diagnostics of a failed run
+// must say what the run did before it failed.
+func TestTokenOrderIsReportedWhenALaterTokenFails(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		action race {
+			attribute x : Integer = 0;
+			attribute n : Integer = 0;
+			first start;
+			fork split;
+			action safe { assign x := 1; }
+			action failing { assign x := 1 / n; }
+			join sync;
+			done;
+			succession first start then split;
+			succession first split then failing;
+			succession first split then safe;
+			succession first safe then sync;
+			succession first failing then sync;
+			succession first sync then done;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "race", ast.DefAction)
+	if sym == nil {
+		t.Fatal("action not found")
+	}
+	_, err := ctx.ExecuteAction(sym)
+	if err == nil || !strings.Contains(err.Error(), "division by zero") {
+		t.Fatalf("err = %v, want the failing token's error", err)
+	}
+	var tokenOrders []ChoicePoint
+	for _, c := range ctx.Choices() {
+		if c.Kind == ChoiceTokenOrder {
+			tokenOrders = append(tokenOrders, c)
+		}
+	}
+	if len(tokenOrders) != 1 {
+		t.Fatalf("token-order choices = %v, want the one step both tokens took part in", tokenOrders)
+	}
+	got := tokenOrders[0]
+	if len(got.Alternatives) != 2 || !strings.HasSuffix(got.Alternatives[0], "@failing") ||
+		!strings.HasSuffix(got.Alternatives[1], "@safe") || got.Taken != 1 {
+		t.Fatalf("choice = %s, want failing and safe as the alternatives, safe taken first", got)
+	}
+}
+
+// One message two parked accepts both answer to goes to whichever is stepped
+// first: the recipient is the executor's choice, and the accept left waiting is
+// the alternative even though it did nothing in the step.
+func TestSharedMessageAcceptIsAChoice(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		action listen {
+			first start;
+			fork split;
+			action left accept a : Integer;
+			action right accept b : Integer;
+			join sync;
+			done;
+			succession first start then split;
+			succession first split then left;
+			succession first split then right;
+			succession first left then sync;
+			succession first right then sync;
+			succession first sync then done;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "listen", ast.DefAction)
+	if sym == nil {
+		t.Fatal("action not found")
+	}
+	exec, err := ctx.CreateActionExecutor(sym)
+	if err != nil {
+		t.Fatalf("create action executor: %v", err)
+	}
+	for i := 0; i < 10 && exec.State() != StateWaiting; i++ {
+		if err := exec.Step(); err != nil {
+			t.Fatalf("step %d: %v", i, err)
+		}
+	}
+	if exec.State() != StateWaiting {
+		t.Fatalf("state = %v, want both accepts parked", exec.State())
+	}
+	if got := ctx.Choices(); len(got) != 0 {
+		t.Fatalf("choices before any message = %v, want none: two parked accepts have nothing to take", got)
+	}
+	at := func(node string) (Token, bool) {
+		for _, tok := range exec.Tokens() {
+			if nodeIdentifier(tok.Location) == node {
+				return tok, true
+			}
+		}
+		return Token{}, false
+	}
+	left, _ := at("left")
+	right, _ := at("right")
+	if left.Wait == nil || right.Wait == nil {
+		t.Fatalf("tokens = %v, want both accepts parked", exec.Tokens())
+	}
+	one := Value{Kind: ValConst, Const: semantics.Value{Kind: semantics.ValInt, Int: 1}}
+	ctx.PostMessage(Message{SignalType: "Integer", Value: &one})
+	if err := exec.Step(); err != nil {
+		t.Fatalf("step with the message in flight: %v", err)
+	}
+	if still, ok := at("left"); !ok || still.Wait == nil {
+		t.Fatalf("tokens = %v, want left to keep waiting", exec.Tokens())
+	}
+	if _, ok := at("right"); ok {
+		t.Fatalf("tokens = %v, want right, stepped first, to take the message and move on", exec.Tokens())
+	}
+	got := ctx.Choices()
+	if len(got) != 1 || got[0].Kind != ChoiceTokenOrder {
+		t.Fatalf("choices = %v, want the one recipient choice", got)
+	}
+	want := fmt.Sprintf("choice step %d: tokens %d@left, %d@right (unordered; took %d@right first)",
+		got[0].Step, left.ID, right.ID, right.ID)
+	if got[0].String() != want {
+		t.Fatalf("choice = %s, want %s", got[0], want)
+	}
+	if pending := ctx.PendingMessages(); len(pending) != 0 {
+		t.Fatalf("pending messages = %+v, want the one message taken", pending)
+	}
+	if err := exec.Step(); err != nil {
+		t.Fatalf("step with nothing in flight: %v", err)
+	}
+	if got := ctx.Choices(); len(got) != 1 {
+		t.Fatalf("choices = %v, want no choice while left waits alone", got)
+	}
+}
+
+// Two tokens writing one feature in one step is a choice point naming both
+// writes and the one that stood, whether or not the values differ: which
+// performance wrote last is the executor's order either way.
+func TestWriteConflictChoice(t *testing.T) {
+	run := func(t *testing.T, leftValue string) []ChoicePoint {
+		src := `package test {
+			private import ScalarValues::*;
+			action race {
+				attribute x : Integer = 0;
+				first start;
+				fork split;
+				action left { assign x := ` + leftValue + `; }
+				action right { assign x := 2; }
+				join sync;
+				done;
+				succession first start then split;
+				succession first split then left;
+				succession first split then right;
+				succession first left then sync;
+				succession first right then sync;
+				succession first sync then done;
+			}
+		}`
+		idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+		sym := findSymbolByName(idx.DocumentRoot("<test>"), "race", ast.DefAction)
+		if sym == nil {
+			t.Fatal("action not found")
+		}
+		if _, err := ctx.ExecuteAction(sym); err != nil {
+			t.Fatalf("execute: %v", err)
+		}
+		var writes []ChoicePoint
+		for _, c := range ctx.Choices() {
+			if c.Kind == ChoiceWriteOrder {
+				writes = append(writes, c)
+			}
+		}
+		return writes
+	}
+
+	conflicting := run(t, "1")
+	if len(conflicting) != 1 {
+		t.Fatalf("write choices = %v, want one", conflicting)
+	}
+	want := "choice step 3: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 1 by token 2 stood)"
+	if got := conflicting[0].String(); got != want {
+		t.Errorf("choice = %q, want %q", got, want)
+	}
+	agreeing := run(t, "2")
+	if len(agreeing) != 1 {
+		t.Fatalf("write choices = %v, want one", agreeing)
+	}
+	want = "choice step 3: writes x := 2 by token 2, x := 2 by token 3 (unordered; x := 2 by token 2 stood)"
+	if got := agreeing[0].String(); got != want {
+		t.Errorf("choice = %q, want %q", got, want)
+	}
+}
+
+// Three tokens writing one feature in one step are one choice point listing
+// every token's write and the one that stood, not two pairwise ones.
+func TestThreeWritersAreOneChoice(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		action race {
+			attribute x : Integer = 0;
+			first start;
+			fork split;
+			action a { assign x := 1; }
+			action b { assign x := 2; }
+			action c { assign x := 3; }
+			join sync;
+			done;
+			succession first start then split;
+			succession first split then a;
+			succession first split then b;
+			succession first split then c;
+			succession first a then sync;
+			succession first b then sync;
+			succession first c then sync;
+			succession first sync then done;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "race", ast.DefAction)
+	if sym == nil {
+		t.Fatal("action not found")
+	}
+	values, err := ctx.ExecuteAction(sym)
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if got := FormatTraceValue(values["x"]); got != "1" {
+		t.Fatalf("x = %s, want the last token stepped (the lowest) to stand", got)
+	}
+	writes := writeChoices(ctx)
+	want := "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)"
+	if len(writes) != 1 || writes[0].String() != want {
+		t.Fatalf("write choices = %v, want exactly [%s]", writes, want)
+	}
+}
+
+// A token writing one feature twice in its step contributes its last write only:
+// had it gone last, that is what would stand.
+func TestRepeatedWritesByOneTokenListItsLast(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		action race {
+			attribute x : Integer = 0;
+			first start;
+			fork split;
+			action left { assign x := 1; assign x := 3; }
+			action right { assign x := 2; }
+			join sync;
+			done;
+			succession first start then split;
+			succession first split then left;
+			succession first split then right;
+			succession first left then sync;
+			succession first right then sync;
+			succession first sync then done;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "race", ast.DefAction)
+	if sym == nil {
+		t.Fatal("action not found")
+	}
+	values, err := ctx.ExecuteAction(sym)
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if got := FormatTraceValue(values["x"]); got != "3" {
+		t.Fatalf("x = %s, want left's last write to stand", got)
+	}
+	writes := writeChoices(ctx)
+	want := "choice step 3: writes x := 3 by token 2, x := 2 by token 3 (unordered; x := 3 by token 2 stood)"
+	if len(writes) != 1 || writes[0].String() != want {
+		t.Fatalf("write choices = %v, want exactly [%s]", writes, want)
+	}
+}
+
+// A feature and the one redefining it are one destination, so writes under either
+// name within one step conflict, direct from the performer or through a chain.
+func TestAliasWritesAreOneDestination(t *testing.T) {
+	flow := func(viaMark, viaLabel string) string {
+		return `
+			first start;
+			fork split;
+			action viaMark { ` + viaMark + ` }
+			action viaLabel { ` + viaLabel + ` }
+			join sync;
+			done;
+			succession first start then split;
+			succession first split then viaMark;
+			succession first split then viaLabel;
+			succession first viaMark then sync;
+			succession first viaLabel then sync;
+			succession first sync then done;`
+	}
+	cases := map[string]struct{ src, fqn string }{
+		"performer": {`package test {
+			private import ScalarValues::*;
+			part def Cell { attribute mark : Integer = 0; }
+			part def Twin :> Cell {
+				attribute :>> mark;
+				attribute label :>> mark;
+				perform action marking {` + flow("assign mark := 1;", "assign label := 2;") + `}
+			}
+		}`, "test::Twin"},
+		"chain": {`package test {
+			private import ScalarValues::*;
+			part def Cell { attribute mark : Integer = 0; }
+			part def Twin :> Cell { attribute label :>> mark; }
+			part def Rig {
+				part cell : Twin;
+				perform action marking {` + flow("assign cell.mark := 1;", "assign cell.label := 2;") + `}
+			}
+		}`, "test::Rig"},
+	}
+	for name, c := range cases {
+		t.Run(name, func(t *testing.T) {
+			ctx, _, err := instantiateWithLibraries(t, c.src, c.fqn)
+			if err != nil {
+				t.Fatalf("instantiate: %v", err)
+			}
+			writes := writeChoices(ctx)
+			if len(writes) != 1 || len(writes[0].Alternatives) != 2 {
+				t.Fatalf("write choices = %v, want one conflict on the cell's mark", writes)
+			}
+			got := writes[0].String()
+			if !strings.Contains(got, " of object #") || !strings.Contains(got, ":= 1 by token 2,") ||
+				!strings.Contains(got, ":= 2 by token 3") || !strings.Contains(got, ":= 1 by token 2 stood") {
+				t.Fatalf("choice = %q, want both names' writes as one destination, the mark's write standing", got)
+			}
+		})
+	}
+}
+
+// writeChoices is the write-order choice points of the last run.
+func writeChoices(ctx *Context) []ChoicePoint {
+	var writes []ChoicePoint
+	for _, c := range ctx.Choices() {
+		if c.Kind == ChoiceWriteOrder {
+			writes = append(writes, c)
+		}
+	}
+	return writes
+}
+
+// An object a probed later guard makes is undone with its identity, so the run's
+// objects are numbered as when no later guard is probed at all.
+func TestProbedGuardLeavesObjectIdentitiesUntouched(t *testing.T) {
+	route := func(second string) string {
+		return `package test {
+			private import ScalarValues::*;
+			item def Cell { attribute v : Integer; }
+			action route {
+				attribute level : Integer = 75;
+				attribute made : Integer = 0;
+				first start;
+				then decide select;
+					if level > 50 then warn;
+					if ` + second + ` then alarm;
+				action warn { assign made := new Cell(2).v; }
+				then done;
+				action alarm { assign made := new Cell(3).v; }
+				then done;
+			}
+		}`
+	}
+	objects := func(t *testing.T, second string) string {
+		idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, route(second)))
+		sym := findSymbolByName(idx.DocumentRoot("<test>"), "route", ast.DefAction)
+		if sym == nil {
+			t.Fatal("action not found")
+		}
+		values, err := ctx.ExecuteAction(sym)
+		if err != nil {
+			t.Fatalf("route with guard %s: %v", second, err)
+		}
+		if got := FormatTraceValue(values["made"]); got != "2" {
+			t.Fatalf("made = %s with guard %s, want the first holding guard's branch", got, second)
+		}
+		if len(ctx.Choices()) != 1 || len(ctx.UnevaluableGuards()) != 0 {
+			t.Fatalf("notes with guard %s = %v, want the one branch choice", second, ctx.Notes())
+		}
+		return fmt.Sprint(ctx.InstanceIDs())
+	}
+	plain := objects(t, "level > 70")
+	probed := objects(t, "new Cell(1).v > 0")
+	if plain != probed {
+		t.Errorf("objects %s after a probed guard made one, %s otherwise; want the same identities", probed, plain)
+	}
+}
+
+// A selected transition whose guard another region's reaction falsified before
+// its turn does not fire, so nothing about selecting it is reported.
+func TestNotesOfATransitionBlockedBeforeFiringAreDropped(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		state Machine {
+			attribute level : Integer = 8;
+			entry; then work;
+			state work parallel {
+				state a {
+					entry; then a1;
+					state a1;
+					state a2;
+					transition first a1 accept Go do assign level := 0 then a2;
+				}
+				state b {
+					entry; then b1;
+					state b1;
+					state b2;
+					state b3;
+					transition first b1 accept Go if level > 5 then b2;
+					transition first b1 accept Go if level > 7 then b3;
+				}
+			}
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Machine", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, []string{"Go"})
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if strings.Join(visited, ",") != "work,a1,b1,a2" {
+		t.Fatalf("visited %v, want region a to fire and region b, its guards blocked by a's effect, to stay", visited)
+	}
+	if got := ctx.Notes(); len(got) != 0 {
+		t.Fatalf("a transition that did not fire was reported: %v", got)
+	}
+}
+
+// A transition that fires and fails in its effect was the run's choice all the
+// same: the choice explains how the run got to the failure.
+func TestNotesOfATransitionFailingInItsEffectAreKept(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		state Dispatcher {
+			attribute level : Integer = 8;
+			entry; then idle;
+			state idle;
+			state low;
+			state high;
+			transition first idle accept Go if level > 5 do assign level := 1 / (level - 8) then low;
+			transition first idle accept Go if level > 7 then high;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Dispatcher", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, _, err := ctx.ExecuteStateWithEvents(sym, []string{"Go"})
+	if err == nil || !strings.Contains(err.Error(), "division by zero") {
+		t.Fatalf("err = %v, want the effect's evaluation error", err)
+	}
+	want := "choice state idle on accept Go: transitions 1->low, 2->high (unordered; took 1->low)"
+	if got := ctx.Choices(); len(got) != 1 || got[0].String() != want {
+		t.Fatalf("choices = %v, want exactly [%s]", got, want)
+	}
+}
+
+// Change-triggered transitions out of one state enabled by one poll are a choice
+// point as event-triggered ones are; the first declared fires.
+func TestChangeTransitionChoice(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		state Monitor {
+			attribute temp : Integer = 0;
+			entry; then start;
+			state start;
+			state watching;
+			state cool;
+			state hot;
+			transition first start do assign temp := 30 then watching;
+			transition first watching accept when temp > 20 then cool;
+			transition first watching accept when temp > 25 then hot;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Monitor", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, nil)
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if strings.Join(visited, ",") != "start,watching,cool" {
+		t.Fatalf("visited %v, want the first declared change transition to fire", visited)
+	}
+	want := "choice state watching on change: transitions 1->cool, 2->hot (unordered; took 1->cool)"
+	if got := ctx.Choices(); len(got) != 1 || got[0].String() != want {
+		t.Fatalf("choices = %v, want exactly [%s]", got, want)
+	}
+}
+
+// A change guard read once an earlier transition is enabled is a probe: one that
+// cannot be evaluated is not enabled and not an error, and stays armed.
+func TestLaterChangeGuardErrorIsNotAChoiceNorAFailure(t *testing.T) {
+	monitor := func(first, second string) string {
+		return `package test {
+			private import ScalarValues::*;
+			state Monitor {
+				attribute temp : Integer = 0;
+				entry; then start;
+				state start;
+				state watching;
+				state cool;
+				state hot;
+				transition first start do assign temp := 30 then watching;
+				transition first watching accept when temp > 20 if ` + first + ` then cool;
+				transition first watching accept when temp > 25 if ` + second + ` then hot;
+			}
+		}`
+	}
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, monitor("temp > 0", "1 / (temp - 30) > 0")))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Monitor", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, nil)
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if strings.Join(visited, ",") != "start,watching,cool" {
+		t.Fatalf("visited %v, want the first enabled change transition to fire", visited)
+	}
+	if got := ctx.Choices(); len(got) != 0 {
+		t.Fatalf("an unevaluable guard was reported as a choice: %v", got)
+	}
+	want := "unevaluable guard state watching on change: transition 2->hot: eval change guard: eval guard of transition watching -> hot: division by zero (not selected)"
+	if got := ctx.UnevaluableGuards(); len(got) != 1 || got[0].String() != want {
+		t.Fatalf("unevaluable guards = %v, want [%s]", got, want)
+	}
+
+	idx, _, ctx = buildRuntime(t, "<test>", parseAndBuild(t, monitor("1 / (temp - 30) > 0", "temp > 0")))
+	sym = findSymbolByName(idx.DocumentRoot("<test>"), "Monitor", ast.DefState)
+	if _, _, err := ctx.ExecuteStateWithEvents(sym, nil); err == nil || !strings.Contains(err.Error(), "division by zero") {
+		t.Fatalf("first guard: err = %v, want its evaluation error to fail the run", err)
+	}
+	if got := ctx.Notes(); len(got) != 0 {
+		t.Fatalf("a first guard's failure was noted: %v", got)
+	}
+}
+
+// A composite state's change transition loses to a nested state's on the same rise
+// and parallel regions fire alongside: only a state with two enabled reports.
+func TestChangeTransitionChoiceUnderHierarchyAndRegions(t *testing.T) {
+	src := `package test {
+		private import ScalarValues::*;
+		state Machine {
+			attribute temp : Integer = 0;
+			entry; then start;
+			state start;
+			state work parallel {
+				state a {
+					entry; then a1;
+					state a1;
+					state a2;
+					state a3;
+					transition first a1 accept when temp > 20 then a2;
+					transition first a1 accept when temp > 25 then a3;
+				}
+				state b {
+					entry; then b1;
+					state b1;
+					state b2;
+					transition first b1 accept when temp > 20 then b2;
+				}
+			}
+			state halted;
+			state stopped;
+			transition first start do assign temp := 30 then work;
+			transition first work accept when temp > 20 then halted;
+			transition first work accept when temp > 25 then stopped;
+		}
+	}`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "Machine", ast.DefState)
+	if sym == nil {
+		t.Fatal("state machine not found")
+	}
+	_, visited, err := ctx.ExecuteStateWithEvents(sym, nil)
+	if err != nil {
+		t.Fatalf("execute: %v", err)
+	}
+	if got := strings.Join(visited, ","); got != "start,work,a1,b1,a2,b2" {
+		t.Fatalf("visited %v, want both regions to take their nested transitions and work to stay active", visited)
+	}
+	want := "choice state a1 on change: transitions 1->a2, 2->a3 (unordered; took 1->a2)"
+	if got := ctx.Choices(); len(got) != 1 || got[0].String() != want {
+		t.Fatalf("choices = %v, want exactly [%s]", got, want)
+	}
+}
diff --git a/internal/core/runtime/classifier_behavior.go b/internal/core/runtime/classifier_behavior.go
index 69f9f7a7d..2c1fe6460 100644
--- a/internal/core/runtime/classifier_behavior.go
+++ b/internal/core/runtime/classifier_behavior.go
@@ -966,6 +966,7 @@ func assignPerformerFeature(ctx *Context, self *Instance, scope *symbols.Scope,
 	if err := self.SetFeatureValue(ctx, name, value); err != nil {
 		return true, fmt.Errorf("write %s of object #%d: %w", name, self.ID, err)
 	}
+	ctx.noteObjectWrite(self, name, value)
 	return true, nil
 }
 
diff --git a/internal/core/runtime/context.go b/internal/core/runtime/context.go
index 6051e6f63..be7cd4f94 100644
--- a/internal/core/runtime/context.go
+++ b/internal/core/runtime/context.go
@@ -167,6 +167,10 @@ type Context struct {
 
 	// trace records evaluation, nil when not tracing.
 	trace *TraceRecorder
+	// notes are what the latest run noted about itself, in order; see note.
+	notes []RunNote
+	// stepWrites is the ledger of the action step under way, nil between steps.
+	stepWrites *stepWriteLedger
 
 	// actionDepth is the number of action invocations currently on the stack,
 	// bounding recursion across nested action executors.
@@ -483,6 +487,35 @@ func (s *idSequence) atLeast(id int64) {
 	}
 }
 
+// release hands out id next again, once every identity taken from it on is
+// abandoned: what a probe made and undid never happened.
+func (s *idSequence) release(id int64) {
+	if id < s.next {
+		s.next = id
+	}
+}
+
+// holdsIdentityFrom reports whether an object, or a connector one set aside,
+// holds an identity at or past id.
+func (ctx *Context) holdsIdentityFrom(id int64) bool {
+	for held, inst := range ctx.instances {
+		if held >= id {
+			return true
+		}
+		for _, kept := range inst.keptConnectors {
+			if kept >= id {
+				return true
+			}
+		}
+		for _, kept := range inst.keptAnonymous {
+			if kept.id >= id {
+				return true
+			}
+		}
+	}
+	return false
+}
+
 // allocateID returns the next instance ID and increments the counter.
 func (ctx *Context) allocateID() int64 {
 	return ctx.ids.take()
@@ -496,6 +529,7 @@ func (ctx *Context) beginRun() func() {
 	if ctx.runDepth == 0 {
 		ctx.steps = 0
 		ctx.elements = 0
+		ctx.notes = nil
 		ctx.calcUsageRuns = make(map[int64]map[calcUsageKey]*calcRun)
 	}
 	ctx.runDepth++
@@ -511,6 +545,7 @@ func (ctx *Context) beginExecutorRun(started *bool) func() {
 	if ctx.runDepth == 0 && !*started {
 		ctx.steps = 0
 		ctx.elements = 0
+		ctx.notes = nil
 		ctx.calcUsageRuns = make(map[int64]map[calcUsageKey]*calcRun)
 	}
 	*started = true
@@ -519,26 +554,30 @@ func (ctx *Context) beginExecutorRun(started *bool) func() {
 }
 
 // beginProbe brackets an evaluation previewing what a run would do, restoring the
-// budget, trace, bus, variant selections, objects made, behaviors attached, every
-// feature value written (see noteProbeWrite) and every other change noted (see
-// noteProbeUndo) after.
-// Behaviors the probe starts are the only ones it runs (see nextRunnableBehavior).
+// budget, trace, bus, variant selections, objects made (identities included),
+// behaviors attached, every feature value written (see noteProbeWrite) and every
+// other change noted (see noteProbeUndo) after. The writes it makes are not the
+// step's (see noteWrite); behaviors it starts are the only ones it runs (see nextRunnableBehavior).
 func (ctx *Context) beginProbe() func() {
-	steps, elements, trace := ctx.steps, ctx.elements, ctx.trace
+	steps, elements, trace, writes := ctx.steps, ctx.elements, ctx.trace, ctx.stepWrites
+	ids, nextID := ctx.ids, ctx.ids.next
 	endBoundary := func() { /* no boundary to close */ }
 	if ctx.probes == 0 {
 		endBoundary = ctx.beginRunBoundary()
 	}
 	_, rollback := ctx.beginJournal()
-	ctx.trace = nil
+	ctx.trace, ctx.stepWrites = nil, nil
 	ctx.runDepth++
 	ctx.probes++
 	return func() {
 		rollback()
 		endBoundary()
+		if ctx.ids == ids && !ctx.holdsIdentityFrom(nextID) {
+			ids.release(nextID)
+		}
 		ctx.probes--
 		ctx.runDepth--
-		ctx.steps, ctx.elements, ctx.trace = steps, elements, trace
+		ctx.steps, ctx.elements, ctx.trace, ctx.stepWrites = steps, elements, trace, writes
 	}
 }
 
diff --git a/internal/core/runtime/robustness_test.go b/internal/core/runtime/robustness_test.go
index fd340bf09..5d0aeb1c0 100644
--- a/internal/core/runtime/robustness_test.go
+++ b/internal/core/runtime/robustness_test.go
@@ -80,6 +80,7 @@ func TestRuntimeRobustness(t *testing.T) {
 	t.Run("first_naming_a_final_node", testFirstNamingAFinalNode)
 	t.Run("fork_branches_assigning_the_same_feature", testForkBranchesAssigningTheSameFeature)
 	t.Run("decision_no_satisfied_guard", testDecisionNoSatisfiedGuard)
+	t.Run("decision_all_guards_false", testDecisionAllGuardsFalse)
 	t.Run("state_dangling_transition", testStateDanglingTransition)
 	t.Run("state_transition_endpoint_misspelled", testStateTransitionEndpointMisspelled)
 	t.Run("state_transition_endpoint_in_another_machine", testStateTransitionEndpointInAnotherMachine)
@@ -5376,6 +5377,54 @@ func testDecisionNoSatisfiedGuard(t *testing.T) {
 	}
 }
 
+// testDecisionAllGuardsFalse: every guard of a decision is evaluated so that
+// several holding at once can be reported; none holding is still the same
+// error, recorded as no choice at all.
+func testDecisionAllGuardsFalse(t *testing.T) {
+	src := `
+		package test {
+			private import ScalarValues::*;
+
+			action pick {
+				attribute level : Integer = 5;
+
+				first start;
+				action low;
+				action high;
+				done;
+
+				succession first start then choose;
+				succession first low then done;
+				succession first high then done;
+
+				decide choose;
+				if level > 10 then low;
+				if level > 20 then high;
+			}
+		}
+	`
+	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	sym := findSymbolByName(idx.DocumentRoot("<test>"), "pick", ast.DefAction)
+	if sym == nil {
+		t.Fatal("action pick not found")
+	}
+
+	exec, err := ctx.CreateActionExecutor(sym)
+	if err != nil {
+		t.Fatalf("create action executor: %v", err)
+	}
+	err = exec.RunToCompletion()
+	if !errors.Is(err, ErrNoEnabledSuccession) {
+		t.Fatalf("error = %v, want ErrNoEnabledSuccession", err)
+	}
+	if !strings.Contains(err.Error(), "decision node choose has no true guard") {
+		t.Fatalf("error = %v, want the decision named", err)
+	}
+	if choices := ctx.Choices(); len(choices) != 0 {
+		t.Fatalf("choices = %v, want none when no guard holds", choices)
+	}
+}
+
 // testStateDanglingTransition: state with transition to nonexistent state
 func testStateDanglingTransition(t *testing.T) {
 	src := `
diff --git a/internal/core/runtime/state_change_trigger.go b/internal/core/runtime/state_change_trigger.go
index 04f9b34af..472e3188c 100644
--- a/internal/core/runtime/state_change_trigger.go
+++ b/internal/core/runtime/state_change_trigger.go
@@ -26,11 +26,12 @@ func (w changeWait) String() string {
 // watches: a transition's condition and guard are evaluated once per poll,
 // however many active leaves the state watching it encloses.
 type changePoll struct {
-	condition map[*lower.Transition]bool
-	guard     map[*lower.Transition]bool
-	blocked   map[*lower.Transition]bool
-	waits     []changeWait
-	waited    map[*lower.Transition]bool
+	condition   map[*lower.Transition]bool
+	guard       map[*lower.Transition]bool
+	blocked     map[*lower.Transition]bool
+	unevaluable map[*lower.Transition]UnevaluableGuard
+	waits       []changeWait
+	waited      map[*lower.Transition]bool
 }
 
 // pollChangeEvents re-tests the ChangeEvent conditions the active configuration
@@ -42,10 +43,11 @@ type changePoll struct {
 // same edge again, and only a condition observed false re-arms it.
 func (e *StateExecutor) pollChangeEvents() (bool, error) {
 	poll := &changePoll{
-		condition: make(map[*lower.Transition]bool),
-		guard:     make(map[*lower.Transition]bool),
-		blocked:   make(map[*lower.Transition]bool),
-		waited:    make(map[*lower.Transition]bool),
+		condition:   make(map[*lower.Transition]bool),
+		guard:       make(map[*lower.Transition]bool),
+		blocked:     make(map[*lower.Transition]bool),
+		unevaluable: make(map[*lower.Transition]UnevaluableGuard),
+		waited:      make(map[*lower.Transition]bool),
 	}
 	e.changeRearmed = make(map[*lower.Transition]bool)
 	defer func() { e.changeRearmed = nil }()
@@ -58,8 +60,9 @@ func (e *StateExecutor) pollChangeEvents() (bool, error) {
 		return false, nil
 	}
 
-	candidates, err := e.selectCandidates(func(state *ast.StateNode) (*lower.Transition, error) {
-		return e.risenChangeTransition(state, poll)
+	candidates, err := e.selectCandidates(func(state *ast.StateNode) (*lower.Transition, []RunNote, error) {
+		trans, notes := e.risenChangeTransition(state, poll)
+		return trans, notes, nil
 	})
 	if err != nil {
 		e.changeWaits = poll.waits
@@ -89,7 +92,7 @@ func (e *StateExecutor) pollChangeEvents() (bool, error) {
 		e.changeFired[candidate.trans] = true
 		e.firingChange = candidate.trans
 		fired = true
-		_, err = e.fireFrom(candidate.source, candidate.trans)
+		_, err = e.fireFrom(candidate.source, candidate.trans, candidate.notes)
 		e.firingChange = nil
 		if err != nil {
 			return fired, fmt.Errorf("fire transition out of %s: %w", candidate.source.Name, err)
@@ -128,7 +131,9 @@ func (e *StateExecutor) consumeRise(poll *changePoll) {
 func (e *StateExecutor) observeChangeConditions(poll *changePoll) error {
 	for _, leaf := range e.activeLeaves() {
 		for _, source := range e.getParentChain(leaf) {
-			for _, trans := range e.graph.Transitions[source] {
+			transitions := e.graph.Transitions[source]
+			decided := false
+			for i, trans := range transitions {
 				changeEvent, ok := trans.Trigger.(*ast.ChangeEvent)
 				if !ok {
 					continue
@@ -152,12 +157,14 @@ func (e *StateExecutor) observeChangeConditions(poll *changePoll) error {
 				}
 				// The guard is read once per poll, alongside the condition, so which
 				// transitions this rise enables does not depend on selection order.
-				satisfied, err := e.passesGuard(trans)
-				if err != nil {
+				if decided {
+					poll.guard[trans] = e.probeChangeGuard(poll, source, transitions, i)
+				} else if poll.guard[trans], err = e.passesGuard(trans); err != nil {
 					return fmt.Errorf("state %s: eval change guard: %w", source.Name, err)
 				}
-				poll.guard[trans] = satisfied
-				if !satisfied {
+				if poll.guard[trans] {
+					decided = true
+				} else if _, unevaluable := poll.unevaluable[trans]; !unevaluable {
 					poll.blocked[trans] = true
 					poll.wait(trans, source.Name, "guard is false")
 				}
@@ -167,6 +174,21 @@ func (e *StateExecutor) observeChangeConditions(poll *changePoll) error {
 	return nil
 }
 
+// probeChangeGuard reads the guard of the transition at position i out of state
+// once an earlier one is enabled, as a probe the context undoes whole. One that
+// cannot be evaluated is not enabled, consumes nothing and is noted on the poll.
+func (e *StateExecutor) probeChangeGuard(poll *changePoll, state *ast.StateNode, transitions []*lower.Transition, i int) bool {
+	var pass bool
+	var err error
+	e.preview(func() { pass, err = e.passesGuard(transitions[i]) })
+	if err != nil {
+		poll.unevaluable[transitions[i]] = e.unevaluableTransition(state, transitions, i, fmt.Errorf("eval change guard: %w", err))
+		poll.wait(transitions[i], state.Name, "guard is not evaluable")
+		return false
+	}
+	return pass
+}
+
 // changeConditionHolds evaluates one change condition in the scope the
 // transition was written in, the machine's data shadowing it.
 func (e *StateExecutor) changeConditionHolds(changeEvent *ast.ChangeEvent, trans *lower.Transition) (bool, error) {
@@ -181,21 +203,30 @@ func (e *StateExecutor) changeConditionHolds(changeEvent *ast.ChangeEvent, trans
 }
 
 // risenChangeTransition returns the state's first change-triggered transition
-// whose condition has risen and whose guard does not block it. A blocked one
-// consumes nothing and stays armed, so its guard is re-tested next poll.
-func (e *StateExecutor) risenChangeTransition(state *ast.StateNode, poll *changePoll) (*lower.Transition, error) {
-	for _, trans := range e.graph.Transitions[state] {
+// whose condition has risen and whose guard does not block it, several enabled at
+// once being a choice point. A blocked one stays armed for the next poll.
+func (e *StateExecutor) risenChangeTransition(state *ast.StateNode, poll *changePoll) (*lower.Transition, []RunNote) {
+	var enabled []int
+	var notes []RunNote
+	transitions := e.graph.Transitions[state]
+	for i, trans := range transitions {
 		if _, ok := trans.Trigger.(*ast.ChangeEvent); !ok {
 			continue
 		}
-		if !poll.condition[trans] || e.changeFired[trans] {
-			continue
+		if poll.condition[trans] && !e.changeFired[trans] && poll.guard[trans] {
+			enabled = append(enabled, i)
 		}
-		if poll.guard[trans] {
-			return trans, nil
+		if unevaluable, ok := poll.unevaluable[trans]; ok {
+			notes = append(notes, unevaluable)
 		}
 	}
-	return nil, nil
+	if len(enabled) == 0 {
+		return nil, nil
+	}
+	if choice, ok := e.transitionChoice(state, transitions, enabled); ok {
+		notes = append([]RunNote{choice}, notes...)
+	}
+	return transitions[enabled[0]], notes
 }
 
 // wait records, once per transition, a change condition the configuration is
diff --git a/internal/core/runtime/state_executor.go b/internal/core/runtime/state_executor.go
index 8cbdc1834..0067d9e26 100644
--- a/internal/core/runtime/state_executor.go
+++ b/internal/core/runtime/state_executor.go
@@ -12,6 +12,7 @@ import (
 	"github.com/Open-MBEE/OpenSysML/internal/core/lower"
 	"github.com/Open-MBEE/OpenSysML/internal/core/resolve"
 	"github.com/Open-MBEE/OpenSysML/internal/core/semantics"
+	"github.com/Open-MBEE/OpenSysML/internal/core/source"
 	"github.com/Open-MBEE/OpenSysML/internal/core/symbols"
 )
 
@@ -112,6 +113,10 @@ type StateExecutor struct {
 	// state entries it causes must leave alone.
 	firingChange *lower.Transition
 
+	// firingNotes is what selecting the transition being taken noted, recorded
+	// once its guard's final reading lets it fire (see transitionDecided).
+	firingNotes []RunNote
+
 	// changeRearmed collects, while a poll runs, the watches a state entry armed
 	// for a new activation, so the poll's earlier observation does not latch them.
 	changeRearmed map[*lower.Transition]bool
@@ -579,7 +584,7 @@ func (e *StateExecutor) dispatchEvent(event Event) (Dispatch, error) {
 			// region's active state, so the region is resolved by containment.
 			var err error
 			if sourceState != nil {
-				dispatch.Fired, err = e.fireFrom(sourceState, lowerTrans)
+				dispatch.Fired, err = e.fireFrom(sourceState, lowerTrans, nil)
 			} else {
 				dispatch.Fired, err = e.fireTransition(lowerTrans)
 			}
@@ -700,7 +705,7 @@ func (e *StateExecutor) broadcastEvent(event *Event) (bool, error) {
 			unbind()
 			return consumed, fmt.Errorf("state %s: %w", candidate.source.Name, err)
 		}
-		fired, err := e.fireFrom(candidate.source, candidate.trans)
+		fired, err := e.fireFrom(candidate.source, candidate.trans, candidate.notes)
 		if err != nil {
 			return consumed, fmt.Errorf("fire transition out of %s: %w", candidate.source.Name, err)
 		}
@@ -713,11 +718,13 @@ func (e *StateExecutor) broadcastEvent(event *Event) (bool, error) {
 }
 
 // dispatchCandidate is the transition one active leaf selected for an event,
-// taken out of the leaf itself or out of a composite state enclosing it.
+// taken out of the leaf itself or out of a composite state enclosing it. What
+// selecting it found worth noting is recorded only if it fires.
 type dispatchCandidate struct {
 	leaf   *ast.StateNode
 	source *ast.StateNode
 	trans  *lower.Transition
+	notes  []RunNote
 }
 
 // selectTransitions picks one transition per leaf active when the event is
@@ -727,21 +734,22 @@ type dispatchCandidate struct {
 // walk carries on past it. Leaves in sibling regions of one composite state
 // select the same transition out of it, which the event still takes only once.
 func (e *StateExecutor) selectTransitions(event *Event) ([]dispatchCandidate, error) {
-	return e.selectCandidates(func(source *ast.StateNode) (*lower.Transition, error) {
+	return e.selectCandidates(func(source *ast.StateNode) (*lower.Transition, []RunNote, error) {
 		return e.enabledTransition(source, event)
 	})
 }
 
 // selectCandidates walks outward from every active leaf, asking enabled for the
-// transition that state offers, and collects one candidate per leaf.
+// transition that state offers and what selecting it noted, and collects one
+// candidate per leaf.
 func (e *StateExecutor) selectCandidates(
-	enabled func(*ast.StateNode) (*lower.Transition, error),
+	enabled func(*ast.StateNode) (*lower.Transition, []RunNote, error),
 ) ([]dispatchCandidate, error) {
 	var candidates []dispatchCandidate
 	selected := make(map[*lower.Transition]bool)
 	for _, leaf := range e.activeLeaves() {
 		for _, source := range e.getParentChain(leaf) {
-			trans, err := enabled(source)
+			trans, notes, err := enabled(source)
 			if err != nil {
 				return nil, fmt.Errorf("state %s: %w", source.Name, err)
 			}
@@ -750,7 +758,7 @@ func (e *StateExecutor) selectCandidates(
 			}
 			if !selected[trans] {
 				selected[trans] = true
-				candidates = append(candidates, dispatchCandidate{leaf: leaf, source: source, trans: trans})
+				candidates = append(candidates, dispatchCandidate{leaf: leaf, source: source, trans: trans, notes: notes})
 			}
 			break
 		}
@@ -881,14 +889,24 @@ func lessPath(a, b []int) bool {
 // fireFrom takes a transition whose source is the given active state, which is
 // either the active leaf or a composite state enclosing it. A source lying in an
 // active orthogonal region moves that region; one outside every active region
-// moves the machine's single active hierarchy.
-func (e *StateExecutor) fireFrom(source *ast.StateNode, trans *lower.Transition) (bool, error) {
+// moves the machine's single active hierarchy. notes are recorded only if it fires.
+func (e *StateExecutor) fireFrom(source *ast.StateNode, trans *lower.Transition, notes []RunNote) (bool, error) {
+	saved := e.firingNotes
+	e.firingNotes = notes
+	defer func() { e.firingNotes = saved }()
 	if region := e.activeRegionOf(source); region != nil {
 		return e.fireTransitionInRegion(region, trans)
 	}
 	return e.fireTransition(trans)
 }
 
+// transitionDecided records what selecting the transition now firing noted, its
+// guard having passed its final reading.
+func (e *StateExecutor) transitionDecided() {
+	e.ctx.noteAll(e.firingNotes)
+	e.firingNotes = nil
+}
+
 // activeRegionOf returns the innermost active orthogonal region the state is
 // declared in, or nil when it lies outside every active region.
 func (e *StateExecutor) activeRegionOf(state *ast.StateNode) *ast.StateRegion {
@@ -920,42 +938,144 @@ func (e *StateExecutor) enclosesActiveRegion(state *ast.StateNode) bool {
 // transition whose guard is false does not consume the event, so a later one
 // still gets its chance. Selecting a transition leaves the machine's data as it
 // was: the caller binds the trigger's arguments again before firing.
-func (e *StateExecutor) enabledTransition(state *ast.StateNode, event *Event) (*lower.Transition, error) {
-	for _, trans := range e.graph.Transitions[state] {
-		matches, err := e.matchesEvent(trans, event)
-		if err != nil {
-			return nil, err
-		}
-		if !matches {
-			continue
+// Every transition is examined so that several enabled at once are a choice
+// point; the notes are the caller's to record if the transition fires, since a
+// state selected through several leaves, or outranked by a nested one, is not a
+// choice the run made.
+func (e *StateExecutor) enabledTransition(state *ast.StateNode, event *Event) (*lower.Transition, []RunNote, error) {
+	var enabled []int
+	var notes []RunNote
+	transitions := e.graph.Transitions[state]
+	// Once one is enabled the transition is decided; the rest are probed only to
+	// report the choice, which leaves the run as it was.
+	for i, trans := range transitions {
+		var ok bool
+		if len(enabled) > 0 {
+			var unevaluable *UnevaluableGuard
+			if ok, unevaluable = e.probeTransition(state, transitions, i, event); unevaluable != nil {
+				notes = append(notes, *unevaluable)
+			}
+		} else {
+			var err error
+			if ok, err = e.transitionEnabled(trans, event); err != nil {
+				return nil, nil, err
+			}
 		}
-		// A call trigger's arguments are bound before the guard runs: the guard is
-		// written against the parameters the trigger declares. A transition that
-		// does not fire must leave no trace of them in the machine's data.
-		unbind, err := e.bindTriggerArguments(trans, event)
-		if err != nil {
-			unbind()
-			return nil, err
+		if ok {
+			enabled = append(enabled, i)
 		}
-		pass, err := e.passesGuard(trans)
+	}
+	if len(enabled) == 0 {
+		return nil, nil, nil
+	}
+	if choice, ok := e.transitionChoice(state, transitions, enabled); ok {
+		notes = append([]RunNote{choice}, notes...)
+	}
+	return transitions[enabled[0]], notes, nil
+}
+
+// probeTransition reads whether the transition at position i out of state reacts
+// to event once another already does, as a probe the context undoes whole. One
+// that cannot be evaluated is not selected and is returned as the note to record.
+func (e *StateExecutor) probeTransition(state *ast.StateNode, transitions []*lower.Transition, i int, event *Event) (bool, *UnevaluableGuard) {
+	var ok bool
+	var err error
+	e.preview(func() { ok, err = e.transitionEnabled(transitions[i], event) })
+	if err != nil {
+		note := e.unevaluableTransition(state, transitions, i, err)
+		return false, &note
+	}
+	return ok, nil
+}
+
+// transitionEnabled reports whether trans reacts to event: its trigger matches,
+// its guard holds and the join it may lead into is ready to fire.
+func (e *StateExecutor) transitionEnabled(trans *lower.Transition, event *Event) (bool, error) {
+	matches, err := e.matchesEvent(trans, event)
+	if err != nil || !matches {
+		return false, err
+	}
+	// A call trigger's arguments are bound before the guard runs: the guard is
+	// written against the parameters the trigger declares. A transition that
+	// does not fire must leave no trace of them in the machine's data.
+	unbind, err := e.bindTriggerArguments(trans, event)
+	if err != nil {
 		unbind()
-		if err != nil {
-			return nil, err
-		}
-		if !pass {
-			continue
-		}
-		// A transition into a join whose other branches have not arrived is not
-		// enabled either: firing it would move nothing.
-		synchronized, err := e.joinSynchronized(trans)
-		if err != nil {
-			return nil, err
-		}
-		if synchronized {
-			return trans, nil
-		}
+		return false, err
+	}
+	pass, err := e.passesGuard(trans)
+	unbind()
+	if err != nil || !pass {
+		return false, err
+	}
+	// A transition into a join whose other branches have not arrived is not
+	// enabled either: firing it would move nothing.
+	return e.joinSynchronized(trans)
+}
+
+// transitionChoice is the transitions out of state enabled for one event, at
+// their declared positions, as a choice point; there is none under two.
+func (e *StateExecutor) transitionChoice(state *ast.StateNode, transitions []*lower.Transition, enabled []int) (ChoicePoint, bool) {
+	if len(enabled) < 2 {
+		return ChoicePoint{}, false
+	}
+	alts := make([]string, len(enabled))
+	for i, pos := range enabled {
+		alts[i] = transitionName(transitions, pos)
+	}
+	taken := transitions[enabled[0]]
+	file, span := e.transitionLocation(state, taken)
+	return ChoicePoint{
+		Kind:         ChoiceTransition,
+		Where:        transitionWhere(state, taken),
+		Alternatives: alts,
+		Taken:        0,
+		File:         file,
+		Span:         span,
+	}, true
+}
+
+// unevaluableTransition is the transition at position pos out of state, probed
+// once another was enabled, as the note that it cannot be evaluated.
+func (e *StateExecutor) unevaluableTransition(state *ast.StateNode, transitions []*lower.Transition, pos int, err error) UnevaluableGuard {
+	trans := transitions[pos]
+	file, span := e.transitionLocation(state, trans)
+	if trans.Guard != nil {
+		span = trans.Guard.Span()
+	}
+	return UnevaluableGuard{
+		Where:       transitionWhere(state, trans),
+		Alternative: transitionName(transitions, pos),
+		Reason:      err.Error(),
+		File:        file,
+		Span:        span,
+	}
+}
+
+// transitionName names a transition out of a state by declared position and target.
+func transitionName(transitions []*lower.Transition, pos int) string {
+	return fmt.Sprintf("%d->%s", pos+1, getNodeName(transitions[pos].Target))
+}
+
+// transitionWhere names the state and the event trans reacts to, for a note.
+func transitionWhere(state *ast.StateNode, trans *lower.Transition) string {
+	where := "state " + state.Name
+	if name := triggerName(trans.Trigger); name != "" {
+		where += " on " + name
+	}
+	return where
+}
+
+// transitionLocation is where trans was declared, or state when it has no declaration.
+func (e *StateExecutor) transitionLocation(state *ast.StateNode, trans *lower.Transition) (string, source.Span) {
+	file := e.stateMachine.DocName
+	if trans.Scope != nil && trans.Scope.DocName() != "" {
+		file = trans.Scope.DocName()
+	}
+	if trans.Decl != nil {
+		return file, trans.Decl.Span()
 	}
-	return nil, nil
+	return file, state.Span()
 }
 
 // bindTriggerArguments binds the parameters a call trigger declares to the
@@ -1146,6 +1266,7 @@ func (e *StateExecutor) fireTransition(trans *lower.Transition) (bool, error) {
 		if err != nil || !pass {
 			return false, err
 		}
+		e.transitionDecided()
 		switch ps.Kind {
 		case ast.PseudostateFork:
 			return true, e.fireForkTransition(trans, ps)
@@ -1186,6 +1307,7 @@ func (e *StateExecutor) fireTransition(trans *lower.Transition) (bool, error) {
 	if err != nil || !pass {
 		return false, err
 	}
+	e.transitionDecided()
 
 	return true, e.transitionTo(trans, targetState)
 }
diff --git a/internal/core/runtime/state_region_transition.go b/internal/core/runtime/state_region_transition.go
index e9d76529a..684565a71 100644
--- a/internal/core/runtime/state_region_transition.go
+++ b/internal/core/runtime/state_region_transition.go
@@ -196,6 +196,7 @@ func (e *StateExecutor) fireTransitionInRegion(region *ast.StateRegion, trans *l
 	if err != nil || !pass {
 		return false, err
 	}
+	e.transitionDecided()
 
 	target, err := e.transitionTarget(trans)
 	if err != nil {
diff --git a/internal/core/runtime/testdata/conformance/action_accept_suspends_until_message.trace.golden b/internal/core/runtime/testdata/conformance/action_accept_suspends_until_message.trace.golden
index fe3f7624b..abb22b327 100644
--- a/internal/core/runtime/testdata/conformance/action_accept_suspends_until_message.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_accept_suspends_until_message.trace.golden
@@ -3,6 +3,7 @@ step 2: token 2@reader, token 3@gate
 step 3: token 2@reader, token 3@sender
 stmt send
   eval literal 7 -> 7
+choice step 4: tokens 2@reader, 3@sender (unordered; took 3@sender first)
 step 4: token 2@sync, token 3@sync
 step 5: token 4@recorder
 stmt assign received
diff --git a/internal/core/runtime/testdata/conformance/action_accept_two_waiters.trace.golden b/internal/core/runtime/testdata/conformance/action_accept_two_waiters.trace.golden
index c83042d5c..1e37f35ec 100644
--- a/internal/core/runtime/testdata/conformance/action_accept_two_waiters.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_accept_two_waiters.trace.golden
@@ -5,6 +5,7 @@ stmt send
   eval literal "go" -> "go"
 stmt send
   eval literal 5 -> 5
+choice step 4: tokens 2@listenNumber, 3@listenText, 4@sender (unordered; took 4@sender first)
 step 4: token 2@sync, token 3@sync, token 4@sync
 step 5: token 5@recorder
 stmt assign number
diff --git a/internal/core/runtime/testdata/conformance/action_block_flow_if_branch_own_flow.trace.golden b/internal/core/runtime/testdata/conformance/action_block_flow_if_branch_own_flow.trace.golden
index 1cf7b07fb..b8993f3b0 100644
--- a/internal/core/runtime/testdata/conformance/action_block_flow_if_branch_own_flow.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_block_flow_if_branch_own_flow.trace.golden
@@ -9,6 +9,7 @@ enter action node: split
       eval literal 20 -> 20
     stmt assign a
       eval literal 10 -> 10
+choice step 2: tokens 3@left, 4@right (unordered; took 4@right first)
     stmt assign sum
         eval chain a -> 10
         eval chain b -> 20
diff --git a/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.expected.json b/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.expected.json
new file mode 100644
index 000000000..e502e4fac
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.expected.json
@@ -0,0 +1,10 @@
+{
+	"type": "action",
+	"evaluate": "test::calibrate",
+	"trace": true,
+	"outcomes": [
+		{"outputs": {"seen": {"type": "Real", "value": 1.5}}},
+		{"outputs": {"seen": {"type": "Real", "value": 2.5}}}
+	],
+	"admissible": "Concurrent branches writing one feature: the value is open, the writes are not"
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.sysml b/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.sysml
new file mode 100644
index 000000000..0625ca0ad
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.sysml
@@ -0,0 +1,33 @@
+package test {
+	private import ScalarValues::*;
+
+	part def Sensor {
+		attribute reading : Real = 0.0;
+	}
+
+	part s : Sensor;
+
+	// Oracle (docs/project/behavior-semantic-oracle.md): both branches write the
+	// sensor's `reading` through the chain `s.reading` in the same step; the
+	// library leaves which write stands open, so the executor reports the
+	// conflict on the object written and the value that stood.
+	action calibrate {
+		attribute seen : Real = 0.0;
+
+		first start;
+		fork split;
+		action coarse { assign s.reading := 1.5; }
+		action fine { assign s.reading := 2.5; }
+		join settle;
+		action read { assign seen := s.reading; }
+		done;
+
+		succession first start then split;
+		succession first split then coarse;
+		succession first split then fine;
+		succession first coarse then settle;
+		succession first fine then settle;
+		succession first settle then read;
+		succession first read then done;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.trace.golden b/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.trace.golden
new file mode 100644
index 000000000..cc68ebbe4
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_chained_write_conflict.trace.golden
@@ -0,0 +1,15 @@
+step 1: token 1@split
+step 2: token 2@coarse, token 3@fine
+stmt assign s.reading
+  eval literal 2.5 -> 2.5
+materialize: s #1
+stmt assign s.reading
+  eval literal 1.5 -> 1.5
+choice step 3: writes reading of object #1 := 1.5 by token 2, reading of object #1 := 2.5 by token 3 (unordered; reading of object #1 := 1.5 by token 2 stood)
+choice step 3: tokens 2@coarse, 3@fine (unordered; took 3@fine first)
+step 3: token 2@settle, token 3@settle
+step 4: token 4@read
+stmt assign seen
+  eval chain reading -> 1.5
+step 5: token 4@done
+step 6: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.expected.json b/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.expected.json
new file mode 100644
index 000000000..bf2b65909
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.expected.json
@@ -0,0 +1,19 @@
+{
+	"type": "action",
+	"trace": true,
+	"outcomes": [
+		{
+			"outputs": {
+				"level": {"type": "Integer", "value": 75},
+				"handler": {"type": "Integer", "value": 1}
+			}
+		},
+		{
+			"outputs": {
+				"level": {"type": "Integer", "value": 75},
+				"handler": {"type": "Integer", "value": 2}
+			}
+		}
+	],
+	"admissible": "A decision with several holding guards: exactly one branch follows, which one is open"
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.sysml b/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.sysml
new file mode 100644
index 000000000..0ada7995a
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.sysml
@@ -0,0 +1,23 @@
+package test {
+	private import ScalarValues::*;
+
+	// Oracle (docs/project/behavior-semantic-oracle.md): both guards hold for
+	// level = 75, and the library says only that exactly one branch follows the
+	// decision, not which; the executor takes the first declared and reports the
+	// choice.
+	action route {
+		attribute level : Integer = 75;
+		attribute handler : Integer = 0;
+
+		first start;
+		then decide select;
+			if level > 50 then warn;
+			if level > 70 then alarm;
+
+		action warn { assign handler := 1; }
+		then done;
+
+		action alarm { assign handler := 2; }
+		then done;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.trace.golden b/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.trace.golden
new file mode 100644
index 000000000..271e6a5e0
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.trace.golden
@@ -0,0 +1,10 @@
+step 1: token 1@select
+  eval feature level -> 75
+  eval literal 50 -> 50
+eval operator > -> true
+choice step 2: decision select branches 1->warn, 2->alarm hold (unordered; took 1->warn)
+step 2: token 1@warn
+stmt assign handler
+  eval literal 1 -> 1
+step 3: token 1@done
+step 4: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.expected.json b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.expected.json
new file mode 100644
index 000000000..c177cefb4
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.expected.json
@@ -0,0 +1,8 @@
+{
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"leftCount": {"type": "Integer", "value": 1},
+		"rightCount": {"type": "Integer", "value": 10}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.sysml b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.sysml
new file mode 100644
index 000000000..82abc76c8
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.sysml
@@ -0,0 +1,26 @@
+package test {
+	private import ScalarValues::*;
+
+	// Oracle (docs/project/behavior-semantic-oracle.md): the library orders
+	// neither branch before the other; each writes its own feature, so the outcome
+	// is fixed and only the order the branches were stepped in is the executor's
+	// choice, which the trace reports.
+	action tally {
+		attribute leftCount : Integer = 0;
+		attribute rightCount : Integer = 0;
+
+		first start;
+		fork split;
+		action left { assign leftCount := leftCount + 1; }
+		action right { assign rightCount := rightCount + 10; }
+		join sync;
+		done;
+
+		succession first start then split;
+		succession first split then left;
+		succession first split then right;
+		succession first left then sync;
+		succession first right then sync;
+		succession first sync then done;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.golden b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.golden
new file mode 100644
index 000000000..8c7a5dce5
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.golden
@@ -0,0 +1,14 @@
+step 1: token 1@split
+step 2: token 2@left, token 3@right
+stmt assign rightCount
+    eval feature rightCount -> 0
+    eval literal 10 -> 10
+  eval operator + -> 10
+stmt assign leftCount
+    eval feature leftCount -> 0
+    eval literal 1 -> 1
+  eval operator + -> 1
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
+step 3: token 2@sync, token 3@sync
+step 4: token 4@done
+step 5: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.order b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.order
new file mode 100644
index 000000000..27fd979bc
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.order
@@ -0,0 +1,6 @@
+# The fork precedes both branches; the join waits for both. The library does
+# not order left against right.
+split < left
+split < right
+left < sync
+right < sync
diff --git a/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.expected.json b/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.expected.json
new file mode 100644
index 000000000..3d9f38939
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.expected.json
@@ -0,0 +1,8 @@
+{
+	"type": "instance",
+	"instantiate": "test::Host",
+	"trace": true,
+	"slots": {
+		"mark": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.sysml b/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.sysml
new file mode 100644
index 000000000..8f5c0f65a
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.sysml
@@ -0,0 +1,27 @@
+package test {
+	private import ScalarValues::*;
+
+	// Oracle (docs/project/behavior-semantic-oracle.md): both branches of the
+	// performed action write the performing part's `mark` in the same step. The
+	// value is the same either way, but the library leaves which write stands
+	// open, so the executor reports the conflict on the performer all the same.
+	part def Host {
+		attribute mark : Integer = 0;
+
+		perform action marking {
+			first start;
+			fork split;
+			action left { assign mark := 1; }
+			action right { assign mark := 1; }
+			join sync;
+			done;
+
+			succession first start then split;
+			succession first split then left;
+			succession first split then right;
+			succession first left then sync;
+			succession first right then sync;
+			succession first sync then done;
+		}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.trace.golden b/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.trace.golden
new file mode 100644
index 000000000..aa123f203
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_performer_write_conflict.trace.golden
@@ -0,0 +1,15 @@
+materialize: Host #1
+start: performed action marking of #1
+materialize: marking #2
+run: performed action marking of #1
+step 1: token 1@split
+step 2: token 2@left, token 3@right
+stmt assign mark
+  eval literal 1 -> 1
+stmt assign mark
+  eval literal 1 -> 1
+choice step 3: writes mark of object #1 := 1 by token 2, mark of object #1 := 1 by token 3 (unordered; mark of object #1 := 1 by token 2 stood)
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
+step 3: token 2@sync, token 3@sync
+step 4: token 4@done
+step 5: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.expected.json b/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.expected.json
new file mode 100644
index 000000000..558d3baf0
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.expected.json
@@ -0,0 +1,21 @@
+{
+	"type": "action",
+	"trace": true,
+	"outcomes": [
+		{
+			"outputs": {
+				"winner": {"type": "String", "value": "hare"},
+				"hareRan": {"type": "Boolean", "value": true},
+				"tortoiseRan": {"type": "Boolean", "value": true}
+			}
+		},
+		{
+			"outputs": {
+				"winner": {"type": "String", "value": "tortoise"},
+				"hareRan": {"type": "Boolean", "value": true},
+				"tortoiseRan": {"type": "Boolean", "value": true}
+			}
+		}
+	],
+	"admissible": "Concurrent branches writing one feature: the value is open, the writes are not"
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.sysml b/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.sysml
new file mode 100644
index 000000000..8615153b2
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.sysml
@@ -0,0 +1,26 @@
+package test {
+	private import ScalarValues::*;
+
+	// Oracle (docs/project/behavior-semantic-oracle.md): both branches write
+	// `winner` in the same step; the library leaves which write stands open, so
+	// the executor reports the conflict and the value that stood.
+	action race {
+		attribute winner : String = "none";
+		attribute hareRan : Boolean = false;
+		attribute tortoiseRan : Boolean = false;
+
+		first start;
+		fork split;
+		action hare { assign winner := "hare"; assign hareRan := true; }
+		action tortoise { assign winner := "tortoise"; assign tortoiseRan := true; }
+		join finish;
+		done;
+
+		succession first start then split;
+		succession first split then hare;
+		succession first split then tortoise;
+		succession first hare then finish;
+		succession first tortoise then finish;
+		succession first finish then done;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.trace.golden b/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.trace.golden
new file mode 100644
index 000000000..cdfb71c9c
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.trace.golden
@@ -0,0 +1,15 @@
+step 1: token 1@split
+step 2: token 2@hare, token 3@tortoise
+stmt assign winner
+  eval literal "tortoise" -> "tortoise"
+stmt assign tortoiseRan
+  eval literal true -> true
+stmt assign winner
+  eval literal "hare" -> "hare"
+stmt assign hareRan
+  eval literal true -> true
+choice step 3: writes winner := "hare" by token 2, winner := "tortoise" by token 3 (unordered; winner := "hare" by token 2 stood)
+choice step 3: tokens 2@hare, 3@tortoise (unordered; took 3@tortoise first)
+step 3: token 2@finish, token 3@finish
+step 4: token 4@done
+step 5: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.expected.json b/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.expected.json
new file mode 100644
index 000000000..0c055180f
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.expected.json
@@ -0,0 +1,8 @@
+{
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"a": {"type": "Integer", "value": 2},
+		"b": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.sysml b/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.sysml
new file mode 100644
index 000000000..eb63556a9
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.sysml
@@ -0,0 +1,44 @@
+package test {
+	private import ScalarValues::*;
+
+	// Two accepts of one type park in parallel branches while a third branch
+	// sends one Integer at a time. The first message answers both accepts, so
+	// which one takes it is the executor's order: a choice point naming both
+	// accepts. The second message finds one accept waiting: no choice.
+	action listen {
+		attribute a : Integer = 0;
+		attribute b : Integer = 0;
+
+		first start;
+
+		fork split;
+
+		action sendOne send 1;
+
+		action sendTwo send 2;
+
+		action left accept x : Integer;
+
+		action right accept y : Integer;
+
+		join sync;
+
+		action recorder {
+			assign a := x;
+			assign b := y;
+		}
+
+		done;
+
+		succession first start then split;
+		succession first split then sendOne;
+		succession first split then left;
+		succession first split then right;
+		succession first sendOne then sendTwo;
+		succession first sendTwo then sync;
+		succession first left then sync;
+		succession first right then sync;
+		succession first sync then recorder;
+		succession first recorder then done;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.trace.golden b/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.trace.golden
new file mode 100644
index 000000000..86b46ad95
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_shared_message_accept.trace.golden
@@ -0,0 +1,17 @@
+step 1: token 1@split
+step 2: token 2@sendOne, token 3@left, token 4@right
+stmt send
+  eval literal 1 -> 1
+step 3: token 2@sendTwo, token 3@left, token 4@right
+stmt send
+  eval literal 2 -> 2
+choice step 4: tokens 2@sendTwo, 3@left, 4@right (unordered; took 4@right first)
+step 4: token 2@sync, token 3@left, token 4@sync
+step 5: token 2@sync, token 3@sync, token 4@sync
+step 6: token 5@recorder
+stmt assign a
+  eval feature x -> 2
+stmt assign b
+  eval feature y -> 1
+step 7: token 5@done
+step 8: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.expected.json b/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.expected.json
new file mode 100644
index 000000000..65437b8cf
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.expected.json
@@ -0,0 +1,8 @@
+{
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"level": {"type": "Integer", "value": 75},
+		"handler": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.sysml b/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.sysml
new file mode 100644
index 000000000..2080a6c28
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.sysml
@@ -0,0 +1,23 @@
+package test {
+	private import ScalarValues::*;
+
+	// Oracle (docs/project/behavior-semantic-oracle.md): the first guard holds for
+	// level = 75; the second has no result (it divides by zero). A guard with no
+	// result is not true, so its branch is not selected and the run is unchanged;
+	// the executor reports the guard it could not evaluate.
+	action route {
+		attribute level : Integer = 75;
+		attribute handler : Integer = 0;
+
+		first start;
+		then decide select;
+			if level > 50 then warn;
+			if 1 / (level - 75) > 0 then alarm;
+
+		action warn { assign handler := 1; }
+		then done;
+
+		action alarm { assign handler := 2; }
+		then done;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.trace.golden b/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.trace.golden
new file mode 100644
index 000000000..7995925cf
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/action_choice_unevaluable_guard.trace.golden
@@ -0,0 +1,10 @@
+step 1: token 1@select
+  eval feature level -> 75
+  eval literal 50 -> 50
+eval operator > -> true
+unevaluable guard step 2: decision select branch 2->alarm: division by zero (not selected)
+step 2: token 1@warn
+stmt assign handler
+  eval literal 1 -> 1
+step 3: token 1@done
+step 4: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_explicit_succession_fork_join.trace.golden b/internal/core/runtime/testdata/conformance/action_explicit_succession_fork_join.trace.golden
index 9788088bd..f0e00fef2 100644
--- a/internal/core/runtime/testdata/conformance/action_explicit_succession_fork_join.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_explicit_succession_fork_join.trace.golden
@@ -4,6 +4,7 @@ stmt assign rightValue
   eval literal 2 -> 2
 stmt assign leftValue
   eval literal 1 -> 1
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
 step 3: token 2@sync, token 3@sync
 step 4: token 4@done
 step 5: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_fork_branches_share_features.trace.golden b/internal/core/runtime/testdata/conformance/action_fork_branches_share_features.trace.golden
index 8b734a52a..cf8e904a7 100644
--- a/internal/core/runtime/testdata/conformance/action_fork_branches_share_features.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_fork_branches_share_features.trace.golden
@@ -4,6 +4,7 @@ stmt assign y
   eval literal 2 -> 2
 stmt assign x
   eval literal 1 -> 1
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
 step 3: token 2@sync, token 3@sync
 step 4: token 4@done
 step 5: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_fork_branches_write_one_feature.trace.golden b/internal/core/runtime/testdata/conformance/action_fork_branches_write_one_feature.trace.golden
index f08f46bcf..cb0367a36 100644
--- a/internal/core/runtime/testdata/conformance/action_fork_branches_write_one_feature.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_fork_branches_write_one_feature.trace.golden
@@ -8,6 +8,8 @@ stmt assign x
   eval literal 1 -> 1
 stmt assign leftRan
   eval literal true -> true
+choice step 3: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 1 by token 2 stood)
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
 step 3: token 2@sync, token 3@sync
 step 4: token 4@done
 step 5: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_join_one_token_per_incoming_succession.trace.golden b/internal/core/runtime/testdata/conformance/action_join_one_token_per_incoming_succession.trace.golden
index c33394cfb..c3107e4dd 100644
--- a/internal/core/runtime/testdata/conformance/action_join_one_token_per_incoming_succession.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_join_one_token_per_incoming_succession.trace.golden
@@ -1,6 +1,8 @@
 step 1: token 1@split
 step 2: token 2@l1, token 3@l2, token 4@r1
+choice step 3: tokens 2@l1, 3@l2, 4@r1 (unordered; took 4@r1 first)
 step 3: token 2@left, token 3@left, token 4@r2
+choice step 4: tokens 3@left, 4@r2 (unordered; took 4@r2 first)
 step 4: token 4@r3, token 5@sync
 step 5: token 4@right, token 5@sync
 stmt assign log
diff --git a/internal/core/runtime/testdata/conformance/action_join_same_succession_twice.trace.golden b/internal/core/runtime/testdata/conformance/action_join_same_succession_twice.trace.golden
index 52592767c..4a1c492df 100644
--- a/internal/core/runtime/testdata/conformance/action_join_same_succession_twice.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_join_same_succession_twice.trace.golden
@@ -4,17 +4,22 @@ stmt assign n
     eval feature n -> 0
     eval literal 1 -> 1
   eval operator + -> 1
+choice step 3: tokens 2@tick, 3@s1 (unordered; took 3@s1 first)
 step 3: token 2@tee, token 3@s2
+choice step 4: tokens 2@tee, 3@s2 (unordered; took 3@s2 first)
 step 4: token 3@s3, token 4@sync, token 5@again
   eval feature n -> 1
   eval literal 2 -> 2
 eval operator < -> true
+choice step 5: tokens 3@s3, 5@again (unordered; took 5@again first)
 step 5: token 3@s4, token 4@sync, token 5@tick
 stmt assign n
     eval feature n -> 1
     eval literal 1 -> 1
   eval operator + -> 2
+choice step 6: tokens 3@s4, 5@tick (unordered; took 5@tick first)
 step 6: token 3@s5, token 4@sync, token 5@tee
+choice step 7: tokens 3@s5, 5@tee (unordered; took 5@tee first)
 step 7: token 3@s6, token 4@sync, token 6@sync, token 7@again
   eval feature n -> 2
   eval literal 2 -> 2
@@ -22,6 +27,7 @@ eval operator < -> false
   eval feature n -> 2
   eval literal 2 -> 2
 eval operator >= -> true
+choice step 8: tokens 3@s6, 7@again (unordered; took 7@again first)
 step 8: token 3@right, token 4@sync, token 6@sync, token 7@tickEnd
 stmt assign m
     eval feature m -> 0
@@ -33,6 +39,7 @@ stmt assign log
     eval operator * -> 0
     eval literal 1 -> 1
   eval operator + -> 1
+choice step 9: tokens 3@right, 7@tickEnd (unordered; took 7@tickEnd first)
 step 9: token 3@sync, token 4@sync, token 6@sync
 step 10: token 6@sync, token 8@after
 stmt assign log
diff --git a/internal/core/runtime/testdata/conformance/action_join_three_two_arrive_together.trace.golden b/internal/core/runtime/testdata/conformance/action_join_three_two_arrive_together.trace.golden
index 16debacbc..a74e96737 100644
--- a/internal/core/runtime/testdata/conformance/action_join_three_two_arrive_together.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_join_three_two_arrive_together.trace.golden
@@ -8,6 +8,8 @@ stmt assign arrived
     eval feature arrived -> 1
     eval literal 1 -> 1
   eval operator + -> 2
+choice step 3: writes arrived := 2 by token 2, arrived := 1 by token 3 (unordered; arrived := 2 by token 2 stood)
+choice step 3: tokens 2@a, 3@b, 4@c1 (unordered; took 4@c1 first)
 step 3: token 2@sync, token 3@sync, token 4@c2
 step 4: token 2@sync, token 3@sync, token 4@c3
 stmt assign arrived
diff --git a/internal/core/runtime/testdata/conformance/action_join_waits_for_slowest_branch.trace.golden b/internal/core/runtime/testdata/conformance/action_join_waits_for_slowest_branch.trace.golden
index ae1720b49..0e26160eb 100644
--- a/internal/core/runtime/testdata/conformance/action_join_waits_for_slowest_branch.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_join_waits_for_slowest_branch.trace.golden
@@ -4,11 +4,13 @@ stmt assign arrived
     eval feature arrived -> 0
     eval literal 1 -> 1
   eval operator + -> 1
+choice step 3: tokens 2@a, 3@b1, 4@c1 (unordered; took 4@c1 first)
 step 3: token 2@sync, token 3@b2, token 4@c2
 stmt assign arrived
     eval feature arrived -> 1
     eval literal 1 -> 1
   eval operator + -> 2
+choice step 4: tokens 3@b2, 4@c2 (unordered; took 4@c2 first)
 step 4: token 2@sync, token 3@sync, token 4@c3
 stmt assign arrived
     eval feature arrived -> 2
diff --git a/internal/core/runtime/testdata/conformance/action_merge_fork_branch_and_loop.trace.golden b/internal/core/runtime/testdata/conformance/action_merge_fork_branch_and_loop.trace.golden
index 4e8e88c95..0b8226043 100644
--- a/internal/core/runtime/testdata/conformance/action_merge_fork_branch_and_loop.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_merge_fork_branch_and_loop.trace.golden
@@ -4,6 +4,7 @@ stmt assign merged
     eval feature merged -> 0
     eval literal 1 -> 1
   eval operator + -> 1
+choice step 3: tokens 2@gate, 3@prep (unordered; took 3@prep first)
 step 3: token 2@work, token 3@gate
 stmt assign merged
     eval feature merged -> 1
@@ -13,6 +14,7 @@ stmt assign worked
     eval feature worked -> 0
     eval literal 1 -> 1
   eval operator + -> 1
+choice step 4: tokens 2@work, 3@gate (unordered; took 3@gate first)
 step 4: token 2@more, token 3@work
 stmt assign worked
     eval feature worked -> 1
@@ -25,6 +27,7 @@ stmt assign passes
   eval feature passes -> 1
   eval literal 3 -> 3
 eval operator < -> true
+choice step 5: tokens 2@more, 3@work (unordered; took 3@work first)
 step 5: token 2@gate, token 3@more
 stmt assign passes
     eval feature passes -> 1
@@ -37,6 +40,7 @@ stmt assign merged
     eval feature merged -> 2
     eval literal 1 -> 1
   eval operator + -> 3
+choice step 6: tokens 2@gate, 3@more (unordered; took 3@more first)
 step 6: token 2@work, token 3@gate
 stmt assign merged
     eval feature merged -> 3
@@ -46,6 +50,7 @@ stmt assign worked
     eval feature worked -> 2
     eval literal 1 -> 1
   eval operator + -> 3
+choice step 7: tokens 2@work, 3@gate (unordered; took 3@gate first)
 step 7: token 2@more, token 3@work
 stmt assign worked
     eval feature worked -> 3
@@ -61,6 +66,7 @@ eval operator < -> false
   eval feature passes -> 3
   eval literal 3 -> 3
 eval operator >= -> true
+choice step 8: tokens 2@more, 3@work (unordered; took 3@work first)
 step 8: token 2@done, token 3@more
 stmt assign passes
     eval feature passes -> 3
@@ -72,5 +78,6 @@ eval operator < -> false
   eval feature passes -> 4
   eval literal 3 -> 3
 eval operator >= -> true
+choice step 9: tokens 2@done, 3@more (unordered; took 3@more first)
 step 9: token 3@done
 step 10: no active tokens
diff --git a/internal/core/runtime/testdata/conformance/action_nested_flow_in_fork_join.trace.golden b/internal/core/runtime/testdata/conformance/action_nested_flow_in_fork_join.trace.golden
index 448ce09f9..a769d8497 100644
--- a/internal/core/runtime/testdata/conformance/action_nested_flow_in_fork_join.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_nested_flow_in_fork_join.trace.golden
@@ -2,6 +2,7 @@ step 1: token 1@split
 step 2: token 2@left, token 3@right
 enter action node: right
 enter action node: left
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
 step 3: token 2@leftStep, token 3@rightStep
 stmt assign rightValue
   eval literal 2 -> 2
@@ -9,6 +10,7 @@ leave action node: right
 stmt assign leftValue
   eval literal 1 -> 1
 leave action node: left
+choice step 4: tokens 2@leftStep, 3@rightStep (unordered; took 3@rightStep first)
 step 4: token 2@sync, token 3@sync
 step 5: token 4@tally
 stmt assign leftValue
diff --git a/internal/core/runtime/testdata/conformance/action_nested_node_two_successions_per_performance.trace.golden b/internal/core/runtime/testdata/conformance/action_nested_node_two_successions_per_performance.trace.golden
index 6799a9994..57eb72a78 100644
--- a/internal/core/runtime/testdata/conformance/action_nested_node_two_successions_per_performance.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_nested_node_two_successions_per_performance.trace.golden
@@ -3,6 +3,7 @@ step 2: token 2@one, token 3@two
 eval literal 0 -> 0
 step 1: token 1@split
 step 2: token 2@l1, token 3@l2
+choice step 3: tokens 2@l1, 3@l2 (unordered; took 3@l2 first)
 step 3: token 2@both, token 3@both
 stmt assign hits
     eval feature hits -> 0
@@ -13,6 +14,7 @@ step 5: no active tokens
 eval literal 0 -> 0
 step 1: token 1@split
 step 2: token 2@l1, token 3@l2
+choice step 3: tokens 2@l1, 3@l2 (unordered; took 3@l2 first)
 step 3: token 2@both, token 3@both
 stmt assign hits
     eval feature hits -> 0
@@ -20,6 +22,7 @@ stmt assign hits
   eval operator + -> 1
 step 4: token 4@done
 step 5: no active tokens
+choice step 3: tokens 2@one, 3@two (unordered; took 3@two first)
 step 3: token 2@sync, token 3@sync
 step 4: token 4@tally
 stmt assign total
diff --git a/internal/core/runtime/testdata/conformance/action_node_concurrent_nested_bindings.trace.golden b/internal/core/runtime/testdata/conformance/action_node_concurrent_nested_bindings.trace.golden
index 42facdcfa..5aae82607 100644
--- a/internal/core/runtime/testdata/conformance/action_node_concurrent_nested_bindings.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_node_concurrent_nested_bindings.trace.golden
@@ -4,6 +4,7 @@ stmt assign v
   eval literal 2 -> 2
 stmt assign v
   eval literal 1 -> 1
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
 step 3: token 2@leg, token 3@leg
 enter action node: leg
 step 4: token 4@inner
diff --git a/internal/core/runtime/testdata/conformance/action_node_concurrent_performances.trace.golden b/internal/core/runtime/testdata/conformance/action_node_concurrent_performances.trace.golden
index 114ef8de9..d5bd1d820 100644
--- a/internal/core/runtime/testdata/conformance/action_node_concurrent_performances.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_node_concurrent_performances.trace.golden
@@ -4,6 +4,7 @@ stmt assign v
   eval literal 2 -> 2
 stmt assign v
   eval literal 1 -> 1
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
 step 3: token 2@stage, token 3@stage
 enter action node: stage
 step 4: token 4@scale
diff --git a/internal/core/runtime/testdata/conformance/action_node_with_two_incoming_successions_runs_once.trace.golden b/internal/core/runtime/testdata/conformance/action_node_with_two_incoming_successions_runs_once.trace.golden
index b5549dc9e..40be2dd5e 100644
--- a/internal/core/runtime/testdata/conformance/action_node_with_two_incoming_successions_runs_once.trace.golden
+++ b/internal/core/runtime/testdata/conformance/action_node_with_two_incoming_successions_runs_once.trace.golden
@@ -1,5 +1,6 @@
 step 1: token 1@split
 step 2: token 2@l1, token 3@l2
+choice step 3: tokens 2@l1, 3@l2 (unordered; took 3@l2 first)
 step 3: token 2@both, token 3@both
 stmt assign hits
     eval feature hits -> 0
diff --git a/internal/core/runtime/testdata/conformance/f63_merge_body_runs_on_traversal.trace.golden b/internal/core/runtime/testdata/conformance/f63_merge_body_runs_on_traversal.trace.golden
index 9cdeff059..692259565 100644
--- a/internal/core/runtime/testdata/conformance/f63_merge_body_runs_on_traversal.trace.golden
+++ b/internal/core/runtime/testdata/conformance/f63_merge_body_runs_on_traversal.trace.golden
@@ -5,6 +5,7 @@ stmt assign mergeRuns
     eval literal 1 -> 1
   eval operator + -> 1
 eval feature ready -> false
+choice step 3: tokens 2@gate, 3@slow (unordered; took 3@slow first)
 step 3: token 3@slower
 stmt assign ready
   eval literal true -> true
diff --git a/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.expected.json b/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.expected.json
new file mode 100644
index 000000000..c5ba4ac7b
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.expected.json
@@ -0,0 +1,11 @@
+{
+	"type": "state",
+	"trace": true,
+	"events": [{"signal": "Go"}],
+	"finalState": "a2+b1",
+	"stateVisits": ["work", "a1", "b1", "a2"],
+	"outputs": {
+		"level": {"type": "Integer", "value": 8},
+		"route": {"type": "Integer", "value": 3}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.sysml b/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.sysml
new file mode 100644
index 000000000..481a2b372
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.sysml
@@ -0,0 +1,33 @@
+package test {
+	// Region `a` reacts to Go from its own substate `a1`, so the transitions out
+	// of the enclosing parallel state `work` lose to it (UML orders the innermost
+	// enabled transition first) although both of their guards hold. The
+	// alternatives out of `work` were never the run's to choose among: no choice
+	// point is reported.
+	state Machine {
+		attribute level : Integer = 8;
+		attribute route : Integer = 0;
+
+		entry; then work;
+		state work parallel {
+			state a {
+				entry; then a1;
+				state a1;
+				state a2 {
+					entry { assign route := 3; }
+				}
+				transition first a1 accept Go then a2;
+			}
+			state b { entry; then b1; state b1; }
+		}
+		state low {
+			entry { assign route := 1; }
+		}
+		state high {
+			entry { assign route := 2; }
+		}
+
+		transition first work accept Go if level > 5 then low;
+		transition first work accept Go if level > 7 then high;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.trace.golden b/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.trace.golden
new file mode 100644
index 000000000..204364e2b
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_ancestor_outranked_not_reported.trace.golden
@@ -0,0 +1,8 @@
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+exit: a1
+enter: a2 (entry action)
+stmt assign route
+  eval literal 3 -> 3
+transition: a1 -> a2 (event: accept Go)
diff --git a/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.expected.json b/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.expected.json
new file mode 100644
index 000000000..e7e31dbc8
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.expected.json
@@ -0,0 +1,11 @@
+{
+	"type": "state",
+	"trace": true,
+	"events": [{"signal": "Tick"}],
+	"finalState": "warm",
+	"stateVisits": ["running", "fine", "warm"],
+	"outputs": {
+		"temp": {"type": "Integer", "value": 30},
+		"path": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.sysml b/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.sysml
new file mode 100644
index 000000000..046cab184
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.sysml
@@ -0,0 +1,25 @@
+package test {
+	// The substate `fine` and the composite `running` enclosing it both react to
+	// Tick with a holding guard. UML orders these: the innermost enabled transition
+	// fires, so this is a rule, not a choice, and no choice point is reported.
+	state Monitor {
+		attribute temp : Integer = 30;
+		attribute path : Integer = 0;
+
+		entry; then running;
+		state running {
+			entry; then fine;
+			state fine;
+			state warm {
+				entry { assign path := 1; }
+			}
+
+			transition first fine accept Tick if temp > 20 then warm;
+		}
+		state halted {
+			entry { assign path := 2; }
+		}
+
+		transition first running accept Tick if temp > 10 then halted;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.trace.golden b/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.trace.golden
new file mode 100644
index 000000000..f48919d0a
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.trace.golden
@@ -0,0 +1,11 @@
+  eval feature temp -> 30
+  eval literal 20 -> 20
+eval operator > -> true
+  eval feature temp -> 30
+  eval literal 20 -> 20
+eval operator > -> true
+exit: fine
+enter: warm (entry action)
+stmt assign path
+  eval literal 1 -> 1
+transition: fine -> warm (event: accept Tick)
diff --git a/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.expected.json b/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.expected.json
new file mode 100644
index 000000000..509af02b7
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.expected.json
@@ -0,0 +1,23 @@
+{
+	"type": "state",
+	"trace": true,
+	"outcomes": [
+		{
+			"finalState": "cool",
+			"stateVisits": ["start", "watching", "cool"],
+			"outputs": {
+				"temp": {"type": "Integer", "value": 30},
+				"route": {"type": "Integer", "value": 1}
+			}
+		},
+		{
+			"finalState": "hot",
+			"stateVisits": ["start", "watching", "hot"],
+			"outputs": {
+				"temp": {"type": "Integer", "value": 30},
+				"route": {"type": "Integer", "value": 2}
+			}
+		}
+	],
+	"admissible": "Two transitions out of one state enabled by one event: exactly one fires, which one is open"
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.sysml b/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.sysml
new file mode 100644
index 000000000..780ecbcf5
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.sysml
@@ -0,0 +1,24 @@
+package test {
+	// Oracle (docs/project/behavior-semantic-oracle.md): two change-triggered
+	// transitions out of `watching` rise on the one write of temp, both conditions
+	// turning true for temp = 30; the library says one fires, not which. The
+	// executor fires the first declared and reports the choice.
+	state Monitor {
+		attribute temp : Integer = 0;
+		attribute route : Integer = 0;
+
+		entry; then start;
+		state start;
+		state watching;
+		state cool {
+			entry { assign route := 1; }
+		}
+		state hot {
+			entry { assign route := 2; }
+		}
+
+		transition first start do assign temp := 30 then watching;
+		transition first watching accept when temp > 20 then cool;
+		transition first watching accept when temp > 25 then hot;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.trace.golden b/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.trace.golden
new file mode 100644
index 000000000..73ee5e602
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_change_transition_conflict.trace.golden
@@ -0,0 +1,17 @@
+exit: start
+stmt assign temp
+  eval literal 30 -> 30
+enter: watching
+transition: start -> watching
+  eval feature temp -> 30
+  eval literal 20 -> 20
+eval operator > -> true
+  eval feature temp -> 30
+  eval literal 25 -> 25
+eval operator > -> true
+choice state watching on change: transitions 1->cool, 2->hot (unordered; took 1->cool)
+exit: watching
+enter: cool (entry action)
+stmt assign route
+  eval literal 1 -> 1
+transition: watching -> cool (event: change)
diff --git a/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.expected.json b/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.expected.json
new file mode 100644
index 000000000..928e10cee
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.expected.json
@@ -0,0 +1,24 @@
+{
+	"type": "state",
+	"trace": true,
+	"events": [{"signal": "Go"}],
+	"outcomes": [
+		{
+			"finalState": "low",
+			"stateVisits": ["work", "a1", "b1", "low"],
+			"outputs": {
+				"level": {"type": "Integer", "value": 8},
+				"route": {"type": "Integer", "value": 1}
+			}
+		},
+		{
+			"finalState": "high",
+			"stateVisits": ["work", "a1", "b1", "high"],
+			"outputs": {
+				"level": {"type": "Integer", "value": 8},
+				"route": {"type": "Integer", "value": 2}
+			}
+		}
+	],
+	"admissible": "Two transitions out of one state enabled by one event: exactly one fires, which one is open"
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.sysml b/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.sysml
new file mode 100644
index 000000000..76e6442d0
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.sysml
@@ -0,0 +1,25 @@
+package test {
+	// Oracle (docs/project/behavior-semantic-oracle.md): two transitions out of
+	// the parallel state `work` are enabled by one Go. Both regions select the
+	// same transition out of `work`, which the event takes once; the choice among
+	// the transitions out of `work` is likewise made once and reported once.
+	state Machine {
+		attribute level : Integer = 8;
+		attribute route : Integer = 0;
+
+		entry; then work;
+		state work parallel {
+			state a { entry; then a1; state a1; }
+			state b { entry; then b1; state b1; }
+		}
+		state low {
+			entry { assign route := 1; }
+		}
+		state high {
+			entry { assign route := 2; }
+		}
+
+		transition first work accept Go if level > 5 then low;
+		transition first work accept Go if level > 7 then high;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.trace.golden b/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.trace.golden
new file mode 100644
index 000000000..a09fe5dad
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_shared_ancestor_regions.trace.golden
@@ -0,0 +1,17 @@
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+choice state work on accept Go: transitions 1->low, 2->high (unordered; took 1->low)
+exit: a1
+exit: b1
+exit: work
+enter: low (entry action)
+stmt assign route
+  eval literal 1 -> 1
+transition: work -> low (event: accept Go)
diff --git a/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.expected.json b/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.expected.json
new file mode 100644
index 000000000..af8119da3
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.expected.json
@@ -0,0 +1,24 @@
+{
+	"type": "state",
+	"trace": true,
+	"events": [{"signal": "Go"}],
+	"outcomes": [
+		{
+			"finalState": "low",
+			"stateVisits": ["idle", "low"],
+			"outputs": {
+				"level": {"type": "Integer", "value": 8},
+				"route": {"type": "Integer", "value": 1}
+			}
+		},
+		{
+			"finalState": "high",
+			"stateVisits": ["idle", "high"],
+			"outputs": {
+				"level": {"type": "Integer", "value": 8},
+				"route": {"type": "Integer", "value": 2}
+			}
+		}
+	],
+	"admissible": "Two transitions out of one state enabled by one event: exactly one fires, which one is open"
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.sysml b/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.sysml
new file mode 100644
index 000000000..8436f0538
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.sysml
@@ -0,0 +1,22 @@
+package test {
+	// Oracle (docs/project/behavior-semantic-oracle.md): two transitions out of
+	// `idle` are enabled by one Go, both guards holding for level = 8; the library
+	// says one fires, not which. The executor fires the first declared and reports
+	// the choice.
+	state Dispatcher {
+		attribute level : Integer = 8;
+		attribute route : Integer = 0;
+
+		entry; then idle;
+		state idle;
+		state low {
+			entry { assign route := 1; }
+		}
+		state high {
+			entry { assign route := 2; }
+		}
+
+		transition first idle accept Go if level > 5 then low;
+		transition first idle accept Go if level > 7 then high;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.trace.golden b/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.trace.golden
new file mode 100644
index 000000000..f022b5a62
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_transition_conflict.trace.golden
@@ -0,0 +1,12 @@
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+choice state idle on accept Go: transitions 1->low, 2->high (unordered; took 1->low)
+exit: idle
+enter: low (entry action)
+stmt assign route
+  eval literal 1 -> 1
+transition: idle -> low (event: accept Go)
diff --git a/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.expected.json b/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.expected.json
new file mode 100644
index 000000000..c83289243
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.expected.json
@@ -0,0 +1,11 @@
+{
+	"type": "state",
+	"trace": true,
+	"events": [{"signal": "Go"}],
+	"finalState": "low",
+	"stateVisits": ["idle", "low"],
+	"outputs": {
+		"level": {"type": "Integer", "value": 8},
+		"route": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.sysml b/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.sysml
new file mode 100644
index 000000000..7d969d1ab
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.sysml
@@ -0,0 +1,23 @@
+package test {
+	// Oracle (docs/project/behavior-semantic-oracle.md): the first transition out
+	// of `idle` is enabled by Go; the second's guard has no result (it divides by
+	// zero). A guard with no result is not true, so that transition is not
+	// selected and the run is unchanged; the executor reports the guard it could
+	// not evaluate.
+	state Dispatcher {
+		attribute level : Integer = 8;
+		attribute route : Integer = 0;
+
+		entry; then idle;
+		state idle;
+		state low {
+			entry { assign route := 1; }
+		}
+		state high {
+			entry { assign route := 2; }
+		}
+
+		transition first idle accept Go if level > 5 then low;
+		transition first idle accept Go if 1 / (level - 8) > 0 then high;
+	}
+}
diff --git a/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.trace.golden b/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.trace.golden
new file mode 100644
index 000000000..329a11ba6
--- /dev/null
+++ b/internal/core/runtime/testdata/conformance/state_choice_unevaluable_transition.trace.golden
@@ -0,0 +1,12 @@
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+  eval feature level -> 8
+  eval literal 5 -> 5
+eval operator > -> true
+unevaluable guard state idle on accept Go: transition 2->high: eval guard of transition idle -> high: division by zero (not selected)
+exit: idle
+enter: low (entry action)
+stmt assign route
+  eval literal 1 -> 1
+transition: idle -> low (event: accept Go)
diff --git a/internal/core/runtime/testdata/conformance/w7d_send_via_port_to_receiver.trace.golden b/internal/core/runtime/testdata/conformance/w7d_send_via_port_to_receiver.trace.golden
index 9befb2eff..b7763d6fd 100644
--- a/internal/core/runtime/testdata/conformance/w7d_send_via_port_to_receiver.trace.golden
+++ b/internal/core/runtime/testdata/conformance/w7d_send_via_port_to_receiver.trace.golden
@@ -9,6 +9,8 @@ stmt assign siblingGot
   eval feature value -> 7
 stmt assign receiverGot
   eval feature value -> 42
+choice step 4: writes value := 42 by token 2, value := 7 by token 3 (unordered; value := 42 by token 2 stood)
+choice step 4: tokens 2@receiver, 3@sibling (unordered; took 3@sibling first)
 step 4: token 2@sync, token 3@sync
 step 5: token 4@done
 step 6: no active tokens
diff --git a/internal/core/runtime/trace.go b/internal/core/runtime/trace.go
index 4705439eb..cf3d80188 100644
--- a/internal/core/runtime/trace.go
+++ b/internal/core/runtime/trace.go
@@ -74,6 +74,15 @@ func (tr *TraceRecorder) RecordActionStep(step int, tokens []Token) {
 	tr.entries = append(tr.entries, fmt.Sprintf("step %d: %s", step, strings.Join(parts, ", ")))
 }
 
+// RecordNote records a run's note where it was made: before the step line of the
+// action step it belongs to, or before the transition it decided.
+func (tr *TraceRecorder) RecordNote(n RunNote) {
+	if !tr.enabled {
+		return
+	}
+	tr.entries = append(tr.entries, n.String())
+}
+
 // RecordStateTransition records a state transition with event.
 func (tr *TraceRecorder) RecordStateTransition(fromState, toState string, event string) {
 	if !tr.enabled {
diff --git a/internal/core/runtime/value.go b/internal/core/runtime/value.go
index 5ba79c3f5..ccf3208c0 100644
--- a/internal/core/runtime/value.go
+++ b/internal/core/runtime/value.go
@@ -237,6 +237,11 @@ func NewEnumLiteral(sym *symbols.Symbol) Value {
 }
 
 // Str is the text of a ValString; "" for every other kind.
+// isBool reports whether v is a boolean constant.
+func (v Value) isBool() bool {
+	return v.Kind == ValConst && v.Const.Kind == semantics.ValBool
+}
+
 func (v Value) Str() string {
 	if v.Kind != ValString {
 		return ""
diff --git a/internal/grpc/analysis.go b/internal/grpc/analysis.go
index 529cf3746..b1ae83f8f 100644
--- a/internal/grpc/analysis.go
+++ b/internal/grpc/analysis.go
@@ -60,7 +60,8 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) (
 	}
 
 	// A verification case runs the same body, and its run answers with the
-	// verdict that body produced as well.
+	// verdict that body produced as well. The choices a run made are reported
+	// with its outcome, failed or not.
 	var verdicts []runtime.VerificationVerdict
 	var result runtime.AnalysisResult
 	if runtime.IsVerificationCaseSymbol(sym) {
@@ -69,6 +70,7 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) (
 			return &pb.RunAnalysisResponse{
 				Error:         fmt.Sprintf("verification run failed: %v", verr),
 				FailureReason: failureReason(verr),
+				Diagnostics:   RunNoteDiagnosticsToProto(v.runtime.Notes(), v.cached),
 			}, nil
 		}
 		result = verified.Run
@@ -77,12 +79,14 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) (
 		return &pb.RunAnalysisResponse{
 			Error:         fmt.Sprintf("analysis run failed: %v", err),
 			FailureReason: failureReason(err),
+			Diagnostics:   RunNoteDiagnosticsToProto(v.runtime.Notes(), v.cached),
 		}, nil
 	}
+	diags := RunNoteDiagnosticsToProto(v.runtime.Notes(), v.cached)
 	// The case reports the subject it ran on: the one supplied, or the one the
 	// usage or the enclosing case bound.
 	subject = result.Subject
-	resp := &pb.RunAnalysisResponse{Instances: v.instanceGraph(subject)}
+	resp := &pb.RunAnalysisResponse{Instances: v.instanceGraph(subject), Diagnostics: diags}
 	for _, out := range result.Outputs {
 		resp.Outputs = append(resp.Outputs, &pb.CalcOutput{
 			Name:  out.Name,
diff --git a/internal/grpc/cache.go b/internal/grpc/cache.go
index af20e6b6c..e517d8a5e 100644
--- a/internal/grpc/cache.go
+++ b/internal/grpc/cache.go
@@ -91,6 +91,19 @@ func (m *CachedModel) DocumentRoots() []*symbols.Scope {
 	return roots
 }
 
+// document is the source of the model's document named name, nil when none is.
+func (m *CachedModel) document(name string) *source.SourceFile {
+	if name == "" {
+		return nil
+	}
+	for _, doc := range m.Documents {
+		if doc.Source.Name() == name {
+			return doc.Source
+		}
+	}
+	return nil
+}
+
 // PrimaryRoot is the root scope of the document the model is named by.
 func (m *CachedModel) PrimaryRoot() *symbols.Scope {
 	return m.Index.DocumentRoot(m.Primary().Source.Name())
diff --git a/internal/grpc/choice_test.go b/internal/grpc/choice_test.go
new file mode 100644
index 000000000..d1176c620
--- /dev/null
+++ b/internal/grpc/choice_test.go
@@ -0,0 +1,343 @@
+package grpc
+
+import (
+	"context"
+	"strings"
+	"testing"
+
+	pb "github.com/Open-MBEE/OpenSysML/api/proto"
+)
+
+// choiceDiagnostics keeps the choice-point diagnostics of a response.
+func choiceDiagnostics(diags []*pb.Diagnostic) []*pb.Diagnostic {
+	var out []*pb.Diagnostic
+	for _, d := range diags {
+		if strings.HasPrefix(d.Message, "choice point: ") {
+			out = append(out, d)
+		}
+	}
+	return out
+}
+
+// A run that chose among unordered alternatives reports each choice as an
+// informational diagnostic located at the declaration it was made at; a run
+// with one possible order reports none.
+func TestExecuteAction_ChoicePointDiagnostics(t *testing.T) {
+	srv := mustNewService(t, 10)
+
+	content := `
+package Test {
+  action tally {
+    attribute leftCount : Integer = 0;
+    attribute rightCount : Integer = 0;
+
+    first start;
+    fork split;
+    action left { assign leftCount := leftCount + 1; }
+    action right { assign rightCount := rightCount + 10; }
+    join sync;
+    done;
+
+    succession first start then split;
+    succession first split then left;
+    succession first split then right;
+    succession first left then sync;
+    succession first right then sync;
+    succession first sync then done;
+  }
+
+  action single {
+    attribute n : Integer = 0;
+    first start;
+    then action one { assign n := 1; }
+    then done;
+  }
+}
+`
+	parseResp, err := srv.ParseFile(context.Background(), &pb.ParseFileRequest{
+		Source:      &pb.ParseFileRequest_Content{Content: content},
+		ContentHash: "test-execute-action-choices",
+	})
+	if err != nil {
+		t.Fatalf("ParseFile failed: %v", err)
+	}
+
+	resp, err := srv.ExecuteAction(context.Background(), &pb.ExecuteActionRequest{
+		ModelHash:      parseResp.ModelHash,
+		ActionSymbolId: "Test::tally",
+	})
+	if err != nil {
+		t.Fatalf("ExecuteAction failed: %v", err)
+	}
+	if resp.Error != "" {
+		t.Fatalf("execution error: %s", resp.Error)
+	}
+	choices := choiceDiagnostics(resp.Diagnostics)
+	if len(choices) != 1 {
+		t.Fatalf("choice diagnostics = %v, want one", resp.Diagnostics)
+	}
+	d := choices[0]
+	if d.Severity != "info" {
+		t.Errorf("severity = %q, want info", d.Severity)
+	}
+	want := "choice point: step 3: tokens 2@left, 3@right (unordered; took 3@right first)"
+	if d.Message != want {
+		t.Errorf("message = %q, want %q", d.Message, want)
+	}
+	if d.Span == nil || d.Span.StartLine == 0 {
+		t.Errorf("choice diagnostic carries no location: %v", d.Span)
+	}
+
+	resp, err = srv.ExecuteAction(context.Background(), &pb.ExecuteActionRequest{
+		ModelHash:      parseResp.ModelHash,
+		ActionSymbolId: "Test::single",
+	})
+	if err != nil {
+		t.Fatalf("ExecuteAction failed: %v", err)
+	}
+	if resp.Error != "" {
+		t.Fatalf("execution error: %s", resp.Error)
+	}
+	if got := choiceDiagnostics(resp.Diagnostics); len(got) != 0 {
+		t.Errorf("a run with one order reported choices: %v", got)
+	}
+}
+
+// A run that fails in a step one token had already taken reports the order the
+// two tokens went in alongside the error: the failure may depend on that order.
+func TestExecuteAction_ChoicePointDiagnosticsOnFailure(t *testing.T) {
+	srv := mustNewService(t, 10)
+
+	content := `
+package Test {
+  action race {
+    attribute x : Integer = 0;
+    attribute n : Integer = 0;
+    first start;
+    fork split;
+    action safe { assign x := 1; }
+    action failing { assign x := 1 / n; }
+    join sync;
+    done;
+    succession first start then split;
+    succession first split then failing;
+    succession first split then safe;
+    succession first safe then sync;
+    succession first failing then sync;
+    succession first sync then done;
+  }
+}
+`
+	parseResp, err := srv.ParseFile(context.Background(), &pb.ParseFileRequest{
+		Source:      &pb.ParseFileRequest_Content{Content: content},
+		ContentHash: "test-execute-action-choices-on-failure",
+	})
+	if err != nil {
+		t.Fatalf("ParseFile failed: %v", err)
+	}
+
+	resp, err := srv.ExecuteAction(context.Background(), &pb.ExecuteActionRequest{
+		ModelHash:      parseResp.ModelHash,
+		ActionSymbolId: "Test::race",
+	})
+	if err != nil {
+		t.Fatalf("ExecuteAction failed: %v", err)
+	}
+	if !strings.Contains(resp.Error, "division by zero") {
+		t.Fatalf("error = %q, want the failing token's error", resp.Error)
+	}
+	choices := choiceDiagnostics(resp.Diagnostics)
+	want := "choice point: step 3: tokens 2@failing, 3@safe (unordered; took 3@safe first)"
+	if len(choices) != 1 || choices[0].Message != want || choices[0].Severity != "info" {
+		t.Fatalf("choice diagnostics = %v, want one info %q", choices, want)
+	}
+}
+
+// An analysis whose performed action forked reports the order the executor
+// took among the branches and between their writes, with the case's outputs.
+func TestRunAnalysis_ChoicePointDiagnostics(t *testing.T) {
+	srv := mustNewService(t, 10)
+	hash := mustVerifyModel(t, srv, `
+package An {
+	private import ScalarValues::*;
+
+	action def Tally {
+		out r : Integer = 0;
+		first start;
+		fork split;
+		action left { assign r := r + 1; }
+		action right { assign r := r + 10; }
+		join sync;
+		done;
+		succession first start then split;
+		succession first split then left;
+		succession first split then right;
+		succession first left then sync;
+		succession first right then sync;
+		succession first sync then done;
+	}
+
+	analysis forked {
+		out r : Integer;
+		perform action tally : Tally;
+		return : Integer = r;
+	}
+}
+`, "analysis-choices")
+
+	resp := runAnalysis(t, srv, &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: "An::forked"})
+	if resp.Error != "" {
+		t.Fatalf("RunAnalysis reported %q", resp.Error)
+	}
+	choices := choiceDiagnostics(resp.Diagnostics)
+	want := []string{
+		"choice point: step 3: writes r := 11 by token 2, r := 10 by token 3 (unordered; r := 11 by token 2 stood)",
+		"choice point: step 3: tokens 2@left, 3@right (unordered; took 3@right first)",
+	}
+	if len(choices) != len(want) {
+		t.Fatalf("choice diagnostics = %v, want %d", resp.Diagnostics, len(want))
+	}
+	for i, d := range choices {
+		if d.Message != want[i] || d.Severity != "info" {
+			t.Errorf("diagnostic %d = %s %q, want info %q", i, d.Severity, d.Message, want[i])
+		}
+	}
+}
+
+// Two transitions out of one state enabled by one event are reported on the
+// state response; the first declared still fires.
+func TestExecuteState_ChoicePointDiagnostics(t *testing.T) {
+	srv := mustNewService(t, 10)
+
+	content := `
+package Test {
+  state Dispatcher {
+    attribute level : Integer = 8;
+    entry; then idle;
+    state idle;
+    state low;
+    state high;
+    transition first idle accept Go if level > 5 then low;
+    transition first idle accept Go if level > 7 then high;
+  }
+}
+`
+	parseResp, err := srv.ParseFile(context.Background(), &pb.ParseFileRequest{
+		Source:      &pb.ParseFileRequest_Content{Content: content},
+		ContentHash: "test-execute-state-choices",
+	})
+	if err != nil {
+		t.Fatalf("ParseFile failed: %v", err)
+	}
+
+	resp, err := srv.ExecuteState(context.Background(), &pb.ExecuteStateRequest{
+		ModelHash:            parseResp.ModelHash,
+		StateMachineSymbolId: "Test::Dispatcher",
+		Events:               []string{"Go"},
+	})
+	if err != nil {
+		t.Fatalf("ExecuteState failed: %v", err)
+	}
+	if resp.Error != "" {
+		t.Fatalf("execution error: %s", resp.Error)
+	}
+	if got := strings.Join(resp.StatesVisited, ","); got != "idle,low" {
+		t.Fatalf("states visited %q, want idle,low", got)
+	}
+	choices := choiceDiagnostics(resp.Diagnostics)
+	if len(choices) != 1 {
+		t.Fatalf("choice diagnostics = %v, want one", resp.Diagnostics)
+	}
+	want := "choice point: state idle on accept Go: transitions 1->low, 2->high (unordered; took 1->low)"
+	if choices[0].Message != want || choices[0].Severity != "info" {
+		t.Errorf("diagnostic = %s %q, want info %q", choices[0].Severity, choices[0].Message, want)
+	}
+}
+
+// A guard the run read only to report a choice and could not evaluate is an
+// informational diagnostic naming the decision, the branch and the failure; the
+// run itself is unchanged, and a first guard's failure still fails it.
+func TestExecuteAction_UnevaluableGuardDiagnostics(t *testing.T) {
+	srv := mustNewService(t, 10)
+
+	content := `
+package Test {
+  action route {
+    attribute level : Integer = 75;
+    attribute handler : Integer = 0;
+    first start;
+    then decide select;
+      if level > 50 then warn;
+      if 1 / (level - 75) > 0 then alarm;
+    action warn { assign handler := 1; }
+    then done;
+    action alarm { assign handler := 2; }
+    then done;
+  }
+  action broken {
+    attribute level : Integer = 75;
+    first start;
+    then decide select;
+      if 1 / (level - 75) > 0 then alarm;
+      if level > 50 then warn;
+    action warn;
+    then done;
+    action alarm;
+    then done;
+  }
+}
+`
+	parseResp, err := srv.ParseFile(context.Background(), &pb.ParseFileRequest{
+		Source:      &pb.ParseFileRequest_Content{Content: content},
+		ContentHash: "test-execute-action-unevaluable-guard",
+	})
+	if err != nil {
+		t.Fatalf("ParseFile failed: %v", err)
+	}
+
+	resp, err := srv.ExecuteAction(context.Background(), &pb.ExecuteActionRequest{
+		ModelHash:      parseResp.ModelHash,
+		ActionSymbolId: "Test::route",
+	})
+	if err != nil {
+		t.Fatalf("ExecuteAction failed: %v", err)
+	}
+	if resp.Error != "" {
+		t.Fatalf("execution error: %s", resp.Error)
+	}
+	if got := choiceDiagnostics(resp.Diagnostics); len(got) != 0 {
+		t.Errorf("an unevaluable guard was reported as a choice: %v", got)
+	}
+	var unevaluable []*pb.Diagnostic
+	for _, d := range resp.Diagnostics {
+		if strings.HasPrefix(d.Message, "guard not evaluable: ") {
+			unevaluable = append(unevaluable, d)
+		}
+	}
+	if len(unevaluable) != 1 {
+		t.Fatalf("unevaluable-guard diagnostics = %v, want one", resp.Diagnostics)
+	}
+	want := "guard not evaluable: step 2: decision select branch 2->alarm: division by zero (not selected)"
+	if unevaluable[0].Message != want || unevaluable[0].Severity != "info" {
+		t.Errorf("diagnostic = %s %q, want info %q", unevaluable[0].Severity, unevaluable[0].Message, want)
+	}
+	if unevaluable[0].Span == nil || unevaluable[0].Span.StartLine != 9 {
+		t.Errorf("diagnostic is not located at the guard: %v", unevaluable[0].Span)
+	}
+
+	resp, err = srv.ExecuteAction(context.Background(), &pb.ExecuteActionRequest{
+		ModelHash:      parseResp.ModelHash,
+		ActionSymbolId: "Test::broken",
+	})
+	if err != nil {
+		t.Fatalf("ExecuteAction failed: %v", err)
+	}
+	if !strings.Contains(resp.Error, "division by zero") {
+		t.Fatalf("error = %q, want the first guard's evaluation failure", resp.Error)
+	}
+	for _, d := range resp.Diagnostics {
+		if strings.HasPrefix(d.Message, "guard not evaluable: ") {
+			t.Errorf("the first guard's failure was reported as unevaluable: %q", d.Message)
+		}
+	}
+}
diff --git a/internal/grpc/convert.go b/internal/grpc/convert.go
index 09b4fd013..bb7ae42bf 100644
--- a/internal/grpc/convert.go
+++ b/internal/grpc/convert.go
@@ -93,6 +93,26 @@ func DiagnosticToProto(diag passes.Diagnostic, sf *source.SourceFile) *pb.Diagno
 	}
 }
 
+// RunNoteDiagnosticsToProto converts what a run noted about itself — its choice
+// points and the guards it could not evaluate — to informational diagnostics,
+// located in their model document; one outside the model carries no span.
+func RunNoteDiagnosticsToProto(notes []runtime.RunNote, model *CachedModel) []*pb.Diagnostic {
+	if len(notes) == 0 {
+		return nil
+	}
+	pbDiags := make([]*pb.Diagnostic, 0, len(notes))
+	for _, n := range notes {
+		diag := n.Diagnostic()
+		file, _ := n.Location()
+		if sf := model.document(file); sf != nil {
+			pbDiags = append(pbDiags, DiagnosticToProto(diag, sf))
+			continue
+		}
+		pbDiags = append(pbDiags, &pb.Diagnostic{Severity: diag.Severity.String(), Message: diag.Message})
+	}
+	return pbDiags
+}
+
 // ParserDiagnosticToProto converts a parser.Diagnostic to protobuf.
 func ParserDiagnosticToProto(diag parser.Diagnostic, sf *source.SourceFile) *pb.Diagnostic {
 	li := sf.Lines()
diff --git a/internal/grpc/service.go b/internal/grpc/service.go
index 699005caf..a2a3e68ee 100644
--- a/internal/grpc/service.go
+++ b/internal/grpc/service.go
@@ -734,9 +734,13 @@ func (s *Service) ExecuteAction(ctx context.Context, req *pb.ExecuteActionReques
 
 	// Execute action with the supplied inputs
 	outputs, err := runtimeCtx.ExecuteActionWithInputs(action, inputs)
+	// The choices the run made are reported with its outcome, failed or not: a
+	// failure may hang on the order taken.
+	diags := RunNoteDiagnosticsToProto(runtimeCtx.Notes(), cached)
 	if err != nil {
 		return &pb.ExecuteActionResponse{
-			Error: fmt.Sprintf("action execution failed: %v", err),
+			Error:       fmt.Sprintf("action execution failed: %v", err),
+			Diagnostics: diags,
 		}, nil
 	}
 
@@ -747,7 +751,8 @@ func (s *Service) ExecuteAction(ctx context.Context, req *pb.ExecuteActionReques
 	}
 
 	return &pb.ExecuteActionResponse{
-		Outputs: pbOutputs,
+		Outputs:     pbOutputs,
+		Diagnostics: diags,
 	}, nil
 }
 
@@ -775,9 +780,11 @@ func (s *Service) ExecuteState(ctx context.Context, req *pb.ExecuteStateRequest)
 	// Execute state machine, injecting the requested events and capturing the
 	// real ordered state-visit trace.
 	finalContext, statesVisited, err := runtimeCtx.ExecuteStateWithEvents(stateMachine, req.Events)
+	diags := RunNoteDiagnosticsToProto(runtimeCtx.Notes(), cached)
 	if err != nil {
 		return &pb.ExecuteStateResponse{
-			Error: fmt.Sprintf("state machine execution failed: %v", err),
+			Error:       fmt.Sprintf("state machine execution failed: %v", err),
+			Diagnostics: diags,
 		}, nil
 	}
 
@@ -790,6 +797,7 @@ func (s *Service) ExecuteState(ctx context.Context, req *pb.ExecuteStateRequest)
 	return &pb.ExecuteStateResponse{
 		StatesVisited: statesVisited,
 		FinalContext:  pbContext,
+		Diagnostics:   diags,
 	}, nil
 }
 
diff --git a/internal/repl/choice_test.go b/internal/repl/choice_test.go
new file mode 100644
index 000000000..051fa957e
--- /dev/null
+++ b/internal/repl/choice_test.go
@@ -0,0 +1,210 @@
+package repl
+
+import "testing"
+
+const choiceForkSource = `
+package Debug {
+	private import ScalarValues::*;
+	action tally {
+		attribute leftCount : Integer = 0;
+		attribute rightCount : Integer = 0;
+
+		first start;
+		fork split;
+		action left { assign leftCount := leftCount + 1; }
+		action right { assign rightCount := rightCount + 10; }
+		join sync;
+		done;
+
+		succession first start then split;
+		succession first split then left;
+		succession first split then right;
+		succession first left then sync;
+		succession first right then sync;
+		succession first sync then done;
+	}
+}
+`
+
+// A debugger step that picked among unordered tokens says so in one line, and
+// points at %trace when the choices themselves are not being shown.
+func TestStepReportsChoicePoints(t *testing.T) {
+	s := loadSource(t, choiceForkSource)
+	run(t, s, "%action tally")
+
+	// start -> split: one token, nothing to choose.
+	rejects(t, run(t, s, "%step"), "choice point")
+	// split forks: still one token acted.
+	rejects(t, run(t, s, "%step"), "choice point")
+	// left and right both act: the executor ordered them.
+	wants(t, run(t, s, "%step"), "✓ Step complete", "  1 choice point; %trace on to see them")
+}
+
+// With tracing on the choice is in the trace, so the summary drops the hint.
+func TestStepChoiceSummaryWithTraceOn(t *testing.T) {
+	s := loadSource(t, choiceForkSource)
+	run(t, s, "%trace on")
+	run(t, s, "%action tally")
+	run(t, s, "%step")
+	run(t, s, "%step")
+	out := run(t, s, "%step")
+	wants(t, out, "choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)", "  1 choice point")
+	rejects(t, out, "%trace on to see them")
+}
+
+// %continue counts the choices of the run it completed, and the plural form
+// when there were several.
+func TestContinueReportsChoicePoints(t *testing.T) {
+	s := loadSource(t, choiceForkSource)
+	run(t, s, "%action tally")
+	wants(t, run(t, s, "%continue"), "✓ Action completed", "  1 choice point; %trace on to see them")
+
+	s = loadSource(t, `
+package Debug {
+	private import ScalarValues::*;
+	action race {
+		attribute x : Integer = 0;
+		first start;
+		fork split;
+		action left { assign x := 1; }
+		action right { assign x := 2; }
+		join sync;
+		done;
+		succession first start then split;
+		succession first split then left;
+		succession first split then right;
+		succession first left then sync;
+		succession first right then sync;
+		succession first sync then done;
+	}
+}
+`)
+	run(t, s, "%action race")
+	wants(t, run(t, s, "%continue"), "✓ Action completed", "  2 choice points; %trace on to see them")
+}
+
+// A run that fails still reports the choices it made before failing, so the
+// error can be told from a scheduling artefact.
+func TestContinueReportsChoicePointsBeforeFailure(t *testing.T) {
+	s := loadSource(t, `
+package Debug {
+	private import ScalarValues::*;
+	action crash {
+		attribute x : Integer = 0;
+		attribute zero : Integer = 0;
+		first start;
+		fork split;
+		action left { assign x := 1; }
+		action right { assign x := 2; }
+		join sync;
+		action divide { assign x := x / zero; }
+		done;
+		succession first start then split;
+		succession first split then left;
+		succession first split then right;
+		succession first left then sync;
+		succession first right then sync;
+		succession first sync then divide;
+		succession first divide then done;
+	}
+}
+`)
+	run(t, s, "%action crash")
+	wants(t, run(t, s, "%continue"), "error: execution failed:", "  2 choice points; %trace on to see them")
+}
+
+// %advance on a state machine reports a transition conflict it dispatched
+// through; an event with one enabled transition reports none.
+func TestAdvanceReportsChoicePoints(t *testing.T) {
+	s := loadSource(t, `
+package Debug {
+	private import ScalarValues::*;
+	attribute def Go;
+	attribute def Stop;
+	state def Dispatcher {
+		attribute level : Integer = 8;
+		entry; then idle;
+		state idle;
+		state low;
+		state high;
+		state halted;
+		transition first idle accept Go if level > 5 then low;
+		transition first idle accept Go if level > 7 then high;
+		transition first low accept Stop then halted;
+	}
+	part def Router {
+		exhibit state dispatch : Dispatcher;
+	}
+	part router : Router;
+}
+`)
+	wants(t, run(t, s, "%instantiate router"), "✓ Created instance")
+	wants(t, run(t, s, "%state router"), "Current state: idle")
+	run(t, s, "%send Go")
+	wants(t, run(t, s, "%advance 1"), "Current state: low", "  1 choice point; %trace on to see them")
+	run(t, s, "%send Stop")
+	out := run(t, s, "%advance 1")
+	wants(t, out, "Current state: halted")
+	rejects(t, out, "choice point")
+}
+
+// A guard read only to report a choice that could not be evaluated is counted in
+// the summary line beside the choices, and shown in the trace when it is on.
+func TestStepReportsUnevaluableGuards(t *testing.T) {
+	src := `
+package Debug {
+	private import ScalarValues::*;
+	action route {
+		attribute level : Integer = 75;
+		attribute handler : Integer = 0;
+		first start;
+		then decide select;
+			if level > 50 then warn;
+			if 1 / (level - 75) > 0 then alarm;
+		action warn { assign handler := 1; }
+		then done;
+		action alarm { assign handler := 2; }
+		then done;
+	}
+	action mixed {
+		attribute level : Integer = 75;
+		attribute handler : Integer = 0;
+		first start;
+		then decide select;
+			if level > 50 then warn;
+			if level > 70 then alarm;
+			if 1 / (level - 75) > 0 then halt;
+		action warn { assign handler := 1; }
+		then done;
+		action alarm { assign handler := 2; }
+		then done;
+		action halt { assign handler := 3; }
+		then done;
+	}
+}
+`
+	s := loadSource(t, src)
+	run(t, s, "%action route")
+	rejects(t, run(t, s, "%step"), "guard not evaluable")
+	out := run(t, s, "%step")
+	wants(t, out, "✓ Step complete", "  1 guard not evaluable; %trace on to see them")
+	rejects(t, out, "choice point")
+
+	s = loadSource(t, src)
+	run(t, s, "%trace on")
+	run(t, s, "%action route")
+	run(t, s, "%step")
+	out = run(t, s, "%step")
+	wants(t, out,
+		"unevaluable guard step 2: decision select branch 2->alarm: division by zero (not selected)",
+		"  1 guard not evaluable")
+	rejects(t, out, "%trace on to see them")
+
+	s = loadSource(t, src)
+	run(t, s, "%action route")
+	wants(t, run(t, s, "%continue"), "✓ Action completed", "  1 guard not evaluable; %trace on to see them")
+
+	run(t, s, "%action mixed")
+	wants(t, run(t, s, "%continue"), "✓ Action completed",
+		"  1 choice point; 1 guard not evaluable; %trace on to see them")
+}
diff --git a/internal/repl/meta.go b/internal/repl/meta.go
index 42e2d8009..e5848521b 100644
--- a/internal/repl/meta.go
+++ b/internal/repl/meta.go
@@ -2305,9 +2305,11 @@ func (s *Session) doStep() ([]string, bool, error) {
 	}
 
 	// Step
+	noted := s.actionExec.rtCtx.NoteCount()
 	err := exec.Step()
 	if err != nil {
-		return []string{fmt.Sprintf("error: step failed: %v", err)}, false, nil
+		out := []string{fmt.Sprintf("error: step failed: %v", err)}
+		return append(out, s.noteSummary(s.actionExec.rtCtx, noted)...), false, nil
 	}
 
 	// Display state
@@ -2317,6 +2319,7 @@ func (s *Session) doStep() ([]string, bool, error) {
 		fmt.Sprintf("  State: %s", exec.State()),
 		fmt.Sprintf("  Tokens: %d", len(tokens)),
 	}
+	out = append(out, s.noteSummary(s.actionExec.rtCtx, noted)...)
 	if node := exec.PausedAt(); node != "" {
 		out = append(out, fmt.Sprintf("  ⏸ Paused at breakpoint %q", node))
 	}
@@ -2349,18 +2352,19 @@ func (s *Session) continueAction() ([]string, []NamedValue, error) {
 	}
 
 	// Run to completion, or to the first breakpoint hit
+	noted := s.actionExec.rtCtx.NoteCount()
 	if err := exec.RunToCompletion(); err != nil {
-		return nil, nil, fmt.Errorf("execution failed: %w", err)
+		return s.noteSummary(s.actionExec.rtCtx, noted), nil, fmt.Errorf("execution failed: %w", err)
 	}
 
 	if node := exec.PausedAt(); node != "" {
-		return []string{
+		out := []string{
 			fmt.Sprintf("⏸ Paused at breakpoint %q", node),
 			fmt.Sprintf("  State: %s", exec.State()),
 			fmt.Sprintf("  Tokens: %d", len(exec.Tokens())),
-			"",
-			"Use %tokens to inspect, %step or %continue to resume",
-		}, nil, nil
+		}
+		out = append(out, s.noteSummary(s.actionExec.rtCtx, noted)...)
+		return append(out, "", "Use %tokens to inspect, %step or %continue to resume"), nil, nil
 	}
 
 	// Display results
@@ -2368,6 +2372,7 @@ func (s *Session) continueAction() ([]string, []NamedValue, error) {
 		"✓ Action completed",
 		fmt.Sprintf("  Final state: %s", exec.State()),
 	}
+	out = append(out, s.noteSummary(s.actionExec.rtCtx, noted)...)
 	out = append(out, renderResults(s.actionExec.contextOf(), exec.Results())...)
 
 	return out, namedValues(s.actionExec.contextOf(), exec.Results()), nil
@@ -2862,16 +2867,19 @@ func (s *Session) stepState() ([]string, bool, error) {
 		return []string{fmt.Sprintf("✓ State machine %s (%s)", exec.State(), currentStateName(exec))}, false, nil
 	}
 
+	noted := s.stateExec.rtCtx.NoteCount()
 	step, err := s.stateStep(exec)
 	if err != nil {
-		return []string{errPrefix + err.Error()}, false, nil
+		out := []string{errPrefix + err.Error()}
+		return append(out, s.noteSummary(s.stateExec.rtCtx, noted)...), false, nil
 	}
-	return []string{
+	out := []string{
 		"✓ " + step,
 		fmt.Sprintf("  Current state: %s", currentStateName(exec)),
 		timeLabel + semantics.FormatReal(exec.CurrentTime()),
 		fmt.Sprintf("  Events: %d", exec.EventQueue().Len()),
-	}, false, nil
+	}
+	return append(out, s.noteSummary(s.stateExec.rtCtx, noted)...), false, nil
 }
 
 // stateStep performs one step and reports what it was.
@@ -3140,13 +3148,13 @@ func (s *Session) doAdvance(timeStr string) ([]string, bool, error) {
 	}
 	lines, err := s.advanceBy(duration)
 	if err != nil {
-		return []string{errPrefix + err.Error()}, false, nil
+		return append([]string{errPrefix + err.Error()}, lines...), false, nil
 	}
 	return lines, false, nil
 }
 
 // advanceBy advances simulation time by duration, reporting a failed event or do
-// behavior as an error.
+// behavior as an error alongside the choice summary of the steps taken before it.
 func (s *Session) advanceBy(duration float64) ([]string, error) {
 	if s.stateExec == nil {
 		return nil, s.noStateSessionErr()
@@ -3163,6 +3171,7 @@ func (s *Session) advanceBy(duration float64) ([]string, error) {
 	// same one the executors report.
 	maxEvents, maxDoActions := s.budgets.MaxStateEvents, s.budgets.MaxDoSteps
 	startTime := exec.CurrentTime()
+	noted := s.stateExec.rtCtx.NoteCount()
 	var processed, doActions int64
 	var dropped []string
 	for exec.State() == runtime.StateRunning &&
@@ -3170,7 +3179,7 @@ func (s *Session) advanceBy(duration float64) ([]string, error) {
 		// The poll comes first, and runs once more at quiescence, so a condition
 		// a do action has just made true is taken in this call.
 		if fired, err := exec.PollChangeEvents(); err != nil {
-			return nil, fmt.Errorf("change condition failed: %w", err)
+			return s.noteSummary(s.stateExec.rtCtx, noted), fmt.Errorf("change condition failed: %w", err)
 		} else if fired {
 			processed++
 			continue
@@ -3182,7 +3191,7 @@ func (s *Session) advanceBy(duration float64) ([]string, error) {
 		// the step RunToCompletion would take here.
 		if exec.HasPendingSignal() {
 			if err := exec.ProcessNextEvent(); err != nil {
-				return nil, fmt.Errorf("event processing failed: %w", err)
+				return s.noteSummary(s.stateExec.rtCtx, noted), fmt.Errorf("event processing failed: %w", err)
 			}
 			processed++
 			dropped = appendNote(dropped, droppedSignalNote(exec))
@@ -3196,7 +3205,7 @@ func (s *Session) advanceBy(duration float64) ([]string, error) {
 			}
 			ran, err := exec.RunDoRound()
 			if err != nil {
-				return nil, fmt.Errorf("do behavior failed: %w", err)
+				return s.noteSummary(s.stateExec.rtCtx, noted), fmt.Errorf("do behavior failed: %w", err)
 			}
 			if ran == 0 {
 				break
@@ -3205,7 +3214,7 @@ func (s *Session) advanceBy(duration float64) ([]string, error) {
 			continue
 		}
 		if err := exec.ProcessNextEvent(); err != nil {
-			return nil, fmt.Errorf("event processing failed: %w", err)
+			return s.noteSummary(s.stateExec.rtCtx, noted), fmt.Errorf("event processing failed: %w", err)
 		}
 		processed++
 		dropped = appendNote(dropped, droppedSignalNote(exec))
@@ -3228,6 +3237,7 @@ func (s *Session) advanceBy(duration float64) ([]string, error) {
 		"  Last event at: " + semantics.FormatReal(exec.CurrentTime()),
 		fmt.Sprintf("  Remaining events: %d", exec.EventQueue().Len()),
 	}
+	out = append(out, s.noteSummary(s.stateExec.rtCtx, noted)...)
 
 	if doActions > 0 {
 		out = append(out, fmt.Sprintf("  Do behavior actions run: %d", doActions))
diff --git a/internal/repl/run.go b/internal/repl/run.go
index 48d956e42..ae2420344 100644
--- a/internal/repl/run.go
+++ b/internal/repl/run.go
@@ -42,10 +42,10 @@ func namedValues(ctx *runtime.Context, results map[string]runtime.Value) []Named
 }
 
 // errorLines adapts a command that reports its failures as errors to the
-// prompt, which prints them as output.
+// prompt, which prints them as output ahead of any lines the failed run left.
 func errorLines(lines []string, _ []NamedValue, err error) ([]string, bool, error) {
 	if err != nil {
-		return []string{"error: " + err.Error()}, false, nil
+		return append([]string{"error: " + err.Error()}, lines...), false, nil
 	}
 	return lines, false, nil
 }
diff --git a/internal/repl/trace.go b/internal/repl/trace.go
index bd7cf9afc..8e505ded5 100644
--- a/internal/repl/trace.go
+++ b/internal/repl/trace.go
@@ -1,6 +1,42 @@
 package repl
 
-import "github.com/Open-MBEE/OpenSysML/internal/core/runtime"
+import (
+	"fmt"
+	"strings"
+
+	"github.com/Open-MBEE/OpenSysML/internal/core/runtime"
+)
+
+// noteSummary is the line a debugger command adds when the steps it ran noted
+// choice points or guards it could not evaluate beyond the before notes it
+// started with: how many of each, and how to see them.
+func (s *Session) noteSummary(ctx *runtime.Context, before int) []string {
+	notes := ctx.Notes()
+	if before >= len(notes) {
+		return nil
+	}
+	var choices, unevaluable int
+	for _, n := range notes[before:] {
+		switch n.(type) {
+		case runtime.ChoicePoint:
+			choices++
+		case runtime.UnevaluableGuard:
+			unevaluable++
+		}
+	}
+	var parts []string
+	if choices > 0 {
+		parts = append(parts, fmt.Sprintf("%d %s", choices, plural(choices, "choice point", "choice points")))
+	}
+	if unevaluable > 0 {
+		parts = append(parts, fmt.Sprintf("%d %s", unevaluable, plural(unevaluable, "guard not evaluable", "guards not evaluable")))
+	}
+	line := "  " + strings.Join(parts, "; ")
+	if s.trace == nil {
+		line += "; %trace on to see them"
+	}
+	return []string{line}
+}
 
 // tracePrefix marks a recorded execution step, so a trace is distinguishable
 // from a command's own output.