fix(grpc): verification RPCs naming no subject evaluate over the held population

changes/unreleased/grpc-verify-held-population.fixed.md

@@ -0,0 +1,2 @@
+- gRPC `VerifyConstraint`, `VerifyRequirement` and `RunAnalysis` naming no `subject_symbol_id` now evaluate over the objects `Instantiate` holds for the model, as `VerifySatisfaction` already did and as the REPL's checks are about the objects a session holds: a verification case a definition owns runs once per held object of the definition and its `verification_verdicts` name each object, a constraint or requirement a definition owns is checked on the held object carrying it (ambiguous over several), and a case a definition owns runs as a feature of the held object of that definition. Before, `VerifyRequirement` after `Instantiate` answered a definition-owned case `inconclusive: needs an object … none is instantiated` while `VerifySatisfaction` on the same model reported it `pass` per object. A named subject keeps a worker of its own. A sweep over the population that would pass the `OPENSYSML_GRPC_MAX_HELD_OBJECTS` bound is `RESOURCE_EXHAUSTED`, as `Instantiate` is, rather than an error verdict quoting the runtime; `runtime.VerificationVerdict` carries the error an error verdict reports, and a `this` read keeps its cause in the error chain.
+- A `RunAnalysis` run of a verification case over the held population that would pass the held-objects bound is `RESOURCE_EXHAUSTED` too, and a `RunAnalysis` tool dry run over the population undoes the preview's writes and puts the runtime's tool runner back, as the REPL's preview does.

changes/unreleased/satisfy-indexed-object-labels.fixed.md

@@ -0,0 +1 @@
+- `%satisfy`, `-satisfy` and the gRPC `VerifySatisfaction` sweep over a definition's `satisfy r;` now label each object they decide by the indexed path `%validate` and `-validate=` print for it — `satisfy costReq holds (on test::fleet.cheap[1] ID: 2)` rather than `(on test::fleet.cheap ID: 2)` — the runtime spelling a carrier's path once, as the validation walk spells the object it reaches; the gRPC satisfy verdict carries it as `instance_path`.

cmd/sysml/satisfy_label_test.go

@@ -0,0 +1,42 @@
+package main
+
+import (
+	"strings"
+	"testing"
+)
+
+// repeatedPartModel holds two objects of a definition stating a satisfaction
+// under one usage with a multiplicity.
+const repeatedPartModel = `package test {
+	private import ScalarValues::Real;
+	requirement def CostRequirement {
+		subject product : Definition;
+		attribute maximumCost : Real;
+		require constraint costOk { product.cost <= maximumCost }
+	}
+	requirement costReq : CostRequirement { :>> maximumCost = 100.0; }
+	part def Definition {
+		attribute cost : Real;
+		satisfy costReq;
+	}
+	part def Fleet { part cheap : Definition [2] { attribute :>> cost = 80.0; } }
+	part fleet : Fleet;
+}`
+
+// TestSatisfyLabelsObjectsAsValidateDoes checks that -satisfy names each object a
+// definition's `satisfy r;` is decided on by the indexed path -validate prints for it.
+func TestSatisfyLabelsObjectsAsValidateDoes(t *testing.T) {
+	binary := buildCLI(t)
+	files := map[string]string{"fleet.sysml": repeatedPartModel}
+	labels := []string{
+		"✓ satisfy costReq holds (on test::fleet.cheap[1] ID: 2)",
+		"✓ satisfy costReq holds (on test::fleet.cheap[2] ID: 3)",
+	}
+	satisfied := checkFiles(t, binary, files, "-instantiate", "test::fleet", "-satisfy")
+	wantReport(t, satisfied, 0, labels...)
+	validated := checkFiles(t, binary, files, "-instantiate", "test::fleet", "-validate=test::fleet")
+	wantReport(t, validated, 0, labels...)
+	if strings.Contains(satisfied.output(), "fleet.cheap ID") {
+		t.Errorf("-satisfy labels an object by its feature alone, not its indexed path:\n%s", satisfied.output())
+	}
+}

docs/reference/wire-contract.md

@@ -1745,6 +1745,23 @@ never both.
 one per assertion. All three return the `instances` they built, in the same shape as
 `Instantiate`.
 
+With no `subjectSymbolId`, the three — and `RunAnalysis` — evaluate over the objects
+`Instantiate` holds for the model, as the REPL's `%constraint`, `%requirement`, `%satisfy` and
+`%analysis` are about the objects a session holds: a constraint or requirement a definition owns
+is checked on the one held object carrying it (ambiguous over several of distinct declarations, as
+the REPL answers; one declaration instantiated twice is checked on its newest object), a
+verification case a definition owns runs once per held object of that definition and reports a
+`verificationVerdicts` entry about each, naming the object by `instanceId`, and a `satisfy`
+a definition states is decided per held object with `instancePath` spelling the object's path
+from the root it was instantiated under (`cheap[2]`), as `ValidateInstance` spells it. The
+`instances` carry every object a verdict is about. With nothing held, the answer is about
+declared defaults, and a definition-owned case is `inconclusive` asking for an object. A
+sweep that would make one more object than `OPENSYSML_GRPC_MAX_HELD_OBJECTS` allows is
+`RESOURCE_EXHAUSTED`, as `Instantiate` is, and leaves the population as it was. A `RunAnalysis`
+tool dry run over the held population leaves it as it was too: the preview's writes are undone
+and the runner it previewed with is taken off. An `explore` schedule is the exception: its runs
+are made on runtimes of their own, one per linearization, holding nothing, as the REPL's are.
+
 A constraint or requirement whose condition reads `in` parameters takes their values on the
 request: `arguments` is a positional list bound in declaration order, `namedArguments` binds by
 parameter name, and the two may be mixed, as `RunAnalysis` binds a case's inputs; the values are

internal/exec/runtime/condition.go

@@ -1068,16 +1068,16 @@ func (ctx *Context) reachCarriers(roots []*Instance, carries func(*Instance) boo
 	var out []carrier
 	seen := make(map[int64]bool, len(roots))
 	path := make(map[*symbols.Symbol]bool)
-	var descend func(root, inst *Instance, through string, features []string)
-	descend = func(root, inst *Instance, through string, features []string) {
+	var descend func(root, inst *Instance, through string, features, segments []string)
+	descend = func(root, inst *Instance, through string, features, segments []string) {
 		// A destroyed object a live holder retains is no carrier, and holds nothing to walk.
 		if inst == nil || seen[inst.ID] || ctx.checkNotDestroyed(inst) != nil {
 			return
 		}
 		seen[inst.ID] = true
 		if carries(inst) {
 			occurrence := carrierOccurrence{through: through, decl: inst.Type}
-			out = append(out, carrier{instance: inst, root: root, features: features, occurrence: occurrence})
+			out = append(out, carrier{instance: inst, root: root, features: features, segments: segments, occurrence: occurrence})
 		}
 		if inst.Type != nil {
 			if path[inst.Type] {
@@ -1088,11 +1088,12 @@ func (ctx *Context) reachCarriers(roots []*Instance, carries func(*Instance) boo
 		}
 		for _, child := range ctx.nestedObjects(inst) {
 			nested := append(features[:len(features):len(features)], child.feature)
-			descend(root, child.instance, through+"/"+strconv.Quote(child.feature), nested)
+			walked := append(segments[:len(segments):len(segments)], child.segment)
+			descend(root, child.instance, through+"/"+strconv.Quote(child.feature), nested, walked)
 		}
 	}
 	for _, root := range roots {
-		descend(root, root, ctx.rootPath(root), nil)
+		descend(root, root, ctx.rootPath(root), nil, nil)
 	}
 	return out
 }
@@ -1128,9 +1129,12 @@ func (ctx *Context) rootPath(root *Instance) string {
 // carrier is an object a search reached: the object the search started from and
 // the features walked from it name a nested one, which has no name of its own.
 type carrier struct {
-	instance   *Instance
-	root       *Instance
-	features   []string
+	instance *Instance
+	root     *Instance
+	features []string
+	// segments spell the features walked as a path names them, a collection's
+	// element indexed: what a verdict about the carrier labels it by.
+	segments   []string
 	occurrence carrierOccurrence
 }
 
@@ -1150,6 +1154,9 @@ type carrierOccurrence struct {
 type heldObject struct {
 	feature  string
 	instance *Instance
+	// segment names the object under its feature as a path spells it: the
+	// feature's name, indexed for a collection's element (`wheels[2]`).
+	segment string
 }
 
 // nestedObjects returns the objects the object-valued features of inst hold,
@@ -1199,9 +1206,9 @@ func (ctx *Context) heldObjectsOf(inst *Instance, through func(*Instance, Object
 			}
 			held = NewSequenceValue(&Sequence{elements: standingElements(fv.HeldValue())})
 		}
-		for _, id := range heldObjects(held) {
-			if child, ok := ctx.instances[id]; ok {
-				out = append(out, heldObject{feature: of.Name, instance: child})
+		for _, held := range heldSegments(held, source.NameText(of.Name)) {
+			if child, ok := ctx.instances[held.id]; ok {
+				out = append(out, heldObject{feature: of.Name, instance: child, segment: held.segment})
 			}
 		}
 	}
@@ -1226,11 +1233,18 @@ func objectFeature(sym *symbols.Symbol) bool {
 	return objectUsageKind(usage.Kind) || usage.Kind == ast.UsagePort
 }
 
-// heldObjects returns the identities a feature value denotes, a collection's
-// elements included.
-func heldObjects(val Value) []int64 {
+// heldSegment is the identity of an object a feature value holds and the segment
+// naming it there.
+type heldSegment struct {
+	segment string
+	id      int64
+}
+
+// heldSegments returns the identities a feature value denotes, a collection's elements
+// included, each under the segment a path names it by: the name, indexed for an element.
+func heldSegments(val Value, name string) []heldSegment {
 	if id, ok := val.Object(); ok {
-		return []int64{id}
+		return []heldSegment{{segment: name, id: id}}
 	}
 	var elements []Value
 	switch {
@@ -1239,15 +1253,32 @@ func heldObjects(val Value) []int64 {
 	case val.Kind == ValSet && val.Set() != nil:
 		elements = val.Set().Elements()
 	}
-	var out []int64
-	for _, element := range elements {
+	var out []heldSegment
+	for i, element := range elements {
 		if id, ok := element.Object(); ok {
-			out = append(out, id)
+			out = append(out, heldSegment{segment: indexedSegment(name, i), id: id})
 		}
 	}
 	return out
 }
 
+// heldObjects returns the identities a feature value denotes, a collection's
+// elements included.
+func heldObjects(val Value) []int64 {
+	held := heldSegments(val, "")
+	out := make([]int64, len(held))
+	for i, h := range held {
+		out[i] = h.id
+	}
+	return out
+}
+
+// indexedSegment names a collection's element in a path: the feature's name
+// indexed from 1, `wheels[2]`, as every surface reporting an object spells it.
+func indexedSegment(name string, i int) string {
+	return fmt.Sprintf("%s[%d]", name, i+1)
+}
+
 // carrierLabels names carriers as a diagnostic can quote them: the definition
 // each is an object of, its identity, and the feature path telling two apart.
 func (ctx *Context) carrierLabels(carriers []carrier) []string {
@@ -1277,14 +1308,20 @@ func qualifiedText(names []string) string {
 	return strings.Join(parts, "::")
 }
 
+// carrierDeclaration is the name of the declaration a carrier materializes where
+// it is not the definition it is an object of; empty where it is.
+func carrierDeclaration(c carrier, definition string) string {
+	if c.instance.Type != nil && c.instance.Type.Name != definition {
+		return c.instance.Type.Name
+	}
+	return ""
+}
+
 // carrierPath names a carrier apart from its siblings: the features walked to
 // it, ending in the declaration it materializes — which differs from the feature
 // holding it when a collection gathers objects of several declarations.
 func carrierPath(c carrier, definition string) []string {
-	decl := ""
-	if c.instance.Type != nil && c.instance.Type.Name != definition {
-		decl = c.instance.Type.Name
-	}
+	decl := carrierDeclaration(c, definition)
 	if len(c.features) == 0 {
 		if decl == "" {
 			return nil
@@ -1298,17 +1335,23 @@ func carrierPath(c carrier, definition string) []string {
 	return walked
 }
 
-// carrierFeatures is the feature path to a nested carrier, one name a segment,
-// corrected the way carrierLabels names an ambiguity's carriers.
+// carrierFeatures is a verdict's path to a nested carrier: the segments walked from its root,
+// a collection's element indexed as validation spells it, ending in the declaration it materializes.
 func (ctx *Context) carrierFeatures(c carrier) []string {
-	if len(c.features) == 0 || c.instance == nil {
+	if len(c.segments) == 0 || c.instance == nil {
 		return nil
 	}
 	name := "object"
 	if def := ctx.definitionOf(c.instance.Type); def != nil && def.Name != "" {
 		name = def.Name
 	}
-	return carrierPath(c, name)
+	decl := carrierDeclaration(c, name)
+	if decl == "" || c.features[len(c.features)-1] == decl {
+		return c.segments
+	}
+	walked := append([]string(nil), c.segments...)
+	walked[len(walked)-1] = source.NameText(decl)
+	return walked
 }
 
 // definitionOf is the definition objects of sym are objects of: sym itself when

internal/exec/runtime/eval.go

@@ -1423,7 +1423,7 @@ func (ec *EvalContext) thisValue() (Value, error) {
 	if occurrence == nil && ec.thisOccurrence != nil {
 		materialized, err := ec.thisOccurrence()
 		if err != nil {
-			return Value{}, fmt.Errorf("%w: %v", errThisNotAnObject, err)
+			return Value{}, fmt.Errorf("%w: %w", errThisNotAnObject, err)
 		}
 		occurrence = materialized
 		ec.occurrence = materialized

internal/exec/runtime/validate.go

@@ -405,7 +405,7 @@ func (w *validationWalk) heldChildren(fv *FeatureValue, segment string) []heldCh
 		}
 	}
 	for i, val := range elements {
-		reach(val, fmt.Sprintf("%s[%d]", segment, i+1))
+		reach(val, indexedSegment(segment, i))
 	}
 	return out
 }

internal/exec/runtime/verification_cases.go

@@ -194,7 +194,7 @@ func (ctx *Context) verificationResultOn(sym *symbols.Symbol, self *Instance) Ve
 	result, err := ctx.RunVerification(sym, AnalysisArgs{}, scope, self)
 	if err != nil {
 		return VerificationResult{Verdict: VerificationVerdict{
-			Case: ctx.QualifiedName(sym), Symbol: sym, Kind: verdictError, Detail: err.Error(), Subject: self,
+			Case: ctx.QualifiedName(sym), Symbol: sym, Kind: verdictError, Detail: err.Error(), Err: err, Subject: self,
 		}}
 	}
 	if result.Verdict.Subject == nil {

internal/exec/runtime/verification_run.go

@@ -52,6 +52,10 @@ type VerificationVerdict struct {
 	// decided nothing; empty for pass and fail.
 	Detail string
 
+	// Err is the failure an error verdict reports, so a caller can tell a
+	// resource bound from a fault of the model; nil for every other verdict.
+	Err error
+
 	// Subcase marks the verdict of a case performed by another, which the
 	// library states no roll-up for and which is therefore reported on its own.
 	Subcase bool
@@ -145,7 +149,7 @@ func (ctx *Context) RunVerification(sym *symbols.Symbol, args AnalysisArgs, scop
 			}, nil
 		}
 		return VerificationResult{
-			Verdict: VerificationVerdict{Case: name, Symbol: sym, Kind: verdictError, Detail: err.Error(), Subject: performer},
+			Verdict: VerificationVerdict{Case: name, Symbol: sym, Kind: verdictError, Detail: err.Error(), Err: err, Subject: performer},
 		}, nil
 	}
 	result := VerificationResult{Verdict: ctx.bodyVerdict(sym, name, caseRun, run), Run: run}

internal/frontend/grpc/analysis.go

@@ -50,9 +50,21 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) (
 	if explores {
 		return s.exploreAnalysis(ctx, policy, v, req, sym)
 	}
-	if err := v.runtime.SetSchedule(schedule); err != nil {
+	// A case naming no subject runs over the objects the model holds, a type-owned
+	// one as a feature of the object of its type held, as the REPL's %analysis does.
+	if on, unlock := v.overHeld(ctx, args.Subject); on != v {
+		defer unlock()
+		v = on
+		// Read again on the runtime the run is made on, as an explored run reads them.
+		if args, resp, err = v.analysisArgs(req); resp != nil || err != nil {
+			return resp, err
+		}
+	}
+	reset, err := v.scheduled(schedule)
+	if err != nil {
 		return nil, statusError(connect.CodeInvalidArgument, err.Error())
 	}
+	defer reset()
 	if req.ToolDryRun {
 		return s.toolDryRun(ctx, v, sym, args)
 	}
@@ -62,9 +74,39 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) (
 	if gone := callerGone(ctx, err); gone != nil {
 		return nil, gone
 	}
+	if status := v.exhaustedRun(run, err); status != nil {
+		return nil, status
+	}
 	return v.caseResponse(run, plan, err), nil
 }
 
+// exhaustedRun is the RESOURCE_EXHAUSTED status of a held-population run that passed
+// its bound, in the call's error or in a verification verdict's; nil for any other run.
+func (v *verifyContext) exhaustedRun(run caseRun, err error) error {
+	if status := v.exhausted(err); status != nil {
+		return status
+	}
+	for _, verdict := range run.verdicts() {
+		if status := v.exhausted(verdict.Err); status != nil {
+			return status
+		}
+	}
+	return nil
+}
+
+// scheduled sets the runtime's schedule for this request and returns what puts back
+// the one it had, so the held population's runtime is left as found; unsettable is the error.
+func (v *verifyContext) scheduled(policy runtime.SchedulePolicy) (func(), error) {
+	was := v.runtime.Schedule()
+	if err := v.runtime.SetSchedule(policy); err != nil {
+		return nil, err
+	}
+	return func() {
+		// The policy the runtime held was set once already, so it is settable.
+		_ = v.runtime.SetSchedule(was)
+	}, nil
+}
+
 // caseResponse reports one run of a case: its outputs, verdicts, evaluations
 // and instances, or the failure that stopped it, with the plan's standing.
 func (v *verifyContext) caseResponse(run caseRun, plan analysis.Plan, err error) *pb.RunAnalysisResponse {