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

.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`.

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.

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.

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).