fix(runtime): perform every target of several successions out of an ordinary action node

[devin-ai-integration]

What and why

An action body such as action a; first start then a; succession a then done; succession a then b; action b; failed with "more than one succession is enabled: action node a has multiple successors". An action node, a statement node (if, while, loop, for, assign, send), the start node and a [0] step now follow every enabled succession out of them. The token splits as a fork's does (follow/split in action_executor.go, which stepForkNode now shares), after the node's data flows have been applied once. Branch tokens are appended in declaration order. ErrAmbiguousSuccession had no remaining producer, so it is removed.

Policy choices:

• Decision: unchanged. It takes exactly one branch, the first declared, and records it as a choice.
• Join and merge: both keep refusing several outgoing successions. For the join this follows validateJoinNodeOutgoingSuccessions. For the merge it follows validateMergeNodeOutgoingSuccessions (SysML v2 §8.3.17, already enforced statically as merge-outgoing-successions). MergeAction's library text constrains only incoming links, but the validation constraint bounds outgoing ones, and TestControlNodeStaticRuleAgreesWithRuntime pins the runtime to that static rule. A robustness case now covers this refusal.
• Rejoin at a plain node: this is the existing synchronize rule. A plain node that several successions reach is one performance after every succession that can still deliver. A pruned link never delivers, so the node runs once on the surviving branch. This is how a fork with a pruned branch into a plain node already behaved. A join instead awaits every declared incoming succession, so a pruned branch into a join deadlocks (ErrActionDeadlock).
• Repeated source a[3]: the strict end-multiplicity policy is kept. A plain then out of it is still refused, and written end multiplicities on each edge work. A [0] source forwards to every successor.
• Scheduling: the branches are unordered, as a fork's are. -schedule reverse and explore/-engine check reach both writes of a shared feature (x = 1, x = 2).
• SMT: a non-decision node with several outgoing edges takes the existing fork encoding (Flow.fansOut, tokenStep.fork). sizeSlots counts every fan-out, and Cyclic covers a fan-out on a cycle. A plain node that fan-out branches rejoin at would need an implicit join, which the encoding does not cover. That case gets the precise UnsupportedError{Construct: "implicit join"} refusal. The encoding never follows just one branch.
• gRPC gateOf: unchanged. It looks for the unique decision that gates a path. A node with several edges is a fan-out, not a gate, so stopping there is still correct.
• SysML v1 migrator: unchanged. The explicit fork it inserts for a UML implicit fork is now equivalent to native fan-out when the source is an action. It is still required when the source is a merge or join, whose outgoing bound would otherwise be violated, so keeping it is the uniform, correct choice.

Specification basis

• A succession is a connector typed by Occurrences::HappensBefore. It orders its source performance completely before its target performance, and it does not select or exclude a target. A step with no written multiplicity is one performance (Actions::Action.subactions : Action[0..*]). So two successions out of a mean both targets are performed after a, unordered relative to each other.
• Actions::ForkAction "has no inherent behavior". A fork only requires the 1..1 target multiplicity that an ordinary node's successions leave unwritten.
• Only DecisionAction/DecisionPerformance says "exactly one of the Successions" (ControlPerformances.kerml).
• A guarded succession out of a non-decision node is a NonStateTransitionPerformance (Actions::DecisionTransitionAction). Its guard constrains its own transitionLink : HappensBefore[0..1], and nothing makes the guards exclusive. So every holding guard is followed, and a false guard prunes only its own link.

The compliance map gains a row for ordinary-node fan-out (✅ Faithful). The fork row and the guarded-succession row no longer say that two holding guards are reported. behavior-semantic-oracle.md gains the section "Several successions out of an ordinary action node: every target follows, in which order is open".

Pre-existing expectations changed

All three of these asserted that two holding guards out of an ordinary node are an error because "which one wins is not stated". Under the derivation above, nothing has to win: both links exist.

• conformance/action_succession_guard_two_hold: was the error has multiple successors, now level = 12, low = 1, high = 1. The derivation is in the fixture comment, and a trace golden was added.
• action_executor_test.go TestActionExecutor_GuardedSuccession_TwoGuardsHold: now asserts one token at each target.
• robustness_test.go, "two guards hold at once" and the first-node two-successions case: both now expect both branch outputs instead of the ambiguity error.
• robustness_object_flow_test.go guarded_branches_with_object_flows_stay_ambiguous (from develop): renamed guarded_branches_with_object_flows_both_follow; two holding guards out of produce now run both targets instead of ErrAmbiguousSuccession, for the same reason.
• Trace goldens object_flow_implicit_fork and object_flow_queued_value_control_arrival (from develop): token IDs only. develop kept the source token on the first succession flow; this PR gives every branch a fresh token, as an explicit fork does and as the SMT encoding counts, so the branches read token 2, token 3 instead of token 1, token 2. Steps, statements and outcomes are unchanged.
• develop's ambiguousSuccession/advance and SMT Flow.checkSuccessors (which allowed fan-out only along succession flows) are replaced by follow and Flow.fansOut; their compliance row and the migrate-object-flows changelog fragment no longer say two plain successions are ambiguous.

How it was verified

New tests:

• Conformance fixtures, each with a trace golden:
  • action_succession_fan_out_rejoin (with .trace.order)
  • _guard_pruned_rejoin
  • _data_flows
  • _statement_node
  • _from_start
  • _writes_one_feature: both outcomes, plus .check.expected.json, .declared and .seed-1 goldens and .trace.order
  • action_step_multiplicity_fan_out
  • _fan_out_plain (refused)
  • _zero_fan_out
• TestStatementNodeFanOut, covering assign, if, while, loop, for and send.
• robustness_succession_fan_out_test.go TestRuntimeRobustnessSuccessionFanOut, covering:
  • a pruned branch into a deadlocking join
  • a guard that cannot be evaluated on one link
  • a fan-out in a loop that spends the budget
  • a self-loop fan-out that spends the budget
  • a merge with two outgoing successions
• action_succession_fan_out_one_guard_holds and action_fork_one_branch_beside_live_token, each with .check.expected.json. They pin the SMT token identity: an ordinary node with one enabled succession keeps its token, and a fork with one branch replaces it. The SMT referee replays both witnesses of each. In the first, q writes x := 3 behind a false guard, so an engine that ignored the guard would reach an outcome the set does not admit.
• TestEncodeFanOutJoinCompletes and TestEncodeFanOutPlainRejoinRefused (SMT).

A case may now state "solverBudget": {"moves": N} beside outcomes. The SMT referee then encodes the case to N moves instead of the default 40. The conformance schema check rejects a budget stated without outcomes or with fewer than 1 move, and the conformance README documents it. action_succession_fan_out_one_guard_holds states 20 moves: every run ends within 12. At 40 moves, z3 takes about a minute locally to show that every schedule ends (unsat). On CI that ran past the referee's five-minute timeout. An explicit-fork rewrite of the same model times out at 40 moves even locally, so the cost comes from the fork encoding, not from the fan-out. The completion query still proves that every run ends within the bound.

• Parser golden action_succession_fan_out.

Gates run locally:

• go build ./..., go vet ./... and gofmt -l . (empty).
• go test ./...
• make lint, make docs-check and python3 scripts/changelog.py check.
• go test -race on internal/exec/runtime, internal/exec/smt and tests/parser.
• The four corpus gates, with the corpora downloaded and the OPENSYSML_REQUIRE_* variables set. training_examples_expected.txt is untouched.

Checklist

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

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

[devin-ai-integration]

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

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

End-to-end CLI check on 3556c2c56, compared with develop at ceaf5ea55: the explicit-succession repro now completes, where develop refused it with "multiple successors".

Develop	This PR

• Guards: when both guards hold, both branches run (low=1, high=1). A false guard prunes only its own link.
• Rejoin: a plain node where the branches rejoin runs once. A pruned branch into a join reports a deadlock promptly, without hanging.
• Scheduling: -schedule declared gives x=2 and -schedule reverse gives x=1. explore, -engine check and SMT -check-diverge x each report both values. SMT refuses a plain-node rejoin as implicit join.
• Kept restrictions: a merge or join with two outgoing successions is refused. A decision still takes one branch. A self-loop fan-out stops at the step budget. a[3] followed by plain then successions is still refused.
• Other cases: fan-out from the start node, from an if node and from a [0] step gives the expected values. So do explicit repeated-step multiplicities, and data flows: the source runs once and both targets receive the value.

Limits of this check: only the if statement node was driven through the CLI; TestStatementNodeFanOut covers the others. Typed-error identity cannot be observed from the CLI. The merge/join refusals are reported by static validation before the runtime runs.

[devin-ai-integration]

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

• internal/exec/runtime/action_executor.go (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)

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

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

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

[devin-ai-integration]

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