From 4d5eb107551933d0df460f8e53dd144590b56e25 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 00:04:13 +0000 Subject: [PATCH 1/6] fix(runtime): perform every target of several successions out of an ordinary action node Co-Authored-By: jason.han --- .agents/skills/testing-sysml-repl/SKILL.md | 8 +- .../unreleased/succession-fan-out.fixed.md | 10 ++ docs/project/behavior-semantic-oracle.md | 74 ++++++++++++ docs/project/spec-compliance.md | 5 +- internal/exec/runtime/action_executor.go | 94 +++++---------- internal/exec/runtime/action_executor_test.go | 17 +-- .../exec/runtime/action_step_multiplicity.go | 9 +- .../runtime/action_succession_fan_out_test.go | 49 ++++++++ .../robustness_succession_fan_out_test.go | 108 ++++++++++++++++++ internal/exec/runtime/robustness_test.go | 45 +++++--- ...on_step_multiplicity_fan_out.expected.json | 9 ++ .../action_step_multiplicity_fan_out.sysml | 17 +++ ...p_multiplicity_fan_out_plain.expected.json | 5 + ...tion_step_multiplicity_fan_out_plain.sysml | 16 +++ ...ep_multiplicity_zero_fan_out.expected.json | 9 ++ ...ction_step_multiplicity_zero_fan_out.sysml | 16 +++ ...tep_multiplicity_zero_fan_out.trace.golden | 8 ++ ...uccession_fan_out_data_flows.expected.json | 13 +++ ...action_succession_fan_out_data_flows.sysml | 22 ++++ ...succession_fan_out_data_flows.trace.golden | 16 +++ ...uccession_fan_out_from_start.expected.json | 9 ++ ...action_succession_fan_out_from_start.sysml | 16 +++ ...succession_fan_out_from_start.trace.golden | 7 ++ ..._fan_out_guard_pruned_rejoin.expected.json | 11 ++ ...ccession_fan_out_guard_pruned_rejoin.sysml | 26 +++++ ...n_fan_out_guard_pruned_rejoin.trace.golden | 14 +++ ...on_succession_fan_out_rejoin.expected.json | 10 ++ .../action_succession_fan_out_rejoin.sysml | 26 +++++ ...ion_succession_fan_out_rejoin.trace.golden | 14 +++ ...tion_succession_fan_out_rejoin.trace.order | 5 + ...ssion_fan_out_statement_node.expected.json | 10 ++ ...on_succession_fan_out_statement_node.sysml | 18 +++ ...ession_fan_out_statement_node.trace.golden | 14 +++ ...out_writes_one_feature.check.expected.json | 5 + ...t_writes_one_feature.declared.trace.golden | 15 +++ ...n_fan_out_writes_one_feature.expected.json | 22 ++++ ...out_writes_one_feature.seed-1.trace.golden | 15 +++ ...uccession_fan_out_writes_one_feature.sysml | 26 +++++ ...on_fan_out_writes_one_feature.trace.golden | 15 +++ ...ion_fan_out_writes_one_feature.trace.order | 5 + ...on_succession_guard_two_hold.expected.json | 7 +- .../action_succession_guard_two_hold.sysml | 7 +- ...ion_succession_guard_two_hold.trace.golden | 15 +++ internal/exec/smt/encode.go | 27 ++--- internal/exec/smt/encode_test.go | 76 ++++++++++++ internal/exec/smt/support.go | 38 +++--- .../parse/action_succession_fan_out.golden | 35 ++++++ .../parse/action_succession_fan_out.sysml | 16 +++ 48 files changed, 908 insertions(+), 146 deletions(-) create mode 100644 changes/unreleased/succession-fan-out.fixed.md create mode 100644 internal/exec/runtime/action_succession_fan_out_test.go create mode 100644 internal/exec/runtime/robustness_succession_fan_out_test.go create mode 100644 internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_step_multiplicity_fan_out_plain.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_step_multiplicity_zero_fan_out.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_data_flows.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_from_start.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_guard_pruned_rejoin.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_rejoin.trace.order create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.check.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.declared.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.seed-1.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_writes_one_feature.trace.order create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_guard_two_hold.trace.golden create mode 100644 tests/parser/testdata/parse/action_succession_fan_out.golden create mode 100644 tests/parser/testdata/parse/action_succession_fan_out.sysml diff --git a/.agents/skills/testing-sysml-repl/SKILL.md b/.agents/skills/testing-sysml-repl/SKILL.md index 1d5532d7ea..08901ba380 100644 --- a/.agents/skills/testing-sysml-repl/SKILL.md +++ b/.agents/skills/testing-sysml-repl/SKILL.md @@ -4068,10 +4068,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/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 56c9d06979..865b3e8172 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -355,6 +355,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 943b049a15..29eecd146e 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -694,12 +694,13 @@ checked after the result is bound is not a form the runtime offers, and none is | 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_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:` (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` (`.declared.trace.golden` and `.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, at body granularity (a body's statements are not interleaved). 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 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) | @@ -746,7 +747,7 @@ checked after the result is bound is not a form the runtime offers, and none is | `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. 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) | | Qualified succession at namespace level (`first part1::action1 then requirement1;`) | `parser/namespace.go` (a succession is a namespace member), `parser/succession.go` | `parse/behavior_namespace_succession.golden`, `negative_test.go:namespace_succession_no_target`, `lower/namespace_succession_test.go:TestNamespaceSuccessionHasNoTokenFlowOrNeighborGraphAttachment` | ⚠️ Approximate (parsed and carried in the AST with both ends, and pinned as a gap rather than left unobserved: lowering is behavior-owned, a namespace has no token flow to lower such a succession into, and the reproducer asserts the edge is neither dropped into nor attached to a neighbouring behavior's graph — the root cause is that `lower/` builds a graph per behavior body, so ordering two namespace members would need an owner the notation does not give) | | 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) | diff --git a/internal/exec/runtime/action_executor.go b/internal/exec/runtime/action_executor.go index 2f9599c03c..b47d152333 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 " @@ -1981,14 +1977,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. @@ -2053,8 +2043,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{ @@ -2068,13 +2078,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 @@ -2288,27 +2294,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 len(successors) > 1 { - return fmt.Errorf("%w: action node %s has multiple successors (decision nodes not yet supported)", - ErrAmbiguousSuccession, node.Name) - } // 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); err != nil { return err } - - if len(successors) == 0 { - return e.retireToken(tokenIdx) - } - - e.move(&e.tokens[tokenIdx], successors[0]) - return nil + return e.follow(tokenIdx, successors) } // stepNestedAction performs a nested action usage in a frame of its own. @@ -2452,14 +2448,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 len(successors) > 1 { - return fmt.Errorf("%w: action node %s has multiple successors", ErrAmbiguousSuccession, ActionNodeName(node)) - } // The flows out of this node carry what this performance produced to the // pins the nodes downstream read. @@ -2469,12 +2462,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. - if len(successors) == 0 { - return e.retireToken(tokenIdx) - } - - e.move(&e.tokens[tokenIdx], successors[0]) - return nil + return e.follow(tokenIdx, successors) } // triggerReady probes a change event's condition first: a test finding it not @@ -2749,33 +2737,7 @@ func (e *ActionExecutor) leaveStatementNode(tokenIdx int, frame *actionFrame, no if err != nil { return err } - if len(successors) > 1 { - return fmt.Errorf("%s node has multiple successors", statementNodeKeyword(node)) - } - if len(successors) == 0 { - return e.retireToken(tokenIdx) - } - e.move(&e.tokens[tokenIdx], successors[0]) - return nil -} - -// 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'" - 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 6231b49dfb..da5bc84fc3 100644 --- a/internal/exec/runtime/action_step_multiplicity.go +++ b/internal/exec/runtime/action_step_multiplicity.go @@ -92,14 +92,7 @@ func (e *ActionExecutor) passZeroStep(tokenIdx int, node ast.Node) error { if err != nil { return err } - if len(successors) > 1 { - return fmt.Errorf("%w: action node %s has multiple successors", ErrAmbiguousSuccession, ActionNodeName(node)) - } - if len(successors) == 0 { - return e.retireToken(tokenIdx) - } - e.move(&e.tokens[tokenIdx], successors[0]) - return nil + 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, "", parseAndBuild(t, src)) + sym := findSymbolByName(idx.DocumentRoot(""), "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/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, "", parseAndBuild(t, src)) + if tc.steps > 0 { + ctx.maxActionSteps = tc.steps + } + sym := findSymbolByName(idx.DocumentRoot(""), "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 a81394359d..d98395bff6 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 { @@ -6863,20 +6870,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, "", parseAndBuild(t, src)) + idx, _, ctx := buildRuntimeWithLibraries(t, "", parseAndBuild(t, src)) sym := findSymbolByName(idx.DocumentRoot(""), "seq", ast.DefAction) if sym == nil { @@ -6888,12 +6899,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/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_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..3130e5f1bb --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_statement_node.trace.golden @@ -0,0 +1,14 @@ +step 1: token 1@*ast.IfActionNode +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/smt/encode.go b/internal/exec/smt/encode.go index 5565b666bc..d61197b80a 100644 --- a/internal/exec/smt/encode.go +++ b/internal/exec/smt/encode.go @@ -1006,12 +1006,14 @@ func (e *Encoding) tokens(t, n int, node ast.Node, prev, next *State, m *Move, g switch node.(type) { case *ast.FinalNode: s.terms = append(s.terms, s.retire()) - case *ast.ForkNode: - s.fork() case *ast.DecisionNode: s.decide() default: - s.succeed() + if e.Flow.fansOut(node) { + s.fork() + } else { + s.succeed() + } } s.others() s.terms = append(s.terms, eq(solve.VarTerm(next.NextID), s.nextID)) @@ -1191,25 +1193,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 149101b1d3..7b414fcef6 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/support.go b/internal/exec/smt/support.go index ed4a807763..40868f24a5 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. @@ -339,9 +339,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 out > 1 { - return &FlowError{Node: label, Reason: "the action node has multiple successors"} - } case *ast.Usage: if lower.IsCaseNode(n) { return &UnsupportedError{Node: label, Construct: "case", Reason: "a nested case is not encoded"} @@ -349,13 +346,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 out > 1 { - return &FlowError{Node: label, Reason: "the action node has multiple successors"} - } case *ast.WhileLoopActionNode, *ast.IfActionNode, *ast.AssignmentActionNode: - if out > 1 { - return &FlowError{Node: label, Reason: "the statement node has multiple successors"} - } case *ast.SendStatement: return &UnsupportedError{Node: label, Construct: "send", Reason: "messages are encoded by a later stage"} case *ast.TerminateStatement: @@ -445,29 +436,32 @@ func (f *Flow) checkBlock(node ast.Node, label string, block lower.Block) error } // 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 { - continue - } - extra := len(f.Outgoing[fork]) - 1 - if extra <= 0 { + if !f.fansOut(node) { 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 @@ -518,7 +512,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; +} From 0692e61da11190963e171305b2d896d18e8ee411 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 00:14:59 +0000 Subject: [PATCH 2/6] docs(skills): note fan-out CLI checks in the REPL testing skill Co-Authored-By: jason.han --- .agents/skills/testing-sysml-repl/SKILL.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/.agents/skills/testing-sysml-repl/SKILL.md b/.agents/skills/testing-sysml-repl/SKILL.md index 08901ba380..f4ae7420ec 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 ` asks whether execution holds, not for the table + of final values. Use `-engine smt -action -check-diverge ` 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 From 028fa48f18cd31ab157d5e70c8ad2e7e08f07791 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 01:01:38 +0000 Subject: [PATCH 3/6] chore(ci): re-run checks after a transient Reference-FMUs download failure Co-Authored-By: jason.han From 8258d4c9dac7636717ffea76a7d01a581131b0ea Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 02:10:16 +0000 Subject: [PATCH 4/6] fix(smt): keep the token's identity when one succession out of an ordinary node is enabled Co-Authored-By: jason.han --- docs/project/spec-compliance.md | 2 +- ...one_branch_beside_live_token.expected.json | 9 ++++++ ...on_fork_one_branch_beside_live_token.sysml | 26 +++++++++++++++++ ...sion_fan_out_one_guard_holds.expected.json | 9 ++++++ ...n_succession_fan_out_one_guard_holds.sysml | 28 +++++++++++++++++++ internal/exec/smt/encode.go | 17 +++++++---- 6 files changed, 85 insertions(+), 6 deletions(-) create mode 100644 internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.sysml create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.sysml diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 29eecd146e..6dd1918e38 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -700,7 +700,7 @@ checked after the result is bound is not a form the runtime offers, and none is | 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_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) | +| 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:` (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` (`.declared.trace.golden` and `.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, at body granularity (a body's statements are not interleaved). 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 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) | 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_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..3ed99c5c03 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.expected.json @@ -0,0 +1,9 @@ +{ + "libraries": true, + "type": "action", + "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/smt/encode.go b/internal/exec/smt/encode.go index d61197b80a..03ae12a6ad 100644 --- a/internal/exec/smt/encode.go +++ b/internal/exec/smt/encode.go @@ -1006,11 +1006,13 @@ func (e *Encoding) tokens(t, n int, node ast.Node, prev, next *State, m *Move, g switch node.(type) { case *ast.FinalNode: s.terms = append(s.terms, s.retire()) + case *ast.ForkNode: + s.fork(false) case *ast.DecisionNode: s.decide() default: if e.Flow.fansOut(node) { - s.fork() + s.fork(true) } else { s.succeed() } @@ -1098,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)) @@ -1109,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]] @@ -1116,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...))) @@ -1145,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))) From 4da614ea84d3d84fa0d13ae54158e5ab3bd07765 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 02:36:37 +0000 Subject: [PATCH 5/6] test(smt): keep the one-guard fan-out referee case within the solver budget Co-Authored-By: jason.han --- .../conformance/action_succession_fan_out_one_guard_holds.sysml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index ba34393a4e..604390a310 100644 --- 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 @@ -11,7 +11,7 @@ package test { first start; then fork f; action p; - action q { assign x := 3; } + action q; action r { assign x := 1; } action w { assign x := 2; } join j; From 4b7de4112e99355c4b835149efd699de21dfc36c Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Sat, 3 Oct 2026 03:44:43 +0000 Subject: [PATCH 6/6] test(smt): restore the false-guard writer and give its referee case a solver budget The one-guard fan-out fixture again assigns x := 3 in q, so an engine that ignores the false guard reaches an outcome the set does not admit. The referee's completion query over the default 40 moves takes z3 about a minute locally (unsat, not unknown), and on CI it ran past the five-minute referee timeout. Every run of the case ends within 12 moves, and the solve time is heavy-tailed in the unrolling rather than in the model, so the case states "solverBudget": {"moves": 20}. The completion query still proves every run ends within that bound. Both fixtures with an admissible set that the fork-identity fix added gain the check expectations TestCheckConformanceOracles requires. Co-Authored-By: jason.han --- internal/exec/runtime/conformance_test.go | 20 +++++++++++++++++++ .../runtime/testdata/conformance/README.md | 6 ++++++ ...anch_beside_live_token.check.expected.json | 5 +++++ ...an_out_one_guard_holds.check.expected.json | 5 +++++ ...sion_fan_out_one_guard_holds.expected.json | 1 + ...n_succession_fan_out_one_guard_holds.sysml | 2 +- internal/exec/smt/referee_test.go | 13 +++++++++++- 7 files changed, 50 insertions(+), 2 deletions(-) create mode 100644 internal/exec/runtime/testdata/conformance/action_fork_one_branch_beside_live_token.check.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/action_succession_fan_out_one_guard_holds.check.expected.json diff --git a/internal/exec/runtime/conformance_test.go b/internal/exec/runtime/conformance_test.go index 8c030cec9a..c67358c8b4 100644 --- a/internal/exec/runtime/conformance_test.go +++ b/internal/exec/runtime/conformance_test.go @@ -137,6 +137,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"` @@ -733,6 +736,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. @@ -745,11 +754,17 @@ func admissibleSchemaProblems(expected ExpectedOutcome, oracleTitles map[string] if expected.ExploreBudget != nil { problems = append(problems, "exploreBudget is stated without outcomes to explore") } + if expected.SolverBudget != nil { + problems = append(problems, "solverBudget is stated without outcomes to referee") + } return problems } 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)) } @@ -2432,6 +2447,7 @@ func TestAdmissibleOutcomesSchema(t *testing.T) { {Outputs: map[string]ExpectedValue{"x": one}}, {Outputs: map[string]ExpectedValue{"x": two}}, } + zero, twenty := 0, 20 tests := []struct { name string expected ExpectedOutcome @@ -2449,6 +2465,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/testdata/conformance/README.md b/internal/exec/runtime/testdata/conformance/README.md index 370a3d5b47..d3cc1919fa 100644 --- a/internal/exec/runtime/testdata/conformance/README.md +++ b/internal/exec/runtime/testdata/conformance/README.md @@ -183,6 +183,12 @@ a case that hits it fails with a message telling the author to raise it: budget is the answer to 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. Cases without `outcomes` are not explored by the harness. The default schedule is deterministic, so a case with an admissible set still keeps its exact golden trace. 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_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 index 3ed99c5c03..83239ab9e9 100644 --- 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 @@ -1,6 +1,7 @@ { "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}}} 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 index 604390a310..ba34393a4e 100644 --- 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 @@ -11,7 +11,7 @@ package test { first start; then fork f; action p; - action q; + action q { assign x := 3; } action r { assign x := 1; } action w { assign x := 2; } join j; 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()