From a69b891b760877666f0706f69c2929cfe203aa88 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 8 Sep 2026 05:25:07 +0000 Subject: [PATCH 1/7] feat(runtime): report execution choice points Record a choice point wherever an executor picks among alternatives the Kernel Semantic Library leaves unordered: several tokens advancing in one action step, a decision node with several holding guards, two tokens writing one feature in one step, and several transitions out of one state enabled by one event. Scheduling is unchanged (reverse token order, first holding guard, first enabled transition); the pick is now reported as a choice trace line, an informational diagnostic on ExecuteAction, ExecuteState and RunAnalysis responses, and a summary line after the REPL's %step, %continue and %advance. Ancestor-priority transition selection is ordered by the specification and is not reported. Decision nodes now evaluate every guarded succession, so traces of decisions whose first guard held gain the evaluations of the later guards. Co-Authored-By: jason.han --- .../execution-choice-points.added.md | 12 + docs/guide/06-behavior.md | 15 ++ docs/project/behavior-semantic-oracle.md | 67 +++++- docs/project/spec-compliance.md | 6 +- docs/reference/cli.md | 2 +- docs/reference/repl-commands.md | 2 +- docs/reference/wire-contract.md | 34 ++- internal/core/runtime/action_choice.go | 202 ++++++++++++++++ internal/core/runtime/action_executor.go | 23 +- internal/core/runtime/action_frame.go | 12 +- internal/core/runtime/action_subflow.go | 5 +- internal/core/runtime/choice.go | 125 ++++++++++ internal/core/runtime/choice_test.go | 220 ++++++++++++++++++ internal/core/runtime/context.go | 4 + internal/core/runtime/robustness_test.go | 49 ++++ internal/core/runtime/state_executor.go | 46 +++- ...accept_suspends_until_message.trace.golden | 1 + .../action_accept_two_waiters.trace.golden | 1 + ...block_flow_if_branch_own_flow.trace.golden | 1 + ..._decision_overlapping_guards.expected.json | 19 ++ ...n_choice_decision_overlapping_guards.sysml | 23 ++ ...e_decision_overlapping_guards.trace.golden | 13 ++ ...tion_choice_fork_token_order.expected.json | 8 + .../action_choice_fork_token_order.sysml | 26 +++ ...ction_choice_fork_token_order.trace.golden | 14 ++ ...action_choice_fork_token_order.trace.order | 6 + ...ice_same_step_write_conflict.expected.json | 21 ++ ...tion_choice_same_step_write_conflict.sysml | 26 +++ ...oice_same_step_write_conflict.trace.golden | 15 ++ ...explicit_succession_fork_join.trace.golden | 1 + ..._fork_branches_share_features.trace.golden | 1 + ...rk_branches_write_one_feature.trace.golden | 2 + ...token_per_incoming_succession.trace.golden | 2 + ...on_join_same_succession_twice.trace.golden | 13 ++ ...oin_three_two_arrive_together.trace.golden | 2 + ...join_waits_for_slowest_branch.trace.golden | 2 + ...on_merge_fork_branch_and_loop.trace.golden | 13 ++ .../action_merge_loop_reenters.trace.golden | 6 + ...ction_merge_loop_three_passes.trace.golden | 6 + ...tion_nested_flow_in_fork_join.trace.golden | 2 + ...o_successions_per_performance.trace.golden | 3 + ...de_concurrent_nested_bindings.trace.golden | 1 + ..._node_concurrent_performances.trace.golden | 1 + ...ion_node_loop_back_reperforms.trace.golden | 6 + ...ncoming_successions_runs_once.trace.golden | 1 + ..._merge_body_runs_on_traversal.trace.golden | 1 + ...cestor_priority_not_reported.expected.json | 11 + ...hoice_ancestor_priority_not_reported.sysml | 25 ++ ...ncestor_priority_not_reported.trace.golden | 11 + ...e_choice_transition_conflict.expected.json | 24 ++ .../state_choice_transition_conflict.sysml | 22 ++ ...te_choice_transition_conflict.trace.golden | 15 ++ ...w7d_send_via_port_to_receiver.trace.golden | 2 + internal/core/runtime/trace.go | 9 + internal/grpc/analysis.go | 8 +- internal/grpc/cache.go | 13 ++ internal/grpc/choice_test.go | 205 ++++++++++++++++ internal/grpc/convert.go | 18 ++ internal/grpc/service.go | 14 +- internal/repl/choice_test.go | 119 ++++++++++ internal/repl/meta.go | 20 +- internal/repl/trace.go | 23 +- 62 files changed, 1567 insertions(+), 33 deletions(-) create mode 100644 changes/unreleased/execution-choice-points.added.md create mode 100644 internal/core/runtime/action_choice.go create mode 100644 internal/core/runtime/choice.go create mode 100644 internal/core/runtime/choice_test.go create mode 100644 internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.expected.json create mode 100644 internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.sysml create mode 100644 internal/core/runtime/testdata/conformance/action_choice_decision_overlapping_guards.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/action_choice_fork_token_order.expected.json create mode 100644 internal/core/runtime/testdata/conformance/action_choice_fork_token_order.sysml create mode 100644 internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/action_choice_fork_token_order.trace.order create mode 100644 internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.expected.json create mode 100644 internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.sysml create mode 100644 internal/core/runtime/testdata/conformance/action_choice_same_step_write_conflict.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_choice_ancestor_priority_not_reported.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_choice_transition_conflict.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_choice_transition_conflict.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_choice_transition_conflict.trace.golden create mode 100644 internal/grpc/choice_test.go create mode 100644 internal/repl/choice_test.go diff --git a/changes/unreleased/execution-choice-points.added.md b/changes/unreleased/execution-choice-points.added.md new file mode 100644 index 000000000..45389b388 --- /dev/null +++ b/changes/unreleased/execution-choice-points.added.md @@ -0,0 +1,12 @@ +- **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, and two 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 is the same; a decision node now evaluates every + guard rather than stopping at the first that holds, so a trace of one with several guards shows + the later guards being evaluated. 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..97d6df7fa 100644 --- a/docs/guide/06-behavior.md +++ b/docs/guide/06-behavior.md @@ -187,6 +187,21 @@ the state or the data a guard reads changes between the send and the dispatch, t - `%advance