feat(runtime): execute repeated action steps beyond plain successions

[devin-ai-integration]

What and why

Exact action-step multiplicity (a[n]) executed only between plain successions; every other shape around a repeated step was refused with action-step-multiplicity-unsupported. This PR executes the shapes KerML/SysML determine and keeps a typed refusal for the ones they leave open. Unchanged: the strict refusal of an ambiguous plain then around a repeated step, [0] as a no-op, refusal of non-fixed counts ([0..1], [*]), ErrIntegerUnaddressable for bounds beyond 64 bits, and validate/run/explore/check agreement (the SMT engine now refuses every shape CheckStep refuses).

Now executes

Shape	Behaviour
a[n] in a while/for/if body	n performances per body pass, [0] none. Each repetition runs as one move, so explore and check report the result as observed, not proved or bounded, with a typed reason (their interleavings are not explored).
perform action run[n] on a part	n distinct occurrences, each with its own behaviour, kept through held images. PerformedActionsOf(run) returns all n, so a request to run run on that part is ambiguous (ErrAmbiguousAction, "performs run 2 times").
a.x read outside a	The values of every performance's x, duplicates kept, in repetition-index order. Reading before all n end gives ErrNodeNotPerformed. Inside a performance, x is that performance's own value.
action a[n] { in x = c; }	Each performance binds its own x.
Owned bind a.x = e, e single-valued	An in-pin gives every performance e's value. An out-pin requires all n values to agree, otherwise ErrBindingConflict.
a[n] → join, or → merge as its only incoming succession	The ends force the control node to perform n times, once per performance of a (derived below). The other edges at the node are checked under that count.
succession first [*] a then f; into a fork or decision	Barrier: f performs once, under the same ⚠️ one-performance reading as an ordinary unwritten tally in first [*] a then [1] tally. Its ends do not force another count.
join/merge → then [*] a	Fans out of a single control performance, under the same reading.
first p if g then [*] a; (guard into a written target end)	When g holds, every performance is ordered after p. The parser now admits that end (GuardedSuccession/GuardedTargetSuccession → TransitionSuccession → ConnectorEnd OwnedCrossMultiplicityMember). It goes through the AST codec, DeclaredSuccessions and RDF export/import.
SMT (sysml -engine smt)	a[n] is encoded as the runtime runs it: n-1 sibling tokens placed in free slots on the split move that follows arrival (from a fork too), a retire-until-last barrier (or per-performance crossing into a join/merge), [0] as a pass-through, and a false guard into a written target end as a failing move.

Still refused, and why

Shape	Code	Reason
flow from a.out to b.in and connections at a repeated pin	unsupported	KerML §9.2.7 / Transfers.kerml: flow ends have no multiplicity in the grammar and a flow defaults to [0..*] (SysML §7.6.3), so how many transfers there are, and from which performances, is undetermined.
bind a.x = e with a multi-valued e into in-pins	unsupported	Which of e's values goes to which performance is open.
A guarded succession out of a[n]	unsupported	GuardedSuccession has no source end you can write, so KERML-29 leaves it open.
A guarded succession into a[n] with no written target end	unsupported	Same as above.
A false guard into a written target end of a step performed more than once	action-step-order-open	The exact count still requires n performances, but nothing orders them. Validate warns when the guard is literal false. Into a single performance (a[1]) the false guard just prunes the edge (guard_false_single).
Plain then from a[n] into a fork or decision, or from a join or merge into a[n]	unsatisfiable or order-open (project plain-then policy)	The a-side end is not mandated.
A merge or decision that carries another succession beside the repeated step's	unsatisfiable	Under the one-performance reading, the mandated 0..1 ends cannot take n crossings.
A fork, or a decision whose only outgoing succession goes to a[n]	unsatisfiable or order-open at the node's incoming edge	The node is derived to perform n times, and its predecessor, which performs once, cannot order n crossings.
a[n] in a while/for/if body next to another member, with no succession written	action-step-order-open	Only the executor's declaration order sequences the body, so nothing orders every performance. Same stance as plain then.
A written end that contradicts a mandated control-node end	unsatisfiable	Contradicts SysML §8.3.17.6–§8.3.17.13.
SMT: a repeated step a token can reach again while its performances are live (cycle, or more than one arrival)	unsupported	Two repetition groups would share the barrier.
SMT: a repeated step that has its own features or flows	unsupported	One feature variable per state cannot hold each performance's values.

Specification basis

• KerML 1.0 §7.3.2: cardinality is the number of values per instance of the featuring type, so a[n] is n performances per performance of the action, body pass or part that features a.
• SysML v2.0 §7.6.3, as semantics.ImplicitMultiplicityApplies/EffectiveParameterRange implement it: the implicit [1..1] reaches only owned attribute, item, part and port usages. Any other usage takes what it subsets or redefines, else [0..*]. A control node is an action usage specializing Actions::Action::controls : ControlAction[0..*], and merges is [0..*]. forks, joins and decisions declare nothing, so they inherit [0..*]. An unwritten control node's count is therefore [0..*], and only its successions can fix it:
  • a[n] → join (both ends mandated 1..1): a bijection, so n join performances.
  • a[n] → merge as its only incoming succession: target 1..1 plus ControlPerformances.kerml MergePerformance::incomingHBLink : HappensBefore[1], so n.
  • fork → a[n], and a lone-outgoing decision → a[n] (DecisionPerformance::outgoingHBLink[1]), are derived the same way. Both then refuse at the node's predecessor.
  • No other adjacency forces a count, so the node takes the executor's one-performance reading. This is the same reading an ordinary unwritten step gets. A fork barrier and an ordinary tally barrier therefore differ only in their mandated ends, not in their defaults.
• The same clause gives an ordinary unwritten action usage [0..*], so running it once per token arrival is the executor's reading, not a derived rule. Its compliance row is now ⚠️, and the semantics.AssumedRange comment no longer attributes [1..1] to KerML §7.4.5, which says "the usual default of 0..*".
• SysML v2.0 §8.3.17.6–§8.3.17.13 / §8.4.13.4: these clauses mandate control-node ends "even if not shown":
  • into any control node: target 1..1;
  • out of any control node: source 1..1;
  • into a join: source 1..1; into a merge: source 0..1;
  • out of a fork: target 1..1; out of a decision: target 0..1.
• SysML §8.4.13.3 and TransitionPerformances.kerml (guarded successions):
  • the guard is evaluated after the single source performance;
  • a true guard asserts HappensBefore;
  • a false guard asserts no ordering.
• KerML §8.4.4.6.2 (binding connectors are SelfLink) and KerML §7.4.11 (feature values).
• ControlFunctions.kerml '.': source and result [0..*], nonunique.
• LoopPerformance / IfThenPerformance: each body pass is a performance of its own.
• SysML §8.4.13.11, Parts::performedActions and Occurrences::enactedPerformances: the basis for part-level performed actions.
• The spec is silent on how a flow or a multi-valued binding over repeated performances distributes its values, which is why those shapes stay refused. UML, fUML and PSSM were not used to decide anything.

The derivation is recorded in docs/project/behavior-semantic-oracle.md (repeated action steps), the SMT encoding in docs/internals/design/smt-model-checking.md, and the RDF form in docs/reference/rdf-mapping.md. In docs/project/spec-compliance.md:

• the block-flow row stays ⚠️ Approximate (block-body interleavings of repeated performances are not explored; explore and check report observed);
• the one-performance row for an unwritten step moves from ✅ to ⚠️ (executor's reading, see above);
• a new row covers repeated-step features, pins and bindings (✅, with the refused shapes noted as open in the spec);
• the succession-ordering row and the part-level row now describe the control-node, guarded and part-perform behaviour.

How it was verified

• Parser goldens: action_step_multiplicity_loop_body, perform_action_multiplicity, guarded_succession_target_multiplicity.
• Execution conformance fixtures:
  • action_step_multiplicity_ while_body, for_body, if_body, unordered_loop_body;
  • part_perform, external_read, pin_value, bind_input, bind_output;
  • join_per_performance, merge_per_performance;
  • fork_barrier, decision_barrier, merge_fanout, which run under the one-performance reading;
  • while_body, unordered_loop_body and merge_per_performance keep exploreBudget: {"runs": 8192}, and join_per_performance keeps 2048. The default 1024 runs leave their exploration incomplete. The budget is pinned for completeness only and does not affect the observed standing;
  • loop_body_race: the admitted set is {c = 1, c = 2}. Exploration reaches only c = 2, and the fixture pins the observed standing through a new exploreNotes schema field. while_body, for_body, if_body and unordered_loop_body carry the same note, with outcomes unchanged;
  • guard_true, guard_false, guard_false_single, fork_into_repeated.
• Trace goldens: the loop body and the five control-node cases.
• Robustness: robustness_repeated_step_coverage_test.go:TestRuntimeRobustnessRepeatedStepCoverage covers:
  • an out-pin binding conflict, and the multi-valued input refusal;
  • an unordered read before completion, and the repeated-pin flow refusal;
  • perform action run[0], and per-inner-pass counting for while nested in for;
  • [0..2] in a loop staying not-fixed;
  • the control-node and guarded cases, and explore agreeing with run;
  • observed (not proved or bounded) explore and check strengths for a repeated step in a stated and in an unstated block body, with a flat a[2] unaffected;
  • the declaration-order refusal in an unstated body.
• Check-engine coverage: every accepted control-node, exact, zero, guard-true, external-read and pin/binding fixture has a .check.expected.json. TestCheckConformanceOracles, TestCheckAgreesWithExploreOverTheConformanceCorpus and TestCheckWitnessesReplayOverTheConformanceCorpus run them through the explicit-state check, exploration and witness replay.
  • For this, the conformance schema now accepts an exploreBudget without outcomes when the case has a check expectation (join_per_performance needs 1680 exploration runs). New schema-test rows pin both the refusal and the allowance.
  • The loop-body fixtures carry no check expectation. -engine check already refuses while/for/if bodies on develop without any repetition (token 1 is not one the step may move). That is a pre-existing limitation, not in scope here; run and explore agree on those fixtures.
• Other unit tests:
  • lowerer and behavior-pass tests for each accepted and refused edge shape;
  • held-image distinct occurrences;
  • SMT outcome tests (exact, zero, fork barrier, merge fan-out, join and merge per performance, guard true/false, shared-writer race) and SMT refusals (cycle, non-fixed, unaddressable, every CheckStep refusal);
  • semantics target-end tests, and an RDF round trip of both guarded forms with sysx:sourceText stripped.

Results:

go build ./...                     ok
go vet ./...                       ok
gofmt -l .                         (empty)
go test ./...                      ok
go test -race ./internal/exec/runtime/... ./internal/exec/smt/... ./internal/ir/lower/...   ok
make docs-check                    OK
python3 scripts/changelog.py check OK
make lint                          ok (staticcheck + gosec)

At the latest head, go build/vet/gofmt, the lower, behavior-pass, SMT, analysis and runtime packages, the runtime race suite (conformance, traces, robustness), ./tests/..., make docs-check and the changelog check were rerun: all ok.

Corpus gates ran with OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_PILOT_LIBRARY_XMI=1 OPENSYSML_REQUIRE_PSSM_SUITE=1, after all four download scripts:

• ./tests/..., ./cmd/sysml/..., ./internal/exec/analysis/..., ./internal/exec/solve/..., ./internal/frontend/repl/..., ./internal/workspace/model/...: ok;
• go test -C tools ./referee/pssm/... ./oracle/errata/...: ok;
• go run -C tools ./cmd/pilot-diff -check: 381 files, 343 fully agreeing, baseline reproduced.

SMT referee corpus: 7 encoded, 10 refused, 7 agreeing (unchanged by the CheckStep agreement fix). No baseline moved, so nothing was regenerated, and training_examples_expected.txt is untouched.

Two defects that end-to-end CLI testing found are fixed here:

• Exploring and checking the per-performance join diverged, because a synchronization that mints the performing token was not credited as the tried token's act (stepTokenNoting).
• SMT violation witnesses over repeated steps did not replay, because the encoding put the sibling split on the arriving move while the interpreter spends its own step on it. The split now takes a Pending move, and TestEngineWitnessesReplayOverRepeatedSteps pins that the witnesses replay (exact, fork barrier, merge fan-out, join and merge per performance).

A flat a[2] { t := c; c := t + 1; } outside any block still explores as proved over c = 2 only. That is the leaf-body indivisibility the separate body-interleaving change addresses, and it holds on develop too. Merged with that change, the flat case reaches {c = 1, c = 2}, but the block-body cases do not, which is why they report observed here.

The SMT engine already refuses any nested block flow, so it never encodes a repeated step inside a loop or if body.

internal/workspace/libs/stdlib.snapshot is regenerated with make stdlib-snapshot, because the AST codec now encodes the succession target ends.

Two existing tests now assert shapes that are newly supported. Neither was weakened:

• TestAnalyzeRefusesRepeatedActionSteps became TestAnalyzeCountsRepeatedActionSteps.
• TestFirstThenWithADeclaringEndIsRefused now grafts its [2] bound onto the source end. then [2] b is legal grammar, and the source end still has no notation.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/repeated-step-coverage.added.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (no gate count moved)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

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

[devin-ai-integration]

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

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

I tested the built CLI/REPL at a75f494 across 129 commands. The full command matrix changed only in the five results the two fixes target.

• Join per performance: run and complete exploration agree on c=3 (1,680 runs). -engine check is exhaustive (69 states, 110 moves).
• SMT: the exact, fork-barrier and merge-fanout controls (belowFinal) now report violations whose witnesses replay (exit 1). Their ceiling properties still hold.
• Golden path: loop-body counts and two distinct part-perform occurrences check out. The false-guard ordering error and the typed refusals (plain then, [0..2], repeated-pin flow, multi-valued binding, guard out of a repeated step, fork into one, contradictory join end, 64-bit overflow) are unchanged.
• RDF: round trips with and without source text keep the guarded [*].

-engine check on while/for/if bodies still refuses, exactly as on develop without repetition. That is the pre-existing limitation noted in the description.

Join: exhaustive check	Merge: ceiling holds, violation replays

Part perform: distinct occurrences	While body results

[devin-ai-integration]

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

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

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

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

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

[devin-ai-integration]

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