From b52fcc1ec7f6dbc5bf982c8ecb332651e117fe83 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 28 Oct 2026 03:12:46 +0000 Subject: [PATCH 1/6] test(smt): expect features valued by an expression to encode and agree with explore Co-Authored-By: jason.han --- internal/exec/smt/derived_test.go | 114 ++++++++++++++++++++++++++++++ internal/exec/smt/encode.go | 17 ++++- 2 files changed, 130 insertions(+), 1 deletion(-) create mode 100644 internal/exec/smt/derived_test.go diff --git a/internal/exec/smt/derived_test.go b/internal/exec/smt/derived_test.go new file mode 100644 index 0000000000..e9ea207f34 --- /dev/null +++ b/internal/exec/smt/derived_test.go @@ -0,0 +1,114 @@ +package smt + +import ( + "errors" + "maps" + "slices" + "strings" + "testing" + + "github.com/Open-MBEE/OpenSysML/internal/exec/analysis" + "github.com/Open-MBEE/OpenSysML/internal/semantic/symbols" +) + +// derivedPins are the outcomes a case whose action holds a feature valued by an +// expression over other features must prove, per feature: `y = x + 1` read after +// two racing writers of `x` stands on the choice between them, as does `z` +// written from it, rather than on the value `y` held at the start. +var derivedPins = map[string]map[string][]string{ + "action_order_write_from_bound_read": {"x": {"1", "2"}, "y": {"2", "3"}, "z": {"12", "13"}, "w": {"1"}}, +} + +// TestDerivedFeaturesAgreeWithExplore runs every conformance action holding a +// feature valued by an expression over other features through the encoding and +// the exhaustive exploration: the encoding admits the action, the outcomes the +// solver enumerates are the exploration's, every witness replays, and the set of +// values the solver proves for each feature is the set the exploration reached. +func TestDerivedFeaturesAgreeWithExplore(t *testing.T) { + solver := requireSolver(t) + cases := refereeCases(t) + covered := 0 + for _, name := range slices.Sorted(maps.Keys(cases)) { + c := cases[name] + d, action := corpusDocument(t, name, c) + budget := analysis.Budget{Depth: c.solverMoves()} + if !holdsDerived(t, d, action, budget) { + continue + } + covered++ + t.Run(name, func(t *testing.T) { + encoding, refusal := encodeDocument(t, d, action, budget) + if errors.Is(refusal, ErrMalformedFlow) { + // A calculation holds derived features too but performs no flow to encode. + t.Logf("outside the stage: %v", refusal) + return + } + if refusal != nil { + t.Fatalf("refused: %v", refusal) + } + exploration := explore(t, c.exploreBudget(), d.fresh(budget), action) + if !exploration.Complete() { + t.Fatalf("exploration %s", exploration.Status()) + } + outcomes := compareOutcomes(t, solver, encoding, d, action, budget, exploration) + if !outcomes.agreeing || outcomes.replayed != outcomes.witnesses { + t.Errorf("%d witnesses, %d replayed, agreeing %v", outcomes.witnesses, outcomes.replayed, outcomes.agreeing) + } + explored, proved := valuesPerFeature(outcomes.explored), valuesPerFeature(outcomes.found) + for feature, values := range explored { + if !slices.Equal(values, proved[feature]) { + t.Errorf("%s: the exploration reaches %v, the solver proves %v", feature, values, proved[feature]) + } + } + for feature, values := range derivedPins[name] { + if !slices.Equal(proved[feature], values) { + t.Errorf("%s: the solver proves %v, the pin says %v", feature, proved[feature], values) + } + } + }) + } + if covered == 0 { + t.Fatal("no conformance action holds a feature valued by an expression over other features") + } + t.Logf("%d actions hold a feature valued by an expression over other features", covered) +} + +// holdsDerived reports whether the action, started as the encoding is given it, +// holds a feature valued by an expression over other features. +func holdsDerived(t *testing.T, d *document, action *symbols.Symbol, budget analysis.Budget) bool { + t.Helper() + ctx, err := d.fresh(budget)() + if err != nil { + t.Fatalf("context: %v", err) + } + graph, held := started(t, ctx, action) + for _, attr := range held.Features() { + if _, derived := derivation(graph, attr); derived { + return true + } + } + return false +} + +// valuesPerFeature projects outcome identities (`x = 1; y = 2`) onto the sorted +// set of values each feature takes across them. +func valuesPerFeature(identities []string) map[string][]string { + values := make(map[string]map[string]bool) + for _, identity := range identities { + for _, binding := range strings.Split(identity, "; ") { + name, value, ok := strings.Cut(binding, " = ") + if !ok { + continue + } + if values[name] == nil { + values[name] = make(map[string]bool) + } + values[name][value] = true + } + } + out := make(map[string][]string, len(values)) + for name, set := range values { + out[name] = slices.Sorted(maps.Keys(set)) + } + return out +} diff --git a/internal/exec/smt/encode.go b/internal/exec/smt/encode.go index 4b05897aba..7ca1cd4e88 100644 --- a/internal/exec/smt/encode.go +++ b/internal/exec/smt/encode.go @@ -253,7 +253,7 @@ func (e *Encoding) collectAttribute(attr lower.Attribute, declared map[string]bo if attr.Shadowed && attr.Symbol != nil { written = attr.Symbol.Name } - if fp := lower.ExpressionFootprint(graph.Resolver(), graph.Semantics(), scope, attr.Value); attr.Binding && (len(fp.Reads) > 0 || fp.Dynamic) { + if _, derived := derivation(graph, attr); derived { return &UnsupportedError{Node: nodeLabel(graph.Initial), Construct: "attribute " + attr.Name, Reason: "a feature valued by an expression over other features is computed as it is read; the states carry only values written"} } @@ -289,6 +289,21 @@ func (e *Encoding) collectAttribute(attr lower.Attribute, declared map[string]bo return nil } +// derivation reports whether attr is valued by an expression over other +// features (`y = x + 1`, a binding the interpreter computes at every read rather +// than a `:=` initial value), with what the expression reads. +func derivation(graph *lower.ActionGraph, attr lower.Attribute) (lower.Footprint, bool) { + if !attr.Binding || attr.Value == nil { + return lower.Footprint{}, false + } + scope := attr.Scope + if scope == nil { + scope = graph.Scope + } + fp := lower.ExpressionFootprint(graph.Resolver(), graph.Semantics(), scope, attr.Value) + return fp, len(fp.Reads) > 0 || fp.Dynamic +} + // collectNode translates what one node evaluates: its flows, its body, an // inline expression and its result pin, and the guards of its outgoing edges. func (e *Encoding) collectNode(node ast.Node, declared map[string]bool) error { From 9c11f7b4fb32902600f1127b65e88ee0bfe3145f Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 28 Oct 2026 03:28:14 +0000 Subject: [PATCH 2/6] feat(smt): encode features valued by an expression over other features A feature valued by an expression over other features keeps its variable in every state but is never framed: each state defines it by the expression over the state's values, and a read within a move substitutes the expression over the move's current environment, through features so valued in turn. An unresolvable footprint, a narrowing declared type, an assignment to such a feature and a release of one are refused naming the reason. A result of a feature the interpreter holds as a sequence of one value is spelled as such. Co-Authored-By: jason.han --- internal/exec/smt/derived_test.go | 124 +++++++++++++++++++++++++++ internal/exec/smt/encode.go | 135 +++++++++++++++++++++++++++++- internal/exec/smt/input.go | 4 + internal/exec/smt/property.go | 6 ++ internal/exec/smt/witness.go | 3 + 5 files changed, 268 insertions(+), 4 deletions(-) diff --git a/internal/exec/smt/derived_test.go b/internal/exec/smt/derived_test.go index e9ea207f34..722f68b671 100644 --- a/internal/exec/smt/derived_test.go +++ b/internal/exec/smt/derived_test.go @@ -1,13 +1,16 @@ package smt import ( + "context" "errors" + "fmt" "maps" "slices" "strings" "testing" "github.com/Open-MBEE/OpenSysML/internal/exec/analysis" + "github.com/Open-MBEE/OpenSysML/internal/exec/runtime" "github.com/Open-MBEE/OpenSysML/internal/semantic/symbols" ) @@ -112,3 +115,124 @@ func valuesPerFeature(identities []string) map[string][]string { } return out } + +const derivedSrc = `package test { + private import ScalarValues::*; + action def Gate { + attribute x : Integer = 0; + attribute y : Integer = x + 1; + attribute v : Integer = y * 2; + attribute took : Boolean = false; + requirement tracks { require y == x + 1; } + requirement small { require v < 12; } + first start; + action set { assign x := 5; } + decide pick; + action hi { assign took := true; } + action lo { assign took := false; } + done; + succession first start then set; + succession first set then pick; + succession first pick if y > 3 then hi; + succession first pick if y <= 3 then lo; + succession first hi then done; + succession first lo then done; + } + action def Free { + attribute n : Integer = 0; + attribute y : Integer = n + 1; + requirement nonneg { require n >= 0; } + constraint positive { y > 0 } + first start; + done; + succession first start then done; + } +}` + +// TestDerivedFeatureInGuardAndProperty: a guard, a chained feature and a property +// read a feature valued by an expression at its current value — after the write +// of what it reads, not at its starting value — and an assumption over the +// initial state constrains the released input the expression reads. +func TestDerivedFeatureInGuardAndProperty(t *testing.T) { + e := engine(t) + solver := requireSolver(t) + d := indexed(t, "derived.sysml", derivedSrc) + budget := analysis.Budget{Depth: 8} + + action := lookup(t, d.idx, "test::Gate") + encoding, refusal := encodeDocument(t, d, action, budget) + if refusal != nil { + t.Fatalf("refused: %v", refusal) + } + exploration := explore(t, runtime.DefaultExploreBudget, d.fresh(budget), action) + outcomes := compareOutcomes(t, solver, encoding, d, action, budget, exploration) + if want := []string{"took = true; v = 12; x = 5; y = 6"}; !slices.Equal(outcomes.found, want) || !outcomes.agreeing || outcomes.replayed != 1 { + t.Errorf("the solver reaches %q (agreeing %v, %d replayed), want %q", outcomes.found, outcomes.agreeing, outcomes.replayed, want) + } + expect(t, answer(t, e, d, d.holds(t, "test::Gate", "test::Gate::tracks"), budget), analysis.ClaimHolds, analysis.Proved) + expect(t, answer(t, e, d, d.holds(t, "test::Gate", "test::Gate::small"), budget), analysis.ClaimViolated, analysis.Witnessed) + + q := d.holds(t, "test::Free", "test::Free::nonneg") + q.Holds.Inputs = []string{"n"} + expect(t, answer(t, e, d, q, budget), analysis.ClaimViolated, analysis.Witnessed) + q.Holds.Assume = []*symbols.Symbol{lookup(t, d.idx, "test::Free::positive")} + expect(t, answer(t, e, d, q, budget), analysis.ClaimHolds, analysis.Proved) +} + +// TestDerivedFeatureRefusals: what the encoding of a feature valued by an +// expression does not cover is refused naming the feature and the reason, and a +// cycle among such features is the interpreter's refusal at the start, before +// any encoding. +func TestDerivedFeatureRefusals(t *testing.T) { + t.Run("cycle", func(t *testing.T) { + e := engine(t) + d := indexed(t, "cycle.sysml", `package test { + private import ScalarValues::*; + action m { + attribute y : Integer = w + 1; + attribute w : Integer = y * 2; + first start; + done; + succession first start then done; + } +}`) + _, err := e.Run(context.Background(), d.model, d.holds(t, "test::m", ""), analysis.Budget{Depth: 4}) + if want := "cyclic feature value dependency: y"; err == nil || !strings.Contains(err.Error(), want) { + t.Fatalf("run: %v, want the interpreter's refusal %q", err, want) + } + }) + const flow = ` + first start; + action a { %s } + done; + succession first start then a; + succession first a then done; + } +}` + model := func(features, body string) string { + return "package test {\n\tprivate import ScalarValues::*;\n\taction m {\n" + features + fmt.Sprintf(flow, body) + } + cases := []struct { + name, src, release, want string + }{ + {"assignment", model("attribute x : Integer = 0; attribute y : Integer = x + 1;", "assign y := 7;"), "", + "assignment to y: a feature valued by an expression over other features holds the value written until written again"}, + {"release", model("attribute x : Integer = 0; attribute y : Integer = x + 1;", "assign x := 7;"), "y", + "action m values it by an expression over other features; free a feature it reads instead"}, + {"narrowed type", model("attribute x : Integer = 0; attribute y : Natural = x + 1;", "assign x := 7;"), "", + "attribute y: a feature valued by an expression over other features, with a declared type narrowing its sort, is not encoded"}, + } + for _, c := range cases { + t.Run(c.name, func(t *testing.T) { + ctx, action, graph, held := loweredAction(t, c.src, "test::m") + var releases []string + if c.release != "" { + releases = []string{c.release} + } + _, err := Encode(ctx, action, graph, held, releases, 4, DefaultUnroll) + if err == nil || !strings.Contains(err.Error(), c.want) { + t.Fatalf("encode: %v, want a refusal containing %q", err, c.want) + } + }) + } +} diff --git a/internal/exec/smt/encode.go b/internal/exec/smt/encode.go index 7ca1cd4e88..cfc07ff497 100644 --- a/internal/exec/smt/encode.go +++ b/internal/exec/smt/encode.go @@ -5,6 +5,7 @@ import ( "fmt" "maps" "math/big" + "slices" "sort" "github.com/Open-MBEE/OpenSysML/internal/exec/runtime" @@ -50,6 +51,9 @@ type Encoding struct { flagged map[string]bool domains map[string]*solve.Term exprs map[ast.Node]*solve.Expression + // derived is, by variable name, each feature valued by an expression over + // other features: never framed, defined per state and substituted at every read. + derived map[string]derivedFeature // pins are the features each node's performance starts afresh; pending // holds the delivery an object flow left at a pin, keyed by the pin. pins map[ast.Node][]pin @@ -123,6 +127,7 @@ func Encode(ctx *runtime.Context, action *symbols.Symbol, graph *lower.ActionGra flagged: make(map[string]bool), domains: make(map[string]*solve.Term), exprs: make(map[ast.Node]*solve.Expression), + derived: make(map[string]derivedFeature), pins: make(map[ast.Node][]pin), pending: make(map[string]*solve.Var), marks: make(map[string]*solve.Var), @@ -228,6 +233,9 @@ func (e *Encoding) collectFeatures() error { e.domains[read.Name] = term } } + if err := e.checkDerived(); err != nil { + return err + } for i := range e.Inputs { e.Inputs[i].Domain = e.domainText(e.Inputs[i].Var) } @@ -253,9 +261,8 @@ func (e *Encoding) collectAttribute(attr lower.Attribute, declared map[string]bo if attr.Shadowed && attr.Symbol != nil { written = attr.Symbol.Name } - if _, derived := derivation(graph, attr); derived { - return &UnsupportedError{Node: nodeLabel(graph.Initial), Construct: "attribute " + attr.Name, - Reason: "a feature valued by an expression over other features is computed as it is read; the states carry only values written"} + if fp, derived := derivation(graph, attr); derived { + return e.collectDerived(attr, fp, written, scope, declared) } free, released := e.frees(attr) if free { @@ -289,6 +296,105 @@ func (e *Encoding) collectAttribute(attr lower.Attribute, declared map[string]bo return nil } +// collectDerived declares the variable of a feature valued by an expression over +// other features and keeps the expression: every state defines the variable by it +// and every read within a move substitutes it, as the interpreter computes the +// feature at each read. It is no input: neither pinned nor free in state 0. +func (e *Encoding) collectDerived(attr lower.Attribute, fp lower.Footprint, written string, scope *symbols.Scope, declared map[string]bool) error { + label, construct := nodeLabel(e.Flow.Graph.Initial), "attribute "+attr.Name + if fp.Dynamic { + return &UnsupportedError{Node: label, Construct: construct, + Reason: "a feature valued by an expression whose reads the lowering cannot resolve is not encoded"} + } + v, err := e.variable(written, scope, construct, label) + if err != nil { + return err + } + declared[v.Name] = true + expr, err := e.expression(attr.Value, scope, "value of "+attr.Name, label) + if err != nil { + return err + } + e.derived[v.Name] = derivedFeature{name: attr.Name, expr: expr} + return nil +} + +// derivedFeature is a feature valued by an expression over other features, as +// the performance names it, with the expression translated. +type derivedFeature struct { + name string + expr *solve.Expression +} + +// checkDerived refuses a feature valued by an expression whose declared type +// narrows its sort, then flags each whose value may be undefined: its expression +// has side conditions, or a feature it reads may hold none. A cycle among such +// features never reaches the encoding: the interpreter refuses it at the start. +func (e *Encoding) checkDerived() error { + flagged := make(map[string]bool) + var visit func(name string) bool + visit = func(name string) bool { + if undefined, visited := flagged[name]; visited { + return undefined + } + expr := e.derived[name].expr + undefined := len(expr.Defined) > 0 + for _, read := range expressionReads(expr) { + if _, derived := e.derived[read.Name]; derived { + undefined = visit(read.Name) || undefined + } + undefined = undefined || e.flagged[read.Name] + } + flagged[name] = undefined + return undefined + } + for _, name := range slices.Sorted(maps.Keys(e.derived)) { + if _, narrowed := e.domains[name]; narrowed { + return &UnsupportedError{Node: nodeLabel(e.Flow.Graph.Initial), Construct: "attribute " + e.derived[name].name, + Reason: "a feature valued by an expression over other features, with a declared type narrowing its sort, is not encoded: the value is checked against the type at each read"} + } + if visit(name) { + e.flagged[name] = true + } + } + return nil +} + +// expressionReads are the variables an expression reads, each once, in first-read order. +func expressionReads(expr *solve.Expression) []*solve.Var { + seen := make(map[string]bool) + var vars []*solve.Var + visit := func(t *solve.Term) { + if t.Op == solve.OpVar && !seen[t.Var.Name] { + seen[t.Var.Name] = true + vars = append(vars, t.Var) + } + } + walk(expr.Term, visit) + for _, d := range expr.Defined { + walk(d, visit) + } + return vars +} + +// deriveValues defines each feature valued by an expression in state s by the +// expression over the state's values and, where it may be undefined, its +// presence by the condition under which the interpreter computes it. +func (e *Encoding) deriveValues(s *State, where string) { + env := e.environment(s) + for _, base := range e.Features { + d, derived := e.derived[base.Name] + if !derived { + continue + } + value, defined := env.evaluate(d.expr) + e.assert(eq(solve.VarTerm(s.value(base)), value), where+": "+base.Name) + if e.flagged[base.Name] { + e.assert(eq(solve.VarTerm(s.has(base)), defined), where+": "+base.Name) + } + } +} + // derivation reports whether attr is valued by an expression over other // features (`y = x + 1`, a binding the interpreter computes at every read rather // than a `:=` initial value), with what the expression reads. @@ -488,9 +594,14 @@ func (e *Encoding) collectBody(body []lower.Statement, label string, declared ma if _, err := e.expression(s.Value, s.Scope, "assignment to "+s.Target, label); err != nil { return err } - if _, err := e.variable(s.Target, s.Scope, "assignment to "+s.Target, label); err != nil { + v, err := e.variable(s.Target, s.Scope, "assignment to "+s.Target, label) + if err != nil { return err } + if _, derived := e.derived[v.Name]; derived { + return &UnsupportedError{Node: label, Construct: "assignment to " + s.Target, + Reason: "a feature valued by an expression over other features holds the value written until written again; the encoding computes it from the expression at every read"} + } case lower.Declare: construct := "declaration of " + s.Name v, err := e.variable(s.Name, s.Scope, construct, label) @@ -724,6 +835,9 @@ func (e *Encoding) initial() error { } } for _, base := range e.Features { + if _, derived := e.derived[base.Name]; derived { + continue + } // A flagged feature starts absent, but an optional free input's presence is // the solver's to choose: its state-0 flag stays open. if e.flagged[base.Name] && !open[base.Name] { @@ -737,7 +851,11 @@ func (e *Encoding) initial() error { if err != nil { return err } + e.deriveValues(s, initialState) for _, base := range e.Features { + if _, derived := e.derived[base.Name]; derived { + continue + } if value := env.values[base.Name]; value.Op != solve.OpVar || value.Var != s.value(base) { e.assert(eq(solve.VarTerm(s.value(base)), value), "initial value of "+base.Name) } @@ -851,6 +969,7 @@ func (e *Encoding) move(i int) error { return err } e.featureValues(i, prev, next, effects, acts) + e.deriveValues(next, fmt.Sprintf("move %d", i)) failed, overflow := e.carried(prev, effects, acts) e.loopsPastBound(i, prev, next, effects, acts) @@ -960,6 +1079,9 @@ func (e *Encoding) performances(i int, prev *State, m *Move, acts []*solve.Term) // else to their values before it. func (e *Encoding) featureValues(i int, prev, next *State, effects []*nodeEffect, acts []*solve.Term) { for _, base := range e.Features { + if _, derived := e.derived[base.Name]; derived { + continue + } value := solve.VarTerm(prev.value(base)) var has *solve.Term if e.flagged[base.Name] { @@ -1863,6 +1985,11 @@ func (v *env) write(name string, value *solve.Term) { func (v *env) evaluate(expr *solve.Expression) (value, defined *solve.Term) { var reads []*solve.Term replace := func(base *solve.Var) *solve.Term { + if d, derived := v.enc.derived[base.Name]; derived { + value, defined := v.evaluate(d.expr) + reads = append(reads, defined) + return value + } if has, flagged := v.has[base.Name]; flagged { reads = append(reads, has) } diff --git a/internal/exec/smt/input.go b/internal/exec/smt/input.go index 17f18e205e..a303d26f87 100644 --- a/internal/exec/smt/input.go +++ b/internal/exec/smt/input.go @@ -70,6 +70,7 @@ func (e *Encoding) checkReleases(action string) error { } for _, name := range e.releases { attr, ok := features[name] + _, derived := derivation(e.Flow.Graph, attr) switch { case !ok: return &analysis.InputError{Engine: EngineName, Feature: name, @@ -77,6 +78,9 @@ func (e *Encoding) checkReleases(action string) error { case attr.Output(): return &analysis.InputError{Engine: EngineName, Feature: name, Reason: fmt.Sprintf("action %s writes it back rather than reading it", action)} + case derived: + return &analysis.InputError{Engine: EngineName, Feature: name, + Reason: fmt.Sprintf("action %s values it by an expression over other features; free a feature it reads instead", action)} } } return nil diff --git a/internal/exec/smt/property.go b/internal/exec/smt/property.go index a101f5438e..a93e04ad2c 100644 --- a/internal/exec/smt/property.go +++ b/internal/exec/smt/property.go @@ -259,6 +259,9 @@ type Output struct { Var *solve.Var // Has is nil for an attribute that holds a value in every state. Has *solve.Var + // Sequence reports a feature the interpreter holds as a sequence of its one + // value, which a result spells as such (`[2]`). + Sequence bool } // Outputs are the features the performance holds as the final state leaves @@ -277,6 +280,9 @@ func (e *Encoding) Outputs() []Output { continue } out := Output{Name: attr.Name, Var: final.value(base)} + if held, ok := e.held.Value(attr.Name); ok && held.Kind == runtime.ValSequence { + out.Sequence = true + } if e.flagged[base.Name] { out.Has = final.has(base) } diff --git a/internal/exec/smt/witness.go b/internal/exec/smt/witness.go index c93564f950..80e0fb0a76 100644 --- a/internal/exec/smt/witness.go +++ b/internal/exec/smt/witness.go @@ -353,6 +353,9 @@ func (e *Encoding) DecodeOutputs(values []solve.Assignment) (map[string]string, if err != nil { return nil, &WitnessError{Var: out.Var.Name, Reason: err.Error()} } + if out.Sequence { + text = "[" + text + "]" + } outputs[out.Name] = text } return outputs, nil From a0e3ffcbe2375cced944d3017c3ae029c7cf2473 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 28 Oct 2026 03:39:48 +0000 Subject: [PATCH 3/6] docs(smt): document the encoding of features valued by an expression The six conformance fixtures holding such a feature state a solver budget of 20 moves, within which every run of theirs ends, so cvc5 decides their fixed outcomes within the default timeout as z3 does. Co-Authored-By: jason.han --- changes/unreleased/smt-derived-features.added.md | 1 + docs/internals/design/smt-model-checking.md | 2 ++ docs/project/spec-compliance.md | 4 ++-- ...ction_order_bound_chain_of_racing_writer.expected.json | 1 + ...action_order_bound_read_of_racing_writer.expected.json | 1 + ...n_order_bound_read_of_unraced_stays_bare.expected.json | 1 + ...er_inherited_bound_read_of_racing_writer.expected.json | 1 + ...r_positional_bound_read_of_racing_writer.expected.json | 1 + .../action_order_write_from_bound_read.expected.json | 1 + internal/exec/smt/encode.go | 8 ++++++-- 10 files changed, 17 insertions(+), 4 deletions(-) create mode 100644 changes/unreleased/smt-derived-features.added.md diff --git a/changes/unreleased/smt-derived-features.added.md b/changes/unreleased/smt-derived-features.added.md new file mode 100644 index 0000000000..2bddc9c287 --- /dev/null +++ b/changes/unreleased/smt-derived-features.added.md @@ -0,0 +1 @@ +- The `smt` engine encodes a feature valued by an expression over other features (`attribute y : Integer = x + 1`) as the interpreter computes it, at every read over the current values: each state defines the feature by its expression and every read within a move substitutes it, through features so valued in turn, so guards, loop conditions, properties, assumptions and results all see the derived value. Such an action was refused (`a feature valued by an expression over other features is computed as it is read`). One whose reads the lowering cannot resolve, one whose declared type narrows its sort, an assignment to one and a `-check-input` release of one are still refused, each naming its reason; a cycle among such features is refused by the interpreter at the start, before any encoding. diff --git a/docs/internals/design/smt-model-checking.md b/docs/internals/design/smt-model-checking.md index 53bd4c123e..0a38100f0d 100644 --- a/docs/internals/design/smt-model-checking.md +++ b/docs/internals/design/smt-model-checking.md @@ -135,6 +135,7 @@ verdict names it. | Tokens | `ActionExecutor.tokens`, ids assigned on spawn | `T` **token slots**, `T` computed from the graph: the widest set of tokens `k` moves can hold, one per fork branch reachable within the bound, plus one per nested flow. `at_i[t]` is a finite datatype over the graph's nodes with `Absent`, `Done` and `Parked` | | Node performances | `stepToken`, `stepJoinNode`, `stepMergeNode` | `joined_i[j]` — how many of join `j`'s incoming successions have delivered. A merge keeps no state: it is one performance per arrival, so a token at a merge is described by its slot alone | | Feature values | `Instance.FeatureValues`, `actionFrame.data` | one variable per scalar feature per state, `x_i`, in the sort the translator already gives the feature; a frame-local feature is one per (node performance, feature) | +| Features valued by an expression | `deriveBodyCell`: `attribute y : Integer = x + 1` is computed at every read over the values then held (a FeatureValue that is not initial, KerML 1.1 §7.3.4.2; `:= expr` is evaluated once and then written like any value) | `y_i` is kept for every state so results, properties and the two-copy query read it as any feature, but never framed: every state asserts `y_i = ⟦x + 1⟧(s_i)` instead, and a read of `y` within a move — a body statement, a guard, a loop condition — substitutes the expression over the move's current environment, so a statement writing `x` and then reading `y` in one body sees the fresh value as the interpreter does. A chain (`v = y * 2`) substitutes recursively; the expression's side conditions and the presence of what it reads define `has(y)_i` when the value may be undefined. The feature is no input: state 0 asserts the same term over the initial values, which is where `-check-input` free features and `-check-assume` meet it. Refused, each naming its reason: one whose reads the lowering cannot resolve (`Footprint.Dynamic`), one whose declared type narrows its sort (the interpreter checks the bound value at each read), an assignment to one (the interpreter then holds the value written) and a `-check-input` release of one; a cycle among such features (`y = w + 1; w = y * 2`) never reaches the encoding, the interpreter refusing it at the start of the performance (`cyclic feature value dependency`) | | Pins and object flows | `PinBinding`, `DataFlows`, delivered `out` pins | the value carried on an object flow is a variable set by the source node's move and read by the target's | | Messages | `Context.messages`, oldest first | a bounded bus of `M` slots, each `(present, signal type, payload, posted-at)`, `M` computed as the number of `Send` statements reachable in `k` moves | | Clock | `Context.Clock()`, `accept after`/`at` | `now_i : Real` (seconds) and a due time per parked token; `now` never decreases and advances only when no token is enabled, to the earliest due time — time is not a choice, only ties are, as the explicit note says. There is no horizon: `k` moves alone bound the run. The library's `Clocks` and `Occurrences`, and `accept after`/`accept at` over them, fix *when* a timed accept becomes enabled and say nothing about how far a run proceeds; fUML, PSCS and PSSM define no clock at all. A horizon would be a bound the specification does not name, so the rule that adds nothing is the one taken, and `-advance` stays refused for `smt` as `check` refuses it | @@ -362,6 +363,7 @@ solver answers and `explore` confirms. | Successions, fork, join, decision with translatable guards | encoded | yes | — | | Merge, merge-loop | encoded; a back edge is a succession like any other, so a merge-loop's iterations are bounded by `k`, not unrolled | yes, to `depth` | a loop still live at `k` sets `cut_k`: *no violation within k moves*, not *proved* — unless k-induction closes it | | Body `assign` of Boolean, Integer, Natural, Rational, Real, enumeration, variation features; `if`; local `Declare` | encoded through the existing translator | yes | — | +| Features valued by an expression over other features (`attribute y : Integer = x + 1`), chains of them | encoded as a per-state defined term and substituted at every read within a move | yes | an unresolvable footprint, a narrowing declared type, an assignment to one or a release of one: *not covered* naming the feature; a cycle among them is the interpreter's refusal at the start | | Quantities with units | encoded, normalized to base units as exact rationals | yes | proof is qualified *over exact arithmetic* when the evaluator rounds | | Feature chains grounding in a scalar of the performing object | encoded | yes | — | | Object-valued pins, chains through an object a pin carries, `new` | not encoded: no heap | yes | *not covered: dynamic target at node* — a bounded heap of `N` objects per type is a later stage | diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 6b36cbe5f0..0ba30b2b08 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -824,7 +824,7 @@ remain one-shot. | A terminate action usage's body is an ordinary `ActionBody` (SysML.xtext `TerminateActionUsage`), so it states successions as any action body does, and its implicit `TerminateAction::terminateOccurrence` (`Actions.sysml`) is a subaction no succession orders against the body's others: it may end the usage's performance before, between or after them, an output pin left unwritten then binding no value ([derivation](behavior-semantic-oracle.md#a-terminate-action-usages-body-and-its-implicit-terminate-each-is-performed-in-which-order-is-open)) | `lower/action_subflow.go` `lowerTerminateNode` (the body, or the flow it states as a block, then the terminate it stands for); `runtime/action_terminate.go` (a `terminate` naming the usage inside its own body ends the usage's performance) | `action_terminate_usage_body_ends_itself.sysml`, `_body_ends_itself_binds_pin`, `_in_block_names_itself`, `_with_body`, `_binds_output_pin`, `_in_block_binds_pin`, `_body_performs_action` (explored and checked to their full outcome sets, the unbound-pin multiplicity violation among them); `TestRuntimeRobustnessTerminateBodyFlow` (a stated flow runs, a `then` chain reaches the terminate early, a succession cycle and a succession to an unknown step are typed errors) | ⚠️ Approximate: `declared` and `reverse` perform the implicit terminate after the body, a tool-defined linearization; action usages written in an `if` or loop block with no succession between them keep declaration order under every policy | | A witness is a run that can be run again: the `replay:` policy reads a file of `input = ` lines — the inputs a solver chose, each as `InputTaken.String` spells them (a rational exactly, an enumeration or variation-point constructor by its qualified name), any number of them or none, so a stage-1 or `check` witness without them replays as before — followed by choice lines — each as `ChoiceTaken.String` spells them, one per line or joined by `; `, up to the first blank line, so a checker's witness file with a trace body after its header serves as it stands — fixes the inputs on the action as it starts, before its defaults and ahead of the moves, through the same path a caller's `Start` values take, refusing one naming a feature the action does not declare or cannot take with the typed `WitnessInputError` naming it, and resolves the run's choice points in that order, each line having to name the step the run is at and pick among the alternatives it offers, then as `reverse` picks, one token a step, once the lines are spent; a line the run cannot follow — a pick not offered, a step already passed — or one left over at the end fails the run with the typed `ReplayError` naming the move, its choice and what the run faced (`Context.Unfollowed`), never silently running another linearization; a file that is empty or whose lines spell no choice is `SchedulePolicyError` as the policy is parsed, while a header of `no choice points` alone is the witness of a run with none and follows it; accepted wherever a policy is spelled (`sysml -schedule`, `%schedule`, a conformance case's `schedule` pin) except the wire, where a request carries no file of the caller's and the spelling is `INVALID_ARGUMENT` | `runtime/replay.go` `ParseWitness`, `parseInput`, `InputTaken`, `inputParseError`, `WitnessInputError`, `ParseChoices`, `ChoiceParseError`, `ReplayPolicy`, `SchedulePolicy.Replay`, `SchedulePolicy.Witness`; `runtime/action_executor.go` `ActionExecutor.fixWitnessInputs`, `Context.Unfollowed`, `ReplayError`, `ErrReplayRefused`, `replayRun.beginStep`, `replayRun.choose`; `runtime/scheduler.go` `ParseSchedulePolicy` (`replay:`), `ReplaySpelling`, `SchedulePolicyNames`; `grpc/service.go` `schedulePolicy` (the wire refusal); `cmd/sysml/usage.go` (the `-schedule` help) | `runtime/replay_input_test.go:TestParseInputReadsEverySpelling`, `:TestParseWitnessReadsInputsBeforeChoices`, `:TestReplayFixesWitnessInputs`; `smt/input_engine_test.go:TestEngineWitnessWithInputsReplaysThroughTheStart`, `:TestEngineWitnessWithoutInputsReplaysAsBefore`; `runtime/replay_test.go:TestParseChoicesRejectsWhatSpellsNoChoice`, `:TestParseChoicesStopsAtBlankLine`, `:TestParseReplayPolicy`, `repl/checker_test.go:TestReplayStepsAWitnessOfNoChoice`, `cmd/sysml/check_engine_test.go:TestEngineCheckWitnessOfNoChoiceReplays`, `:TestReplayFollowsActionWitnesses`, `:TestReplayFileReproducesTheExploredRun` (every witness `explore` tables replays to its run's trace), `:TestReplayFollowsStateWitnesses`, `:TestReplayRefusesAMoveNotEnabled`, `:TestReplayFallsBackToReverse`, `:TestReplayReadsAStepsOrderInEitherPlace`, `:TestReplayProbeLeavesTheWitnessInPlace`, `check_loop_replay_test.go:TestCheckWitnessesOfALoopingDoRoundReplay` (a `do` body looping through timed waits past the witness's last line, top-level), `:TestCheckWitnessesOfAnInlinePerformanceReplay` (an order recorded at the performer's step, resolved in the inner flow), `robustness_replay_test.go:TestRuntimeRobustnessReplay` (an inner order naming a token of no flow, or mixing two, refused; a witness ending before the run), `conformance/state_do_action_loop_timed_exit` + `.check.expected.json`; `cmd/sysml/spacecraft_showcase_test.go:TestEngineCheckWitnessesTheSpacecraftRaceAndReplaysEach` (every witness `-engine check` writes replays to its values); `grpc/schedule_test.go:TestAReplayScheduleIsInvalidArgument`; `smt/referee_test.go:TestRefereeCorpus`, `:TestRefereeInputs` (every solver witness, with its inputs, replayed under it) | ✅ As designed (an OpenSysML policy, like the others; no run under another policy changes) | | A choice point is reported wherever the executor had several enabled alternatives the library does not order, and nowhere else: several steppable tokens in one step (`token order`), several holding guards of one decision (`decision branch`), several tokens writing one feature in one step (`write order`), several enabled transitions out of one state for one event (`transition`), the next unit among the firings transitions in several regions selected for one event make (`region order`), the next entry among the regions a composite state, a fork or a history enters (`entry order`), and the next exit among the regions a state leaves (`exit order`). Each is one trace line `choice : (unordered; took )`, one informational diagnostic with code `choice-point` at the node, decision, feature or state that made it, and a count on the debugger's summary line; none is an error, and a run under a fixed policy reports the same set another fixed policy would have had to make on the linearization it took | `choice.go` `ChoiceKind` (`ChoiceTokenOrder`, `ChoiceDecisionBranch`, `choiceWriteOrder`, `ChoiceTransition`, `ChoiceRegionOrder`, `choiceEntryOrder`, `choiceExitOrder`), `ChoicePoint.String` (the trace line), `ChoicePoint.Describe`, `ChoicePoint.Diagnostic` (`SeverityInfo`, code `ChoiceDiagnosticCode`), `Context.noteChoice`, `Context.Notes`, `Context.Choices`, `ActionExecutor.Notes`/`StateExecutor.Notes`; `action_choice.go` `noteTokenOrder`, `noteDecisionBranches`, `stepWriteLedger.noteChoices`; `state_executor.go` `transitionChoice`, `chooseRegion`; `repl/trace.go` `Session.noteSummary` (`N choice points; %trace on to see them`, or the lines themselves under `%trace on`); `grpc/convert.go` `RunNoteDiagnosticsToProto` (the `diagnostics` of `ExecuteActionResponse`, `ExecuteStateResponse` and `RunAnalysisResponse`) | `choice_test.go:TestChoicePointRendering`, `:TestChoicesResetPerRun`, `:TestTransitionChoiceNamesStateAndEvent`, `:TestWriteConflictChoice`, `:TestSharedMessageAcceptIsAChoice`, `:TestAncestorPriorityIsNotAChoice`; `explore_test.go:TestExploreSiblingRegionOrder` (the `region order` kind); `conformance/action_choice_fork_token_order`, `action_choice_decision_overlapping_guards`, `action_choice_same_step_write_conflict`, `state_choice_transition_conflict`, `state_explore_region_order`, each `+ .trace.golden` carrying its `choice` line; `repl/choice_test.go:TestStepReportsChoicePoints`, `:TestStepChoiceSummaryWithTraceOn`, `:TestContinueReportsChoicePoints`, `:TestAdvanceReportsChoicePoints`; `grpc/choice_test.go:TestExecuteAction_ChoicePointDiagnostics`, `:TestExecuteState_ChoicePointDiagnostics`, `:TestRunAnalysis_ChoicePointDiagnostics`; `conformance_test.go:TestConformanceDiagnosticsGate` (an informational note is no failure of a conformance case) | ✅ Faithful (the ancestor-priority case between a substate's transition and its enclosing state's is ordered by SysML v2/KerML and is not reported — `state_choice_ancestor_priority_not_reported`, `state_choice_ancestor_outranked_not_reported`) | -| A default run reports its values only up to the partial order the library fixes: `HappensBefore` holds between the occurrences a succession joins and between a send and its accept (Kernel Semantic Library `Occurrences.kerml`, `Performances.kerml`, KerML 1.1 §9.2.4 Occurrences, §9.2.6 Performances), and nothing orders the rest, so a linearization's value of a feature two unordered alternatives both write is one of several the model admits, not the result. Each recorded choice point is classified from the lowered footprints the checker's reduction uses: alternatives that write what another reads or writes, or send and accept on one channel, conflict (a property read or a chained target the declarations do not decide counts as conflicting); alternatives that commute are `independent`, one outcome by construction, and mark nothing. A value a conflicting alternative wrote prints with the marker `x = 1 (order-dependent; 2 choice points — explore shows the set)` on every surface, and so does a value computed from it: a write stands on what its footprint read and on the control it ran under (a guard or condition read, a branch or transition drawn), a message carries what its payload stood on to the accept that binds it, a performance's outputs stand on its inputs, a feature valued by an expression (`attribute y : Integer = x + 1`, a FeatureValue that is not initial, KerML 1.1 §7.3.4.2) stands on what its expression reads at the moment it is read, through features so valued in turn, and a write that reads nothing order-dependent clears the mark; a value nothing order-dependent reached prints as before | `order_dependence.go` `classifyChoice`, `classifyExclusive`, `classifyBy`, `ChoicePoint.Independent`/`Touches`, `Context.OrderDependent`, `OrderDependenceText`; `order_marks.go` `orderMarks.seed`/`rewrite`, `Context.propagateMarks`, `standingOf`, `underControl`, `acceptMarks` (from `statements.go` `stmtEngine.statement`, `ifStatement`, `iteration`, `statementUnder`; `action_executor.go` `stepToken`, `stepDecisionNode`, `awaitSignal`; `action_statements.go` `markPerformance` over `lower.ActionGraph.BindingFootprints`; `state_executor.go` `taking`, `bindAcceptPayload`; `signal.go` `Message.dependence`); per site `action_choice.go` `noteTokenOrder` (`stepOrder.able`), `stepWriteLedger.noteChoices`, `chooseBranch`; `advance.go` `runDue`; `check_run.go` `drawOwner`; `state_unit_front.go` `drain`, `drawOnPath` over `unitQueue.footprint` (`state_unit_footprint.go`); `state_executor.go` `nextEvent` (`eventFootprint`), `stepOrderChoice`, `regionOrderChoice` (a do round by `doStepFootprint`; a join by `lower/state_footprint.go` `JoinSegmentFootprints`: each pending segment's trigger, guard and effects with the exits from its source up to the join's owner, less the owner's exit and the way out every order shares), `branchPoint` over `lower/state_footprint.go` `BranchFootprintsFrom` (a junction or choice branch for the state the transition left: the states exited and entered with the branch's guard and effects, less the exits every branch shares; `BranchFootprints` when no origin is known); `order_dependence.go` `choiceTouches` (a bare name is the behavior's own feature, `this.` the performing object's, so a write to one never marks the other); `state_run_to_completion.go` `entryStep`; `statements.go` `pickStatement` (`lower.StatementOrder.Dependent`); `lower/footprint.go` `footprintBuilder.boundValue`, `redefined` (a lowered footprint reads through a feature valued by an expression, a redefining feature through the value of the one it redefines along `semantics.ParameterRedefinitionChain`, explicit or by position); `order_marks.go` `Context.deriveMarks` from `body_bindings.go` `deriveBodyCell` (the derived feature's place is rewritten with what its expression read); `smt/encode.go` `Encoding.collectAttribute` (the SMT engine refuses an action declaring a feature valued by an expression over other features, `attribute `, rather than hold it at its starting value); surfaces `repl/run.go` `namedValue`, `repl/meta.go` `formatFeatureValue`, `choice.go` `ChoicePoint.Standing`, `grpc/service.go` `orderDependent`, `grpc/convert.go` `RunNoteDiagnosticsToProto` | `robustness_order_dependence_test.go:TestRuntimeRobustnessOrderDependence`, `robustness_order_dependence_transitive_test.go:TestRuntimeRobustnessOrderDependenceTransitive`; conformance `action_explore_three_writers` (`orderDependent` `x: 2`), `action_order_derived_from_racing_writers` (`x: 2, y: 2`), `action_order_bound_read_of_racing_writer` (`x: 2, y: 2`; `y = x + 1` read after the join), `action_order_write_from_bound_read` (`x: 2, y: 2, z: 2`; `w := x + 1` bare), `action_order_bound_chain_of_racing_writer` (`v: 2, x: 2, y: 2, z: 2`), `action_order_bound_read_of_unraced_stays_bare` (`x: 2`; `q = p + 1` bare), `action_order_inherited_bound_read_of_racing_writer` (`x: 2, y: 2, z: 2`; `attribute :>> y;` bound as `Base::y = x + 1`), `action_order_positional_bound_read_of_racing_writer` (`out yRace : Integer;` redefining `out yBase : Integer = x + 1` by position), `action_order_guard_reads_racing_writer` (`x: 2, mode: 2`), `action_order_inherited_guard_reads_racing_writer` (`go: 2, mode: 2`; the guard read in the scope of the succession's declaration), `action_order_independent_sibling_stays_bare` (`x: 2, y: 2`; `p`, `q` bare), `action_order_through_performed_action` (`x: 2, result: 2`), `action_order_send_payload_from_racing_writer` (`x: 2, total: 2`), `state_order_effect_reads_racing_attribute` (`last: 1, derived: 1`), `action_order_rewrite_clears_mark` (none), `action_order_independent_branches` (none), `action_order_overlapping_guards` (`mode: 1`), `state_order_regions_conflict` (`last: 1`), `state_order_regions_independent` (none), `state_order_do_round_conflict` (`log: 1`), `state_junction_several_enabled_branches` (`route: 1`), `state_junction_shared_exit_not_branch_dependent` (`route: 1`, `log` fixed), each with its golden trace; `grpc/choice_test.go`, `grpc/schedule_test.go`, `repl/choice_test.go` | ✅ Faithful (the choice points a value stands on follow the data: a value computed from an order-dependent one, through an assignment, a feature valued by an expression over it, a guard or condition read, a performed action's parameters, a message's payload or a transition's effect, carries the same marks; a write that reads nothing order-dependent clears them; `explore` enumerates the set) | +| A default run reports its values only up to the partial order the library fixes: `HappensBefore` holds between the occurrences a succession joins and between a send and its accept (Kernel Semantic Library `Occurrences.kerml`, `Performances.kerml`, KerML 1.1 §9.2.4 Occurrences, §9.2.6 Performances), and nothing orders the rest, so a linearization's value of a feature two unordered alternatives both write is one of several the model admits, not the result. Each recorded choice point is classified from the lowered footprints the checker's reduction uses: alternatives that write what another reads or writes, or send and accept on one channel, conflict (a property read or a chained target the declarations do not decide counts as conflicting); alternatives that commute are `independent`, one outcome by construction, and mark nothing. A value a conflicting alternative wrote prints with the marker `x = 1 (order-dependent; 2 choice points — explore shows the set)` on every surface, and so does a value computed from it: a write stands on what its footprint read and on the control it ran under (a guard or condition read, a branch or transition drawn), a message carries what its payload stood on to the accept that binds it, a performance's outputs stand on its inputs, a feature valued by an expression (`attribute y : Integer = x + 1`, a FeatureValue that is not initial, KerML 1.1 §7.3.4.2) stands on what its expression reads at the moment it is read, through features so valued in turn, and a write that reads nothing order-dependent clears the mark; a value nothing order-dependent reached prints as before | `order_dependence.go` `classifyChoice`, `classifyExclusive`, `classifyBy`, `ChoicePoint.Independent`/`Touches`, `Context.OrderDependent`, `OrderDependenceText`; `order_marks.go` `orderMarks.seed`/`rewrite`, `Context.propagateMarks`, `standingOf`, `underControl`, `acceptMarks` (from `statements.go` `stmtEngine.statement`, `ifStatement`, `iteration`, `statementUnder`; `action_executor.go` `stepToken`, `stepDecisionNode`, `awaitSignal`; `action_statements.go` `markPerformance` over `lower.ActionGraph.BindingFootprints`; `state_executor.go` `taking`, `bindAcceptPayload`; `signal.go` `Message.dependence`); per site `action_choice.go` `noteTokenOrder` (`stepOrder.able`), `stepWriteLedger.noteChoices`, `chooseBranch`; `advance.go` `runDue`; `check_run.go` `drawOwner`; `state_unit_front.go` `drain`, `drawOnPath` over `unitQueue.footprint` (`state_unit_footprint.go`); `state_executor.go` `nextEvent` (`eventFootprint`), `stepOrderChoice`, `regionOrderChoice` (a do round by `doStepFootprint`; a join by `lower/state_footprint.go` `JoinSegmentFootprints`: each pending segment's trigger, guard and effects with the exits from its source up to the join's owner, less the owner's exit and the way out every order shares), `branchPoint` over `lower/state_footprint.go` `BranchFootprintsFrom` (a junction or choice branch for the state the transition left: the states exited and entered with the branch's guard and effects, less the exits every branch shares; `BranchFootprints` when no origin is known); `order_dependence.go` `choiceTouches` (a bare name is the behavior's own feature, `this.` the performing object's, so a write to one never marks the other); `state_run_to_completion.go` `entryStep`; `statements.go` `pickStatement` (`lower.StatementOrder.Dependent`); `lower/footprint.go` `footprintBuilder.boundValue`, `redefined` (a lowered footprint reads through a feature valued by an expression, a redefining feature through the value of the one it redefines along `semantics.ParameterRedefinitionChain`, explicit or by position); `order_marks.go` `Context.deriveMarks` from `body_bindings.go` `deriveBodyCell` (the derived feature's place is rewritten with what its expression read); `smt/encode.go` `Encoding.collectDerived`, `Encoding.deriveValues`, `env.evaluate` (the SMT engine defines a feature valued by an expression over other features by its expression in every state and substitutes it at every read, rather than hold it at its starting value); surfaces `repl/run.go` `namedValue`, `repl/meta.go` `formatFeatureValue`, `choice.go` `ChoicePoint.Standing`, `grpc/service.go` `orderDependent`, `grpc/convert.go` `RunNoteDiagnosticsToProto` | `robustness_order_dependence_test.go:TestRuntimeRobustnessOrderDependence`, `robustness_order_dependence_transitive_test.go:TestRuntimeRobustnessOrderDependenceTransitive`; conformance `action_explore_three_writers` (`orderDependent` `x: 2`), `action_order_derived_from_racing_writers` (`x: 2, y: 2`), `action_order_bound_read_of_racing_writer` (`x: 2, y: 2`; `y = x + 1` read after the join), `action_order_write_from_bound_read` (`x: 2, y: 2, z: 2`; `w := x + 1` bare), `action_order_bound_chain_of_racing_writer` (`v: 2, x: 2, y: 2, z: 2`), `action_order_bound_read_of_unraced_stays_bare` (`x: 2`; `q = p + 1` bare), `action_order_inherited_bound_read_of_racing_writer` (`x: 2, y: 2, z: 2`; `attribute :>> y;` bound as `Base::y = x + 1`), `action_order_positional_bound_read_of_racing_writer` (`out yRace : Integer;` redefining `out yBase : Integer = x + 1` by position), `action_order_guard_reads_racing_writer` (`x: 2, mode: 2`), `action_order_inherited_guard_reads_racing_writer` (`go: 2, mode: 2`; the guard read in the scope of the succession's declaration), `action_order_independent_sibling_stays_bare` (`x: 2, y: 2`; `p`, `q` bare), `action_order_through_performed_action` (`x: 2, result: 2`), `action_order_send_payload_from_racing_writer` (`x: 2, total: 2`), `state_order_effect_reads_racing_attribute` (`last: 1, derived: 1`), `action_order_rewrite_clears_mark` (none), `action_order_independent_branches` (none), `action_order_overlapping_guards` (`mode: 1`), `state_order_regions_conflict` (`last: 1`), `state_order_regions_independent` (none), `state_order_do_round_conflict` (`log: 1`), `state_junction_several_enabled_branches` (`route: 1`), `state_junction_shared_exit_not_branch_dependent` (`route: 1`, `log` fixed), each with its golden trace; `grpc/choice_test.go`, `grpc/schedule_test.go`, `repl/choice_test.go` | ✅ Faithful (the choice points a value stands on follow the data: a value computed from an order-dependent one, through an assignment, a feature valued by an expression over it, a guard or condition read, a performed action's parameters, a message's payload or a transition's effect, carries the same marks; a write that reads nothing order-dependent clears them; `explore` enumerates the set) | | A guard the executor reads only to report a choice — one after the branch or transition already taken — that fails to evaluate is no alternative and no error: a guard with no result is not true, so its succession is not selected, the run is unchanged, and the failure is an informational `guard-unevaluable` note, while the same failure at the guard the run does take still fails the run | `choice.go` `UnevaluableGuard`, `UnevaluableGuard.Diagnostic` (`SeverityInfo`, code `UnevaluableGuardCode`), `Context.noteUnevaluableGuard`, `Context.unevaluableGuards`; `action_choice.go` `ActionExecutor.noteUnevaluableGuard`; `action_executor.go` `probeGuard` (a `beginProbe` preview that restores the budget, the trace, every effect and the object identities it took); `state_executor.go` `probeTransition`, `unevaluableTransition`; `state_route.go` `probeBranch` (a choice pseudostate's later branch); `state_change_trigger.go` `probeChangeGuard` | `conformance/action_choice_unevaluable_guard` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_transition` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_branch` + `.expected.json` + `.trace.golden`; `choice_test.go:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestLaterChoiceGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestLaterGuardIsProbedWithoutCost`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteAction_UnevaluableGuardDiagnostics`; `repl/choice_test.go:TestStepReportsUnevaluableGuards`; `robustness_action_flow_test.go:decision_no_satisfied_guard` (the taken path still fails) | ✅ Faithful (SysML v2 §7.17.3 selects a succession whose guard is true; a guard that cannot be evaluated is not true, and reading it changed nothing) | | A conformance case that admits several outcomes states the whole set: `outcomes` lists every admissible outcome in full — never "anything" — and `admissible` cites the section of `behavior-semantic-oracle.md` that derives the set; a `.trace.order` beside it states the partial order the library does fix as `earlier < later` over trace labels. The harness checks the run's outcome is exactly one listed member, checks the trace against every order constraint, then explores the case and fails on a listed outcome no linearization reached, a reached outcome the list omits, and a hit budget — each naming the outcome and a witness choice sequence | `conformance_test.go` `ExpectedOutcome.Outcomes`/`Admissible`/`ExploreBudget`, `admissibleSchemaProblems` (an `outcomes` list needs two or more full outcomes, an `admissible` title the oracle has, and no single-outcome fields beside it), `matchOutcome`, `runConformanceCase`, `exploreConformanceCase`; `trace_test.go` `checkTraceOrder`, `parseOrderConstraints`, `orderViolations`; `testdata/conformance/README.md` (the schema) | `conformance_test.go:TestAdmissibleOutcomesSchema`, `:TestMatchOutcomeRequiresExactlyOne`, `:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case), `:TestExecutionConformanceUnderPolicies`; `trace_test.go:TestTraceOrderViolationFails`, `:TestExecutionTrace`; `conformance/action_explore_three_writers` (`outcomes` of three, `.trace.order` of six constraints; explored in six runs), `action_choice_shared_message_accept`, `action_choice_fork_token_order` (one outcome, a `.trace.order` admitting the tokens either way), `state_explore_region_order` | ✅ Faithful (a case without `outcomes` is not explored by the harness, so a fixture pinning one linearization of an unobservable openness stays a one-outcome case; the oracle names which fixtures those are) | | Exploration is bounded and distinguishes setup failures from runtime outcomes: the budget is runs (1024 by default) and choice points per run (64), and a budget hit ends the search as `incomplete: budget hit after N runs`, naming `runs` before `depth`; a fresh-context or root-executor creation failure, or a pure structural start-check failure before root behavior runs, means no linearization ran and is returned without outcomes, while a failure during initial model behavior or later is an error outcome. Any runtime-error linearization makes the verdict fail, including an incomplete exploration; only an incomplete search without a witnessed failure is unresolved, and only a complete search without failures proves the outcome set. JSON and the wire include `failedLinearizations` / `failed_linearizations` only when nonzero; standing evidence names the failing count | `runtime/explore.go` `SetupError`, `Exploration.FailedLinearizations`; `runtime/context.go` root action/state setup classification; `runtime/explore_queue.go` `ExploreWith`, `exploreQueue.work`; `runtime/check.go` checker setup failure; `analysis/explore.go` proof strength; `analysis/standing.go` `Result.evidence`; `repl/explore.go` `explorationVerdict`; `cmd/sysml/report.go` `checkExploration`; `grpc/explore.go` `Service.explore` | `runtime/robustness_explore_failures_test.go:TestRuntimeRobustnessExploreFailures`; `analysis/explore_test.go`; `repl/explore_test.go:TestRunActionExploreSetupFailureRunsNoLinearization`, `:TestRunActionExplorePartialFailureFailsTheVerdict`; `cmd/sysml/run_test.go:TestExploreSetupFailureIsNotAnOutcome`, `:TestExplorePartialFailureFailsAndReportsTheFailedRun`, `:TestExploreInitialEntryFailureIsAnOutcome`; `grpc/explore_test.go:TestExploreSetupFailureIsReturnedInTheResponse`, `:TestExploreReportsAFailingRunAsAnOutcome` | ✅ Faithful (setup failures produce no outcome, while a witnessed runtime failure prevents a proof claim) | @@ -3476,7 +3476,7 @@ library types shows their signatures but no prose documentation, since the libra | External tools: a performance of an action carrying `AnalysisTooling::ToolExecution` is put to the `tool:` engine of its `toolName`, never to the action's body — one process per performance, one JSON object each way over its standard input and output, `toolName` and `uri` passed through uninterpreted, `inputs`/`outputs` keyed by `ToolVariable.name` with value and unit, outputs converted to the coherent unit of the parameter's declared quantity kind; each `*.json` entry of the directory `OPENSYSML_TOOLS` names (`toolName`, `version`, `executable`, `variables`) registers one engine answering `compute` at authority *observed*, listed with its process status like `solve`; a tool with no entry is refused with `tool 'ModelCenter' is not registered; set OPENSYSML_TOOLS`; a non-zero exit, malformed or missing output, an output no parameter receives, a unit the model does not declare and the timeout `OPENSYSML_TOOL_TIMEOUT` (default 10s) are typed errors that fail the performance — no default value is invented; equal inputs answered differently are a `tool-divergence` note of the run. `ToolExecution` on a `calc def` or calc usage is the same contract on every calc surface (`sysml -calc`, `%calc`, `EvaluateCalc`, derived attributes, document formulas): the `in`/`inout` parameters carrying `ToolVariable` are the inputs, the `out`/`inout` parameters carrying it plus the result parameter — under its `ToolVariable` name, else its declared name, else `result` — bind from the reply, and the body never evaluates | `analysis/manifest.go` `LoadManifest`, `ExternalsFromEnv`, `ToolEntry`, `ManifestError`, `ToolAbsentError`; `analysis/registry.go` `DefaultFromEnv`; `analysis/tool.go` `NewTool`, `toolEngine.Covers`, `toolEngine.Run`, `ToolRequestOf`, `ToolReplyOf`, `WrongToolError`, `ToolVariableError`; `analysis/tool_runner.go` `toolRunner.RunTool`; `analysis/dispatch.go` `Registry.AnswerWith` (the plan-scoped runner); `runtime/tool.go` `ActionExecutor.performByTool`, `ToolCall`, `ToolRunner`, `ToolNotRegisteredError`, `ToolError`, `ToolDivergence`; `runtime/tool_calc.go` `calcToolCall`, `computeCalcByTool` with the hooks in `runtime/invoke_calc.go` and `runtime/calc_usage.go`; `runtime/declared.go` `NewDeclaredReaderIn` (derived features read through the held runner); `semantics/coherent_unit.go` `Model.CoherentUnitFor`; `cmd/sysml/main.go`, `grpc/service.go` (`DefaultFromEnv` at startup) | `analysis/tool_fixture_test.go:TestPilotFixtureRunsAgainstTheStandIn` (the pilot `AnalysisAnnotation` against the Go stand-in `testdata/toolstandin`), `:TestPilotFixtureFailsWithTheToolsFault`, `:TestPilotFixtureTimesOut`, `:TestPilotFixtureRefusesAnUnregisteredTool`, `:TestPilotFixtureRefusesAnAbsentExecutable`, `:TestPilotFixtureReportsANonDeterministicTool`, `:TestToolEngineDispatch`; `analysis/tool_test.go:TestManifestReadsOneEntryPerJSONFile`, `:TestManifestFaultsAreTyped`, `:TestManifestRefusesTwoEntriesForOneTool`, `:TestExternalsFromEnvUnsetIsNoTool`, `:TestExternalsFromEnvRegisterEachEntry`, `:TestToolRegistrationIsIsolatedAndUnique`, `:TestToolEngineCoversItsOwnComputationsOnly`, `:TestToolTimeoutFromEnv`, `:TestToolRequestCarriesTheCallUninterpreted`, `:TestToolReplyIsOneObjectOfOutputsOrAnError`; `runtime/tool_test.go:TestToolExecutionPerformsThroughTheRunner`, `:TestToolExecutionWithoutRunnerIsNotRegistered`, `:TestToolExecutionRefusesBadAnswers`, `:TestToolExecutionNotesDivergence`; `runtime/tool_calc_test.go` (`TestToolCalc*` — binding, conversion, derived attributes, a body never run, every typed failure), `runtime/robustness_toolcalc_test.go:TestRuntimeRobustnessToolCalc`; `analysis/tool_calc_test.go` (`TestToolCalc*` against the `testdata/toolcalc` stand-in — answer, refusal, exit, timeout, unregistered); `repl/tool_calc_test.go`, `cmd/sysml/tool_calc_test.go` (`%calc`, `-calc`, `-render-document`); `tests/grpc/testdata/conformance/evaluate_calc_tool*` | 🧩 Extension (OpenSysML, as designed; under `smt`, a tool output is a free input — the contract that engine will meet; it is not on this branch) | | External engines: each `kind: engine` entry of the directory `OPENSYSML_ENGINES` names (read beside `OPENSYSML_TOOLS` under one rule set — outside every workspace, owner-writable only, `command` confined to the manifest directory and never looked up on `PATH`, duplicate names refused across both directories, `policy` and `sampler` entries parsed and listed as not served) registers an engine under its own name, spoken to over its standard input by JSON-RPC-shaped lines — `describe` checked against the entry field by field, `covers`, `run`, `cancel`, `progress` coalesced to a quarter second per open run, errors `unsupported`/`budget`/`internal` — one process per plan, several open requests on it when `concurrent`, one line and the captured standard error each bounded by `OPENSYSML_TOOL_MAX_OUTPUT` (default 64 MiB); the model is handed as `sources` or as `graphs:1`, the versioned byte-stable export of the lowered `ActionGraph`/`StateGraph`, `rdf` refused as a later stage; nothing the engine claims stands unchecked: `violated` is *witnessed* when its schedule replays and the property is false at the move named, `sensitive` when two schedules replay and end the feature differently, `satisfiable` when the assignment is confirmed, a universal claim *observed* over `executions` that replay and otherwise *not covered* with the claim kept, `admit` refused naming the referee-record stage; `auto` reaches an external engine after every built-in engine refused, `all` composes it with them and a stood claim beside a built-in witness is a disagreement; `-engines`, `%engines` and `ListEngines` list it (`-engines -probe` and `%engines probe` start each engine once), the service lists but does not serve it until `-serve-external-engines` | `analysis/manifest.go` `ManifestsFromEnv`, `ExternalsFromEnv`, `EntryKind`; `analysis/engine_entry.go` `EngineEntry`, `confinedPath`, `NotServedError`; `analysis/process.go` `outputLimitFromEnv`, `boundedBuffer`; `analysis/session.go` `session`, `enginePool`, `Reporter`, `ProgressInterval`; `analysis/enginewire/wire.go`; `analysis/external.go` `externalEngine`, `SubjectError`; `analysis/external_question.go`; `analysis/external_standing.go`; `analysis/withheld.go`; `analysis/listing.go` `Listing.Origin`, `Registry.Probed`; `analysis/modelform/graphs.go` `GraphsOf`, `GraphsVersion`; `analysis/modelform/sources.go` `SourcesOf`; `cmd/sysml/main.go` `-engines -probe`; `repl/engines.go` `%engines probe`; `grpc/engines.go` `ListEngines`; `cmd/sysml-grpc/main.go` `-serve-external-engines`; `docs/reference/engine-protocol.schema.json` | `analysis/engine_entry_test.go:TestManifestReadsEveryKind`, `:TestEngineEntryFaultsAreTyped`, `:TestManifestRefusesTwoEntriesForOneEngineName`, `:TestEngineCommandIsConfinedToTheManifestDirectory`, `:TestToolExecutableIsConfinedToTheManifestDirectory`, `:TestEngineEntryPresentChecksTheProgramWithoutRunning`, `:TestManifestUnderAWorkspaceIsNotRead`, `:TestManifestRefusesWritableByOthers`; `analysis/process_test.go:TestOutputLimitFromEnv`, `:TestBoundedBufferKeepsThePrefixAndStops`, `:TestToolOverflowNamesTheBound`; `analysis/session_test.go:TestSessionHandshakeCoversAndRun`, `:TestSessionHandshakeMismatchIsTypedPerField`, `:TestSessionStartupFailuresAreTyped`, `:TestSessionErrorCodesAreTyped`, `:TestSessionProtocolBreaksEndTheSession`, `:TestSessionLineOverTheBoundEndsTheSession`, `:TestSessionExitDuringRunIsTyped`, `:TestSessionCancelIsAnswered`, `:TestSessionIgnoredCancelEndsTheProcess`, `:TestSessionProgressIsCoalesced`, `:TestSessionMatchesConcurrentAnswersByID`, `:TestEnginePoolHonorsConcurrent`, `:TestEnginePoolEndsTheEngineForThePlanAtTheFirstFault`; `analysis/external_standing_test.go:TestExternalViolationStandsAfterReplay`, `:TestExternalViolationRefusedWhenThePropertyHolds`, `:TestExternalViolationIsJudgedAtTheMoveNamed`, `:TestExternalWitnessThatDoesNotReplay`, `:TestExternalWitnessShapeIsChecked`, `:TestExternalWitnessInputsAreReplayed`, `:TestExternalWitnessInputsNeedFreeInputs`, `:TestExternalEntryWithoutWitnessesEarnsNoExistential`, `:TestExternalSensitivityNeedsTwoDivergingSchedules`, `:TestExternalExecutionsAreObservedAfterReplay`, `:TestExternalExecutionsFailingTheClaimEarnNothing`, `:TestExternalUniversalClaimsWithoutExecutionsAreNotCovered`, `:TestExternalNoneIsTheEnginesOwnRefusal`, `:TestExternalAssignmentIsConfirmed`, `:TestExternalEngineInAutoAndAll`, `:TestExternalStoodClaimDisagreesWithBuiltIn`, `:TestExternalPlanIsTheSameUnderEitherConcurrency`, `:TestExternalSubjectsAreDeclarationKinds`; `analysis/schema_test.go:TestSchemaValidatesEveryStandinMessage`, `:TestSchemaRefusesWhatTheSessionRefuses`, `:TestSchemaMatchesTheWireTypes`; `analysis/modelform/graphs_test.go:TestGraphsActionCarriesTheLoweredGraph`, `:TestGraphsStateCarriesTheLoweredGraph`, `:TestGraphsAreByteStable`, `:TestSourcesOfListsEveryDocumentInOrder`, `:TestRefuseRDFFormIsTyped`, `:TestGraphsMatchTheGoldens`; `cmd/sysml/external_engines_test.go:TestEnginesSpawnsNothingAndProbeSpawnsEachEntryOnce`, `:TestEnginesUnderTheWorkspaceIsNotRead`, `:TestProgressGoesToStandardError`; `repl/engines_test.go:TestEnginesListsManifestEnginesAndProbesOnRequest`, `:TestProgressIsPrintedWhereTheSessionSays`; `grpc/engines_test.go:TestManifestEnginesAreListedButNotServedByDefault`, `:TestServeExternalEnginesRunsTheNamedManifestEngines` | 🧩 Extension (OpenSysML, as designed; stage 1 of the [bring-your-own-engine design](../internals/design/bring-your-own-engines.md); referee records and `admit`, `policy`/`sampler` strategies, the `rdf` form, in-process Go, WebAssembly and the `grpc` transport are later stages) | | Parallel runs: `Budget.Jobs` (`-jobs `, `%jobs `, `OPENSYSML_JOBS`; default one per CPU, fewer where the memory available leaves less than 512 MiB per worker; a count below one or no integer is the typed `JobsError` before anything runs; the flag overrides the environment; the gRPC service takes the serving binary's count, no request field) is how many runs of one plan go at once, each on a worker of its own — a resolver and semantic model per job over the shared frozen index, built lazily per plan, `Model.NewContext` being job 0 — so no run sees another's memo; the result of a plan does not depend on `Jobs`: `explore` runs its prefixes on a work queue ordered as the sequential exploration takes them (`Runs` a cut in that order, committed and speculative runs, at most `Jobs` speculative runs discarded in a plan's lifetime, never more than `Runs + Jobs` executions, the table merged by outcome identity with the least witness; a violating run is an outcome of the table as under one job, `explore` answering the universal `outcomes` alone, so the witness cut awaits an existential question on the queue), `all` composes in name order whatever the order of finishing, and `sweep` runs its rows on the `Jobs` workers, each row in a fresh run-owned context over the plan's worker (`SweepRun` takes the row's context; `SweepRow.Context` keeps it for the row's readers, so nothing a row produced is read through another context) and assembles its table in plan order whatever order the rows finish in, `Runs` remaining the row limit and one job the former loop; the REPL, CLI and gRPC paths instantiate a row's subject and `self` in the row's context and carry the arguments' values into it (`Context.Carry`: evaluated once at the prompt, so a held feature a run wrote reads as written; every object a value names — alone, in a collection, as a function's self — the one the row makes for it, the row's subject when they coincide; a deferred expression or a function closing over a run's bindings the typed `notPortableError` under `SweptArgumentError`); the gRPC response renumbers each row's objects so the request-wide `instances` table names every row's own; `%sweep` on a held object runs each row on an object of its own that is the held object as the sweep found it: the held object's declaration materialized afresh when the held closure is pristine — reached from a declaration (one nested in another's feature on the like of its root, walked along the same path), the root not destroyed, no feature written since materialization, no signal posted to it awaiting dispatch, every behavior its type exhibits or performs still as its start left it (the executors record whether they have moved at their own step points — a step that fails after moving a token, writing a performance or leaving a state included — `ActionExecutor.moved`/`StateExecutor.moved`, carried through `Snapshot`/`Restore`), none waiting on a clock that has left zero, no signal open to any taker in flight while it runs a behavior — and otherwise a copy from one image of the held graph (`Context.Image`, `HeldImage.Materialize`: the roots' closure by value — identities, lives, owners, feature values, the messages bound for it and, where it runs a behavior, those open to any taker, occurrences and the executors' captured state — taken once while the session's state is held and made in every row's context under the same identities, with fresh executors on the row's clock; `#id`-named objects admitted when the image holds the identity, feature paths when the copy resolves them, which it does whenever the held graph does), refusing with the typed `SweptObjectError` naming the reason what the image cannot carry (`ErrSnapshotMidRun`, `ErrSnapshotPausedBody`, `notPortableError`, `HeldImageError`), never sharing the session's context, whose state lock is released while the rows run; a deadline met mid-sweep starts no further row, discards the rows in flight and reports the caller's error and no table; `-json` `plan` carries `workers` and `warming` (ms), the human-readable report neither | `analysis/jobs.go` `ParseJobs`, `JobsFromEnv`, `DefaultJobs`, `JobsError`; `analysis/result.go` `Budget.Jobs`, `BudgetOf`; `analysis/worker.go` `Model.WorkerAt`, `Model.NewContextOn`, `warmed`; `analysis/dispatch.go` `answerAll`, `allCoordinator`, `Plan.Workers`, `Plan.Warming`; `runtime/explore.go` `ExploreWith` (`Explore` is its one-job form); `runtime/explore_queue.go` `exploreQueue` (`work`, `next`, `startable`, `finish`, `fold`); `sweep/sweep.go` `SweepRun`, `SweepRow.Context`, `runSweepRow`; `sweep/sweep_queue.go` `RunSweepWith`, `sweepQueue` (`work`, `take`); `runtime/pristine.go` `Context.Pristine`, `heldStateError`; `runtime/action_executor.go` `ActionExecutor.moved`, `newActionExecutorOn`; `runtime/state_executor.go` `StateExecutor.moved`, `newStateExecutorOn`; `runtime/snapshot.go` `actionCapture.moved`, `stateCapture.moved`; `runtime/held_image.go` `Context.Image`, `HeldImage.Materialize`, `HeldImage.Holds`, `HeldImageError`, `errImageIdentityTaken`, `errImageBindingTaken`, `errImageClock`, `errImageBound`, `errImageRoot` (a destroyed root refused as `errOccurrenceDestroyed`; a failed materialization leaving the destination as it found it); `runtime/held_image_behavior.go` (executor state by value and its translation); `runtime/classifier_behavior.go` `bindClassifierBehavior`; `runtime/carry.go` `Context.Carry`, `Bring`, `notPortableError`; `analysis/sweep.go` `sweepEngine.Run` (`Model.NewContextOn` per job); `repl/sweep.go` `Session.runSweep`, `sweptArgs`, `sweptValue`, `sweptHeld`, `sweptImage`, `rowObjects`, `sweptObject`, `sweptOwner`, `sweptRef`, `SweptObjectError`, `SweptArgumentError`, `sweepTableLines`; `repl/lookup.go` `Session.heldRoot`, `heldLabel`; `grpc/sweep.go` `Service.RunSweep`, `sweepResponse`, `rowIDs`; `grpc/verify.go` `verifyContext.on`; `grpc/convert.go` `ValueToProtoIn`, `instanceToProto`; `cmd/sysml/main.go` `-jobs`; `cmd/sysml/report.go` `checkPlan.Workers`/`Warming`; `repl/jobs.go` `Session.Jobs`, `Session.SetJobs`; `repl/meta.go` `%jobs`; `grpc/service.go` `Service.jobs` (from `JobsFromEnv` at construction); `usage/environment.go` `OPENSYSML_JOBS` | `runtime/explore_queue_test.go:TestExploreWithIsExploreOverTheConformanceCorpus` (one job against eight over every case with an admissible set), `:TestExploreWithKeepsTheLeastWitnessOfALaterFasterViolation`, `:TestExploreWithCutsRunsJustAboveTheWitness` (`testdata/later_prefix_violates_faster.sysml`), `:TestExploreWithNeverRunsMoreThanRunsPlusJobs` (conformance `action_explore_slow_first_writer.sysml`, a bounded recursion for the slow prefix), `:TestExploreWithBuildsEachRunOnItsJob`, `:TestExploreWithStopsWhenTheCallerGoesAway`, `:TestExploreWithFailsWhenFreshFails`; `analysis/jobs_test.go:TestJobsFromEnv`, `:TestParseJobsNamesItsSource`; `analysis/isolation_test.go:TestPlansOnOneModelHaveWorkersOfTheirOwn` (`Jobs` workers per plan, two plans on two goroutines under `-race`); `analysis/all_test.go:TestAllPlanCountsTheWorkersOfEveryEngine`; `cmd/sysml/jobs_test.go:TestJobsFlagAndEnvironment`, `:TestJSONIsTheSameOnOneJobAsOnEight` (the three determinism fixtures and a sweep through `-json`), `:TestSweepReportsAreTheSameOnOneJobAsOnEight` (every CLI sweep golden and the trade-study sweep, text and `-json`), `:TestJSONReportsThePlanWorkers`; `repl/jobs_test.go:TestJobsShowsAndSetsTheCount`, `:TestSetJobsReachesTheBudgetAndKeepsTheSession`; `sweep/sweep_queue_test.go:TestRunSweepWithTablesRowsInPlanOrderWhateverTheirArrival` (a context per row among its checks), `:TestRunSweepWithKeepsEachRowsWritesToItself`, `:TestRunSweepWithStopsAtTheDeadline`, `:TestRunSweepWithFailsWhenAJobHasNoContext`; `runtime/carry_test.go:TestCarryTakesAValueIntoAnotherContext`, `:TestCarryRefusesWhatNoOtherContextHolds`; `runtime/value_kinds_test.go:TestEveryValueKindIsDispatched` (carrying among the surfaces walked); `analysis/isolation_test.go:TestSweepsOnOneModelHaveWorkersOfTheirOwn` (two sweeps on one model on two goroutines under `-race`); `repl/sweep_rows_test.go:TestSweepRowsReadAlikeOnOneJobAndOnEight` (every REPL sweep golden, the trade-study sweeps and a descending bounded recursion whose rows arrive out of plan order), `:TestSweepRowsWritingTheSubjectKeepTheWritesToThemselves`, `:TestSweepOverAnObjectNotAsItsDeclarationMadeItRunsOnItsImage`, `:TestSweepOverAMovedStateMachineRunsOnItsImage`, `:TestSweepOverAnObjectNoImageCarriesIsRefused`, `:TestSweepOverADestroyedObjectIsRefused`; `repl/sweep_held_test.go:TestSweepOverAFreshObjectRunningABehaviourReadsAsTheSequentialFormDid` (the sequential form's table pinned on one job and on eight), `:TestSweepOverAMovedPerformedActionRunsOnItsImage`; `runtime/pristine_test.go:TestPristineFollowsAStateMachinesMoves`, `:TestPristineFollowsAPerformedActionsMoves` (the record through the moves and through `Snapshot`/`Restore`; a signal posted refused), `:TestPristineRefusesATimedBehaviorOnceTheClockHasMoved`, `:TestPristineRefusesABehavingObjectWhileAnOpenMessageIsInFlight`, `:TestActionStepFailingAfterAMoveRecordsIt`, `:TestActionBodyFailingAfterAWriteRecordsTheMove`, `:TestStateChangeTransitionFailingRecordsTheMove`; `runtime/held_image_test.go:TestHeldImageCarriesAMovedStateMachine`, `:TestHeldImageOfAFreshObjectIsPristine`, `:TestHeldImageCarriesAParkedAction`, `:TestHeldImageCarriesTheRunsSchedulePolicy`, `:TestHeldImageRefusesWhatItCannotCarry` (a destroyed root among them), `:TestHeldImageRefusesAMessageNamingAnObjectNotHeld`, `:TestHeldImageOfABehaviorlessClosureLeavesTheBusBe`, `:TestHeldImageRefusesADestinationWithAWaitDueBeforeItsInstant` (one already due at the destination's instant among them), `:TestHeldImageRefusesAPausedBody`, `:TestHeldImageMaterializeFailsWhole` (a destination on a shared sequence among them), `:TestHeldImageKeepsTheIdentitiesSetAsideForConnectors`, `:TestHeldImageRefusesAnIdentitySetAsideByTheDestination`, `:TestHeldImageRefusesAUsageDenotingAnotherObjectOfTheDestination`, `:TestHeldImageRoundTrip` (every conformance case the image admits, captured in one context, made in another and run beside the source), `:TestHeldImageServesConcurrentSweeps` (one image, two sweeps of eight rows on two goroutines under `-race`); `cmd/sysml/sweep_test.go:TestSweepOverAnInstantiatedObjectRunningABehaviourThroughCLI`; `grpc/sweep_test.go:TestRunSweepOverASubjectRunningABehaviour`, `:TestRunSweepOverSubjectsRunningABehaviourConcurrently`, `:TestSweepOverAnObjectReachedThroughAnotherRunsOnItsLike`, `:TestSweepArgumentsReadAsThePromptReadsThem`, `:TestSweepArgumentsNamingAnObjectBindTheRowsOwn`, `:TestSweepLeavesADebuggerStepping`; `grpc/sweep_test.go:TestRunSweepAnswersAlikeOnOneJobAndOnEight`, `:TestRunSweepRowsNameTheirOwnObjects`; `make man-check` | 🧩 Extension (OpenSysML; what the image does not carry is refused, typed: a body paused mid-statement, a session inside a step, a value closed over its run) | -| The `smt` engine (`internal/exec/smt`, the [SMT model checking design](../internals/design/smt-model-checking.md), stages 1 to 3): a `holds` question about an action with the schedule free, the inputs free or both is put to an SMT solver over the lowered `ActionGraph` — straight-line bodies, fork, join, merge, decisions (two holding guards are the executor's *decision branch* choice, ranged over, not asserted impossible), body loops unrolled `Budget.Unroll` times (`analysis.DefaultUnroll`, 4, when zero; the `-check-unroll` flag and `%check-bounds unroll=` set it; reported as the `unroll` bound), pins and object flows; clock, messages, nested flows, object-valued assignments, calc invocation and nonlinear arithmetic refuse the whole behavior before any query, naming the node and construct. In `s_0` a feature the model binds — a default, a value the performing object holds, a value the caller fixed through `Start` — is asserted equal to it and a feature it leaves unbound is a free variable whose domain is the declared type's: `Boolean`, `Integer` as the solver's unbounded Int (KerML 1.1 §9.3.2.2.3; the runtime's own size budget is not asserted), `Natural` as an integer `>= 0`, `Real`, `Rational` and a quantity type over one as the solver's reals, an enumeration or variation point as its constructors; a `HoldsAsk.Inputs` name (`-check-input`, `%check-input`) drops a bound feature's binding so it ranges over that domain, and a name that is no feature the action reads (nothing, an output, a result, a node) is the typed `InputError` before any query; a declared type the encoding cannot narrow to a sort (`String`, a collection, an object-valued feature, a type with no translation) is the typed `DomainError` naming the feature and type, *not covered* before any query, never a silent unconstrained variable; a pinned value is checked against its domain the same way. A `HoldsAsk.Assume` constraint or requirement (`-check-assume`, `%check-assume`) is translated as any condition is and asserted over `s_0`, one the translator refuses being refused naming the construct before any query; the assumptions are asked for consistency first and a set no initial state satisfies is *not covered: assumptions admit no initial state*, never *proved*. The requirement or constraint property and the deadlock property are asked as `∃ i ≤ k. ¬R(s_i)` and `∃ i. stutter ∧ ¬complete` over `k = Budget.Depth` moves (`smt.DefaultMoves`, 40, when the engine is asked alone without a depth) under `Budget.Solver`; `unsat` is *proved* only when no schedule reaches the move, unroll or slot bound at `k` and *bounded* otherwise, the proof meaning *for every value of the free inputs in their domains* and its `Result.Inputs` and `Result.Assumptions` listing each input with its type, domain, value or freedom and each assumption; every `sat` model is decoded to the free inputs' values (`InputTaken`, a rational spelled exactly, a constructor by its qualified name) and `ChoiceTaken` lines, replayed through the interpreter under `replay:` with the inputs fixed before the defaults and the moves followed after, and is *violated (witnessed)* only when the replay reaches the state the solver described — a replay that diverges or cannot set an input, `unknown`, a timeout and a refusal are *not covered* with the reason. A `sensitive` question — asked when `-check-diverge`/`%check-diverge` names a feature, whichever engine answers, so `check` and `smt` read one flag and `-engine all` puts one question to both — is decided per feature by a two-copy query: copy B of the whole encoded relation shares `s_0` and the free inputs with copy A and renames every other variable, both copies `complete` within `k` moves and the feature's final values differ; a `sat` decodes to two schedules, both replayed through `runtime.Replay` before the verdict is *sensitive (witnessed)* with the two final values, the first move the schedules part at and the move each took, `Result.Witness` and `Result.Contrast` the pair and `-check-witness` writing `-A` and `-B` files either of which `replay:`/`%replay` follows, a replay that does not reproduce its value *not covered* with the disagreement; on `unsat` the deadlock and typed-error properties are asked next, a `sat` there that *violated* finding, then `∃ schedule. cut_k ∨ loopflag`, whose `sat` is `no sensitivity found within k moves` as (`holds`, *bounded*) — the pair `check`'s clean exhaustive search of the same question answers — and whose `unsat` alone is (`holds`, *proved*); the three are separate queries, so no `CapIncremental` is needed; a feature of the performing object (`this.level`) and a body stage 4 encodes (the clock, a paused nested flow) are per-feature and whole-behavior typed refusals, never a silently narrowed answer, and absent a named feature the default set is `check`'s — the action's attributes, answered, and the performer's, refused each by name. A fixed schedule, `outcomes` and every other question kind are refused with a typed reason; `explore` and `check` keep refusing `FreeInputs` with theirs, so `-engine all` with `-check-input` shows `check` refused in the plan beside `smt`'s answer. The engine is `analysis.External` over `OPENSYSML_SMT`, `z3`, `cvc5`, registered at authority *proved* in the build's registry `engines.Default()` (`internal/exec/engines`, which composes `analysis.Default()` — the framework's own engines, which `smt` imports and so cannot be constructed from — with `smt`; the CLI, REPL and gRPC service build it), so `-engine smt` and `%engine smt` reach it and `-engines`, `%engines` and `ListEngines` list it with its solver as its status; no surface asks `holds` under `auto`, so its registration moved no verdict or plan line, and a tool-computed output is not yet a free input because a body performing a `tool:` engine is refused as stage 1 refuses it | `smt/support.go` `Analyze`, `Flow`, `BodyLoop`, `DefaultUnroll`; `smt/state.go` `Sorts`, `State`, `Move`; `smt/encode.go` `Encode`, `Encoding`, `Encoding.initial`, `Encoding.domain`; `smt/input.go` `Encoding.frees`, `Encoding.checkReleases`, `Encoding.domainText`, `noDomain`; `smt/property.go` `Encoding.Conditions`, `Encoding.Assume`, `Encoding.Deadlock`, `Encoding.Violation`, `Encoding.Failure`, `Encoding.Uncertainty`, `Encoding.Cuts`, `Encoding.Completion`, `Encoding.Outputs`; `smt/witness.go` `Encoding.Decode`, `Encoding.decodeRun`, `Encoding.decodeInputs`, `Encoding.DecodeOutputs`, `Encoding.Fix`; `smt/twocopy.go` `CopyPrefix`, `CopyNames`, `Pair`, `Encoding.Pair`, `Encoding.Sensitivity`, `Encoding.DecodePair`, `Diverging`; `smt/sensitive.go` `run.decideSensitive`, `run.diverging`, `run.sensitive`, `run.replayRun`, `NoSensitivityWithin`; `analysis/ask.go` `CheckKind`; `analysis/check.go` `SensitivityFile`, `divergenceWitness`; `analysis/compose.go` (a stated `ClaimSensitive` stands over `ClaimHolds` about the same feature); `runtime/check.go` `ResolveCheckFeatures`, `FeatureOwner`, `ActionExecutor.performerAttributes`; `smt/engine.go` `New`, `Engine.Unrolling`, `Engine.Covers`, `Engine.Run`, `Engine.Process`, `DefaultMoves`, `NoInitialState`, `run.decide`, `run.inputs`, `run.replay`, `run.write`, `ScheduleError`; `smt/errors.go` `ErrNotEncoded`, `UnsupportedError`, `FlowError`, `ErrSlotOverflow`; `analysis/engine.go` `InputError`, `ErrInput`, `DomainError`, `ErrDomain`, `FreedomError`; `analysis/question.go` `HoldsAsk` (`Conditions`, `Inputs`, `Assume`, `Diverge`), `Question.Holds`, `FreeInputs`; `analysis/result.go` `Result.Contrast`; `analysis/result.go` `Input`, `Result.Inputs`, `Result.Assumptions`, `Budget.Unroll`, `DefaultUnroll`, `Witness.Inputs`; `analysis/standing.go` `Result.inputsEvidence`; `engines/engines.go` `Default`, `DefaultFromEnv`; `runtime/replay.go` `InputTaken`, `parseInput`, `ParseWitness`, `Witness.Inputs`, `WitnessInputError`; `runtime/action_executor.go` `ActionExecutor.fixWitnessInputs`; `cmd/sysml/usage.go` (`-check-input`, `-check-assume`, `-check-unroll`); `cmd/sysml/report.go` `checkInput`; `repl/meta.go` (`%check-input`, `%check-assume`, `%check-bounds unroll=`) | `smt/referee_test.go:TestRefereeCorpus` (checks 1–3 over every corpus action case with `outcomes` whose body encodes: outcome sets equal `explore`'s, every witness replays, the verdict agrees with exhaustive exploration; check 5: every feature the case's action writes is asked as a `sensitive` question, a *sensitive* verdict has both witnesses replayed to two values among the case's `outcomes` and a *not sensitive* feature has one value across them; the refused cases are counted and named), `:TestRefereeInputs` (check 4: every *violated* witness with inputs, replayed under `explore` with those inputs pinned, reproduces the violation), `smt/input_test.go:TestUnboundInputsAreFreeAndBoundOnesPinned`, `:TestFreeInputRangesOverItsDomain`, `:TestReleasingABoundInputDropsItsBinding`, `:TestFreeInputWithoutADomainIsRefused`; `smt/input_engine_test.go:TestEngineRangesOverUnboundInputs`, `:TestEngineNarrowsTheDomainToTheDeclaredType` (*proved* under `Natural`, *violated* under `Integer`), `:TestEngineWitnessNamesAnEnumerationConstructor`, `:TestEngineAssumesOverTheInitialState` (an assumption turns *violated* into *proved*; a contradictory set is *not covered*, never *proved*), `:TestEngineReleasesABoundInput`, `:TestEngineRefusesInputsItCannotFree`, `:TestEngineRefusesAnAssumptionItCannotTranslate`, `:TestEngineWitnessWithInputsReplaysThroughTheStart`, `:TestEngineWitnessWithoutInputsReplaysAsBefore`; `smt/sensitivity_test.go:TestSensitivityOfForkBranchesWritingOneFeature` (`x` sensitive with both witnesses replayed to the oracle's two values, `leftRan` and `rightRan` *proved* not sensitive), `:TestSensitivityWritesBothWitnesses`, `:TestSensitivityShortOfCompletionIsBounded` (*bounded*, never *proved*, below the completing depth), `:TestSensitivityOfJoinWaitingForSlowestBranch` (`arrived` not sensitive), `:TestSensitivityUnderDeadlockIsTheDeadlock`, `:TestSensitivityRefusesTheClockAndPausedFlows` (the stage-4 row, refused naming the construct), `:TestSensitivityRefusesAPairTheInterpreterRefutes`, `:TestPairIsTheRelationTwiceOver` (copy B keeps every sort, declaration, assertion, objective, pin and flag of the query, renamed); `analysis/check_test.go:TestCheckKindAsksSensitiveForANamedFeature`, `:TestCheckAnswersASensitiveQuestionWithAPair`; `analysis/compose_test.go:TestComposeSensitivityWitnessStandsOverNotSensitive`; `cmd/sysml/smt_engine_test.go:TestEngineSMTDecidesSensitivity`, `:TestEngineAllComposesSensitivity`; `repl/smt_test.go:TestEngineSMTDecidesSensitivity`; `smt/discipline_test.go:TestMergeLoopBeyondTheBoundIsBounded`, `:TestBodyWhileBeyondUnrollingIsBounded`, `:TestDivisionByZeroIsReportedNotBounded`, `:TestPinnedMergeOutcomes`, `:TestEngineWithoutASolverIsAbsent`, `:TestEncodingEmitsOnlyPortableFeatures` (the two-copy query of every output among the queries checked); `smt/engine_test.go:TestEngineDescribesItself`, `:TestEngineRefusesWhatItDoesNotAnswer`, `:TestEngineDecidesConditions`, `:TestEngineDecidesDeadlock`, `:TestEngineRefusesWhatItDoesNotEncode`, `:TestEngineReportsUnknownAsNotCovered`, `:TestEngineIntegerArithmeticIsUnbounded`; `smt/property_test.go:TestConditionPropertiesFollowTheRun`, `:TestDeadlockProperty`, `:TestConditionReadingNoValueIsUndefined`, `:TestConditionOverAnObjectIsRefused`; `smt/encode_test.go:TestEncodeForkJoinCompletes`, `:TestEncodePinsAndObjectFlows`, `:TestSortsNameEveryNodeEdgeAndSlot`; `smt/support_test.go:TestAnalyzeNumbersForkJoinFlow`, `:TestAnalyzeRecordsBodyLoops`, `:TestAnalyzeRefusesMessages`, `:TestAnalyzeRefusesNoInitial`; `solve/portability_test.go:TestPortability` (a datatype the query declares for the nodes of a flow; an incremental dialogue over named variables; a free input over an enumeration's datatype; a real-sorted input read back exactly); `runtime/replay_input_test.go:TestParseInputReadsEverySpelling`, `:TestParseWitnessReadsInputsBeforeChoices`, `:TestReplayFixesWitnessInputs` (a witness naming a feature the model lacks is refused naming it); `engines/engines_test.go:TestDefaultHoldsTheFrameworksEnginesAndSMT`, `:TestSMTStatusIsTheSolvers`, `:TestHoldsRanksSMTOverCheck`; `analysis/registry_test.go:TestDefaultHoldsTheFrameworksEngines`, `:TestDefaultPutsHoldsToCheckAlone`; `repl/smt_test.go:TestEngineSMTRangesOverAReleasedInput`, `:TestEngineSMTAssumesOverTheInitialState`, `:TestEngineAllShowsCheckRefusingFreeInputs`, `:TestEngineSMTRefusesAnUnknownInput`; `cmd/sysml/report_test.go:TestCheckResultsReportInputsAndWitnessValues`; `cmd/sysml/engines_test.go:TestEnginesListsTheBuild`; `grpc/engines_test.go:TestListEnginesNamesEveryEngine` | 🧩 Extension (OpenSysML, as designed for stages 1 to 3; every solver test skips with a named reason without a solver and fails under `OPENSYSML_REQUIRE_SMT=1`; a *not sensitive* verdict is a fact about the model asked, not about the runtime's scheduling, so no ordering row moves on its account); clock, messages, nested flows, k-induction, heap and calc inlining, state machines and the engine option on the wire are later stages and refuse with the reason | +| The `smt` engine (`internal/exec/smt`, the [SMT model checking design](../internals/design/smt-model-checking.md), stages 1 to 3): a `holds` question about an action with the schedule free, the inputs free or both is put to an SMT solver over the lowered `ActionGraph` — straight-line bodies, fork, join, merge, decisions (two holding guards are the executor's *decision branch* choice, ranged over, not asserted impossible), body loops unrolled `Budget.Unroll` times (`analysis.DefaultUnroll`, 4, when zero; the `-check-unroll` flag and `%check-bounds unroll=` set it; reported as the `unroll` bound), pins and object flows; clock, messages, nested flows, object-valued assignments, calc invocation and nonlinear arithmetic refuse the whole behavior before any query, naming the node and construct. In `s_0` a feature the model binds — a default, a value the performing object holds, a value the caller fixed through `Start` — is asserted equal to it and a feature it leaves unbound is a free variable whose domain is the declared type's: `Boolean`, `Integer` as the solver's unbounded Int (KerML 1.1 §9.3.2.2.3; the runtime's own size budget is not asserted), `Natural` as an integer `>= 0`, `Real`, `Rational` and a quantity type over one as the solver's reals, an enumeration or variation point as its constructors; a `HoldsAsk.Inputs` name (`-check-input`, `%check-input`) drops a bound feature's binding so it ranges over that domain, and a name that is no feature the action reads (nothing, an output, a result, a node) is the typed `InputError` before any query; a declared type the encoding cannot narrow to a sort (`String`, a collection, an object-valued feature, a type with no translation) is the typed `DomainError` naming the feature and type, *not covered* before any query, never a silent unconstrained variable; a pinned value is checked against its domain the same way. A feature valued by an expression over other features (`attribute y : Integer = x + 1`, a FeatureValue that is not initial, KerML 1.1 §7.3.4.2, which the interpreter computes at every read) is no input: its variable is kept in every state but never framed — each `s_i` asserts it equal to the expression over `s_i`'s values, and a read of it within a move (a body statement, a guard, a loop condition) substitutes the expression over the move's current environment, through features so valued in turn, so guards, loop bounds, properties, assumptions over `s_0` and results all see the derived value; one whose reads the lowering cannot resolve, one whose declared type narrows its sort, an assignment to one and a release of one are each refused naming the feature and reason before any query, and a cycle among such features is the interpreter's refusal at the start of the performance, before any encoding. A `HoldsAsk.Assume` constraint or requirement (`-check-assume`, `%check-assume`) is translated as any condition is and asserted over `s_0`, one the translator refuses being refused naming the construct before any query; the assumptions are asked for consistency first and a set no initial state satisfies is *not covered: assumptions admit no initial state*, never *proved*. The requirement or constraint property and the deadlock property are asked as `∃ i ≤ k. ¬R(s_i)` and `∃ i. stutter ∧ ¬complete` over `k = Budget.Depth` moves (`smt.DefaultMoves`, 40, when the engine is asked alone without a depth) under `Budget.Solver`; `unsat` is *proved* only when no schedule reaches the move, unroll or slot bound at `k` and *bounded* otherwise, the proof meaning *for every value of the free inputs in their domains* and its `Result.Inputs` and `Result.Assumptions` listing each input with its type, domain, value or freedom and each assumption; every `sat` model is decoded to the free inputs' values (`InputTaken`, a rational spelled exactly, a constructor by its qualified name) and `ChoiceTaken` lines, replayed through the interpreter under `replay:` with the inputs fixed before the defaults and the moves followed after, and is *violated (witnessed)* only when the replay reaches the state the solver described — a replay that diverges or cannot set an input, `unknown`, a timeout and a refusal are *not covered* with the reason. A `sensitive` question — asked when `-check-diverge`/`%check-diverge` names a feature, whichever engine answers, so `check` and `smt` read one flag and `-engine all` puts one question to both — is decided per feature by a two-copy query: copy B of the whole encoded relation shares `s_0` and the free inputs with copy A and renames every other variable, both copies `complete` within `k` moves and the feature's final values differ; a `sat` decodes to two schedules, both replayed through `runtime.Replay` before the verdict is *sensitive (witnessed)* with the two final values, the first move the schedules part at and the move each took, `Result.Witness` and `Result.Contrast` the pair and `-check-witness` writing `-A` and `-B` files either of which `replay:`/`%replay` follows, a replay that does not reproduce its value *not covered* with the disagreement; on `unsat` the deadlock and typed-error properties are asked next, a `sat` there that *violated* finding, then `∃ schedule. cut_k ∨ loopflag`, whose `sat` is `no sensitivity found within k moves` as (`holds`, *bounded*) — the pair `check`'s clean exhaustive search of the same question answers — and whose `unsat` alone is (`holds`, *proved*); the three are separate queries, so no `CapIncremental` is needed; a feature of the performing object (`this.level`) and a body stage 4 encodes (the clock, a paused nested flow) are per-feature and whole-behavior typed refusals, never a silently narrowed answer, and absent a named feature the default set is `check`'s — the action's attributes, answered, and the performer's, refused each by name. A fixed schedule, `outcomes` and every other question kind are refused with a typed reason; `explore` and `check` keep refusing `FreeInputs` with theirs, so `-engine all` with `-check-input` shows `check` refused in the plan beside `smt`'s answer. The engine is `analysis.External` over `OPENSYSML_SMT`, `z3`, `cvc5`, registered at authority *proved* in the build's registry `engines.Default()` (`internal/exec/engines`, which composes `analysis.Default()` — the framework's own engines, which `smt` imports and so cannot be constructed from — with `smt`; the CLI, REPL and gRPC service build it), so `-engine smt` and `%engine smt` reach it and `-engines`, `%engines` and `ListEngines` list it with its solver as its status; no surface asks `holds` under `auto`, so its registration moved no verdict or plan line, and a tool-computed output is not yet a free input because a body performing a `tool:` engine is refused as stage 1 refuses it | `smt/support.go` `Analyze`, `Flow`, `BodyLoop`, `DefaultUnroll`; `smt/state.go` `Sorts`, `State`, `Move`; `smt/encode.go` `Encode`, `Encoding`, `Encoding.initial`, `Encoding.domain`, `derivation`, `Encoding.collectDerived`, `Encoding.checkDerived`, `Encoding.deriveValues`, `env.evaluate`; `smt/input.go` `Encoding.frees`, `Encoding.checkReleases`, `Encoding.domainText`, `noDomain`; `smt/property.go` `Encoding.Conditions`, `Encoding.Assume`, `Encoding.Deadlock`, `Encoding.Violation`, `Encoding.Failure`, `Encoding.Uncertainty`, `Encoding.Cuts`, `Encoding.Completion`, `Encoding.Outputs`; `smt/witness.go` `Encoding.Decode`, `Encoding.decodeRun`, `Encoding.decodeInputs`, `Encoding.DecodeOutputs`, `Encoding.Fix`; `smt/twocopy.go` `CopyPrefix`, `CopyNames`, `Pair`, `Encoding.Pair`, `Encoding.Sensitivity`, `Encoding.DecodePair`, `Diverging`; `smt/sensitive.go` `run.decideSensitive`, `run.diverging`, `run.sensitive`, `run.replayRun`, `NoSensitivityWithin`; `analysis/ask.go` `CheckKind`; `analysis/check.go` `SensitivityFile`, `divergenceWitness`; `analysis/compose.go` (a stated `ClaimSensitive` stands over `ClaimHolds` about the same feature); `runtime/check.go` `ResolveCheckFeatures`, `FeatureOwner`, `ActionExecutor.performerAttributes`; `smt/engine.go` `New`, `Engine.Unrolling`, `Engine.Covers`, `Engine.Run`, `Engine.Process`, `DefaultMoves`, `NoInitialState`, `run.decide`, `run.inputs`, `run.replay`, `run.write`, `ScheduleError`; `smt/errors.go` `ErrNotEncoded`, `UnsupportedError`, `FlowError`, `ErrSlotOverflow`; `analysis/engine.go` `InputError`, `ErrInput`, `DomainError`, `ErrDomain`, `FreedomError`; `analysis/question.go` `HoldsAsk` (`Conditions`, `Inputs`, `Assume`, `Diverge`), `Question.Holds`, `FreeInputs`; `analysis/result.go` `Result.Contrast`; `analysis/result.go` `Input`, `Result.Inputs`, `Result.Assumptions`, `Budget.Unroll`, `DefaultUnroll`, `Witness.Inputs`; `analysis/standing.go` `Result.inputsEvidence`; `engines/engines.go` `Default`, `DefaultFromEnv`; `runtime/replay.go` `InputTaken`, `parseInput`, `ParseWitness`, `Witness.Inputs`, `WitnessInputError`; `runtime/action_executor.go` `ActionExecutor.fixWitnessInputs`; `cmd/sysml/usage.go` (`-check-input`, `-check-assume`, `-check-unroll`); `cmd/sysml/report.go` `checkInput`; `repl/meta.go` (`%check-input`, `%check-assume`, `%check-bounds unroll=`) | `smt/referee_test.go:TestRefereeCorpus` (checks 1–3 over every corpus action case with `outcomes` whose body encodes: outcome sets equal `explore`'s, every witness replays, the verdict agrees with exhaustive exploration; check 5: every feature the case's action writes is asked as a `sensitive` question, a *sensitive* verdict has both witnesses replayed to two values among the case's `outcomes` and a *not sensitive* feature has one value across them; the refused cases are counted and named), `:TestRefereeInputs` (check 4: every *violated* witness with inputs, replayed under `explore` with those inputs pinned, reproduces the violation), `smt/derived_test.go:TestDerivedFeaturesAgreeWithExplore` (every corpus action holding a feature valued by an expression over other features encodes and the solver's value set per feature equals `explore`'s; `y ∈ {2, 3}`, `z ∈ {12, 13}` pinned on `action_order_write_from_bound_read`), `:TestDerivedFeatureInGuardAndProperty`, `:TestDerivedFeatureRefusals` (an assignment to one, a release of one, a narrowing declared type; a cycle is the interpreter's refusal at the start); `smt/input_test.go:TestUnboundInputsAreFreeAndBoundOnesPinned`, `:TestFreeInputRangesOverItsDomain`, `:TestReleasingABoundInputDropsItsBinding`, `:TestFreeInputWithoutADomainIsRefused`; `smt/input_engine_test.go:TestEngineRangesOverUnboundInputs`, `:TestEngineNarrowsTheDomainToTheDeclaredType` (*proved* under `Natural`, *violated* under `Integer`), `:TestEngineWitnessNamesAnEnumerationConstructor`, `:TestEngineAssumesOverTheInitialState` (an assumption turns *violated* into *proved*; a contradictory set is *not covered*, never *proved*), `:TestEngineReleasesABoundInput`, `:TestEngineRefusesInputsItCannotFree`, `:TestEngineRefusesAnAssumptionItCannotTranslate`, `:TestEngineWitnessWithInputsReplaysThroughTheStart`, `:TestEngineWitnessWithoutInputsReplaysAsBefore`; `smt/sensitivity_test.go:TestSensitivityOfForkBranchesWritingOneFeature` (`x` sensitive with both witnesses replayed to the oracle's two values, `leftRan` and `rightRan` *proved* not sensitive), `:TestSensitivityWritesBothWitnesses`, `:TestSensitivityShortOfCompletionIsBounded` (*bounded*, never *proved*, below the completing depth), `:TestSensitivityOfJoinWaitingForSlowestBranch` (`arrived` not sensitive), `:TestSensitivityUnderDeadlockIsTheDeadlock`, `:TestSensitivityRefusesTheClockAndPausedFlows` (the stage-4 row, refused naming the construct), `:TestSensitivityRefusesAPairTheInterpreterRefutes`, `:TestPairIsTheRelationTwiceOver` (copy B keeps every sort, declaration, assertion, objective, pin and flag of the query, renamed); `analysis/check_test.go:TestCheckKindAsksSensitiveForANamedFeature`, `:TestCheckAnswersASensitiveQuestionWithAPair`; `analysis/compose_test.go:TestComposeSensitivityWitnessStandsOverNotSensitive`; `cmd/sysml/smt_engine_test.go:TestEngineSMTDecidesSensitivity`, `:TestEngineAllComposesSensitivity`; `repl/smt_test.go:TestEngineSMTDecidesSensitivity`; `smt/discipline_test.go:TestMergeLoopBeyondTheBoundIsBounded`, `:TestBodyWhileBeyondUnrollingIsBounded`, `:TestDivisionByZeroIsReportedNotBounded`, `:TestPinnedMergeOutcomes`, `:TestEngineWithoutASolverIsAbsent`, `:TestEncodingEmitsOnlyPortableFeatures` (the two-copy query of every output among the queries checked); `smt/engine_test.go:TestEngineDescribesItself`, `:TestEngineRefusesWhatItDoesNotAnswer`, `:TestEngineDecidesConditions`, `:TestEngineDecidesDeadlock`, `:TestEngineRefusesWhatItDoesNotEncode`, `:TestEngineReportsUnknownAsNotCovered`, `:TestEngineIntegerArithmeticIsUnbounded`; `smt/property_test.go:TestConditionPropertiesFollowTheRun`, `:TestDeadlockProperty`, `:TestConditionReadingNoValueIsUndefined`, `:TestConditionOverAnObjectIsRefused`; `smt/encode_test.go:TestEncodeForkJoinCompletes`, `:TestEncodePinsAndObjectFlows`, `:TestSortsNameEveryNodeEdgeAndSlot`; `smt/support_test.go:TestAnalyzeNumbersForkJoinFlow`, `:TestAnalyzeRecordsBodyLoops`, `:TestAnalyzeRefusesMessages`, `:TestAnalyzeRefusesNoInitial`; `solve/portability_test.go:TestPortability` (a datatype the query declares for the nodes of a flow; an incremental dialogue over named variables; a free input over an enumeration's datatype; a real-sorted input read back exactly); `runtime/replay_input_test.go:TestParseInputReadsEverySpelling`, `:TestParseWitnessReadsInputsBeforeChoices`, `:TestReplayFixesWitnessInputs` (a witness naming a feature the model lacks is refused naming it); `engines/engines_test.go:TestDefaultHoldsTheFrameworksEnginesAndSMT`, `:TestSMTStatusIsTheSolvers`, `:TestHoldsRanksSMTOverCheck`; `analysis/registry_test.go:TestDefaultHoldsTheFrameworksEngines`, `:TestDefaultPutsHoldsToCheckAlone`; `repl/smt_test.go:TestEngineSMTRangesOverAReleasedInput`, `:TestEngineSMTAssumesOverTheInitialState`, `:TestEngineAllShowsCheckRefusingFreeInputs`, `:TestEngineSMTRefusesAnUnknownInput`; `cmd/sysml/report_test.go:TestCheckResultsReportInputsAndWitnessValues`; `cmd/sysml/engines_test.go:TestEnginesListsTheBuild`; `grpc/engines_test.go:TestListEnginesNamesEveryEngine` | 🧩 Extension (OpenSysML, as designed for stages 1 to 3; every solver test skips with a named reason without a solver and fails under `OPENSYSML_REQUIRE_SMT=1`; a *not sensitive* verdict is a fact about the model asked, not about the runtime's scheduling, so no ordering row moves on its account); clock, messages, nested flows, k-induction, heap and calc inlining, state machines and the engine option on the wire are later stages and refuse with the reason | | Schedule checking: `check` is the explicit-state model checker as an engine — `outcomes` and `holds` over the schedules of an invocation with its inputs as written: the `-action`s and `-state`s started on one clock, run to the `-advance` horizon, and the machines of the objects they materialize — authority *bounded*, `Replays: true`, bounds `depth`, `states`, `deadline` and every executor budget — selected by `-engine check`/`%engine check` for the invocation's `-action`/`-state`/`%action`/`%state` (`RunFor` under the engine searching the behaviors named together, `%advance` the behavior last checked up to that horizon), with `-check-property`, `-check-diverge`, `-check-witness`, `-check-depth` (`Budget.Depth`), `-check-states` (`Budget.Runs`, the checker's unit; under `all` one figure serves `explore` as linearizations) and `-check-timeout` (`Budget.Deadline`, so a search the clock stops is the plan's cancellation naming `time`, not a verdict), and `%check-property`, `%check-diverge`, `%check-witness`, `%check-bounds`, `%replay`; a `-check-*` flag without the engine, the engine without a behavior, a check-only flag under `-engine smt` and a bound that is not a positive integer or duration are refused before anything runs; an exhaustive clean search is (`holds`/`outcomes`, *bounded*), never *proved*; a violation or divergent value is *witnessed* only once `runtime.Replay` replayed it on the plan's workers, a disagreement *not covered* with the reason; `evaluate`, `sweep` and `satisfiable` questions, a fixed schedule and free inputs are typed refusals; registered in `Default()`, and `auto` never picks it over `explore`, so no existing golden moves; the CLI exits `1` on a violation or divergence, `0` on an exhaustive clean search, `2` on a bounded, cancelled or refused one, and `-json` carries a `check` object (`verdict`, `states`, `moves`, `depth`, `boundsHit`, `violations[]`, `divergent[]`, `outcomes[]`, witness paths) on the engine's `results[]` entry; a check ends no debugging session and starts none | `analysis/check.go` `checkEngine`, `NewCheck`, `CheckEngineName`, `Describe`, `Covers`, `Run`, `checkBounds`, `replayWitness`, `DefaultCheckDepth`, `DefaultCheckStates`; `analysis/question.go` `CheckAsk`; `analysis/check.go` `Checked`; `analysis/registry.go` `Default`; `cmd/sysml/check.go` `checkerOptions`, `checkTimeout`, `checks.checkerMisuse`; `cmd/sysml/report.go` `checkSearch`, `checkViolation`, `checkDivergent`; `cmd/sysml/usage.go`; `repl/checker.go` `Session.checkInvocation`, `checkInvocations`, `checking`, `doCheckBounds`, `doReplay`; `repl/invocation.go`; `repl/meta.go`; `examples/self-model/behavior.sysml`, `pipeline.sysml` (the engine in the self-model) | `analysis/check_test.go:TestCheckDescribesItself`, `:TestCheckBoundsNameEachBudgetHit`, `:TestCheckCoversOutcomesAndHoldsOverAnActionsSchedules`, `:TestCheckBoundsAnOutcomeSet`, `:TestCheckWitnessesADivergence`, `:TestCheckHoldsOrWitnessesAProperty`, `:TestCheckWritesEveryWitness`, `:TestCheckWitnessThatFailsReplayIsNotCovered`, `:TestExploreRefereesCheck`, `:TestCheckTakesTheBudgetsDepthAndRuns`, `:TestCheckStopsAtThePlansDeadline`, `:TestChecksOnOneModelHaveWorkersOfTheirOwn` (two checks on two goroutines under `-race`, each on workers of its own); `analysis/check_clock_test.go:TestExploreRefereesCheckOverBehaviorsOnOneClock` (an action's wait and a machine's timer due together: `explore`'s table and the checker's outcome set agree, the tie's divergence witnessed), `:TestChecksOfBehaviorsOnOneClockHaveWorkersOfTheirOwn`; `analysis/scale_test.go:TestEveryEngineClaimStrengthPair` (`check`'s pairs), `:TestNoPathPromotesTheStrength`; `analysis/registry_test.go`; `cmd/sysml/check_engine_test.go:TestEngineCheckWitnessesADivergence`, `:TestEngineCheckJudgesAPropertyOfThePerformer`, `:TestEngineCheckNamesTheBoundsItHits`, `:TestEngineCheckRefusesMisuse`, `:TestEngineCheckSearchesBehaviorsOnOneClock` (`-state` alone, with `-advance`, and beside an `-action` on one clock; the joint outcomes in `-json`), `:TestEngineCheckSearchesAPausedBody`, `:TestJSONReportsTheCheckedPlan`; `cmd/sysml/engines_test.go`; `repl/checker_test.go:TestCheckSettingsShowSetAndClear`, `:TestEngineCheckSearchesTheActionsSchedules`, `:TestEngineCheckJudgesPropertiesOfThePerformer`, `:TestEngineCheckNamesTheBoundsItHits`, `:TestReplayStepsTheRunAWitnessRecords`, `:TestReplayRefusesAWitnessOfAnotherRun`; `repl/checker_state_test.go:TestEngineCheckSearchesStateMachines`, `:TestEngineCheckAdvanceNeedsACheckedInvocation`, `:TestReplayStepsBehaviorsOnOneClock`; `examples/self_model_test.go:TestSelfModelAnalysisFrameworkMatchesImplementation`; every conformance, trace, sweep, REPL/CLI/gRPC golden unchanged; `make man-check` | 🧩 Extension (OpenSysML; single-threaded search: `Jobs` divides the replay of witnesses, not the search; `ExecuteActionRequest` carries no `engine` field, so the checker has no gRPC surface until the wire gains one) | | A `-state` invocation without `-advance` is observed after its initial transition only, under every engine and schedule (the CLI contract `-advance` states; the library fixes no instant to observe a run at): the default run, `-schedule explore` and `-engine check` stop each machine there — check keeps of the machine's moves only those of the entry its initial transition holds, and a wait ahead lies beyond the horizon — so no engine runs a do behavior another skips; with `-advance