docs(runtime): state that a calc body has no choice points and that policies may reach different ones

Co-Authored-By: jason.han <hanhuijun@gmail.com>

Author: devin-ai-integration[bot]

changes/unreleased/scheduling-policy.added.md

@@ -2,22 +2,23 @@
   library orders nothing — several steppable tokens in one step, several holding guards at a
   decision, several enabled transitions out of one state for one event, and so whose same-step
   write to one feature stands — the executors follow a named policy: `reverse` (the default:
-  reverse token order, first holding guard, first enabled transition, so every existing result
-  and trace is unchanged), `declared` (tokens in spawn order, guards and transitions in
-  declaration order) or `seed:<n>` (a pseudo-random order the seed fixes, so one seed replays
-  one run on every platform and two seeds may take two linearizations). The spelling is the same
-  everywhere: `sysml -schedule <policy>` for `-action`, `-state`, `-analysis` and a `-calc` whose
-  body performs actions; `%schedule [<policy>]` in the REPL, shown with no argument and applied
-  to the runs started after it while a debugging session under way keeps its own; a `schedule`
-  field on `ExecuteActionRequest`, `ExecuteStateRequest` and `RunAnalysisRequest`, empty for the
-  default and advertised as the `schedule` capability, with the Go and Python clients taking it
-  as an option (`opensysml.WithSchedule`, `opensysml.Schedule`, `schedule=`); and a `schedule`
-  pin on a conformance case, which the harness runs under. A policy changes only which
-  alternative each choice takes: the same choice points are reported and each `took …` is what
-  the policy took. A spelling naming no policy — an unknown name, `seed` or `seed:` without a
-  number, `seed:-1`, `seed:abc` — is refused before anything runs, as `INVALID_ARGUMENT` on the
-  wire. `explore`, the bounded exhaustive replay, is reserved and refused by name until it exists.
-  The conformance suite also runs whole under `declared` and `seed:1`, requiring every case that
-  pins no policy and lists no `outcomes` to produce its default outputs; the two cases whose
-  default result is one linearization of several — a message two accepts answer to, a send to a
-  same-named port — pin `reverse` until their admissible set is derived.
+  reverse token order, first holding guard, first enabled transition, so every existing result and
+  trace is unchanged), `declared` (tokens in spawn order, guards and transitions in declaration
+  order) or `seed:<n>` (a pseudo-random order the seed fixes, so one seed replays one run on every
+  platform and two seeds may take two linearizations). The spelling is the same everywhere: `sysml
+  -schedule <policy>` for `-action`, `-state` and `-analysis` (a calc's body performs nothing, so
+  `-calc` has no choice to make); `%schedule [<policy>]` in the REPL, shown with no argument and
+  applied to the runs started after it while a debugging session under way keeps its own; a
+  `schedule` field on `ExecuteActionRequest`, `ExecuteStateRequest` and `RunAnalysisRequest`,
+  empty for the default and advertised as the `schedule` capability, with the Go and Python
+  clients taking it as an option (`opensysml.WithSchedule`, `opensysml.Schedule`, `schedule=`);
+  and a `schedule` pin on a conformance case, which the harness runs under. A policy changes only
+  which alternative each choice takes: every choice point a run reaches is reported and each `took
+  …` is what the policy took, though another linearization may reach other choice points. A
+  spelling naming no policy — an unknown name, `seed` or `seed:` without a number, `seed:-1`,
+  `seed:abc` — is refused before anything runs, as `INVALID_ARGUMENT` on the wire. `explore`, the
+  bounded exhaustive replay, is reserved and refused by name until it exists. The conformance
+  suite also runs whole under `declared` and `seed:1`, requiring every case that pins no policy
+  and lists no `outcomes` to produce its default outputs; the two cases whose default result is
+  one linearization of several — a message two accepts answer to, a send to a same-named port —
+  pin `reverse` until their admissible set is derived.

docs/guide/06-behavior.md

@@ -213,14 +213,17 @@ executor can be told to resolve every choice point under another: `declared` tak
 order they were spawned and guards and transitions in declaration order, and `seed:<n>` draws each
 pick from a pseudo-random sequence the non-negative integer `n` fixes, so `seed:1` replays the same
 run every time and on every platform while `seed:2` may take another linearization. The policy is
-spelled the same everywhere — `sysml -schedule declared` for `-action`, `-state`, `-analysis` and a
-`-calc` whose body performs actions, `%schedule seed:7` in the REPL for the runs started after it
-(a debugging session under way keeps its own), a `schedule` field on the gRPC execution requests,
-and a `schedule` pin on a conformance case — and changes only which alternative each choice takes:
-the same choice points are reported, and each `took …` is what the named policy took, so running
-a model under two policies and comparing the outcomes is how a scheduling artefact is told from a
-bug. An unknown spelling — `random`, `seed` without a number, `seed:-1` — is refused before
-anything runs rather than falling back to the default. Where the library orders the alternatives
+spelled the same everywhere — `sysml -schedule declared` for `-action`, `-state` and `-analysis`
+(a calc's body performs nothing, so `-calc` has no choice to make), `%schedule seed:7` in the
+REPL for the runs started after it (a debugging session under way keeps its own), a `schedule`
+field on the gRPC execution requests, and a `schedule` pin on a conformance case — and changes
+only which alternative each choice takes: every choice point the run reaches is reported, and
+each `took …` is what the named policy took, so running a model under two policies and comparing
+the outcomes is how a scheduling artefact is told from a bug. Another linearization can reach
+other choice points — which tokens are steppable in a step depends on the order the earlier ones
+moved — so the count is not fixed across policies, only the reporting is. An unknown spelling —
+`random`, `seed` without a number, `seed:-1` — is refused before anything runs rather than falling
+back to the default. Where the library orders the alternatives
 — the innermost transition over its enclosing state's — there is no choice, and every policy
 follows that order.