fix(runtime): report transition choices only for the transition that fires

Transition choice and guard-unevaluable notes ride on the dispatch candidate and are recorded when it fires, so a transition several regions select through their enclosing state is one choice and a composite state's transitions outranked by a nested one report nothing. An action step that fails after a token already went still records the order it took, including the failing token.

Co-Authored-By: jason.han <hanhuijun@gmail.com>

Author: devin-ai-integration[bot]

docs/project/behavior-semantic-oracle.md

@@ -284,7 +284,11 @@ Derived constraints:
 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.
+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,

docs/project/spec-compliance.md

@@ -776,8 +776,10 @@ time it is entered, so a state entered twice appears twice. `diagnostics` carrie
 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; a transition on a substate
-beating one on the state enclosing it is spec-defined order and is not reported. For `state def Hub { entry;
+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:
 

docs/reference/wire-contract.md

@@ -145,16 +145,15 @@ func (e *ActionExecutor) beginStepOrder() stepOrder {
 
 // 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).
+// 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)
-	if err := e.stepToken(i); err != nil {
-		return err
-	}
-	if order.eligible(before) && e.tokenActed(before, count) {
+	err := e.stepToken(i)
+	if order.eligible(before) && (err != nil || e.tokenActed(before, count)) {
 		order.acted = append(order.acted, before)
 	}
-	return nil
+	return err
 }
 
 // eligible reports whether the token could have gone first in the step and is

internal/core/runtime/action_choice.go

@@ -242,12 +242,6 @@ 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.
@@ -258,32 +252,13 @@ func (e *ActionExecutor) Step() error {
 	order := e.beginStepOrder()
 	defer e.beginStepWrites(e.stepCount + 1)()
 
-	// 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
-		}
-
-		if err := e.stepTokenNoting(i, &order); 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.stepTokenNoting(i, &order); err != nil {
-				e.endPausedBodies()
-				return err
-			}
-		}
-	}
+	err := e.stepTokens(len(e.tokens), paused, &order)
+	// The order the tokens took is a fact of the step whether or not it failed.
 	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
 	// went on.
@@ -1122,6 +1097,33 @@ func (e *ActionExecutor) probeGuard(frame *actionFrame, node *ast.DecisionNode,
 	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]

internal/core/runtime/action_executor.go

@@ -102,15 +102,17 @@ func (e *ActionExecutor) stepSubflow(perf *actionFrame) (bool, error) {
 	defer e.beginSweep()()
 	order := e.beginStepOrder()
 	defer e.beginStepWrites(e.stepCount + 1)()
-	for i := len(e.tokens) - 1; i >= 0; i-- {
+	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.stepTokenNoting(i, &order); err != nil {
-			return false, err
-		}
+		err = e.stepTokenNoting(i, &order)
 	}
 	e.noteTokenOrder(e.stepCount+1, order)
+	if err != nil {
+		return false, err
+	}
 	after := e.subflowLocations(perf)
 	if len(after) != len(before) {
 		return true, nil

internal/core/runtime/action_subflow.go

@@ -180,6 +180,13 @@ 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) {

internal/core/runtime/choice.go

@@ -380,6 +380,135 @@ func TestAncestorPriorityIsNotAChoice(t *testing.T) {
 	}
 }
 
+// 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)
+	}
+}
+
 // 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.

internal/core/runtime/choice_test.go

@@ -58,8 +58,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, err := e.risenChangeTransition(state, poll)
+		return trans, nil, err
 	})
 	if err != nil {
 		e.changeWaits = poll.waits