fix(runtime): explore every order of unordered statements in calc, constraint and case bodies

changes/unreleased/atomic-body-statement-order.fixed.md

@@ -0,0 +1 @@
+- **Exploration and the model checker reach every order of a calc or constraint body's unordered statements.** A calc body whose `assign y := y * 10;` and `assign y := y + 2;` no `then` relates now explores and checks to both `12` and `30` instead of claiming `12` over every schedule, and a constraint whose verdict depends on the order of its body's statements is both satisfied and violated, and violated under `-engine check`. The body is still performed whole inside the step that evaluates it, so its statements are reordered among themselves and never interleaved with another performance; its result expression or condition is evaluated after them. Each invocation whose result depends on the order is one `statement order` choice point between the distinct results, so a recursive calc adds one choice rather than one per level, and a body whose statements commute adds none. A guard whose verdict depends on the order is a `statement order` choice point between the distinct results the orders produce, an evaluation error among them; inside a preview it is reported as not covered, as is a guard whose constraint body can write outside the constraint. `then` between a constraint body's own statements now orders them rather than being refused. Calcs compiled at run time fall back to the interpreter when their statements can reorder under these schedules. `declared` and the default schedule keep declaration order, so default results do not move. A stated succession a calc body cannot perform is refused naming the construct (`` `first` statement``) rather than an internal type.

changes/unreleased/case-step-order.fixed.md

@@ -0,0 +1,6 @@
+- The steps of an analysis or verification case that states no succession are now unordered, as an
+  action definition's subactions are: `explore`, `-engine check`, replay and seeded runs reach every
+  interleaving of them instead of only declaration order, so a case such as
+  `action s1 { assign x := x * 10; } action s2 { assign x := x + 2; }` reports both `12` and `30`.
+  `declared` and the default `reverse` schedule still perform the steps in declaration order, so
+  default results do not change.

changes/unreleased/constraint-body-steps.added.md

@@ -0,0 +1 @@
+- Statements in a constraint or requirement body (`assign`, `if`, `while`/`loop`/`for`, and body-local declarations interleaved with them) now run as steps of the check's own performance before its conditions are evaluated, in declaration order: locals live in a fresh frame per check, the constraint's own parameters are copied into it, and each condition of the body is judged in the state the steps left. Assignments reaching outside the performance — a name it holds no feature for, a chained or qualified target — and effects it cannot perform (`send`, `perform`, `terminate`) are refused with the typed `ErrConstraintExternalAssignment`/`ErrConstraintEffect`, as are stated successions (`ErrStatementNotExecutable`), and a body stating steps but no result expression reports `ErrNoConditions`. The solver refuses to translate the steps of such a body rather than solving its conditions as if they ran.

changes/unreleased/do-flow-node-yields.fixed.md

@@ -0,0 +1 @@
+- **A loop or `if` node of a state's do body stating a flow yields as a statement does.** Adding `then` to a do body made it a stated flow whose `for`, `while` and `if` nodes ran whole in one do round, so two regions' bodies no longer interleaved inside them. Such a node now gives the machine up after each iteration and each branch statement, as the statement-list body does, under every schedule; explore, the model checker, replay and seeds reach those interleavings.

changes/unreleased/explore-body-interleavings.fixed.md

@@ -0,0 +1 @@
+- **Exploration and the model checker reach interleavings inside concurrent action bodies.** A leaf action body's initial values are read when its performance starts and each `assign` writes when it ends, so another concurrent performance may run between them: two performances of `action a[2] { attribute t : Integer := c; assign c := t + 1; }` now explore to `c = 1` and `c = 2` instead of claiming `c = 2` over every schedule, and two fork branches with that body do the same. Such a body yields after its start and after each statement under `explore`, `-engine check`, replay and seeded schedules wherever another performance's moves can change its result; `reverse` and `declared` keep their results, and the SMT engine reports such a flow as not covered (`body interleaving`) rather than encoding one order. The same holds when each branch performs that body as an action of its own (`action a : Inc;` or `perform action pa : Inc;`), and between an `if`'s guard and its branch.

changes/unreleased/explore-statement-order.fixed.md

@@ -0,0 +1 @@
+- **Exploration and the model checker reach every order of a body's unordered statements.** The direct statements of one action, state behavior or calculation body that no succession orders are subactions the library leaves unordered, so `{ assign x := 1; assign y := x; }` now explores and checks to `y = 0` and `y = 1` instead of claiming `y = 1` over every schedule. `then` between statements, an `if`'s guard before its branch and a loop's iterations stay ordered; two statements that touch nothing the other does are explored once. `explore`, `-engine check`, replay and seeded schedules choose the order, recorded as a `statement order` choice point; `declared` and `reverse` run a nested body's statements first to last as before, and an action definition's own statements in the token order each policy already gave them (`reverse` last to first), so default results do not move. An `explore` run whose body has more orders than its run budget reports the search incomplete, and the SMT engine reports such a body as not covered (`statement order`) rather than encoding one order.

changes/unreleased/extent-namespace-bindings-and-performances.fixed.md

@@ -0,0 +1 @@
+- **`all T` now answers three namespace-level shapes it used to get wrong.** Binding connectors owned by a package (`bind a = b`, `bind c = d.w2`) join their ends into one equivalence class denoting the class's one object — several bindings on one usage and bindings written in another package included — instead of each end naming its own; the objects an object's action, state, connection, interface, allocation and flow usages hold — perform and exhibit included — are reached by an extent whose target they may hold; and a package-level collection usage denotes the objects the usages subsetting it denote first, anonymous members only to make up its lower bound, an under-count or over-count a typed `ErrMultiplicityViolation` naming it. A bound class's shared lower bound and a namespace collection's own fill past its subsetters' values are held lazily past 1000 members, as a collection's own lower bound is, so `bind a = b` over `Car[1000000000]` and a subsetter of one count and index without allocating it.

changes/unreleased/terminate-usage-body-flow.fixed.md

@@ -0,0 +1 @@
+- **A terminate action usage's body may state a flow.** `action stop terminate { assign code := 42; then terminate; then assign other := 7; }` now runs its `then` chain, where it was refused as stating no flow of its own. The terminate the usage stands for is unordered against its body's statements: `explore` and `-engine check` reach it falling before, between or after them, an output pin left unwritten binding no value, while `reverse` and `declared` still perform it after the body. A `terminate` naming the usage inside its own body ends the usage's performance rather than the body's.

cmd/sysml/check_test.go

@@ -195,6 +195,22 @@ func TestEvalAfterInstantiateThroughCLI(t *testing.T) {
 	rejectReport(t, answered, "(on ")
 }
 
+// TestEvalOfBoundNamespaceMembersThroughCLI: `-e` reads usages a namespace-owned
+// binding joins through the binding's class, so the valued end's declared value
+// is the class's one object rather than a second construction.
+func TestEvalOfBoundNamespaceMembersThroughCLI(t *testing.T) {
+	binary := buildCLI(t)
+	const model = `package P {
+    part def Car;
+    part x : Car;
+    part y : Car = new Car();
+    bind x = y;
+}
+`
+	got := check(t, binary, model, "-e", "P::x", "-e", "P::y", "-e", "P::x === P::y")
+	wantReport(t, got, 0, "= Instance(ID: 1)", "= true")
+}
+
 // TestCheckOfInheritedConstraintAfterInstantiate checks what `-instantiate p
 // -constraint C` promises: the verdict, and so the exit status a build step reads,
 // is about the object of p rather than about C's declared defaults.

docs/guide/06-behavior.md

@@ -346,7 +346,9 @@ and their bodies may hold whatever an action body holds: a flow of nodes joined
 (`first start; then …`; every node no succession leads to starts with the behavior, unordered),
 forks, joins and decisions, timed and signal accepts, sends, nested action nodes with flows of
 their own, and typed usages with pin bindings (`do action poll : Poll { inout n = ticks; }`). A
-body stating no flow still runs its statements in declaration order. A braced block without the
+body stating no flow leaves the statements no `then` relates unordered: `declared` takes them in
+declaration order, and `explore` and `-engine check` reach every order
+([below](#seeing-the-whole-outcome-set-explore)). A braced block without the
 keyword — `entry { … }`, `do { … }`, `exit { … }`, and a transition's `do { … }` — is one
 anonymous action with that body, the same as `entry action { … }`: an attribute declared inside
 the block is local to it and shadows the state's, and a `terminate;` in it ends the whole block
@@ -768,7 +770,19 @@ tried. Under `explore` an action step is one token advancing one node — not, a
 policies, every steppable token moving once — so the picks fall in consecutive steps and a branch
 of several nodes can run ahead of, or be overtaken by, a concurrent one at each of them. A
 `complete` exploration therefore covers every interleaving of the nodes the library leaves
-unordered, at body granularity: the statements of one body run without interruption. A run that
+unordered. Where another performance's moves can change what a leaf body computes, the body
+yields after its initial values are read and after each statement, so a concurrent branch may
+run between a body's snapshot `attribute t : Integer := c` and its `assign c := t + 1`; the
+statements of a nested body run first to last, and an action definition's own statements in
+the token order each policy gives them (`reverse` last to first). A calc or constraint body is
+performed whole inside the step that evaluates it: no other performance runs between its
+statements, but the statements no `then` relates are unordered among themselves, so `explore`
+and `-engine check` reach every order of them (a calc whose `y := y * 10` and `y := y + 2` are
+unordered returns `12` or `30`), and its result expression or condition is evaluated after
+them; `declared` and `reverse` run calc and constraint bodies in declaration order. A case body
+stating no succession likewise leaves its steps unordered under `explore`, `-engine check`,
+replay and seeded schedules, while `declared` and `reverse` perform them in declaration order.
+A run that
 fails under some order is an outcome of its own (`error: …`), not the end of the exploration; a
 behavior with no choice point explores in exactly one run (`no choice points`
 in the witness column); the same model explores to the same table every time. With `-trace`, the

docs/internals/design/region-order-scheduling.md

@@ -251,7 +251,7 @@ choice at t=0.0: next do top, dispatch AnotherSignal (unordered; ran do top firs
 `%step`, `%continue` and `%advance` count them as they count every choice
 (`2 choice points; %trace on to see them`), `%choices` lists them, and over gRPC and Connect each
 is the informational `choice-point` diagnostic placed at the state or transition drawn. The
-self-model's `choiceKindCount` counts nine kinds.
+self-model's `choiceKindCount` counts thirteen kinds.
 
 ### Witness lines and replay