Merge pull request #125 from Open-MBEE/feature/scheduling-policy

* feat(runtime): select the scheduling policy a run resolves its choice points under

A run follows a named scheduling policy wherever the library orders nothing:
`reverse` (the default, unchanged: reverse token order, first holding guard,
first enabled transition), `declared` (spawn and declaration order) or
`seed:<n>` (a PCG sequence the seed fixes, reproducible on every platform).
Every choice point is still reported and each `took ...` is what the policy
took. `explore` is reserved and refused by name until it exists.

The same spelling is taken by `sysml -schedule`, `%schedule` in the REPL (a
debugging session under way keeps its own), a `schedule` field on
ExecuteActionRequest, ExecuteStateRequest and RunAnalysisRequest advertised as
the `schedule` capability (a spelling naming no policy is INVALID_ARGUMENT),
the Go and Python clients, and a `schedule` pin on a conformance case.

The conformance suite runs whole under `declared` and `seed:1` as well,
requiring every case that pins no policy and lists no outcomes to produce its
default outputs; policy trace goldens pin every outcomes case. The two cases
whose default result is one linearization of several pin `reverse`.

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

* docs(proto): describe the schedule capability in ServerInfoResponse

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

* chore(runtime): mark the seeded scheduler's generator as deliberately non-cryptographic

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

* 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>

* test(runtime): admit both pairings of two accepts racing for two sends

Restate action_choice_shared_message_accept as an outcomes case derived in the
semantic oracle, with a .trace.order and declared/seed-1 trace goldens, in
place of its reverse pin. send_identity_same_named_ports stays pinned: the
via-less accept over-matches a port-addressed transfer, fixed separately.

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

* fix(runtime): read the picked guard for real and keep a driven run's scheduler

A decision branch the policy picks past the first was read only in a probe
the context undoes, so its evaluation left nothing behind. The run now reads
the picked guard once more before taking the branch, as fireTransition reads
a transition's guard again before it fires; the seed:1 trace golden of
action_choice_decision_overlapping_guards gains that reading.

An executor driven call by call (the REPL debuggers) keeps the scheduler its
run started with: another run driven to completion while it is paused no
longer replaces the sequence its remaining choices draw from.

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

* refactor(runtime): tighten the beginExecutorRun doc comment

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

* fix(runtime): ask a shared ancestor state for its transition once per dispatch

selectCandidates remembers per source state which transition it offers, so a composite state reached from every leaf of its orthogonal regions is asked once per event dispatch or change poll: the choice among its enabled transitions draws once, yields one candidate and one choice note, and the run's next choice takes the seed's next draw. Nested transitions keep their priority.

The state_choice_shared_ancestor_regions trace goldens lose the second leaf's redundant re-reading of the first guard.

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

* fix(runtime): pick a state's transition only once it survives conflict resolution

An enclosing state's enabled transitions were chosen, and the seeded draw spent, before losesToNestedTransition dropped the candidate to a nested transition, so a choice that never fired and was never reported shifted every later seeded choice. Candidate discovery now returns the enabled positions and chooseTransition picks among them after conflict resolution, on both the dispatch and the change-poll path; a shared ancestor still draws once.

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

* docs(wire): carry the choice-point code in the scheduled ExecuteAction example

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

* fix(runtime): preview a machine's decision from its own run's scheduler

Decide read the scheduler the context happened to hold, so after another
run had used the context it could name a transition other than the one
ProcessNextEvent then fired. It now previews under the executor's own
scheduler, drawing nothing from it.

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

* fix(runtime): draw a seeded token order only among the tokens able to act

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 steps
taken while tokens wait do not shift the choices the run makes later.

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

* fix(grpc): read RunAnalysis's schedule before requiring verification

A malformed spelling is INVALID_ARGUMENT whether or not the service offers
verification, as it is on ExecuteAction and ExecuteState.

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

* docs(runtime): record that send_identity_same_named_ports runs unpinned

With a via-less state accept routed by the receiver a transfer reaches, the
case has one enabled transition under every policy and needs no schedule pin.

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

---------

Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Co-authored-by: jason.han <hanhuijun@gmail.com>

Author: HuiJun

api/proto/sysml.pb.go

@@ -262,6 +262,10 @@ message RunAnalysisRequest {
   repeated Value arguments = 4;
   // Arguments bound to input parameters by name.
   map<string, Value> named_arguments = 5;
+  // Scheduling policy the run resolves its choice points under: "declared",
+  // "reverse" or "seed:<n>". Empty is the default, "reverse"; any other
+  // spelling is INVALID_ARGUMENT.
+  string schedule = 6;
 }
 
 // RunAnalysisResponse carries what the case computed and decided.
@@ -427,6 +431,10 @@ message ExecuteActionRequest {
   string model_hash = 1;
   string action_symbol_id = 2;   // FQN of action def
   map<string, Value> inputs = 3; // parameter name → value
+  // Scheduling policy the run resolves its choice points under: "declared",
+  // "reverse" or "seed:<n>". Empty is the default, "reverse"; any other
+  // spelling is INVALID_ARGUMENT.
+  string schedule = 4;
 }
 
 // ExecuteActionResponse contains action execution results
@@ -441,6 +449,10 @@ message ExecuteStateRequest {
   string model_hash = 1;
   string state_machine_symbol_id = 2;
   repeated string events = 3;    // sequence of event names to process
+  // Scheduling policy the run resolves its choice points under: "declared",
+  // "reverse" or "seed:<n>". Empty is the default, "reverse"; any other
+  // spelling is INVALID_ARGUMENT.
+  string schedule = 4;
 }
 
 // ExecuteStateResponse contains state machine execution trace
@@ -916,6 +928,11 @@ message ServerInfoResponse {
   //                  Markdown.
   //   "diagnostic_codes" - Diagnostic.code is populated, so an empty code is a
   //                  finding none was assigned; without it every code is empty.
+  //   "schedule"     - ExecuteActionRequest, ExecuteStateRequest and
+  //                  RunAnalysisRequest take a schedule, the scheduling policy
+  //                  the run resolves its choice points under; without it a
+  //                  service drops the field and runs under the default, so a
+  //                  client must not send one.
   repeated string capabilities = 2;
 }
 

api/proto/sysml.proto

@@ -0,0 +1,24 @@
+- **The scheduling policy a run resolves its choice points under is selectable.** Where the
+  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` 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. Two accepts racing for two sends now
+  list both pairings as `outcomes`, with the derivation in the semantic oracle; a send to a
+  same-named port pins `reverse` until the via-less accept that over-matches it is fixed.

changes/unreleased/scheduling-policy.added.md

@@ -52,6 +52,7 @@ type analysisOptions struct {
 	subjectSymbolID string
 	positional      []Value
 	named           []namedArgument
+	schedule        string
 }
 
 type namedArgument struct {
@@ -77,6 +78,13 @@ func Argument(name string, value Value) AnalysisOption {
 	return func(o *analysisOptions) { o.named = append(o.named, namedArgument{name, value}) }
 }
 
+// Schedule names the scheduling policy the actions the case performs resolve
+// their choice points under, as WithSchedule does for ExecuteAction. Requires
+// the schedule capability.
+func Schedule(policy string) AnalysisOption {
+	return func(o *analysisOptions) { o.schedule = policy }
+}
+
 func (c *client) RunAnalysis(
 	ctx context.Context,
 	model *Model,
@@ -98,10 +106,14 @@ func (c *client) RunAnalysis(
 	if err := c.requireValueCapabilities(ctx, values...); err != nil {
 		return nil, err
 	}
+	if err := c.requireSchedule(ctx, options.schedule); err != nil {
+		return nil, err
+	}
 	req := &pb.RunAnalysisRequest{
 		ModelHash:       hash,
 		SymbolId:        symbolID,
 		SubjectSymbolId: options.subjectSymbolID,
+		Schedule:        options.schedule,
 	}
 	for _, argument := range options.positional {
 		sent, err := valueToProto(argument)

client/opensysml/analysis.go

@@ -64,12 +64,15 @@ type Client interface {
 	// requires the complex_values capability, an Array, Vector or
 	// VectorQuantity input the structured_values one, a MeasurementRef input
 	// the measurement_refs one and a Function input the function_values one,
-	// checked before anything is sent.
-	ExecuteAction(ctx context.Context, model *Model, actionSymbolID string, inputs map[string]Value) (*ActionRun, error)
+	// checked before anything is sent. WithSchedule selects the scheduling
+	// policy, which requires the schedule capability, checked the same way.
+	ExecuteAction(ctx context.Context, model *Model, actionSymbolID string, inputs map[string]Value, opts ...ExecuteOption) (*ActionRun, error)
 
 	// ExecuteState runs the named state machine, feeding it the events in
 	// order, and reports the states visited and the context left behind.
-	ExecuteState(ctx context.Context, model *Model, stateMachineSymbolID string, events []string) (*StateRun, error)
+	// WithSchedule selects the scheduling policy, which requires the schedule
+	// capability, checked before anything is sent.
+	ExecuteState(ctx context.Context, model *Model, stateMachineSymbolID string, events []string, opts ...ExecuteOption) (*StateRun, error)
 
 	// VerifyConstraint evaluates the named constraint, optionally Against a
 	// part to instantiate and check. Requires the verification capability.
@@ -96,9 +99,10 @@ type Client interface {
 	// reports its outputs with the verdict of its objective and of each
 	// assertion in its body. Positional arguments bind its inputs in
 	// declaration order; Against names its subject and Binding a parameter by
-	// name. Requires the verification capability, and the complex_values or
-	// structured_values capability for a Complex or a structured argument,
-	// checked before anything is sent.
+	// name; Schedule selects the scheduling policy. Requires the verification
+	// capability, the complex_values or structured_values capability for a
+	// Complex or a structured argument and the schedule capability for a
+	// policy, checked before anything is sent.
 	RunAnalysis(ctx context.Context, model *Model, symbolID string, opts ...AnalysisOption) (*Analysis, error)
 
 	// Query selects the model's elements the query matches, in declaration

client/opensysml/client.go

@@ -2,6 +2,7 @@ package opensysml
 
 import (
 	"context"
+	"fmt"
 	"maps"
 	"slices"
 
@@ -27,17 +28,59 @@ type StateRun struct {
 	Diagnostics []Diagnostic
 }
 
+// ExecuteOption configures ExecuteAction and ExecuteState.
+type ExecuteOption func(*executeOptions)
+
+type executeOptions struct {
+	schedule string
+}
+
+// WithSchedule names the scheduling policy the run resolves its choice points
+// under — "declared", "reverse" (the default) or "seed:<n>" — spelled as the
+// sysml -schedule flag spells it. Requires the schedule capability; a spelling
+// naming no policy is refused with CodeInvalidArgument.
+func WithSchedule(policy string) ExecuteOption {
+	return func(o *executeOptions) { o.schedule = policy }
+}
+
+// requireSchedule refuses to send a policy to a service without the schedule
+// capability, which would run under the default rather than refuse it.
+func (c *client) requireSchedule(ctx context.Context, policy string) error {
+	if policy == "" {
+		return nil
+	}
+	info, err := c.serverInfo(ctx)
+	if err != nil {
+		return err
+	}
+	if !info.Has(CapabilitySchedule) {
+		return &StatusError{
+			Code:    CodeUnimplemented,
+			Message: fmt.Sprintf("capability %q is unavailable", CapabilitySchedule),
+		}
+	}
+	return nil
+}
+
 func (c *client) ExecuteAction(
 	ctx context.Context,
 	model *Model,
 	actionSymbolID string,
 	inputs map[string]Value,
+	opts ...ExecuteOption,
 ) (*ActionRun, error) {
+	var options executeOptions
+	for _, opt := range opts {
+		opt(&options)
+	}
 	hash, err := c.call(model)
 	if err != nil {
 		return nil, err
 	}
-	req := &pb.ExecuteActionRequest{ModelHash: hash, ActionSymbolId: actionSymbolID}
+	if err := c.requireSchedule(ctx, options.schedule); err != nil {
+		return nil, err
+	}
+	req := &pb.ExecuteActionRequest{ModelHash: hash, ActionSymbolId: actionSymbolID, Schedule: options.schedule}
 	if len(inputs) > 0 {
 		if err := c.requireValueCapabilities(ctx, slices.Collect(maps.Values(inputs))...); err != nil {
 			return nil, err
@@ -67,15 +110,24 @@ func (c *client) ExecuteState(
 	model *Model,
 	stateMachineSymbolID string,
 	events []string,
+	opts ...ExecuteOption,
 ) (*StateRun, error) {
+	var options executeOptions
+	for _, opt := range opts {
+		opt(&options)
+	}
 	hash, err := c.call(model)
 	if err != nil {
 		return nil, err
 	}
+	if err := c.requireSchedule(ctx, options.schedule); err != nil {
+		return nil, err
+	}
 	resp, err := c.caller.executeState(ctx, &pb.ExecuteStateRequest{
 		ModelHash:            hash,
 		StateMachineSymbolId: stateMachineSymbolID,
 		Events:               append([]string(nil), events...),
+		Schedule:             options.schedule,
 	})
 	if err != nil {
 		return nil, err