diff --git a/.agents/skills/testing-sysml-repl/SKILL.md b/.agents/skills/testing-sysml-repl/SKILL.md
index d4c67287d1..86a1d931ec 100644
--- a/.agents/skills/testing-sysml-repl/SKILL.md
+++ b/.agents/skills/testing-sysml-repl/SKILL.md
@@ -1151,6 +1151,27 @@ changes:
   `unresolved reference: n`; the CLI has **no** flag for action inputs, so exercise `in`/`out`
   parameters by having a caller action invoke `action call = Callee(a = 3, b = 4);`.
 
+## Action fan-out CLI checks
+
+- Use explicit succession syntax in minimal repros: `succession a then done;`
+  or `first a then done;`. A bare `a then done;` inside an action body can be
+  rejected as `expected a body member` before execution; do not mistake that
+  diagnostic for a runtime fan-out refusal.
+- The default scheduler is `reverse`, not `declared`. Compare explicit
+  `-schedule declared` with `-schedule reverse`; a no-flag run normally agrees
+  with reverse.
+- `-engine smt -action <name>` asks whether execution holds, not for the table
+  of final values. Use `-engine smt -action <name> -check-diverge <feature>` to
+  request two witnessed final values. `-engine check` and `-schedule explore`
+  expose outcomes directly. SMT may explicitly refuse an implicit join at a
+  plain node, whereas the runtime supports it; use an explicit join for a
+  cross-engine scheduling comparison.
+- Bound adversarial loops with `OPENSYSML_MAX_ACTION_STEPS=200`, and wrap the
+  command with `timeout 30`. Assert the step-limit diagnostic and exit 2,
+  not watchdog exit 124. Report CLI diagnostics separately from Go error
+  identity: the CLI does not expose `errors.Is`, and static merge/join
+  validation may prevent reaching the runtime guard.
+
 ## Control flow inside an action node body
 
 `while`, `loop … until` (braced and unbraced), `for … in` and `if`/`else` execute inside an
@@ -4139,10 +4160,10 @@ Traps and recipes:
 - Error wordings to assert: non-Boolean guard →
   `error: execution failed: type mismatch: node s1: guard must evaluate to boolean, got constant`;
   unresolvable name in a guard → `error: execution failed: eval guard of node s1: unresolved
-  reference: nosuch`. Two guards out of one action node that both hold →
-  `error: execution failed: more than one succession is enabled: action node check has multiple
-  successors` (wraps the `ErrAmbiguousSuccession` sentinel; the run stops with the token still on the
-  node and neither branch's attribute written — assert that with `%tokens`, not just the message).
+  reference: nosuch`. Two guards out of one ordinary action node that both hold are no error: each
+  succession is its own `HappensBefore` link, so the token splits as a fork's does and both branch
+  attributes are written (assert both in `Results:`). Only a `decide` node picks one of several
+  holding guards; a `join` or `merge` with two outgoing successions is still refused.
 - Places a guard could still be silently ignored, all worth a one-liner fixture: succession out of a
   real initial node (`then start s1 if …;`), out of a `merge`, out of a `join` (must not deadlock —
   the branch tokens are consumed either way), and one whose target is `done`.
diff --git a/changes/unreleased/migrate-object-flows.added.md b/changes/unreleased/migrate-object-flows.added.md
index 8d61a1f607..070a393d9a 100644
--- a/changes/unreleased/migrate-object-flows.added.md
+++ b/changes/unreleased/migrate-object-flows.added.md
@@ -1,3 +1,3 @@
 - **The SysML v1 migrator writes object flows as succession flows.** An object flow between two actions is `succession flow of T from a.out to b.in`, which orders the actions and carries the value when the source completes; a guarded one is OMG's guarded succession to the flow itself, `first a if g then f; succession flow f of T from a.out to b.in;`, so a false guard moves no value, a guard of literal `true` is no guard, and a flow into a «stream» parameter stays a `flow`. A flow into or out of a fork, join or merge names the node's `inputObjectN`/`outputObjectN` features instead of being rerouted between pins, and an action several object flows reach waits for them without a synthesized join. Edge weights, all UML's default in the measured models, are not written.
-- **Values pass through forks, joins and merges, and several succession flows may leave one action.** A control node holds what a flow delivers to its input features and passes it on when a token reaches it: a fork copies it to every branch, a join gathers one value of each input, a merge passes on the one that arrived. Each succession flow leaving an action starts its target beside the action's other succession, as after a fork; two plain successions still stop the run as ambiguous.
+- **Values pass through forks, joins and merges, and several succession flows may leave one action.** A control node holds what a flow delivers to its input features and passes it on when a token reaches it: a fork copies it to every branch, a join gathers one value of each input, a merge passes on the one that arrived. Each succession flow leaving an action starts its target beside the action's other successions, as after a fork.
 - **A succession may lead to a succession flow.** `first a if g then f; succession flow f from a.y to b.v;` gates the flow on the guard: the runtime and the model checker move the value and order `b` only when `g` holds, so a false guard leaves `b` waiting for that pin (or running on another path's value) rather than on the rejected one. The model form records the guarded succession as the `gate` of the edge and the flow, and action views draw it at its own declaration.
diff --git a/changes/unreleased/succession-fan-out.fixed.md b/changes/unreleased/succession-fan-out.fixed.md
new file mode 100644
index 0000000000..ac47cad009
--- /dev/null
+++ b/changes/unreleased/succession-fan-out.fixed.md
@@ -0,0 +1,10 @@
+- **Every target of several successions out of an ordinary action node is performed.** A
+  succession is a `HappensBefore` link that orders its source before its target and excludes no
+  other target, so `first a then b; first a then c;` now performs both `b` and `c` after `a`,
+  unordered relative to each other, as a fork would; a guarded succession whose guard is false
+  leaves out only its own link, and two holding guards out of a non-decision node follow both
+  instead of failing with "more than one succession is enabled". The same holds for statement
+  nodes (`if`, `while`, `loop`, `for`, `assign`, `send`), the start node and a `[0]` step. Only a
+  `decide` node chooses one branch; a `join` or `merge` with several outgoing successions is still
+  refused, as their validation constraints require, and a repeated step still needs written end
+  multiplicities on each edge out of it. The `smt` engine encodes the fan-out as it encodes a fork.
diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md
index b4f0445811..eded275a9d 100644
--- a/docs/project/behavior-semantic-oracle.md
+++ b/docs/project/behavior-semantic-oracle.md
@@ -358,6 +358,80 @@ 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`).
 
+### Several successions out of an ordinary action node: every target follows, in which order is open
+
+Fixture: `action_succession_fan_out_writes_one_feature` (golden, with `.declared` and `.seed-1`
+goldens); companions `action_succession_fan_out_rejoin`,
+`action_succession_fan_out_guard_pruned_rejoin`, `action_succession_fan_out_data_flows`,
+`action_succession_fan_out_statement_node`, `action_succession_fan_out_from_start`,
+`action_succession_guard_two_hold`, `action_step_multiplicity_fan_out`,
+`action_step_multiplicity_fan_out_plain` and `action_step_multiplicity_zero_fan_out`.
+
+```
+start → split ─→ left  { x := 1; leftRan := true  } ─┐
+              ─→ right { x := 2; rightRan := true } ─┤→ sync → done
+```
+
+`split` is a plain action node, not a fork.
+
+Derived constraints:
+
+- Each of `first split then left` and `first split then right` is a connector typed by
+  `HappensBefore`: it orders the one performance of `split` completely before its target's
+  performance and says nothing else. Neither link selects or excludes the other, and `left` and
+  `right` each declare no multiplicity, so each is one performance after `split`. The library
+  makes outgoing successions exclusive only for a decision (`DecisionPerformance`: "exactly one
+  of the Successions"); a fork adds only the `1..1` target multiplicity an ordinary node's
+  successions leave unwritten, which for an unrepeated target is the one performance it has
+  anyway. So `leftRan` and `rightRan` both end `true`, and `x` is `1` or `2`.
+- A guarded succession out of a non-decision node is a `NonStateTransitionPerformance` whose
+  guard constrains its own `transitionLink : HappensBefore[0..1]`; nothing relates the guards of
+  two such links. Every succession whose guard holds is followed (`action_succession_guard_two_hold`:
+  `low = 1`, `high = 1`), and a false guard leaves out only its own link
+  (`action_succession_fan_out_guard_pruned_rejoin`: `bRan = false`, `cRan = true`).
+- A node both branches reach declares no multiplicity, so it is one performance after every
+  succession that delivers to it (`action_succession_fan_out_rejoin`: `hits = 1`). Behind a
+  pruned link it awaits only what can still reach it, exactly as behind a fork branch a guard
+  pruned (`action_succession_guard_fork_branch_pruned`) or a decision branch not taken; see
+  [A node without multiplicity reached over two successions is performed once, after
+  both](#a-node-without-multiplicity-reached-over-two-successions-is-performed-once-after-both).
+  A join is the exception it always was: it awaits every incoming succession, so a pruned
+  branch into a join deadlocks.
+- `split` is one performance, so the flows out of it are its one set of outputs: they are moved
+  once, before its successors start, and each reaches its own target's pin
+  (`action_succession_fan_out_data_flows`: `runs = 1`, `got = 21`, `doubled = 42`).
+- A repeated step keeps its count rule: each edge out of `a[3]` must state its ends
+  (`succession first [*] a then [1] q;`), and fanning out to two targets is two such edges
+  (`action_step_multiplicity_fan_out`). A plain `then` out of it stays refused
+  (`action_step_multiplicity_fan_out_plain`). A `[0]` step is no performance and both of its
+  successors run (`action_step_multiplicity_zero_fan_out`).
+
+Two control nodes keep a bound on their outgoing side that the static rules state:
+`validateJoinNodeOutgoingSuccessions` and `validateMergeNodeOutgoingSuccessions` each allow at
+most one outgoing succession, so a join or a merge with two is an ill-formed model, reported by
+`join-outgoing-successions` and `merge-outgoing-successions` and refused by the executor
+(`ErrInvalidActionFlow`). `Actions::MergeAction` on its own constrains only the incoming side;
+the outgoing bound is the validation constraint's, not the library's.
+
+Open: the order of `left` against `right`, and so which write of `x` stands — the same openness
+as [Concurrent branches writing one feature: the value is open, the writes are
+not](#concurrent-branches-writing-one-feature-the-value-is-open-the-writes-are-not).
+
+Pinned outcome: the admissible set `{x = 1, x = 2}`, with `leftRan = true` and `rightRan = true`
+in both, stated as `outcomes` citing this section; the `.trace.order` constraints are
+`split < left`, `split < right`, `left < sync`, `right < sync`. Exploration reaches both outcomes
+and no other, one linearization each (2 runs, 2 outcomes, complete), and the exhaustive checker
+finds `x` divergent between `1` and `2`.
+
+Executor: a token leaving an ordinary node, a statement node or the start node along several
+enabled successions splits as a fork's does — one fresh token per succession, appended in
+succession-declaration order — so the scheduling conventions above carry over unchanged: under
+`declared` the last-declared branch is appended last and `right` writes last (`x = 2`); the
+default `reverse` policy steps it first (`x = 1`). The guards out of the node are all evaluated
+before the token leaves, so a guard that cannot be evaluated fails the step before any branch
+starts. The SMT encoding gives the node the fork's encoding (one slot per enabled succession);
+a plain node several tokens may reach together stays refused there as an implicit join.
+
 ### A decision with several holding guards: exactly one branch follows, which one is open
 
 Fixture: `action_choice_decision_overlapping_guards` (golden).
diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md
index 4545d26842..c4117d90f7 100644
--- a/docs/project/spec-compliance.md
+++ b/docs/project/spec-compliance.md
@@ -745,12 +745,13 @@ remain one-shot.
 | An action's result parameter inherited from a function it specializes (a calc, case or use case def — KerML §7.4.7.2, §8.3.4.7.8; SysML §7.17.2, §7.19.2) is an output parameter the body writes and a performer reads; only a `return` whose owner is no function or expression (KerML `validateReturnParameterMembershipOwningType`) is refused with `ErrActionResultParameter` | `semantics/return_parameter.go` `ResultParameterOwnerValid`, `DeclaresFunction`; `runtime/action_subflow.go` `checkResultParameters`, `checkNodeResultParameters`; `passes/return_parameter.go` `checkReturnParameterOwner` | `action_result_inherited_from_calc_def`, `action_result_inherited_from_use_case_def`, `action_result_inherited_from_use_case_library_result`, `action_result_read_by_performer`; `robustness_action_result_parameter_test.go:TestRuntimeRobustnessActionResultParameter` | ✅ 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) |
 | A binding end at a node of a performed action is a statement of the action's body: a simple name there resolves in the body's scope first — a parameter of the enclosing action before a same-named feature of the part performing it (KerML 1.0 §8.2.3.5 name resolution outward through owning namespaces), so `bind noting.n = level` under `perform action relaying { in level : Integer[0..1]; … }` binds the parameter, given none, not the part's `level` — and reaches the performer's features only through names resolving to them. A pin valued by its own name (`inout log = log`, `inout n = n`) names what the pin masks: the pin and the parameter it redefines are one feature (KerML 1.0 §7.3.4.5 Redefinition), so the lookup passes them over and reads the feature of that name around the usage owning the pin, never itself (no `cyclic feature value dependency`). | `runtime/action_frame.go` `bindingEndContext`, `pinSymbol`; `runtime/eval.go` `EvalContext.valuing`, `lookupName`, `namesValuedPin`; `runtime/classifier_behavior.go` `performerHoldsFeature` | `conformance/performed_action_binding_end_names_parameter.sysml`, `robustness_binding_end_names_test.go:TestRuntimeRobustnessBindingEndNames`, `robustness_call_results_test.go:TestRuntimeRobustnessCallResults` | ✅ Faithful |
-| 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 |
+| 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; an ordinary node with several successions fans out the same way (row below) | `action_executor.go` `stepForkNode`, `split` | `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` (`outcomes`: either accept may take either message) + `.trace.order` + trace goldens under the default, `declared` and `seed:1` (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` 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) |
+| An action node with several successions out of it performs every target: each succession is a connector typed by `HappensBefore` (Kernel Semantic Library `Occurrences.kerml`) that orders the source performance before its target and selects or excludes no other target, so each target that declares no multiplicity is one performance after the source, unordered relative to the others — the token behavior of a fork (`Actions::ForkAction` "has no inherent behavior"; it only requires the `1..1` target multiplicity an ordinary node's successions leave unwritten). Only `DecisionPerformance` makes outgoing successions exclusive ("exactly one of the Successions"). A guarded succession out of a non-decision node is a `NonStateTransitionPerformance` whose guard constrains its own `transitionLink : HappensBefore[0..1]`, so every holding guard is followed and a false guard prunes only its own link | `runtime/action_executor.go` `follow` and `split` (the token leaving an initial node, an action node — `leaveExecutionNode`, `completeNode` — or a statement node — `leaveStatementNode` — splits one fresh token per enabled succession, appended in declaration order, after the node's data flows are applied once; `stepForkNode` uses the same `split`), `enabledSuccessions` (every guard out of the node is read before the token leaves); `runtime/action_step_multiplicity.go` `passZeroStep` (a `[0]` step forwards to every successor); `smt/encode.go` `tokenStep.fork` and `smt/support.go` `Flow.fansOut`, `sizeSlots` (the fan-out takes the fork encoding and its slots) | `conformance/action_succession_fan_out_writes_one_feature.sysml` + `.expected.json` (both outcomes admissible) + `.check.expected.json` + trace golden + `.declared` and `.seed-1` goldens + `.trace.order`, `action_succession_fan_out_rejoin` + trace golden + `.trace.order`, `action_succession_fan_out_guard_pruned_rejoin` + trace golden, `action_succession_fan_out_data_flows` + trace golden, `action_succession_fan_out_statement_node` + trace golden, `action_succession_fan_out_from_start` + trace golden, `action_succession_guard_two_hold` + trace golden, `action_succession_fan_out_one_guard_holds` (one enabled succession moves the token on, as the `smt` engine's witnesses replay), `action_fork_one_branch_beside_live_token` (a fork with one succession still replaces its token), `action_step_multiplicity_fan_out`, `action_step_multiplicity_fan_out_plain`, `action_step_multiplicity_zero_fan_out` + trace golden, all derived in [the semantic oracle](behavior-semantic-oracle.md#several-successions-out-of-an-ordinary-action-node-every-target-follows-in-which-order-is-open); `action_succession_fan_out_test.go:TestStatementNodeFanOut` (`assign`, `if`, `while`, `loop`, `for`, `send`); `action_executor_test.go:TestActionExecutor_GuardedSuccession_TwoGuardsHold`; `robustness_succession_fan_out_test.go:TestRuntimeRobustnessSuccessionFanOut` (a pruned branch into a join deadlocks, an unevaluable guard on one link fails the step, a fan-out in a loop and a self-loop fan-out spend the budget, a merge with two outgoing successions is refused); `smt/encode_test.go:TestEncodeFanOutJoinCompletes`, `:TestEncodeFanOutPlainRejoinRefused`; `tests/parser/testdata/parse/action_succession_fan_out.sysml` + golden | ✅ Faithful (the join and merge keep their outgoing bound — `validateJoinNodeOutgoingSuccessions`, `validateMergeNodeOutgoingSuccessions` — and a decision its one branch; a repeated step still needs written end multiplicities on each edge out of it. The `smt` engine refuses a plain node several fan-out branches rejoin at as an implicit join, which it does not encode, rather than encoding one branch) |
 | 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) |
 | Which linearization a run takes where the library orders nothing is tool-defined, so it is a named *scheduling policy* rather than one fixed rule: `reverse` (the default — reverse token-index order, first holding guard, first enabled transition — so every run recorded before policies were selectable replays unchanged), `declared` (tokens in spawn order, guards and transitions in declaration order) and `seed:<n>` (every pick drawn from a PCG sequence the seed fixes, so one seed replays one run on every platform and two seeds may take two linearizations). The policy decides every choice point of the row above and the rows below — token order in a step, the holding guard a decision follows, the enabled transition that fires, the order the orthogonal regions one event enables react in, whose same-step write stands (it follows from the token order) — and nothing else: every choice point a run reaches is reported under every policy, and the `took …` of each is what the policy took (another linearization may reach other choice points, so their count is not fixed across policies). A spelling naming no policy (`seed`, `seed:`, `seed:-1`, `seed:abc`, an unknown name) is `ErrInvalidSchedulePolicy` before anything runs, on every surface: `sysml -schedule`, `%schedule`, and the `schedule` field of `ExecuteActionRequest`, `ExecuteStateRequest` and `RunAnalysisRequest` (`INVALID_ARGUMENT`; the `schedule` capability advertises the field). Guards read in a preview leave the seeded sequence where it was, so reporting a choice does not change which alternative the run takes; a decision branch picked past the first was only previewed, so the run reads its guard once more before taking it (what evaluating it materialized or derived is then the run's), as `fireTransition` reads a transition's guard again before it fires; an executor a debugger drives call by call keeps the scheduler its run started with when another run under another policy is driven to completion in between, and `Decide` previews the transition that run would fire from that same scheduler, putting its draw back; and a composite state every leaf of its orthogonal regions reaches is asked for its transition once per dispatch or change poll, so the choice among its enabled transitions draws once (one candidate, one `took …`), a composite state a nested state outranks draws nothing, the pick among a candidate's enabled transitions being made only once it survives conflict resolution, so the run's next reported choice takes the seed's next draw; and a token parked at a join its other branches have not reached or at an accept no message in flight answers keeps its place in the step's order, so a seed draws only among the tokens able to act and steps taken while every token is parked draw nothing | `runtime/scheduler.go` `SchedulePolicy`, `ParseSchedulePolicy`, `SchedulePolicyError`, `scheduler.orderTokens`, `scheduler.pick`, `scheduler.mark`; `runtime/context.go` `SetSchedule`, `scheduling`, `beginExecutorRun` (a run under way keeps the scheduler it started with, across the other runs driven while it is paused), `previewExecutorRun` (`Decide` previews under it); `action_executor.go` `scheduleTokens`, `parked` (the tokens `Step` and a nested flow in `action_subflow.go` move, in the policy's order, a seed ordering only those able to act), `stepDecisionNode`; `state_executor.go` `enabledTransitions`, `selectCandidates`, `chooseTransition`, `chooseRegion` (the next region to react, drawn from the same `scheduler.pick` and reported whenever two or more can); `state_change_trigger.go` `risenChangeTransitions`; `cmd/sysml/main.go` `schedulePolicy` flag; `repl/schedule.go` `doSchedule`; `grpc/service.go`, `grpc/analysis.go` (`CapabilitySchedule`); `client/opensysml/execute.go` `WithSchedule`, `analysis.go` `Schedule`; `client/python/opensysml/connection.py` `schedule=` | `scheduler_test.go:TestParseSchedulePolicy`, `:TestParseSchedulePolicyRejectsUnknownSpellings`, `:TestReverseAndDeclaredOrders`, `:TestSeededSchedulingIsReproducible`, `:TestSeededTransitionChoiceMatchesTheRun`, `:TestProbeLeavesTheSeededSequenceInPlace`, `:TestPickedGuardIsReadByTheRun`, `:TestDrivenRunKeepsItsSchedulerAcrossOtherRuns`, `:TestDecidePredictsTheDrivenRunsTransition`, `:TestSharedAncestorChoiceDrawsOnce`, `:TestOutrankedChoiceDrawsNothing`, `:TestParkedTokensDrawNothing`, `explore_test.go:TestExploreSiblingRegionOrder` (`reverse` and `declared` take region declaration order and report the choice; `seed:1` and `seed:8` reach the two effect orders, each replaying), `choice_test.go:TestNotesOfATransitionBlockedBeforeFiringAreDropped`; `conformance_test.go:TestExecutionConformance` (the whole suite under the default, every `.expected.json` and `.trace.golden` unchanged), `:TestExecutionConformanceUnderPolicies` (the whole suite under `declared` and `seed:1`: no error, panic or hang, and every case pinning no policy and listing no `outcomes` produces its default outputs), `trace_test.go:TestExecutionTrace` (`<case>.declared.trace.golden` and `<case>.seed-1.trace.golden` for every `outcomes` case); `conformance/action_choice_shared_message_accept` lists `outcomes` (`a = 2, b = 1` and `a = 1, b = 2`, derived in `behavior-semantic-oracle.md` § Two accepts of one type racing for two sends) with a `.trace.order` and `declared`/`seed-1` trace goldens; `send_identity_same_named_ports` runs unpinned (it pinned `"schedule": "reverse"` while the via-less `accept Ping` over-matched a transfer addressed to `alpha.inPort`; with the accept held to the receiver the transfer reaches, `waiting` has one enabled transition under every policy); `cmd/sysml/run_test.go:TestRunActionUnderSchedule`; `repl/schedule_test.go`; `grpc/schedule_test.go`, `grpc/capability_test.go`; `client/opensysml/schedule_test.go`, `schedule_internal_test.go`; `client/python/tests/test_schedule.py`; `conformance/scenarios/06-behavior.json` (`schedule` on the wire, in-process and over every transport) | ✅ Faithful (the three driven policies each take one linearization per run and say which at every choice point; `explore`, the bounded exhaustive replay of the row below, enumerates them all, and the harness checks every listed outcome is reachable and no unlisted one is, so a fixed order is never passed off as the only one. Same-step write order is not a pick of its own: it follows the token order, so under a policy that orders the writing tokens differently the other write stands, which is what the write-conflict goldens under `declared` and `seed:1` pin) |
 | Every linearization the library admits is a valid run, so a model with choice points has a *set* of outcomes, not one: the `explore[:runs=N,depth=D]` policy enumerates it by replay — one run records the alternative each choice point took; each later run is a fresh context on the same lowered model (its own instances, message bus, clock, object behaviors, calc memo and notes — nothing of one run is seen by the next; every run of one exploration is built over that exploration's own resolver and semantic model, an `analysis.Worker` over the shared frozen index, so two explorations on one model, or one beside a gRPC request or a REPL completion, share nothing that memoizes) that follows the recorded prefix and takes the next untried alternative at its end, the prefixes run in plan order — every one departing from the first run at one choice before any departing at two, earliest choice first, so a `runs` budget of one more than the first run's choice points varies each of them once — until no alternative is untried or a budget is hit (a choice point past `depth` takes its first alternative in every run and is never varied). An action step under `explore` is one token advancing one node — the fixed policies move every steppable token once per step — so the tokens able to act are picked among afresh after each move, a branch of several nodes can be overtaken by a concurrent one between any two of them, and a `complete` exploration covers every interleaving of the nodes the library leaves unordered, with a leaf body yielding after its start shot and after each statement wherever another performance may change its outcome (`lower.BodyDivides`; a body's own statements keep declaration order). Runs agreeing on the observables the conformance harness compares — an action's outputs; a state machine's final state, states visited and values; an analysis case's outputs and verdicts — are one canonical outcome, counted by the linearizations reaching it and witnessed by one run's choice sequence (an object is compared by its type and feature values through the run's own context, never by the id that run gave it, so equal objects with different ids are one outcome and different objects under one id are two); a run that fails is an outcome of its own (`error: …`), not the end of the exploration; a behavior with no choice point explores in exactly one run; the same model explores to the same sorted table every time. The budget (1024 runs and 64 choice points per run by default) is never exceeded silently: `incomplete: <budget> budget <limit> hit after N runs` names each budget hit, `runs` before `depth`. `explore` is not a policy one context runs under (`ErrExploreUndriven` from `SetSchedule`), so a step-by-step debugger cannot explore: `%schedule explore` is a typed error at the prompt while `sysml -schedule explore` (`-action`, `-state`, `-analysis`, `-calc`; `-engine explore` is the same selection) tables the outcomes, exit status `2` when incomplete, and the wire answers `outcomes` and `exploration` on `ExecuteActionResponse`, `ExecuteStateResponse` and `RunAnalysisResponse` under the `schedule_explore` capability. A malformed spelling (`explore:`, `explore:runs=0`, `explore:depth=-1`, `explore:bogus`, an option twice) is `ErrInvalidSchedulePolicy` on every surface. The harness explores every case listing `outcomes` and fails when a listed outcome is unreachable or an unlisted one is reached, naming the outcome and a witness, and when the budget is hit, telling the author to raise `exploreBudget`; cases without `outcomes` are not explored by default | `runtime/explore.go` `Explore`, `ExploreBudget`, `DefaultExploreBudget`, `ExploredOutcome`, `Exploration.Status`, `ChoiceTaken`, `FormatChoices`, `exploreRun.pick`/`beginStep`/`resolve`/`nextPrefix` (the replayed prefix and the frontier), `exploreStep.next`/`acted` (one move ends the step); `runtime/scheduler.go` `scheduler.oneMove`, `tokenSchedule.Choice`; `runtime/action_executor.go` `Step` (an exploring step picks among every token able to act, a paused body whose wait has ended among them — `action_body_run.go` `Token.resumable` — where a fixed sweep resumes paused bodies last); `runtime/outcome.go` `Outcome.identity` (the canonical identity, every name quoted so no output name can spell another outcome), `Outcome.String` and `Outcome.RenderedOutputs` (the rendering), `objectSpeller` (objects by type and feature values), `Context.ActionOutcome`, `StateExecutor.Outcome`, `Context.VerifiedOutcome`; `runtime/scheduler.go` `parseExploreOptions`, `ExplorePolicy`, `SchedulePolicy.Exploration`; `runtime/context.go` `beginExploration` (the per-run scheduler of an exploring run), `SetSchedule` (`ErrExploreUndriven`); `action_choice.go` (token order and same-step writes through the exploring run); `cmd/sysml/main.go`, `report.go` (`outcomes`, `exploration` in `-json`); `repl/explore.go` `ExploreAtPromptError`, `exploreVerdict`; `repl/schedule.go` `doSchedule`; `grpc/explore.go` `Service.explore`, `grpc/service.go`, `grpc/analysis.go` (`CapabilityScheduleExplore`); `client/opensysml/explore.go` `ExploreAction`, `ExploreState`, `ExploreAnalysis`; `client/python/opensysml/exploration.py`, `connection.py` `explore_action`, `explore_state`, `explore_analysis` | `explore_test.go:TestExploreThreeWritersReachEveryOutcomeOnce`, `:TestExploreIsDeterministic`, `:TestExploreNoChoicePointsIsOneRun`, `:TestExploreRunsBudgetIsIncomplete`, `:TestExploreDepthZeroIsIncomplete`, `:TestExploreErrorIsAnOutcome`, `:TestExploreDecisionInLoop`, `:TestExploreStateTransitionConflict`, `:TestExploreRejectsOtherPolicies`, `:TestParseExplorePolicy`, `:TestExploreRunsShareNoState`, `:TestExploreTellsObjectsApartByWhatTheyAre`, `:TestExploreEquatesObjectsByWhatTheyAre`, `:TestOutcomeIdentityQuotesNames`, `:TestOutcomeIdentityOpensEveryObject` (a ring of objects is spelled once around, and objects nested past the rendering's depth still tell outcomes apart), `:TestExploreSiblingRegionOrder`, `:TestExplorePausedBodyDueIsAMove`; `explore_order_test.go:TestExploreVariesEveryChoiceOfTheFirstRunFirst` (plan order: the first run's choices varied earliest first, before any twice); `conformance_test.go:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case); `conformance/action_explore_three_writers` (six linearizations, three outcomes, derived in `behavior-semantic-oracle.md` § Three concurrent writers of one feature: six orders, three values), `action_explore_write_between_branch_nodes` (three linearizations, three outcomes, the third reached only when one branch's two nodes both run before the other branch's one; § A write between two nodes of a concurrent branch: three orders, three outcomes), `action_explore_performed_and_accept_due_together` (six linearizations, two outcomes, the paused performed action and the sibling accept due at one instant each resumed first by three; § A performed action and a sibling accept due at one instant: which resumes first is open), `action_explore_early_race_long_tail` (20 linearizations, two outcomes, the open write order met before the closed orders of the branches' tails; § Two writers of one feature before a long tail of closed choices: two values), `action_explore_decision_in_loop` (§ A decision inside a loop: every pass is its own open choice), `state_explore_transition_conflict` (§ Two transitions out of one state enabled by one event: exactly one fires, which one is open), `state_explore_region_order` (§ Transitions in sibling regions enabled by one event: each fires, in which order is open), each with a `.trace.golden` under the default and `declared`/`seed-1` goldens; `cmd/sysml/run_test.go:TestRunUnderExplore`, `:TestJSONReportsExploration`, `spacecraft_showcase_test.go:TestExploreTablesTheSpacecraftRaceWithinItsBudget` (a race past the default depth, tabled within a stated budget at any `-jobs`); `repl/explore_test.go`, `repl/isolation_test.go` (completion answers beside an exploration; a second command waits); `grpc/explore_test.go`, `grpc/evaluate_retention_test.go` (concurrent requests on one model); `analysis/isolation_test.go` (two plans on two goroutines under `-race`, each on its own worker; a run's context takes the budget's `Steps` and `Memory` at construction, a zero field being the context's own); `client/opensysml/explore_test.go`; `client/python/tests/test_explore.py`; `client/rust/opensysml/tests/client.rs`, `client/java/.../ApiIntegrationTest.java`, `client/node/test/client.test.ts` (the `schedule_explore` capability) | ✅ Faithful (exploration is over the choice points the executors report, so a linearization two choice points do not distinguish is not run twice; a replay whose choice points differ from its recorded prefix is `ErrExplorationDiverged` rather than a table nobody can trust) |
@@ -802,7 +803,7 @@ remain one-shot.
 | `then done;` — a final node as a successor target | `parser/behavior.go` `parseFinalNode` (reached by a succession); `lower/action_graph.go` `Finals`; `runtime/action_executor.go` `stepFinalNode` | `parse/behavior_loop_until_succession.golden`, `conformance/action_standard_loop_until_then_done.sysml`, `negative_test.go:then_done_no_semicolon` | ✅ Faithful (the token reaching it ends the flow, as for a declared `done;`) |
 | A flow ending at a node with no outgoing succession (`action a; action b; first a then b;`) | `lower/action_graph.go` `Edges` (the node has no outgoing edge); `runtime/action_executor.go` `retireToken`, called from `stepActionExecutionNode`, `stepNestedAction`, `stepStatementNode` | `conformance/action_last_node_without_a_succession.sysml` + trace golden, `conformance/action_flow_ending_at_a_statement.sysml`, `action_executor_test.go:TestActionExecutor_NodeWithoutSuccessorsRetiresItsToken`, `robustness_test.go:action_whose_last_node_has_no_succession` | ✅ Faithful (`Actions::Action` gives every action a `done` snapshot it inherits, so a flow that runs out of successions ends there and the action completes with what its features hold — an explicit `done;` is one way to write that end, not a requirement. A node reached by a fork retires its own branch; the action completes when the last token does) |
 | A two-ended `first a then b;` in an action body — with or without a body, any number of times, beside `first start;`, `then` chains, `succession first a then b;`, forks, joins, decisions and merges — is the succession a → b (SysML.xtext `ActionBodyItem` → `InitialNodeMember` `TargetSuccessionMember`, `SuccessionAsUsage`): it declares no node and marks no start. An end carrying a crossing multiplicity, `first [0..1] a then [0..1] b;` (§7.13.5: the `succession` keyword may be omitted when the declaration part is empty, and the ends take constraining multiplicities, as its Camera example writes `first [1] focus then [0..1] shoot;`; SysML.xtext:998 `ConnectorEnd` → `OwnedCrossMultiplicityMember`), is read as the `SuccessionAsUsage` the keyword spells, with the multiplicity on that end (`parser/succession.go` `atMultiplicityFirstSuccession`; `parse/action_first_end_multiplicity.golden`). The one-ended `first a;` naming a node the body declares starts the flow at that node; `first start;` (naming nothing declared) is the body's initial node; a body without either starts at its one node no succession leads to | `lower/action_nodes.go` `collectActionNodes` (only a one-ended `first` is collected as the initial node; two of them are `multiple initial nodes`), `lower/action_graph.go` `lowerSuccession` (the edge a two-ended `first` and a `succession` both lower to), `FirstEndReference`, `resolveFirstNode` (the node a one-ended `first` names becomes `Initial`); `passes/action_endpoint.go` (both ends of a two-ended `first` are checked); `semantics/action_succession.go` (a two-ended `first` is an `ActionSuccession` from the node it names) | `lower/action_first_node_test.go:TestToActionGraph_FirstThenIsASuccession`, `:TestToActionGraph_FirstThenBesideFirstStart`, `:TestToActionGraph_FirstThenWithABody`, `:TestToActionGraph_FirstNamesADeclaredNode`, `:TestToActionGraph_FirstDeclaresItsOwnInitialNode`, `:TestToActionGraph_FirstNamesAFinalNode`, conformance `action_first_then_succession.sysml`, `action_first_then_fork_join.sysml` (`first start;` beside a fork and four two-ended `first` ends, `total = 111`), `action_first_names_a_declared_node.sysml` + trace goldens, `parse/behavior_first_then_declared_node.golden`, `robustness_test.go:first_node_with_a_second_succession`, `:first_beside_an_initial_node`, `:two_one_ended_firsts`, `:first_naming_a_final_node`, `runtime/pilot_first_then_test.go` (the OMG `3a-Function-based Behavior-2` `provide power`, `first start;` and eight two-ended `first` ends, runs to its `accept`) | ✅ Faithful (a body states one start, so two one-ended `first` ends are rejected, as is a one-ended `first` naming a final node — the flow cannot start where it ends. The body of a two-ended `first` is a succession's body and lowers only when it holds annotations, as `succession first a then b { … }` does) |
-| A guard on a succession out of a node that is not a decision (`first s1 if c then s2;`, SysML.xtext `GuardedSuccession`) | `lower/action_graph.go` (the guard is carried on the edge); `runtime/action_executor.go` `enabledSuccessions` (every guard out of the node is evaluated before a token leaves it) | `conformance/action_succession_guard_holds.sysml`, `action_succession_guard_fails.sysml`, `action_succession_guard_two_branches.sysml`, `action_succession_guard_fork_branch_pruned.sysml`, `action_succession_guard_not_boolean.sysml`, `action_succession_guard_two_hold.sysml`, `robustness_test.go` `succession_guard_failure_modes` | ✅ Faithful (a guard that does not hold prunes the succession, since `TransitionPerformance::transitionLink` is `HappensBefore[0..1]`; two consequences the notation leaves open are tool-defined and pinned in the goldens: a node whose every succession is pruned ends its flow, and two guards holding at once out of one node is reported rather than resolved — a fork prunes only the branches whose guard fails) |
+| A guard on a succession out of a node that is not a decision (`first s1 if c then s2;`, SysML.xtext `GuardedSuccession`) | `lower/action_graph.go` (the guard is carried on the edge); `runtime/action_executor.go` `enabledSuccessions` (every guard out of the node is evaluated before a token leaves it) | `conformance/action_succession_guard_holds.sysml`, `action_succession_guard_fails.sysml`, `action_succession_guard_two_branches.sysml`, `action_succession_guard_fork_branch_pruned.sysml`, `action_succession_guard_not_boolean.sysml`, `action_succession_guard_two_hold.sysml` + trace golden (both targets performed), `robustness_test.go` `succession_guard_failure_modes` | ✅ Faithful (a guard that does not hold prunes the succession, since `TransitionPerformance::transitionLink` is `HappensBefore[0..1]`; a node whose every succession is pruned ends its flow, one tool-defined consequence pinned in the goldens; two guards holding at once out of a node that is not a decision are two links, both followed, as a fork follows every branch whose guard holds) |
 | `else` branch of a decision in an action flow (`if c then a; else b;`, SysML.xtext `DefaultTargetSuccession`) | `parser/behavior.go` (the `else` clause builds `*ast.ControlFlowEdge{IsElse: true}`); `lower/action_graph.go` (the else edge is the guardless alternative); `runtime/action_executor.go` `stepDecisionNode` | `parse/behavior_decision_else.golden`, `conformance/action_decision_else_branch.sysml`, `conformance/action_decision_guarded_branch.sysml`, `negative_test.go:decision_else_no_target` | ✅ Faithful (the else edge is taken when no guarded branch out of the decision holds) |
 | Succession outside a behavior body (`first part1::action1 then requirement1;`, `first b.g then b.m;`, `first grip then move;` in a part def) orders the performances it relates: featured by its owning type, or by the innermost common featuring type of its ends (KerML §8.3.4.5.3 `deriveConnectorDefaultFeaturingType`, `checkConnectorTypeFeaturing`; §8.4.4.6.1 implied TypeFeaturing), each earlier-end performance happening before each later-end one (`Occurrences::HappensBefore`, SysML §8.4.9.4) | `parser/namespace.go`, `parser/succession.go`; `semantics/succession_featuring.go:BehaviorSuccessionFeaturingType`; `lower/behavior_order.go:BehaviorOrders`; `check/passes/behavior_order.go:BehaviorOrderPass`; `runtime/succession_order.go:shouldDeferBehavior`, `releaseDeferredBehavior`, `checkSuccessionOrderViolation`, `successionCycle`, `noteRefusedBehaviorOrders` | `parse/behavior_namespace_succession.golden`, `parse/namespace_succession_chain_ends.golden`, `parse/type_succession_performed_actions.golden`, conformance `namespace_succession_chain_ends`, `type_succession_performed_actions`, `namespace_succession_qualified_ends`, `namespace_succession_explicit_start_violated`, `namespace_succession_requirement_end` (the first three with trace goldens), `robustness_namespace_succession_test.go:TestRuntimeRobustnessNamespaceSuccession`, `succession_featuring_test.go`, `behavior_order_test.go` (lower and check), `lower/namespace_succession_test.go:TestNamespaceSuccessionHasNoTokenFlowOrNeighborGraphAttachment` | ✅ Implemented where one performance per end per featuring instance is ordered: a type-bound start is held until its predecessor ends (the scheduler is constrained, not fixed to one order); an explicit `perform x.beh.start` or `-action` start that would break the order fails with `succession-order-violated`; a cycle is `succession-order-cycle`. Refused with `succession-orders-nothing` and the reason when one end binds an object behavior and the order cannot be enforced (a requirement end, a missing or repeated performance, open under KERML-29); written end multiplicities follow the action-step rule. Ends with no common featuring type are `connector-type-featuring` errors. Derivation: [behavior-semantic-oracle.md](behavior-semantic-oracle.md#a-succession-outside-a-behavior-body-orders-the-performances-it-relates-wherever-they-run); the pinned pilot's rejection of qualified ends is [gap register #21](spec-pilot-gap-register.md#21-a-succession-whose-ends-are-qualified-names) |
 | A statement written directly among an action's own members (`send`, `assign`, `if`, `while`, `for`, `terminate`) is a subaction of the action and is performed, not ignored | `lower/action_graph.go` `BodyStatementMembers`; `lower/action_nodes.go` (each is a node of the flow); `lower/action_starts.go` `startsConcurrently` | `robustness_unordered_subactions_test.go:TestRuntimeRobustnessUnorderedSubactions/statement_directly_in_an_action_body_*`, conformance `action_unordered_statements`, `action_body_flow_unordered_statement`, `analysis_unordered_statements_beside_flow` (performed once in a case body stating a flow), `analysis_stated_flow_trailing_result` (a trailing result-returning `if` returns after the flow) | ✅ Faithful (no succession reaches it, so it starts with its owner's performance, as the unordered-subactions row above states) |
@@ -821,7 +822,7 @@ remain one-shot.
 | Object flow, streaming (`flow a.out to b.in;`; SysML v2 §7.16: "the input and output parameters are streaming unless designated as succession flows", `Flows::Flow :> Message, FlowTransfer`): each value the source pin takes while the source is being performed reaches the pin of every ongoing performance of the target at once, so a target that reads its pin between two writes sees each; a value written while no performance of the target is under way waits at its pin, and a later write from the same source performance along the same flow replaces it, so the target's next performance begins with the pin's value as it stands (the writes of distinct source performances wait one per target performance, oldest first); each `flow` declaration is a transfer of its own, so two flows out of one pin into one target pin — two routes of a fUML fork, or a pin named by its inherited and its redefining name — each stage the pin's write, and two performances of the target begun afterwards each take one; the source completing carries nothing more where it streamed, and a source pin never written by the time the source completes is `ErrFlowSource`; a value written after the target's last performance ended, which no later performance of the target takes, is `ErrStreamUnreceived` when the enclosing performance completes; a stream to a pin the target does not declare is `ErrNodePin` at the write; the outputs of an action a node performs (`action p : Producer;`) stream from the node as the performance writes them; streaming flows that carry a value back to the pin it was written to are `ErrStreamCycle`; the checker's footprint of a node counts every target pin its writes stream to, through nested bodies and transitively, so a streaming write and a read of the target pin never commute under reduction; the SMT encoding streams each write of a body, declared value or expression result at the write, a queued value the same performance replaces while another's is an overflow, and a value queued after its target's last performance fails the action as it completes | `lower/action_graph.go` `FlowKind` (`FlowStreaming`/`FlowSuccession`), `ObjectFlow.Kind`, `lowerFlow`, `succeedFlow`; `runtime/action_frame.go` `setFrameFeature` → `streamFrom` → `streamFlow` (`ongoing` finds the target's performances under way, `deliverFlow` queues ahead of the next), `actionFrame.streamed`, `actionFrame.unreceived`, `takeDeliveries`, `checkStreamsReceived`; `runtime/action_executor.go` `applyDataFlows` (skips a pin already streamed), `ActionExecutor.streamOutput` with `runtime/action_frame.go` `streamCalleeOutput` (a performed action's output writes reach the node's pin as made, installed by `beginPerformed` before the callee's declared values are seeded); `lower/footprint.go` `flowTarget`, `streamsFrom`, `streams` over `ActionGraph.Enclosing`/`EnclosingNode` (`block_graph.go` `encloseBlockFlows`); `smt/encode.go` `stream`, `carry`, `performedName`/`unreceivedName` marks | `lower/action_flow_kind_test.go`, `lower/footprint_test.go:TestFootprintStreamingWritesReachTargetPins`; conformance `action_flow_streaming_producer_consumer.sysml` + `.expected.json` + trace golden (a producer loop writing 1, 2, 3 beside a consumer loop reading each: total 6), `action_flow_streaming_before_target_begins.sysml`, `action_flow_streaming_in_loop_body.sysml`, `action_flow_streaming_declared_value.sysml`, `action_flow_streaming_from_performed_action.sysml` (a performed `Producer` writes 1, 2, 3 before its consumer begins; the consumer reads the last: total 3), `action_flow_streaming_last_write_before_target_begins.sysml`, `action_flow_streaming_performed_declared_value.sysml` (a performed action's declared output streams as the performance begins), `action_flow_streaming_two_flows_one_pin_to_call.sysml` (two flows out of one pin feed two performances of a nested action definition with a required input: each is bound), `action_flow_streaming_aliased_source_pin.sysml` (the inherited and the redefining name of one pin, two flows: two deliveries), `stream_stage_test.go:TestStagedStreams`, `action_output.sysml`, `action_block_flow_loop_bindings.sysml`; `robustness_streaming_flow_test.go` (`source_never_writes`, `target_completed_before_source_writes`, `target_pin_not_declared`, `later_performance_takes_one_of_two_late_values`, `flows_form_a_cycle`); `check_state_stream_test.go`, `check_reduce_test.go` (`por_streaming_flow`: reduced and unreduced search agree), `smt/encode_test.go:TestEncodeFlowKindsDiffer` (the encoding and the interpreter's exploration agree that a plain `flow` beside its target may arrive late and a `succession flow` never does) | ✅ Faithful |
 | Object flow, succession (`succession flow a.out to b.in;`, `Flows::SuccessionFlow :> Flow, FlowTransferBefore`: the target "cannot begin until the source completes"): the value the source pin holds when the source completes moves to the target pin, and the flow is also the succession source → target | `lower/action_graph.go` `lowerFlow` (`FlowSuccession`), `succeedFlow` (the succession edge); `runtime/action_executor.go` `applyDataFlows` → `deliverFlow` | conformance `action_flow_succession_producer_consumer.sysml` + `.expected.json` + trace golden (the same producer and consumer in sequence: the consumer reads the last value, 3, three times), `robustness_test.go:flow_from_a_node_that_produced_nothing` | ✅ Faithful |
 | Guarded succession leading to a succession flow (`first a if g then f; succession flow f of T from a.y to b.v;`, the SysML v1 to v2 transformation's `ObjectFlowGuard_Mapping`: the TransitionUsage's target is the SuccessionFlowUsage, so the flow and its transfer happen only when the guard holds): the value moves and `b` is ordered after `a` only when `g` holds; when it is false, `b` waits for the pin as a UML action waits for its input, or runs on what another path delivers, never on the rejected value | `behavior/action_endpoint.go` (a succession flow leaving the succession's source is a valid target); `lower/action_graph.go` `resolveGates` (the carrying edge takes the guard, `ObjectFlow.Gate`/`ActionEdge.Gate` keep the succession); `runtime/action_executor.go` `applyDataFlows` (a gated flow delivers only over a taken edge), `starvedPin`; `smt/encode.go` `gated`; `modelform/graphs_action.go` (`gate`); `view/behavior.go` | conformance `object_flow_guard_rejected.sysml` + `.expected.json` + trace golden (false guard, another flow into `b`: `b` runs once on 2), `object_flow_guard_taken.sysml` + trace golden; `robustness_object_flow_test.go`; `smt/encode_test.go:TestEncodeGatedFlowDeliversOnlyWhenTaken`; `modelform/graphs_test.go:TestGraphsActionCarriesTheGateOfAFlow`; `view/render_test.go:TestActionRenderingDrawsTheSuccessionGatingAFlow`; parser golden `succession_to_succession_flow` | ✅ Faithful |
-| Several successions leaving an action node, one of them at most not of a succession flow: each succession is a `HappensBefore` link (Kernel Semantic Library `Occurrences.kerml`) from the node's one performance, so every target follows it — a succession flow's target as well as the node's other successor, as after a fork; two or more successions that are not of succession flows, or two guarded ones, remain a choice no order resolves | `runtime/action_executor.go` `ambiguousSuccession` (`ErrAmbiguousSuccession`), `advance` (one token per succession, the first moving on, each other a new token of the same frame); `lower/action_graph.go` `ActionEdge.Carries`, `succeedFlow`; `smt/support.go` `Flow.checkSuccessors` (the model checker refuses the implicit fork as unencoded) | `conformance/object_flow_implicit_fork.sysml` + `.expected.json` + trace golden; `robustness_object_flow_test.go:TestRuntimeRobustnessObjectFlow` (`guarded_branches_with_object_flows_stay_ambiguous`, `ErrAmbiguousSuccession`) | ✅ Faithful |
+| Several successions leaving an action node, some of them of succession flows: each succession is a `HappensBefore` link (Kernel Semantic Library `Occurrences.kerml`) from the node's one performance, so every enabled target follows it — a succession flow's target as well as the node's other successors, as after a fork, with the node's flows applied once before the token splits | `runtime/action_executor.go` `follow`, `split` (one token per enabled succession, appended in declaration order); `lower/action_graph.go` `ActionEdge.Carries`, `succeedFlow`; `smt/support.go` `Flow.fansOut` (the model checker takes the fork encoding) | `conformance/object_flow_implicit_fork.sysml` + `.expected.json` + trace golden; `robustness_object_flow_test.go:TestRuntimeRobustnessObjectFlow` (`guarded_branches_with_object_flows_both_follow`) | ✅ Faithful |
 | Object values through a fork, join or merge (`fork f { in ref inputObject1; out ref outputObject1 = inputObject1; }`, `join j { in ref inputObject1; in ref inputObject2; out ref outputObject1 nonunique = (inputObject1, inputObject2); }`; the control-node features of the SysML v1 to v2 transformation, ptc/25-04-10 `ControlNodeObjectFlowReferenceUsage_Mapping`): a flow whose target is a feature of the node holds its value there; when a token passes the node, its output features are evaluated over the inputs it holds and each flow out of an output delivers the value — a fork copying its input to every branch, a join gathering one value of each input into a sequence, a merge evaluating only the input whose flow the token arrived by, so it passes on one value per arrival; each value held with the flow that brought it, so a token arriving by a succession flow takes that flow's value and one arriving by a succession that carries nothing takes the one input plain flows left values at, never a value a succession flow holds for its own token | `lower/action_graph.go` `lowerControlFeatures`, `CarriesObjects`; `runtime/action_control_objects.go` `carryObjects`, `arrivingObject`, `queueControlObject`, `actionFrame.takeHeld`; `runtime/action_executor.go` `stepForkNode`, `stepJoinNode`, `stepMergeNode`, `deliverFlow` | `tests/parser/testdata/parse/action_control_node_objects.sysml` + golden; `conformance/object_flow_fork_copies_value`, `object_flow_join_gathers_values`, `object_flow_merge_per_arrival` (a loop through the merge), `object_flow_merge_control_arrival` (a control arrival beside a queued succession-flow value), `object_flow_merge_shared_input` (a plain flow and a succession flow into one input), `object_flow_merge_empty_succession_flow` (a succession flow that carries nothing beside a plain flow into one input) + `.expected.json` + trace goldens; `robustness_object_flow_test.go:TestRuntimeRobustnessObjectFlow` (a join waiting for a value that never comes, `ErrActionDeadlock`; a merge loop with no way out, `ErrActionStepLimitExceeded`; a control arrival at a merge holding plain-flow values at two inputs, `ErrAmbiguousMergeInput`; a failing output expression, `ErrDivisionByZero`) | ✅ Faithful |
 | Succession edges | `lower/action_graph.go:ToActionGraph` | `action_control_flow.sysml` | ✅ Faithful |
 | Object flow from a pin declared admitting no value (`out reading : Real[0..1];` on an action with no body, as a v1 call naming no behavior migrates to) that the performance never wrote: the flow carries nothing, so the target begins with the pin empty rather than the run failing with `ErrFlowSource`; a read of such a pin by path (`measure.reading`), or of the performance itself as a value when the pin is its `result`, is the empty sequence, as a read of its declaration is, and an activity output bound to it is declared admitting no value too; a required pin the performance never wrote stays `ErrFlowSource`, and a required target pin no value reaches stays `NoValueError` naming it, so nothing is made up | `runtime/action_frame.go` `nodePins.optional`, `actionFrame.optional` (filled by `pinsOf`/`addFeatureDirections` from `Context.admitsNoValue` over each lowered `Feature`, as `lower.Attribute.Optional` is), `actionFrame.admitsNoValueAt`, `actionFrame.pin`, `actionFrame.resultValue`; `runtime/action_executor.go` `applyDataFlows` | conformance `stub_action_output_holds_no_value.sysml` + `.expected.json`; `robustness_stub_action_test.go` (`optional_output_flows_no_value`, `required_output_never_written`, `required_target_gets_no_value`, `optional_output_read_by_path`, `optional_result_read_as_value`, `required_result_read_as_value`); `parse/action_declared_parameters_no_body.golden`; `tests/migrate/testdata/xmi/stub_actions.xmi` goldens | ✅ Faithful |
diff --git a/internal/exec/runtime/action_executor.go b/internal/exec/runtime/action_executor.go
index 55dfcbd49c..97d8abbe8e 100644
--- a/internal/exec/runtime/action_executor.go
+++ b/internal/exec/runtime/action_executor.go
@@ -16,10 +16,6 @@ import (
 	"github.com/Open-MBEE/OpenSysML/internal/syntax/ast"
 )
 
-// ErrAmbiguousSuccession reports a node whose flow could continue along more
-// than one succession, which the token semantics do not resolve.
-var ErrAmbiguousSuccession = errors.New("more than one succession is enabled")
-
 // actionLabelPrefix opens the text naming an action in diagnostics and choices.
 const actionLabelPrefix = "action "
 
@@ -2299,14 +2295,8 @@ func (e *ActionExecutor) stepInitialNode(tokenIdx int) error {
 		return err
 	}
 
-	// A guard ruling out the succession the flow starts with ends it here.
-	if len(successors) == 0 {
-		return e.retireToken(tokenIdx)
-	}
-
-	// Move token to first successor (initial should have exactly 1)
-	e.move(token, successors[0])
-	return nil
+	// A guard ruling out every succession the flow starts with ends it here.
+	return e.follow(tokenIdx, successors)
 }
 
 // stepFinalNode consumes token and checks for completion.
@@ -2373,8 +2363,28 @@ func (e *ActionExecutor) stepForkNode(tokenIdx int) error {
 	if len(successors) == 0 {
 		return e.retireToken(tokenIdx)
 	}
+	e.split(tokenIdx, successors)
+	return nil
+}
 
-	// Create N tokens (one per successor), in the flow the fork belongs to
+// follow takes the token at tokenIdx along every enabled succession: none retires
+// it, one moves it on, and several split it as a fork does (Occurrences::HappensBefore).
+func (e *ActionExecutor) follow(tokenIdx int, successors []lower.ActionEdge) error {
+	switch len(successors) {
+	case 0:
+		return e.retireToken(tokenIdx)
+	case 1:
+		e.move(&e.tokens[tokenIdx], successors[0])
+		return nil
+	}
+	e.split(tokenIdx, successors)
+	return nil
+}
+
+// split replaces the token at tokenIdx with a fresh one per succession, appended
+// in declaration order, in the flow the token belongs to.
+func (e *ActionExecutor) split(tokenIdx int, successors []lower.ActionEdge) {
+	frame := e.tokens[tokenIdx].frame
 	newTokens := make([]Token, 0, len(successors))
 	for _, edge := range successors {
 		newToken := Token{
@@ -2388,13 +2398,9 @@ func (e *ActionExecutor) stepForkNode(tokenIdx int) error {
 		newTokens = append(newTokens, newToken)
 		e.noteTraversal(&newToken, edge)
 	}
-
-	// Remove original token, add new tokens
 	e.removeToken(tokenIdx)
 	e.tokens = append(e.tokens, newTokens...)
 	frame.live += len(successors) - 1
-
-	return nil
 }
 
 // stepJoinNode passes the one token a join performs with — synchronize has
@@ -2617,21 +2623,17 @@ func (e *ActionExecutor) stepActionExecutionNode(tokenIdx int) error {
 // leaveExecutionNode takes the token at tokenIdx on from node, whose result its
 // data flows carry, retiring it where the flow leads no further.
 func (e *ActionExecutor) leaveExecutionNode(tokenIdx int, frame *actionFrame, node *ast.ActionExecutionNode) error {
-	// Advance to a succession its guard, where it carries one, leaves enabled.
+	// Advance along every succession its guard, where it carries one, leaves enabled.
 	successors, err := e.enabledSuccessions(frame, node)
 	if err != nil {
 		return err
 	}
 
-	if err := ambiguousSuccession("action node "+node.Name, successors); err != nil {
-		return err
-	}
-
 	// Apply data flows: transfer data from this node's output pins to target input pins
 	if err := e.applyDataFlows(frame, frame.graph, node, nil, frame.data, nil, successors); err != nil {
 		return err
 	}
-	return e.advance(tokenIdx, successors)
+	return e.follow(tokenIdx, successors)
 }
 
 // stepNestedAction performs a nested action usage in a frame of its own.
@@ -2794,14 +2796,11 @@ func (e *ActionExecutor) completeNode(tokenIdx int, perf *actionFrame) error {
 		e.tokens[tokenIdx].repetitionGroup = 0
 	}
 
-	// Advance to a succession its guard, where it carries one, leaves enabled.
+	// Advance along every succession its guard, where it carries one, leaves enabled.
 	successors, err := e.enabledSuccessions(frame, node)
 	if err != nil {
 		return err
 	}
-	if err := ambiguousSuccession("action node "+ActionNodeName(node), successors); err != nil {
-		return err
-	}
 
 	// The flows out of this node carry what this performance produced to the
 	// pins the nodes downstream read.
@@ -2811,41 +2810,7 @@ func (e *ActionExecutor) completeNode(tokenIdx int, perf *actionFrame) error {
 
 	// A node the flow leads no further from is where this flow ends: the action
 	// inherits its `done` snapshot, so no succession to a final node is needed.
-	return e.advance(tokenIdx, successors)
-}
-
-// ambiguousSuccession reports successions out of node that state a choice no order
-// resolves: two not of succession flows, guarded or not, which a fork states.
-// The successions of succession flows each follow the node beside another.
-func ambiguousSuccession(node string, successors []lower.ActionEdge) error {
-	control := 0
-	for _, edge := range successors {
-		if !edge.Carries {
-			control++
-		}
-	}
-	if control > 1 {
-		return fmt.Errorf("%w: %s has multiple successors", ErrAmbiguousSuccession, node)
-	}
-	return nil
-}
-
-// advance takes the token at tokenIdx along every enabled succession out of an action
-// node, each target following it as after a fork; none retires the token.
-func (e *ActionExecutor) advance(tokenIdx int, successors []lower.ActionEdge) error {
-	if len(successors) == 0 {
-		return e.retireToken(tokenIdx)
-	}
-	frame := e.tokens[tokenIdx].frame
-	e.move(&e.tokens[tokenIdx], successors[0])
-	for _, edge := range successors[1:] {
-		token := Token{ID: e.nextTokenID, frame: frame}
-		e.nextTokenID++
-		e.move(&token, edge)
-		e.tokens = append(e.tokens, token)
-		frame.live++
-	}
-	return nil
+	return e.follow(tokenIdx, successors)
 }
 
 // triggerReady reports whether a change event's condition currently holds.
@@ -3170,33 +3135,7 @@ func (e *ActionExecutor) leaveStatementNode(tokenIdx int, frame *actionFrame, no
 	if err != nil {
 		return err
 	}
-	if err := ambiguousSuccession(statementNodeKeyword(node)+" node", successors); err != nil {
-		return err
-	}
-	return e.advance(tokenIdx, successors)
-}
-
-// statementNodeKeyword names a statement node for a message about it, since a
-// node written as a statement has no name to report.
-func statementNodeKeyword(node ast.Node) string {
-	switch n := node.(type) {
-	case *ast.WhileLoopActionNode:
-		return "a '" + n.Kind.String() + "' loop"
-	case *ast.IfActionNode:
-		return "an 'if'"
-	case *ast.AssignmentActionNode:
-		return "an 'assign'"
-	case *ast.SendStatement:
-		return "a 'send'"
-	case *ast.TerminateStatement:
-		return "a 'terminate'"
-	case *ast.PerformActionNode:
-		return "a 'perform'"
-	case *ast.Usage:
-		return "the assertion " + ActionNodeName(n)
-	default:
-		return fmt.Sprintf("a %T", node)
-	}
+	return e.follow(tokenIdx, successors)
 }
 
 // applyDataFlows moves what the completed performance produced along graph's flows out
diff --git a/internal/exec/runtime/action_executor_test.go b/internal/exec/runtime/action_executor_test.go
index 2fce9e858f..38e8b00cdb 100644
--- a/internal/exec/runtime/action_executor_test.go
+++ b/internal/exec/runtime/action_executor_test.go
@@ -2496,8 +2496,8 @@ func TestActionExecutor_GuardedSuccession_PrunesAForkBranch(t *testing.T) {
 	}
 }
 
-// Two successions out of one node whose guards both hold state no order between
-// them, so the ambiguity is reported rather than resolved.
+// Two successions out of one node whose guards both hold are two HappensBefore
+// links, neither excluding the other: the token splits, one to each target.
 func TestActionExecutor_GuardedSuccession_TwoGuardsHold(t *testing.T) {
 	initial := &ast.InitialNode{First: &ast.QualifiedName{Parts: []ast.NameSegment{{Text: "start"}}}}
 	s1 := &ast.ActionExecutionNode{Name: "s1", Expression: &ast.LiteralInteger{Value: "1"}}
@@ -2542,12 +2542,15 @@ func TestActionExecutor_GuardedSuccession_TwoGuardsHold(t *testing.T) {
 		t.Fatalf("step initial: %v", err)
 	}
 
-	err = exec.stepToken(0)
-	if err == nil {
-		t.Fatal("two successions holding at once were traversed without an error")
+	if err := exec.stepToken(0); err != nil { // s1 → s2 and s3
+		t.Fatalf("step s1: %v", err)
 	}
-	if !containsText(err.Error(), "has multiple successors") {
-		t.Errorf("unexpected error: %v", err)
+	locations := make(map[ast.Node]bool, len(exec.tokens))
+	for _, token := range exec.tokens {
+		locations[token.Location] = true
+	}
+	if len(exec.tokens) != 2 || !locations[s2] || !locations[s3] {
+		t.Errorf("s1 left %d tokens at %v, want one each at s2 and s3", len(exec.tokens), locations)
 	}
 }
 
diff --git a/internal/exec/runtime/action_step_multiplicity.go b/internal/exec/runtime/action_step_multiplicity.go
index 9708ceed95..da5bc84fc3 100644
--- a/internal/exec/runtime/action_step_multiplicity.go
+++ b/internal/exec/runtime/action_step_multiplicity.go
@@ -92,10 +92,7 @@ func (e *ActionExecutor) passZeroStep(tokenIdx int, node ast.Node) error {
 	if err != nil {
 		return err
 	}
-	if err := ambiguousSuccession("action node "+ActionNodeName(node), successors); err != nil {
-		return err
-	}
-	return e.advance(tokenIdx, successors)
+	return e.follow(tokenIdx, successors)
 }
 
 func (e *ActionExecutor) trackRepeated(tokenID int64, perf *actionFrame) {
diff --git a/internal/exec/runtime/action_succession_fan_out_test.go b/internal/exec/runtime/action_succession_fan_out_test.go
new file mode 100644
index 0000000000..99ca9d2874
--- /dev/null
+++ b/internal/exec/runtime/action_succession_fan_out_test.go
@@ -0,0 +1,49 @@
+package runtime
+
+import (
+	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/syntax/ast"
+)
+
+// TestStatementNodeFanOut: two successions out of a statement node are two
+// HappensBefore links, so both targets are performed once, whatever the node.
+func TestStatementNodeFanOut(t *testing.T) {
+	for _, tc := range []struct{ name, node string }{
+		{"assign", "then assign x := 1;"},
+		{"if", "then if x == 0 { assign x := 1; }"},
+		{"while", "then while x < 1 { assign x := x + 1; }"},
+		{"loop", "then loop { assign x := x + 1; } until x == 1;"},
+		{"for", "then for i in (1, 2) { assign x := x + i; }"},
+		{"send", "then send x to self;"},
+	} {
+		t.Run(tc.name, func(t *testing.T) {
+			src := `package test {
+				private import ScalarValues::*;
+				action fan {
+					attribute x : Integer = 0;
+					attribute b1 : Integer = 0;
+					attribute c1 : Integer = 0;
+					first start;
+					` + tc.node + `
+					then b;
+					then c;
+					action b { assign b1 := b1 + 1; }
+					action c { assign c1 := c1 + 1; }
+				}
+			}`
+			idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, src))
+			sym := findSymbolByName(idx.DocumentRoot("<test>"), "fan", ast.DefAction)
+			if sym == nil {
+				t.Fatal("action fan not found")
+			}
+			results, err := ctx.ExecuteAction(sym)
+			if err != nil {
+				t.Fatalf("ExecuteAction: %v", err)
+			}
+			if b, c := results["b1"].Const.Int, results["c1"].Const.Int; b != 1 || c != 1 {
+				t.Errorf("b1 = %d, c1 = %d, want each target performed once", b, c)
+			}
+		})
+	}
+}
diff --git a/internal/exec/runtime/conformance_test.go b/internal/exec/runtime/conformance_test.go
index 38d1dbaa09..ff85299bed 100644
--- a/internal/exec/runtime/conformance_test.go
+++ b/internal/exec/runtime/conformance_test.go
@@ -140,6 +140,9 @@ type ExpectedOutcome struct {
 	// ExploreBudget raises the budget the harness explores the case's outcomes
 	// under, for a case whose choice tree the default budget does not cover.
 	ExploreBudget *ExpectedExploreBudget `json:"exploreBudget,omitempty"`
+	// SolverBudget lowers the moves the SMT referee unrolls the case to, for a case
+	// whose every run ends well within them but the default unrolling outlasts the solver.
+	SolverBudget *ExpectedSolverBudget `json:"solverBudget,omitempty"`
 
 	// Action fields
 	Outputs    map[string]ExpectedValue `json:"outputs,omitempty"`
@@ -761,6 +764,12 @@ func (b *ExpectedExploreBudget) budget() ExploreBudget {
 	return budget
 }
 
+// ExpectedSolverBudget is the solverBudget of a case: the moves the SMT referee
+// encodes its action to, in place of the engine's default.
+type ExpectedSolverBudget struct {
+	Moves *int `json:"moves,omitempty"`
+}
+
 // admissibleSchemaProblems reports how a case misuses outcomes and admissible:
 // the two go together, replace the single outcome rather than sit beside it,
 // list at least two distinct results, and cite a section the oracle has.
@@ -774,6 +783,9 @@ func admissibleSchemaProblems(expected ExpectedOutcome, oracleTitles map[string]
 		if expected.ExploreBudget != nil && !hasSingleOutcome {
 			problems = append(problems, "exploreBudget is stated without outcomes to explore")
 		}
+		if expected.SolverBudget != nil {
+			problems = append(problems, "solverBudget is stated without outcomes to referee")
+		}
 		if expected.ExploreBudget != nil && hasSingleOutcome {
 			if expected.Type != "action" && expected.Type != "state" {
 				problems = append(problems, fmt.Sprintf("exploreBudget applies to action and state cases, not %q", expected.Type))
@@ -787,6 +799,9 @@ func admissibleSchemaProblems(expected ExpectedOutcome, oracleTitles map[string]
 	if _, err := ExplorePolicy(expected.ExploreBudget.budget()); err != nil {
 		problems = append(problems, "exploreBudget: "+err.Error())
 	}
+	if b := expected.SolverBudget; b != nil && (b.Moves == nil || *b.Moves < 1) {
+		problems = append(problems, "solverBudget: moves must be stated and at least 1")
+	}
 	if expected.Type != "action" && expected.Type != "state" {
 		problems = append(problems, fmt.Sprintf("outcomes apply to action and state cases, not %q", expected.Type))
 	}
@@ -2519,6 +2534,7 @@ func TestAdmissibleOutcomesSchema(t *testing.T) {
 		{Outputs: map[string]ExpectedValue{"x": one}},
 		{Outputs: map[string]ExpectedValue{"x": two}},
 	}
+	zero, twenty := 0, 20
 	runs := 65536
 	tests := []struct {
 		name     string
@@ -2540,6 +2556,10 @@ func TestAdmissibleOutcomesSchema(t *testing.T) {
 		{"one outcome listed", ExpectedOutcome{Type: "action", Outcomes: outcomes[:1], Admissible: cited}, 1},
 		{"empty outcome", ExpectedOutcome{Type: "action", Outcomes: []AdmittedOutcome{outcomes[0], {}}, Admissible: cited}, 1},
 		{"calc case", ExpectedOutcome{Type: "calc", Outcomes: outcomes, Admissible: cited}, 1},
+		{"solver budget", ExpectedOutcome{Type: "action", Outcomes: outcomes, Admissible: cited, SolverBudget: &ExpectedSolverBudget{Moves: &twenty}}, 0},
+		{"solver budget without moves", ExpectedOutcome{Type: "action", Outcomes: outcomes, Admissible: cited, SolverBudget: &ExpectedSolverBudget{}}, 1},
+		{"solver budget of no moves", ExpectedOutcome{Type: "action", Outcomes: outcomes, Admissible: cited, SolverBudget: &ExpectedSolverBudget{Moves: &zero}}, 1},
+		{"solver budget without outcomes", ExpectedOutcome{Type: "action", Outputs: outcomes[0].Outputs, SolverBudget: &ExpectedSolverBudget{Moves: &twenty}}, 1},
 	}
 	for _, tt := range tests {
 		t.Run(tt.name, func(t *testing.T) {
diff --git a/internal/exec/runtime/robustness_object_flow_test.go b/internal/exec/runtime/robustness_object_flow_test.go
index a9cff2945c..ce2ff4ca4a 100644
--- a/internal/exec/runtime/robustness_object_flow_test.go
+++ b/internal/exec/runtime/robustness_object_flow_test.go
@@ -47,7 +47,7 @@ func TestRuntimeRobustnessObjectFlow(t *testing.T) {
 		}
 	})
 
-	t.Run("guarded_branches_with_object_flows_stay_ambiguous", func(t *testing.T) {
+	t.Run("guarded_branches_with_object_flows_both_follow", func(t *testing.T) {
 		err := runObjectFlowCase(t, `package test {
 			private import ScalarValues::*;
 			action run {
@@ -59,8 +59,8 @@ func TestRuntimeRobustnessObjectFlow(t *testing.T) {
 				action right;
 			}
 		}`)
-		if !errors.Is(err, ErrAmbiguousSuccession) {
-			t.Fatalf("run error = %v, want ErrAmbiguousSuccession", err)
+		if err != nil {
+			t.Fatalf("run error = %v, want both guarded targets to follow", err)
 		}
 	})
 
diff --git a/internal/exec/runtime/robustness_succession_fan_out_test.go b/internal/exec/runtime/robustness_succession_fan_out_test.go
new file mode 100644
index 0000000000..274e5bd380
--- /dev/null
+++ b/internal/exec/runtime/robustness_succession_fan_out_test.go
@@ -0,0 +1,108 @@
+package runtime
+
+import (
+	"errors"
+	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/syntax/ast"
+)
+
+// TestRuntimeRobustnessSuccessionFanOut exercises a token leaving an ordinary
+// node along several successions where the flow beyond cannot finish: a pruned
+// branch into a join deadlocks, a guard that cannot be evaluated fails the step,
+// a fan-out in a loop spends the budget, and a merge with two outgoing
+// successions is refused.
+func TestRuntimeRobustnessSuccessionFanOut(t *testing.T) {
+	cases := []struct {
+		name  string
+		body  string
+		steps int64
+		want  error
+	}{
+		{
+			name: "pruned_branch_into_a_join_deadlocks",
+			body: `
+				attribute armed : Integer = 0;
+				first start;
+				then action a;
+				action b; action c;
+				join sync;
+				done;
+				succession first a if armed > 0 then b;
+				succession first a then c;
+				succession first b then sync;
+				succession first c then sync;
+				succession first sync then done;
+			`,
+			want: ErrActionDeadlock,
+		},
+		{
+			name: "guard_on_one_link_cannot_be_evaluated",
+			body: `
+				first start;
+				then action a;
+				action b; action c;
+				succession first a if missing > 0 then b;
+				succession first a then c;
+			`,
+			want: ErrUnresolvedReference,
+		},
+		{
+			name: "fan_out_in_a_loop_spends_the_budget",
+			body: `
+				attribute n : Integer = 0;
+				first start;
+				merge m;
+				action a;
+				action b { assign n := n + 1; }
+				succession first start then m;
+				succession first m then a;
+				succession first a then m;
+				succession first a then b;
+			`,
+			steps: 200,
+			want:  ErrActionStepLimitExceeded,
+		},
+		{
+			name: "self_loop_fan_out_spends_the_budget",
+			body: `
+				attribute n : Integer = 0;
+				first start;
+				then action a;
+				action b { assign n := n + 1; }
+				succession first a then a;
+				succession first a then b;
+			`,
+			steps: 200,
+			want:  ErrActionStepLimitExceeded,
+		},
+		{
+			name: "merge_with_two_outgoing_successions_is_refused",
+			body: `
+				first start;
+				merge m;
+				action b; action c;
+				succession first start then m;
+				succession first m then b;
+				succession first m then c;
+			`,
+			want: ErrInvalidActionFlow,
+		},
+	}
+	for _, tc := range cases {
+		t.Run(tc.name, func(t *testing.T) {
+			src := "package test {\n private import ScalarValues::*;\n action fan {" + tc.body + "}\n}"
+			idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, src))
+			if tc.steps > 0 {
+				ctx.maxActionSteps = tc.steps
+			}
+			sym := findSymbolByName(idx.DocumentRoot("<test>"), "fan", ast.DefAction)
+			if sym == nil {
+				t.Fatal("action fan not found")
+			}
+			if _, err := ctx.ExecuteAction(sym); !errors.Is(err, tc.want) {
+				t.Fatalf("ExecuteAction err = %v, want %v", err, tc.want)
+			}
+		})
+	}
+}
diff --git a/internal/exec/runtime/robustness_test.go b/internal/exec/runtime/robustness_test.go
index 517d9de09f..aa9d60d3f0 100644
--- a/internal/exec/runtime/robustness_test.go
+++ b/internal/exec/runtime/robustness_test.go
@@ -1397,14 +1397,16 @@ func testBindingNestedContainerIsNotACycle(t *testing.T) {
 }
 
 // testSuccessionGuardFailureModes: a guard on a succession leaving an ordinary
-// action node is evaluated, so its failure modes — a value that is not Boolean,
-// a guard nothing supplies a name for, and two guards holding at once — are each
-// reported as a typed error rather than a panic, a hang or a chosen branch.
+// action node is evaluated, so its failure modes — a value that is not Boolean and
+// a guard nothing supplies a name for — are each reported as a typed error rather
+// than a panic or a hang. Two guards holding at once are no failure: each
+// succession is its own HappensBefore link, so both targets are performed.
 func testSuccessionGuardFailureModes(t *testing.T) {
 	for _, tc := range []struct {
-		name string
-		body string
-		want error
+		name    string
+		body    string
+		want    error
+		results map[string]int64
 	}{
 		{
 			name: "guard is not a boolean",
@@ -1440,7 +1442,7 @@ func testSuccessionGuardFailureModes(t *testing.T) {
 				succession first check if level > 10 then alert;
 				succession first check if level > 5 then idle;
 			`,
-			want: ErrAmbiguousSuccession,
+			results: map[string]int64{"high": 1, "low": 1},
 		},
 	} {
 		t.Run(tc.name, func(t *testing.T) {
@@ -1458,7 +1460,12 @@ func testSuccessionGuardFailureModes(t *testing.T) {
 						done <- fmt.Errorf("panic: %v", r)
 					}
 				}()
-				_, err := ctx.ExecuteAction(sym)
+				results, err := ctx.ExecuteAction(sym)
+				for name, want := range tc.results {
+					if got, ok := results[name]; err == nil && (!ok || got.Const.Int != want) {
+						err = fmt.Errorf("%s = %v, want %d", name, got, want)
+					}
+				}
 				done <- err
 			}()
 			select {
@@ -6873,20 +6880,24 @@ func testActionWhoseLastNodeHasNoSuccession(t *testing.T) {
 }
 
 // testFirstNodeWithASecondSuccession: `first s1 then s2;` is a succession out of
-// s1, so a second succession out of that node is ambiguous.
+// s1, so a second succession out of that node is a second HappensBefore link
+// from it, and both s2 and s3 are performed after s1.
 func testFirstNodeWithASecondSuccession(t *testing.T) {
 	src := `
 		package test {
+			private import ScalarValues::*;
 			action seq {
+				attribute two : Integer = 0;
+				attribute three : Integer = 0;
 				action s1;
-				action s2;
-				action s3;
+				action s2 { assign two := 2; }
+				action s3 { assign three := 3; }
 				first s1 then s2;
 				succession first s1 then s3;
 			}
 		}
 	`
-	idx, _, ctx := buildRuntime(t, "<test>", parseAndBuild(t, src))
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, src))
 
 	sym := findSymbolByName(idx.DocumentRoot("<test>"), "seq", ast.DefAction)
 	if sym == nil {
@@ -6898,12 +6909,12 @@ func testFirstNodeWithASecondSuccession(t *testing.T) {
 		t.Fatalf("create action executor: %v", err)
 	}
 
-	err = exec.RunToCompletion()
-	if err == nil {
-		t.Fatal("a first node with two successions ran to completion")
+	if err := exec.RunToCompletion(); err != nil {
+		t.Fatalf("a first node with two successions: %v", err)
 	}
-	if !strings.Contains(err.Error(), "multiple successors") {
-		t.Fatalf("error = %q, want it to report multiple successors", err)
+	results := exec.Results()
+	if results["two"].Const.Int != 2 || results["three"].Const.Int != 3 {
+		t.Fatalf("two = %v, three = %v, want both successors performed", results["two"], results["three"])
 	}
 }
 
diff --git a/internal/exec/runtime/testdata/conformance/README.md b/internal/exec/runtime/testdata/conformance/README.md
index 63640e62e8..70a85803e3 100644
--- a/internal/exec/runtime/testdata/conformance/README.md
+++ b/internal/exec/runtime/testdata/conformance/README.md
@@ -184,6 +184,12 @@ a case that hits it fails with a message telling the author to raise it:
   a model with more linearizations than the default covers, never to an outcome
   the set is missing: an unlisted outcome is a derivation to add to the oracle
   or a bug to fix.
+- `solverBudget`: optional beside `outcomes`, `{"moves": N}` with N at least 1. The
+  SMT referee (`TestRefereeCorpus`) encodes the case's action to N moves instead of
+  the engine's default 40. State it only for a case whose every run ends well within
+  N moves but whose default unrolling the solver cannot decide within the referee's
+  timeout; the referee's completion query still proves every run ends within N, so a
+  budget too low fails the case rather than hiding behavior.
 
 `TestExecutionConformance` explores cases with `outcomes`; the check corpus can
 also explore a single-result case with a `.check.expected.json` entry. The
diff --git a/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.check.expected.json b/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.check.expected.json
new file mode 100644
index 0000000000..a78dc61d87
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.check.expected.json
@@ -0,0 +1,5 @@
+{
+	"verdict": "divergent",
+	"divergent": {"x": ["1", "2"]},
+	"agreed": {}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.expected.json b/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.expected.json
new file mode 100644
index 0000000000..c83b9e1fe2
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.expected.json
@@ -0,0 +1,9 @@
+{
+	"libraries": true,
+	"type": "action",
+	"outcomes": [
+		{"outputs": {"x": {"type": "Integer", "value": 1}}},
+		{"outputs": {"x": {"type": "Integer", "value": 2}}}
+	],
+	"admissible": "Concurrent branches writing one feature: the value is open, the writes are not"
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.sysml b/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.sysml
new file mode 100644
index 0000000000..508c3c3082
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.sysml
@@ -0,0 +1,26 @@
+package test {
+	private import ScalarValues::*;
+
+	// A fork with one outgoing succession still replaces the token it receives,
+	// beside the outer fork's live branch w; which of r and w writes x last is open.
+	action oneBranch {
+		attribute x : Integer = 0;
+
+		first start;
+		then fork f;
+		action p;
+		fork g;
+		action r { assign x := 1; }
+		action w { assign x := 2; }
+		join j;
+		done;
+
+		succession first f then p;
+		succession first f then w;
+		succession first p then g;
+		succession first g then r;
+		succession first r then j;
+		succession first w then j;
+		succession first j then done;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.expected.json b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.expected.json
new file mode 100644
index 0000000000..0b62730841
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.expected.json
@@ -0,0 +1,9 @@
+{
+	"libraries": true,
+	"type": "action",
+	"outputs": {
+		"sum": {"type": "Integer", "value": 3},
+		"seenByQ": {"type": "Integer", "value": 3},
+		"seenByR": {"type": "Integer", "value": 3}
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.sysml b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.sysml
new file mode 100644
index 0000000000..fd36f11929
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.sysml
@@ -0,0 +1,17 @@
+package test {
+	private import ScalarValues::*;
+
+	// Two successions out of a repeated step, each with written end multiplicities:
+	// all three performances of a precede the one of q and the one of r.
+	action def FanOut {
+		attribute sum : Integer = 0;
+		attribute seenByQ : Integer = 0;
+		attribute seenByR : Integer = 0;
+		action a[3] { assign sum := sum + 1; }
+		action q { assign seenByQ := sum; }
+		action r { assign seenByR := sum; }
+		succession first start then a;
+		succession first [*] a then [1] q;
+		succession first [*] a then [1] r;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.expected.json b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.expected.json
new file mode 100644
index 0000000000..c68fd214b0
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.expected.json
@@ -0,0 +1,5 @@
+{
+	"libraries": true,
+	"type": "action",
+	"error": "the succession's end multiplicities exclude the declared step count"
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.sysml b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.sysml
new file mode 100644
index 0000000000..0b1caf92a3
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.sysml
@@ -0,0 +1,16 @@
+package test {
+	private import ScalarValues::*;
+
+	// A plain `then` out of a repeated step does not say whether one performance of
+	// its target follows every performance of a or one each; fanning out to two
+	// targets leaves each edge as open as one does, so the order is refused.
+	action def FanOutPlain {
+		attribute sum : Integer = 0;
+		action a[3] { assign sum := sum + 1; }
+		action q;
+		action r;
+		succession first start then a;
+		succession first a then q;
+		succession first a then r;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.expected.json b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.expected.json
new file mode 100644
index 0000000000..0a59a20f2f
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.expected.json
@@ -0,0 +1,9 @@
+{
+	"libraries": true,
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"c": {"type": "Integer", "value": 7},
+		"d": {"type": "Integer", "value": 8}
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.sysml b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.sysml
new file mode 100644
index 0000000000..ce641f40ee
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.sysml
@@ -0,0 +1,16 @@
+package test {
+	private import ScalarValues::*;
+
+	// A [0] step is no performance, so nothing waits on it: both of its successors
+	// still run, each once.
+	action def ZeroFanOut {
+		attribute c : Integer = 0;
+		attribute d : Integer = 0;
+		first start then a;
+		action a[0];
+		then q;
+		then r;
+		action q { assign c := 7; }
+		action r { assign d := 8; }
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.trace.golden b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.trace.golden
new file mode 100644
index 0000000000..98be0cefbe
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.trace.golden
@@ -0,0 +1,8 @@
+step 1: token 1@a
+step 2: token 2@q, token 3@r
+stmt assign d
+  eval literal 8 -> 8
+stmt assign c
+  eval literal 7 -> 7
+choice step 3: tokens 2@q, 3@r (unordered; took 3@r first)
+step 3: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.expected.json
new file mode 100644
index 0000000000..1c6323f000
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.expected.json
@@ -0,0 +1,13 @@
+{
+	"libraries": true,
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"runs": {"type": "Integer", "value": 1},
+		"got": {"type": "Integer", "value": 21},
+		"doubled": {"type": "Integer", "value": 42},
+		"p.v": {"type": "Integer", "value": 21},
+		"q.v": {"type": "Integer", "value": 21},
+		"r.v": {"type": "Integer", "value": 21}
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.sysml b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.sysml
new file mode 100644
index 0000000000..2a884be7aa
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.sysml
@@ -0,0 +1,22 @@
+package test {
+	private import ScalarValues::*;
+
+	// p is one performance with two successions out of it, so its output is moved
+	// once, before its token splits, and each flow out of it delivers to its own
+	// target's pin.
+	action pipe {
+		attribute runs : Integer = 0;
+		attribute got : Integer = 0;
+		attribute doubled : Integer = 0;
+
+		first start;
+		then action p { out v : Integer; assign v := 21; assign runs := runs + 1; }
+		action q { in v : Integer; assign got := v; }
+		action r { in v : Integer; assign doubled := v * 2; }
+
+		succession first p then q;
+		succession first p then r;
+		flow p.v to q.v;
+		flow p.v to r.v;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.trace.golden
new file mode 100644
index 0000000000..c73dfaa38e
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.trace.golden
@@ -0,0 +1,16 @@
+step 1: token 1@p
+stmt assign v
+  eval literal 21 -> 21
+stmt assign runs
+    eval feature runs -> 0
+    eval literal 1 -> 1
+  eval operator + -> 1
+step 2: token 2@q, token 3@r
+stmt assign doubled
+    eval feature v -> 21
+    eval literal 2 -> 2
+  eval operator * -> 42
+stmt assign got
+  eval feature v -> 21
+choice step 3: tokens 2@q, 3@r (unordered; took 3@r first)
+step 3: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.expected.json
new file mode 100644
index 0000000000..1dac1f3fc5
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.expected.json
@@ -0,0 +1,9 @@
+{
+	"libraries": true,
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"x": {"type": "Integer", "value": 1},
+		"y": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.sysml b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.sysml
new file mode 100644
index 0000000000..6b07a0d8b1
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.sysml
@@ -0,0 +1,16 @@
+package test {
+	private import ScalarValues::*;
+
+	// Two successions out of the start node: each target is performed once.
+	action twoFirsts {
+		attribute x : Integer = 0;
+		attribute y : Integer = 0;
+
+		action a assign x := 1;
+		action b assign y := 1;
+
+		first start;
+		succession first start then a;
+		succession first start then b;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.trace.golden
new file mode 100644
index 0000000000..4b792641d0
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.trace.golden
@@ -0,0 +1,7 @@
+step 1: token 2@a, token 3@b
+stmt assign y
+  eval literal 1 -> 1
+stmt assign x
+  eval literal 1 -> 1
+choice step 2: tokens 2@a, 3@b (unordered; took 3@b first)
+step 2: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.expected.json
new file mode 100644
index 0000000000..de02d3f1fa
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.expected.json
@@ -0,0 +1,11 @@
+{
+	"libraries": true,
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"armed": {"type": "Integer", "value": 0},
+		"bRan": {"type": "Boolean", "value": false},
+		"cRan": {"type": "Boolean", "value": true},
+		"hits": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.sysml b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.sysml
new file mode 100644
index 0000000000..167e1c63f0
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.sysml
@@ -0,0 +1,26 @@
+package test {
+	private import ScalarValues::*;
+
+	// A false guard on one of two successions out of an ordinary node leaves out
+	// only that HappensBefore link (transitionLink : HappensBefore[0..1]): c is
+	// performed, b is not. d, which both branches reach, awaits only what can still
+	// reach it, as behind a fork branch a guard pruned, so it performs once after c.
+	action pruned {
+		attribute armed : Integer = 0;
+		attribute bRan : Boolean = false;
+		attribute cRan : Boolean = false;
+		attribute hits : Integer = 0;
+
+		first start;
+		then action a;
+		action b { assign bRan := true; }
+		action c { assign cRan := true; }
+		action d { assign hits := hits + 1; }
+
+		succession first a if armed > 0 then b;
+		succession first a then c;
+		succession first b then d;
+		succession first c then d;
+		succession first d then done;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.trace.golden
new file mode 100644
index 0000000000..b98a6a7a40
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.trace.golden
@@ -0,0 +1,14 @@
+step 1: token 1@a
+  eval feature armed -> 0
+  eval literal 0 -> 0
+eval operator > -> false
+step 2: token 1@c
+stmt assign cRan
+  eval literal true -> true
+step 3: token 1@d
+stmt assign hits
+    eval feature hits -> 0
+    eval literal 1 -> 1
+  eval operator + -> 1
+step 4: token 1@done
+step 5: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.check.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.check.expected.json
new file mode 100644
index 0000000000..7a1ae42731
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.check.expected.json
@@ -0,0 +1,5 @@
+{
+	"verdict": "divergent",
+	"divergent": {"x": ["1", "2"]},
+	"agreed": {"armed": "false"}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.expected.json
new file mode 100644
index 0000000000..83239ab9e9
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.expected.json
@@ -0,0 +1,10 @@
+{
+	"libraries": true,
+	"type": "action",
+	"solverBudget": {"moves": 20},
+	"outcomes": [
+		{"outputs": {"armed": {"type": "Boolean", "value": false}, "x": {"type": "Integer", "value": 1}}},
+		{"outputs": {"armed": {"type": "Boolean", "value": false}, "x": {"type": "Integer", "value": 2}}}
+	],
+	"admissible": "Several successions out of an ordinary action node: every target follows, in which order is open"
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.sysml b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.sysml
new file mode 100644
index 0000000000..ba34393a4e
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.sysml
@@ -0,0 +1,28 @@
+package test {
+	private import ScalarValues::*;
+
+	// Two successions out of the ordinary node p, one guard false: only the link to
+	// r exists, so p's performance is followed by r alone, beside the fork's other
+	// branch w; which of r and w writes x last is open.
+	action oneHolds {
+		attribute armed : Boolean = false;
+		attribute x : Integer = 0;
+
+		first start;
+		then fork f;
+		action p;
+		action q { assign x := 3; }
+		action r { assign x := 1; }
+		action w { assign x := 2; }
+		join j;
+		done;
+
+		succession first f then p;
+		succession first f then w;
+		succession first p if armed then q;
+		succession first p then r;
+		succession first r then j;
+		succession first w then j;
+		succession first j then done;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.expected.json
new file mode 100644
index 0000000000..27bece4079
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.expected.json
@@ -0,0 +1,10 @@
+{
+	"libraries": true,
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"bRan": {"type": "Boolean", "value": true},
+		"cRan": {"type": "Boolean", "value": true},
+		"hits": {"type": "Integer", "value": 1}
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.sysml b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.sysml
new file mode 100644
index 0000000000..b78d78c77f
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.sysml
@@ -0,0 +1,26 @@
+package test {
+	private import ScalarValues::*;
+
+	// Two successions out of an ordinary action node are two HappensBefore links
+	// (Occurrences.kerml): each orders a before its target and neither selects or
+	// excludes the other, so b and c are both performed, unordered relative to each
+	// other. d, reached over two successions and declaring no multiplicity, is one
+	// performance after both.
+	action fanOut {
+		attribute bRan : Boolean = false;
+		attribute cRan : Boolean = false;
+		attribute hits : Integer = 0;
+
+		first start;
+		then action a;
+		action b { assign bRan := true; }
+		action c { assign cRan := true; }
+		action d { assign hits := hits + 1; }
+
+		succession first a then b;
+		succession first a then c;
+		succession first b then d;
+		succession first c then d;
+		succession first d then done;
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.golden
new file mode 100644
index 0000000000..f85a173310
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.golden
@@ -0,0 +1,14 @@
+step 1: token 1@a
+step 2: token 2@b, token 3@c
+stmt assign cRan
+  eval literal true -> true
+stmt assign bRan
+  eval literal true -> true
+choice step 3: tokens 2@b, 3@c (unordered; took 3@c first)
+step 3: token 2@d, token 3@d
+stmt assign hits
+    eval feature hits -> 0
+    eval literal 1 -> 1
+  eval operator + -> 1
+step 4: token 4@done
+step 5: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.order b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.order
new file mode 100644
index 0000000000..20984110dc
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.order
@@ -0,0 +1,5 @@
+# a precedes both of its targets; d follows both.
+a < b
+a < c
+b < d
+c < d
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.expected.json
new file mode 100644
index 0000000000..0e1ff96bd0
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.expected.json
@@ -0,0 +1,10 @@
+{
+	"libraries": true,
+	"type": "action",
+	"trace": true,
+	"outputs": {
+		"x": {"type": "Integer", "value": 1},
+		"bRan": {"type": "Boolean", "value": true},
+		"cRan": {"type": "Boolean", "value": true}
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.sysml b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.sysml
new file mode 100644
index 0000000000..e383f0e95d
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.sysml
@@ -0,0 +1,18 @@
+package test {
+	private import ScalarValues::*;
+
+	// A statement node is a step like any other: two successions out of an `if`
+	// node are two HappensBefore links, so both b and c follow it.
+	action branches {
+		attribute x : Integer = 0;
+		attribute bRan : Boolean = false;
+		attribute cRan : Boolean = false;
+
+		first start;
+		then if x == 0 { assign x := 1; }
+		then b;
+		then c;
+		action b { assign bRan := true; }
+		action c { assign cRan := true; }
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.trace.golden
new file mode 100644
index 0000000000..0e60967f0e
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.trace.golden
@@ -0,0 +1,14 @@
+step 1: token 1@if
+stmt if
+    eval feature x -> 0
+    eval literal 0 -> 0
+  eval operator == -> true
+  stmt assign x
+    eval literal 1 -> 1
+step 2: token 2@b, token 3@c
+stmt assign cRan
+  eval literal true -> true
+stmt assign bRan
+  eval literal true -> true
+choice step 3: tokens 2@b, 3@c (unordered; took 3@c first)
+step 3: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.check.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.check.expected.json
new file mode 100644
index 0000000000..114183a029
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.check.expected.json
@@ -0,0 +1,5 @@
+{
+	"verdict": "divergent",
+	"divergent": {"x": ["1", "2"]},
+	"agreed": {"leftRan": "true", "rightRan": "true"}
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.declared.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.declared.trace.golden
new file mode 100644
index 0000000000..5f744d0343
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.declared.trace.golden
@@ -0,0 +1,15 @@
+step 1: token 1@split
+step 2: token 2@left, token 3@right
+stmt assign x
+  eval literal 1 -> 1
+stmt assign leftRan
+  eval literal true -> true
+stmt assign x
+  eval literal 2 -> 2
+stmt assign rightRan
+  eval literal true -> true
+choice step 3: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 2 by token 3 stood)
+choice step 3: tokens 2@left, 3@right (unordered; took 2@left first)
+step 3: token 2@sync, token 3@sync
+step 4: token 4@done
+step 5: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.expected.json
new file mode 100644
index 0000000000..e8f6d01cf2
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.expected.json
@@ -0,0 +1,22 @@
+{
+	"libraries": true,
+	"type": "action",
+	"trace": true,
+	"outcomes": [
+		{
+			"outputs": {
+				"x": {"type": "Integer", "value": 1},
+				"leftRan": {"type": "Boolean", "value": true},
+				"rightRan": {"type": "Boolean", "value": true}
+			}
+		},
+		{
+			"outputs": {
+				"x": {"type": "Integer", "value": 2},
+				"leftRan": {"type": "Boolean", "value": true},
+				"rightRan": {"type": "Boolean", "value": true}
+			}
+		}
+	],
+	"admissible": "Several successions out of an ordinary action node: every target follows, in which order is open"
+}
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.seed-1.trace.golden
new file mode 100644
index 0000000000..5f744d0343
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.seed-1.trace.golden
@@ -0,0 +1,15 @@
+step 1: token 1@split
+step 2: token 2@left, token 3@right
+stmt assign x
+  eval literal 1 -> 1
+stmt assign leftRan
+  eval literal true -> true
+stmt assign x
+  eval literal 2 -> 2
+stmt assign rightRan
+  eval literal true -> true
+choice step 3: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 2 by token 3 stood)
+choice step 3: tokens 2@left, 3@right (unordered; took 2@left first)
+step 3: token 2@sync, token 3@sync
+step 4: token 4@done
+step 5: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.sysml b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.sysml
new file mode 100644
index 0000000000..ae93090284
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.sysml
@@ -0,0 +1,26 @@
+package test {
+	private import ScalarValues::*;
+
+	// The fan-out counterpart of a fork whose branches write one feature: two
+	// successions out of the ordinary node split order it before left and right,
+	// and nothing orders left against right, so which write of x stands is open.
+	action clash {
+		attribute x : Integer = 0;
+		attribute leftRan : Boolean = false;
+		attribute rightRan : Boolean = false;
+
+		first start;
+		action split;
+		action left { assign x := 1; assign leftRan := true; }
+		action right { assign x := 2; assign rightRan := true; }
+		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/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.golden
new file mode 100644
index 0000000000..cb0367a36f
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.golden
@@ -0,0 +1,15 @@
+step 1: token 1@split
+step 2: token 2@left, token 3@right
+stmt assign x
+  eval literal 2 -> 2
+stmt assign rightRan
+  eval literal true -> true
+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/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.order b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.order
new file mode 100644
index 0000000000..dd2a2433be
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.order
@@ -0,0 +1,5 @@
+# The ordinary node precedes both of its targets; the join waits for both.
+split < left
+split < right
+left < sync
+right < sync
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.expected.json b/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.expected.json
index c3249d9fef..238237257a 100644
--- a/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.expected.json
+++ b/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.expected.json
@@ -1,4 +1,9 @@
 {
 	"type": "action",
-	"error": "has multiple successors"
+	"trace": true,
+	"outputs": {
+		"level": {"type": "Integer", "value": 12},
+		"low": {"type": "Integer", "value": 1},
+		"high": {"type": "Integer", "value": 1}
+	}
 }
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.sysml b/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.sysml
index e2ae6da0a6..93e47e47f5 100644
--- a/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.sysml
+++ b/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.sysml
@@ -1,7 +1,10 @@
 package test {
 	// Two guarded successions out of one ordinary action node whose guards both
-	// hold: which one wins is not stated by the notation, so neither is chosen and
-	// the ambiguity is reported. A model that means a choice writes a decision.
+	// hold. Each guarded succession is its own transition performance whose guard
+	// constrains only its own HappensBefore link (TransitionPerformances.kerml,
+	// NonStateTransitionPerformance, transitionLink : HappensBefore[0..1]), and
+	// only a decision makes its successions exclusive (DecisionPerformance). So
+	// neither link excludes the other: both alert and idle are performed after check.
 	action route {
 		attribute level : Integer = 12;
 		attribute low : Integer = 0;
diff --git a/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.trace.golden b/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.trace.golden
new file mode 100644
index 0000000000..a7b877fdd3
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.trace.golden
@@ -0,0 +1,15 @@
+stmt assign level
+  eval feature level -> 12
+  eval feature level -> 12
+  eval literal 10 -> 10
+eval operator > -> true
+  eval feature level -> 12
+  eval literal 5 -> 5
+eval operator > -> true
+step 1: token 2@alert, token 3@idle
+stmt assign low
+  eval literal 1 -> 1
+stmt assign high
+  eval literal 1 -> 1
+choice step 2: tokens 2@alert, 3@idle (unordered; took 3@idle first)
+step 2: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/object_flow_implicit_fork.trace.golden b/internal/exec/runtime/testdata/conformance/object_flow_implicit_fork.trace.golden
index 857254be3b..306bffb402 100644
--- a/internal/exec/runtime/testdata/conformance/object_flow_implicit_fork.trace.golden
+++ b/internal/exec/runtime/testdata/conformance/object_flow_implicit_fork.trace.golden
@@ -1,6 +1,6 @@
 step 1: token 1@produce
 stmt assign y
   eval literal 5.0 -> 5.0
-step 2: token 1@left, token 2@right
-choice step 3: tokens 1@left, 2@right (unordered; took 2@right first)
+step 2: token 2@left, token 3@right
+choice step 3: tokens 2@left, 3@right (unordered; took 3@right first)
 step 3: no active tokens
diff --git a/internal/exec/runtime/testdata/conformance/object_flow_queued_value_control_arrival.trace.golden b/internal/exec/runtime/testdata/conformance/object_flow_queued_value_control_arrival.trace.golden
index 9e748a20b6..c61fa11989 100644
--- a/internal/exec/runtime/testdata/conformance/object_flow_queued_value_control_arrival.trace.golden
+++ b/internal/exec/runtime/testdata/conformance/object_flow_queued_value_control_arrival.trace.golden
@@ -1,28 +1,28 @@
 step 1: token 1@a
 stmt assign y
   eval literal 7 -> 7
-step 2: token 1@b, token 2@b
+step 2: token 2@b, token 3@b
 stmt assign runs
     eval feature runs -> 0
     eval literal 1 -> 1
   eval operator + -> 1
 stmt assign took
   eval feature v -> 7
-step 3: token 3@check
+step 3: token 4@check
   eval feature runs -> 1
   eval literal 2 -> 2
 eval operator < -> true
-step 4: token 3@c
-step 5: token 3@b
+step 4: token 4@c
+step 5: token 4@b
 stmt assign runs
     eval feature runs -> 1
     eval literal 1 -> 1
   eval operator + -> 2
 stmt assign took
   eval feature v -> 7
-step 6: token 3@check
+step 6: token 4@check
   eval feature runs -> 2
   eval literal 2 -> 2
 eval operator < -> false
-step 7: token 3@done
+step 7: token 4@done
 step 8: no active tokens
diff --git a/internal/exec/smt/encode.go b/internal/exec/smt/encode.go
index 99444af2ab..0bd1a37e4a 100644
--- a/internal/exec/smt/encode.go
+++ b/internal/exec/smt/encode.go
@@ -1007,11 +1007,15 @@ func (e *Encoding) tokens(t, n int, node ast.Node, prev, next *State, m *Move, g
 	case *ast.FinalNode:
 		s.terms = append(s.terms, s.retire())
 	case *ast.ForkNode:
-		s.fork()
+		s.fork(false)
 	case *ast.DecisionNode:
 		s.decide()
 	default:
-		s.succeed()
+		if e.Flow.fansOut(node) {
+			s.fork(true)
+		} else {
+			s.succeed()
+		}
 	}
 	s.others()
 	s.terms = append(s.terms, eq(solve.VarTerm(next.NextID), s.nextID))
@@ -1096,8 +1100,8 @@ func (s *tokenStep) stay() *solve.Term {
 }
 
 // fork gives each enabled succession a fresh token, in order: the first in the
-// actor's slot, the rest in the free slots in order.
-func (s *tokenStep) fork() {
+// actor's slot, the rest in the free slots in order. keepsOne moves a lone token on.
+func (s *tokenStep) fork(keepsOne bool) {
 	e, f, out, prev, next := s.e, s.e.Flow, s.out, s.prev, s.next
 	guards := s.guards.holds
 	rank := make([]*solve.Term, len(out))
@@ -1107,6 +1111,11 @@ func (s *tokenStep) fork() {
 		count = add(count, ite(guards[p], solve.IntTerm(1), solve.IntTerm(0)))
 	}
 	none := eq(count, solve.IntTerm(0))
+	// An ordinary node moves its token on when one succession is enabled; a fork always replaces it.
+	moves := solve.BoolTerm(false)
+	if keepsOne {
+		moves = eq(count, solve.IntTerm(1))
+	}
 	var actor []*solve.Term
 	for p := range out {
 		edge := f.Edges[out[p]]
@@ -1114,7 +1123,7 @@ func (s *tokenStep) fork() {
 		actor = append(actor, implies(isFirst, and(
 			eq(solve.VarTerm(next.Slots[s.t].At), nodeValue(e.Sorts, f, f.Index[edge.Target])),
 			eq(solve.VarTerm(next.Slots[s.t].Via), edgeValue(e.Sorts, f, out[p])),
-			eq(solve.VarTerm(next.Slots[s.t].ID), s.base),
+			eq(solve.VarTerm(next.Slots[s.t].ID), ite(moves, s.actorID, s.base)),
 			eq(s.travel, edgeValue(e.Sorts, f, out[p])))))
 	}
 	s.terms = append(s.terms, implies(none, s.retire()), implies(not(none), and(actor...)))
@@ -1143,7 +1152,7 @@ func (s *tokenStep) fork() {
 		}
 		s.placed[u] = and(s.free[u], or(here...))
 	}
-	s.nextID = add(s.base, count)
+	s.nextID = ite(moves, s.base, add(s.base, count))
 	s.fails = or(undefinedGuards(s.guards.defined)...)
 	if f.Cyclic {
 		s.full = gt(count, add(running, solve.IntTerm(1)))
@@ -1191,25 +1200,16 @@ func (s *tokenStep) decide() {
 	s.fails = or(undefined...)
 }
 
-// succeed takes the one enabled succession; none retires the token; several
-// out of a node other than the initial one is an error.
+// succeed takes the node's one succession where its guard holds and retires the
+// token otherwise; a node with several fans out instead.
 func (s *tokenStep) succeed() {
-	guards := s.guards.holds
-	_, initial := s.node.(*ast.InitialNode)
-	count := solve.IntTerm(0)
 	taken := solve.BoolTerm(false)
 	for p := range s.out {
-		isFirst := and(guards[p], not(taken))
-		s.terms = append(s.terms, implies(isFirst, s.take(p)))
-		taken = or(taken, guards[p])
-		count = add(count, ite(guards[p], solve.IntTerm(1), solve.IntTerm(0)))
+		s.terms = append(s.terms, implies(s.guards.holds[p], s.take(p)))
+		taken = s.guards.holds[p]
 	}
 	s.terms = append(s.terms, implies(not(taken), s.retire()))
-	failures := undefinedGuards(s.guards.defined)
-	if !initial && len(s.out) > 1 {
-		failures = append(failures, gt(count, solve.IntTerm(1)))
-	}
-	if len(failures) > 0 {
+	if failures := undefinedGuards(s.guards.defined); len(failures) > 0 {
 		s.fails = or(failures...)
 	}
 }
diff --git a/internal/exec/smt/encode_test.go b/internal/exec/smt/encode_test.go
index 8f1b09ca35..6fb1966443 100644
--- a/internal/exec/smt/encode_test.go
+++ b/internal/exec/smt/encode_test.go
@@ -167,6 +167,82 @@ func TestEncodeForkJoinCompletes(t *testing.T) {
 	}
 }
 
+// TestEncodeFanOutJoinCompletes: two successions out of an ordinary node are
+// encoded as a fork's are, so both branches run and the join completes.
+func TestEncodeFanOutJoinCompletes(t *testing.T) {
+	solver := requireSolver(t)
+	src := `package test {
+	private import ScalarValues::*;
+	action clash {
+		attribute leftRan : Boolean = false;
+		attribute rightRan : Boolean = false;
+		first start;
+		action split;
+		action left { assign leftRan := true; }
+		action right { assign rightRan := true; }
+		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;
+	}
+}`
+	ctx, action, graph, held := loweredAction(t, src, "test::clash")
+	const k = 7
+	enc, err := Encode(ctx, action, graph, held, nil, k, DefaultUnroll)
+	if err != nil {
+		t.Fatalf("encode: %v", err)
+	}
+	fans := false
+	for _, node := range graph.Nodes {
+		fans = fans || (nodeLabel(node) == "split" && enc.Flow.fansOut(node))
+	}
+	if !fans {
+		t.Fatal("split is not encoded as a fan-out")
+	}
+	q := *enc.Query
+	q.Assertions = append(q.Assertions, solve.Assertion{Term: enc.Completed[k]})
+	result, err := solver.Solve(context.Background(), &q)
+	if err != nil {
+		t.Fatalf("solve: %v\n%s", err, solve.Script(&q))
+	}
+	if result.Status != solve.StatusSat {
+		t.Fatalf("status %v, want sat\n%s", result.Status, solve.Script(&q))
+	}
+	last := enc.States[k]
+	for _, base := range enc.Features {
+		v := last.value(base)
+		if assigned(t, result, v.Name) != "true" {
+			t.Errorf("%s = %s at move %d, want true", v.Name, assigned(t, result, v.Name), k)
+		}
+	}
+}
+
+// TestEncodeFanOutPlainRejoinRefused: a plain node both branches of a fan-out
+// reach synchronizes as the interpreter does, which the encoding does not cover.
+func TestEncodeFanOutPlainRejoinRefused(t *testing.T) {
+	src := `package test {
+	action fan {
+		first start;
+		then action a;
+		action b; action c; action d;
+		succession first a then b;
+		succession first a then c;
+		succession first b then d;
+		succession first c then d;
+	}
+}`
+	ctx, action, graph, held := loweredAction(t, src, "test::fan")
+	_, err := Encode(ctx, action, graph, held, nil, 8, DefaultUnroll)
+	var unsupported *UnsupportedError
+	if !errors.As(err, &unsupported) || unsupported.Construct != "implicit join" {
+		t.Fatalf("encode err = %v, want the implicit join refused", err)
+	}
+}
+
 // status solves enc's query with the completion at k and extra asserted.
 func status(t *testing.T, solver *solve.Solver, enc *Encoding, k int, extra *solve.Term) solve.Status {
 	t.Helper()
diff --git a/internal/exec/smt/referee_test.go b/internal/exec/smt/referee_test.go
index e4b262b43b..3b5c6fdb55 100644
--- a/internal/exec/smt/referee_test.go
+++ b/internal/exec/smt/referee_test.go
@@ -43,6 +43,9 @@ type corpusCase struct {
 		Runs  *int `json:"runs"`
 		Depth *int `json:"depth"`
 	} `json:"exploreBudget"`
+	SolverBudget *struct {
+		Moves *int `json:"moves"`
+	} `json:"solverBudget"`
 }
 
 // refereeCases are the action cases of the corpus that list outcomes, by name.
@@ -262,7 +265,7 @@ func TestRefereeInputs(t *testing.T) {
 // refereeCase holds one case to the interpreter, adding to the tally.
 func refereeCase(t *testing.T, solver *solve.Solver, name string, c corpusCase, tally *refereeTally) {
 	d, action := corpusDocument(t, name, c)
-	budget := analysis.Budget{Depth: DefaultMoves, Solver: solver.Timeout}
+	budget := analysis.Budget{Depth: c.solverMoves(), Solver: solver.Timeout}
 	encoding, refusal := encodeDocument(t, d, action, budget)
 	if refusal != nil {
 		tally.refused++
@@ -600,6 +603,14 @@ func (c corpusCase) exploreBudget() runtime.ExploreBudget {
 	return budget
 }
 
+// solverMoves is the moves a case's action is encoded to.
+func (c corpusCase) solverMoves() int {
+	if c.SolverBudget != nil && c.SolverBudget.Moves != nil {
+		return *c.SolverBudget.Moves
+	}
+	return DefaultMoves
+}
+
 // explore runs every linearization of the action under the budget.
 func explore(t *testing.T, budget runtime.ExploreBudget, fresh func() (*runtime.Context, error), action *symbols.Symbol) *runtime.Exploration {
 	t.Helper()
diff --git a/internal/exec/smt/support.go b/internal/exec/smt/support.go
index 271551fc5d..e1c166ce90 100644
--- a/internal/exec/smt/support.go
+++ b/internal/exec/smt/support.go
@@ -48,8 +48,8 @@ type Flow struct {
 	// Slots is how many tokens may be in flight at once within k moves, over
 	// every frame: the bound T.
 	Slots int
-	// Cyclic is set when a fork lies on a cycle, so the tokens in flight are
-	// bounded by k rather than by the graph, and the state records a full fork.
+	// Cyclic is set when a fan-out lies on a cycle, so the tokens in flight are
+	// bounded by k rather than by the graph, and the state records a full fan-out.
 	Cyclic bool
 	// Delivers is set when an object flow delivers to a node performing in a
 	// frame of its own, whose pin queues the deliveries it has yet to take.
@@ -342,9 +342,6 @@ func (f *Flow) checkNodeKind(node ast.Node, label string) error {
 		if n.ActionRef != nil {
 			return &UnsupportedError{Node: label, Construct: "action invocation", Reason: "a node performing another action is encoded by a later stage"}
 		}
-		if err := f.checkSuccessors(node, label, "the action node has multiple successors"); err != nil {
-			return err
-		}
 	case *ast.Usage:
 		if lower.IsCaseNode(n) {
 			return &UnsupportedError{Node: label, Construct: "case", Reason: "a nested case is not encoded"}
@@ -352,13 +349,7 @@ func (f *Flow) checkNodeKind(node ast.Node, label string) error {
 		if performsAction(n) {
 			return &UnsupportedError{Node: label, Construct: "action invocation", Reason: "a node performing another action is encoded by a later stage"}
 		}
-		if err := f.checkSuccessors(node, label, "the action node has multiple successors"); err != nil {
-			return err
-		}
 	case *ast.WhileLoopActionNode, *ast.IfActionNode, *ast.AssignmentActionNode:
-		if err := f.checkSuccessors(node, label, "the statement node has multiple successors"); err != nil {
-			return err
-		}
 	case *ast.SendStatement:
 		return &UnsupportedError{Node: label, Construct: "send", Reason: "messages are encoded by a later stage"}
 	case *ast.TerminateStatement:
@@ -369,27 +360,6 @@ func (f *Flow) checkNodeKind(node ast.Node, label string) error {
 	return nil
 }
 
-// checkSuccessors refuses a node other than a fork that several successions leave:
-// two not of succession flows are a choice the interpreter refuses, and the one beside
-// a succession flow's starts with it, as after a fork, which the stage does not encode.
-func (f *Flow) checkSuccessors(node ast.Node, label, reason string) error {
-	out := f.Outgoing[node]
-	if len(out) < 2 {
-		return nil
-	}
-	control := 0
-	for _, i := range out {
-		if !f.Edges[i].Carries {
-			control++
-		}
-	}
-	if control > 1 {
-		return &FlowError{Node: label, Reason: reason}
-	}
-	return &UnsupportedError{Node: label, Construct: "implicit fork",
-		Reason: "the successions of succession flows leaving a node start beside its other succession, which only a fork is encoded as"}
-}
-
 // checkImplicitJoin refuses a node other than a join or a merge that several
 // successions enter while forks put several tokens in flight: the interpreter
 // synchronizes it over the successions still reachable, which is not encoded.
@@ -483,29 +453,32 @@ func (f *Flow) checkBlock(graph *lower.ActionGraph, node ast.Node, label string,
 }
 
 // sizeSlots decides how many tokens the frame's flow may hold at once within k
-// moves: one, plus what each fork adds per time a token reaches it, at most k times.
+// moves: one, plus what each fan-out adds per time a token reaches it, at most k times.
 func (f *Flow) sizeSlots(fr *Frame, k int) {
 	arrivals := f.arrivals(fr, k)
 	slots, widest := 1, 0
 	for _, node := range fr.Nodes {
-		fork, ok := node.(*ast.ForkNode)
-		if !ok {
+		if !f.fansOut(node) {
 			continue
 		}
-		extra := len(f.Outgoing[fork]) - 1
-		if extra <= 0 {
-			continue
-		}
-		if f.reaches(fork, fork) {
+		extra := len(f.Outgoing[node]) - 1
+		if f.reaches(node, node) {
 			f.Cyclic = true
 		}
 		widest = max(widest, extra)
-		slots += min(arrivals[fork], k) * extra
+		slots += min(arrivals[node], k) * extra
 	}
-	// Each of the k moves performs at most one fork.
+	// Each of the k moves performs at most one fan-out.
 	fr.Slots = min(slots, 1+k*widest)
 }
 
+// fansOut reports a node a token leaves along every enabled succession of
+// several: any node but a decision, which takes one.
+func (f *Flow) fansOut(node ast.Node) bool {
+	_, decision := node.(*ast.DecisionNode)
+	return !decision && len(f.Outgoing[node]) > 1
+}
+
 // arrivals bounds how often a token may reach each node of the frame within k
 // moves: a fork or decision passes on all that reach it, a merge sums them, a
 // join passes on the most over one succession, and a cycle multiplying tokens
@@ -556,7 +529,7 @@ func (f *Flow) entering(fr *Frame, comp []ast.Node, cyclic bool, leaving map[ast
 				entering += leaving[source]
 			}
 		}
-		if _, ok := node.(*ast.ForkNode); ok && cyclic && len(f.Outgoing[node]) > 1 {
+		if cyclic && f.fansOut(node) {
 			multiplies = true
 		}
 	}
diff --git a/tests/parser/testdata/parse/action_succession_fan_out.golden b/tests/parser/testdata/parse/action_succession_fan_out.golden
new file mode 100644
index 0000000000..19a79e129b
--- /dev/null
+++ b/tests/parser/testdata/parse/action_succession_fan_out.golden
@@ -0,0 +1,35 @@
+(RootNamespace
+  (Membership visibility="default"
+    (Definition kind="action" abstract=false variation=false name="FanOut"
+      (Membership visibility="default"
+        (Usage kind="attribute" name="armed" ref=false direction="none" composite=false derived=false ordered=false nonunique=false
+          (Relationship kind="typing" target=Integer
+            (*ast.QualifiedName))
+          (LiteralInteger value="0")))
+      (InitialNode name="start" successor="")
+      (Usage kind="action" name="a" ref=false direction="none" composite=false derived=false ordered=false nonunique=false)
+      (SuccessionEdge source="start" target="a")
+      (Usage kind="action" name="b" ref=false direction="none" composite=false derived=false ordered=false nonunique=false)
+      (Usage kind="action" name="c" ref=false direction="none" composite=false derived=false ordered=false nonunique=false)
+      (Usage kind="action" name="d" ref=false direction="none" composite=false derived=false ordered=false nonunique=false)
+      (Membership visibility="default"
+        (Usage kind="succession" name="" ref=false direction="none" composite=false derived=false ordered=false nonunique=false
+          (ConnectorEnd target="a"
+            (*ast.QualifiedName))
+          (ConnectorEnd target="b"
+            (*ast.QualifiedName))))
+      (Membership visibility="default"
+        (TransitionMember source="a" target="c"
+          (OperatorExpr operator=">"
+            (FeatureReference name="armed")
+            (LiteralInteger value="0"))))
+      (InitialNode name="a" successor="d")
+      (IfActionNode
+        (OperatorExpr operator="=="
+          (FeatureReference name="armed")
+          (LiteralInteger value="0"))
+        (IfBranchNode kind="then"
+          (*ast.AssignmentActionNode)))
+      (SuccessionEdge source="a" target="@if")
+      (SuccessionEdge source="@if" target="b")
+      (SuccessionEdge source="@if" target="c"))))
\ No newline at end of file
diff --git a/tests/parser/testdata/parse/action_succession_fan_out.sysml b/tests/parser/testdata/parse/action_succession_fan_out.sysml
new file mode 100644
index 0000000000..5c6e8f24ae
--- /dev/null
+++ b/tests/parser/testdata/parse/action_succession_fan_out.sysml
@@ -0,0 +1,16 @@
+action def FanOut {
+	attribute armed : Integer = 0;
+
+	first start;
+	then action a;
+	action b;
+	action c;
+	action d;
+
+	succession first a then b;
+	succession first a if armed > 0 then c;
+	first a then d;
+	then if armed == 0 { assign armed := 1; }
+	then b;
+	then c;
+}