From 0cd4051f3e8be4e18f0b6cc15f939d91912546b5 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:13:40 +0000 Subject: [PATCH 01/10] test(grpc): pin VerifyRequirement without a subject over the held population After Instantiate, VerifyRequirement naming no subject must run a definition-owned verification case on every object the model holds, as the REPL's %requirement does after %instantiate and as VerifySatisfaction already does; it reports the case inconclusive instead. Co-Authored-By: jason.han --- .../grpc/held_population_verify_test.go | 75 +++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 internal/frontend/grpc/held_population_verify_test.go diff --git a/internal/frontend/grpc/held_population_verify_test.go b/internal/frontend/grpc/held_population_verify_test.go new file mode 100644 index 0000000000..732d8b9b1f --- /dev/null +++ b/internal/frontend/grpc/held_population_verify_test.go @@ -0,0 +1,75 @@ +package grpc + +import ( + "context" + "strings" + "testing" + + pb "github.com/Open-MBEE/OpenSysML/api/proto" +) + +// heldPopulationModel owns a verification case in a definition two objects of +// which a holder repeats; the case's verdict calls the requirement on `this`. +const heldPopulationModel = `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; + verification costTest { + objective costObjective { verify costReq; } + return verdict = VerificationCases::PassIf(costReq(this)); + } + } + part def Fleet { part cheap : Definition [2] { attribute :>> cost = 80.0; } } + part fleet : Fleet; +}` + +// TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation verifies that +// VerifyRequirement naming no subject answers over the objects Instantiate holds, +// as the REPL's %requirement does after %instantiate: the requirement's own verdict +// is undecided, its subject being unbound, and the definition-owned case runs once +// on each held object of the definition — the same verdicts VerifySatisfaction reports. +func TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation(t *testing.T) { + srv := mustNewService(t, 10) + hash := mustVerifyModel(t, srv, heldPopulationModel, "held-population-requirement") + ctx := context.Background() + made, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: hash, SymbolId: "test::fleet"}) + if err != nil || made.Error != "" { + t.Fatalf("Instantiate(test::fleet): %v %q", err, made.GetError()) + } + + satisfied, err := srv.VerifySatisfaction(ctx, &pb.VerifySatisfactionRequest{ModelHash: hash}) + if err != nil { + t.Fatalf("VerifySatisfaction: %v", err) + } + wantVerdicts(t, "VerifySatisfaction", satisfied.VerificationVerdicts, "test::Definition::costTest=pass", "test::Definition::costTest=pass") + + required, err := srv.VerifyRequirement(ctx, &pb.VerifyRequirementRequest{ModelHash: hash, SymbolId: "test::costReq"}) + if err != nil { + t.Fatalf("VerifyRequirement: %v", err) + } + if required.Error != "" { + t.Fatalf("VerifyRequirement reported %q", required.Error) + } + if v := required.Verdict; v.Status != statusUndecided || !strings.Contains(v.Error, "product subject is unbound") { + t.Errorf("requirement verdict = %v, want undecided with the subject unbound, as the REPL answers", v) + } + wantVerdicts(t, "VerifyRequirement", required.VerificationVerdicts, "test::Definition::costTest=pass", "test::Definition::costTest=pass") + wantVerdictObjects(t, "VerifyRequirement", required.VerificationVerdicts, required.Instances, "test::Fleet::cheap", "test::Fleet::cheap") + // The verdicts are about the held objects, the ones VerifySatisfaction decided. + heldObjects := map[int64]bool{} + for _, v := range satisfied.VerificationVerdicts { + heldObjects[v.InstanceId] = true + } + for _, v := range required.VerificationVerdicts { + if !heldObjects[v.InstanceId] { + t.Errorf("VerifyRequirement verdict on object #%d, which the model does not hold (held %v)", v.InstanceId, heldObjects) + } + } +} From 20f6bc00bcb152e4fe61f7a4451de0a87a3b79f0 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:24:07 +0000 Subject: [PATCH 02/10] fix(grpc): verification RPCs naming no subject evaluate over the held population VerifyConstraint, VerifyRequirement and RunAnalysis with no subject named now evaluate on the runtime holding the objects Instantiate created, under its lock, as Instantiate and VerifySatisfaction do: a definition-owned verification case runs once per held object, a type-owned constraint is checked on the held object carrying it, and a case a definition owns runs as a feature of the held object of that definition. A named subject keeps its own worker. A run over the population that would pass the held-objects bound is RESOURCE_EXHAUSTED, as Instantiate is; VerificationVerdict carries the error it reports so surfaces can classify it, and the `this` read keeps the cause in its error chain. Co-Authored-By: jason.han --- internal/exec/runtime/eval.go | 2 +- internal/exec/runtime/verification_cases.go | 2 +- internal/exec/runtime/verification_run.go | 6 +- internal/frontend/grpc/analysis.go | 31 ++++- .../grpc/held_population_verify_test.go | 91 +++++++++++++++ .../grpc/robustness_held_population_test.go | 59 ++++++++++ internal/frontend/grpc/validate.go | 6 +- internal/frontend/grpc/verify.go | 110 +++++++++++++++--- 8 files changed, 286 insertions(+), 21 deletions(-) create mode 100644 internal/frontend/grpc/robustness_held_population_test.go diff --git a/internal/exec/runtime/eval.go b/internal/exec/runtime/eval.go index 036f40ff5e..3920c50d74 100644 --- a/internal/exec/runtime/eval.go +++ b/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 diff --git a/internal/exec/runtime/verification_cases.go b/internal/exec/runtime/verification_cases.go index 2ad230bebb..f713cc5ff3 100644 --- a/internal/exec/runtime/verification_cases.go +++ b/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 { diff --git a/internal/exec/runtime/verification_run.go b/internal/exec/runtime/verification_run.go index 1cf836bb1b..fb8ec49737 100644 --- a/internal/exec/runtime/verification_run.go +++ b/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} diff --git a/internal/frontend/grpc/analysis.go b/internal/frontend/grpc/analysis.go index 8475f04b59..3b4a35cbd5 100644 --- a/internal/frontend/grpc/analysis.go +++ b/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,26 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) ( if gone := callerGone(ctx, err); gone != nil { return nil, gone } + if status := v.exhausted(err); status != nil { + return nil, status + } return v.caseResponse(run, plan, err), nil } +// scheduled sets the runtime's schedule for this request and returns what puts +// back the one it had, so a request leaves the held population's runtime as it +// found it; a policy the runtime cannot be set to 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 { diff --git a/internal/frontend/grpc/held_population_verify_test.go b/internal/frontend/grpc/held_population_verify_test.go index 732d8b9b1f..98c0d3059c 100644 --- a/internal/frontend/grpc/held_population_verify_test.go +++ b/internal/frontend/grpc/held_population_verify_test.go @@ -73,3 +73,94 @@ func TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation(t *testing.T) { } } } + +// TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier verifies that a +// constraint a definition owns, asked about with no subject, is checked on the +// one held object carrying it, is ambiguous over two, and reads declared defaults +// when the model holds none — as the REPL's %constraint decides it. +func TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier(t *testing.T) { + srv := mustNewService(t, 10) + hash := mustVerifyModel(t, srv, `package Tanks { + private import ScalarValues::Real; + part def Tank { + attribute volume : Real default := 5.0; + constraint positive { volume > 0.0 } + } + part full : Tank { attribute :>> volume = 8.0; } + part drained : Tank { attribute :>> volume = -1.0; } +}`, "held-carrier-constraint") + ctx := context.Background() + verify := func(t *testing.T) *pb.Verdict { + t.Helper() + resp, err := srv.VerifyConstraint(ctx, &pb.VerifyConstraintRequest{ModelHash: hash, SymbolId: "Tanks::Tank::positive"}) + if err != nil { + t.Fatalf("VerifyConstraint: %v", err) + } + if resp.Error != "" { + t.Fatalf("VerifyConstraint reported %q", resp.Error) + } + return resp.Verdict + } + if v := verify(t); v.Status != statusHolds || v.InstanceId != 0 { + t.Errorf("verdict with no object held = %v, want holds on the declared default and no object", v) + } + + drained, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: hash, SymbolId: "Tanks::drained"}) + if err != nil || drained.Error != "" { + t.Fatalf("Instantiate(drained): %v %q", err, drained.GetError()) + } + if v := verify(t); v.Status != statusViolated || v.InstanceId != drained.Instance.Id { + t.Errorf("verdict with drained held = %v, want violated on object #%d", v, drained.Instance.Id) + } + + if full, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: hash, SymbolId: "Tanks::full"}); err != nil || full.Error != "" { + t.Fatalf("Instantiate(full): %v %q", err, full.GetError()) + } + if v := verify(t); v.Status != statusUndecided || v.FailureReason != pb.FailureReason_FAILURE_REASON_AMBIGUOUS_SUBJECT { + t.Errorf("verdict with two carriers held = %v, want undecided with an ambiguous subject", v) + } + // A named subject keeps its own object, whatever the model holds. + resp, err := srv.VerifyConstraint(ctx, &pb.VerifyConstraintRequest{ModelHash: hash, SymbolId: "Tanks::Tank::positive", SubjectSymbolId: "Tanks::full"}) + if err != nil { + t.Fatalf("VerifyConstraint on full: %v", err) + } + if v := resp.Verdict; v.Status != statusHolds || v.InstanceTypeId != "Tanks::full" { + t.Errorf("verdict on full = %v, want holds on an object of Tanks::full", v) + } +} + +// TestRunAnalysisWithoutASubjectRunsOnTheHeldObject verifies that a case a +// definition owns, run with no subject, is a feature of the one held object of +// the definition, is ambiguous over two, and asks for one when the model holds +// holds none — as the REPL's %analysis decides it. +func TestRunAnalysisWithoutASubjectRunsOnTheHeldObject(t *testing.T) { + srv := mustNewService(t, 10) + hash := mustVerifyModel(t, srv, definitionOwnedCaseModel, "held-definition-owned-analysis") + ctx := context.Background() + const kase = "Cost::Definition::costTest" + + resp := runAnalysis(t, srv, &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: kase}) + wantVerdicts(t, "RunAnalysis with no object", resp.VerificationVerdicts, kase+"=inconclusive") + + if made, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: hash, SymbolId: "Cost::dear"}); err != nil || made.Error != "" { + t.Fatalf("Instantiate(dear): %v %q", err, made.GetError()) + } + resp = runAnalysis(t, srv, &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: kase}) + if resp.Error != "" { + t.Fatalf("RunAnalysis with dear held reported %q", resp.Error) + } + wantVerdicts(t, "RunAnalysis with dear held", resp.VerificationVerdicts, kase+"=fail") + wantVerdictObjects(t, "RunAnalysis with dear held", resp.VerificationVerdicts, resp.Instances, "Cost::dear") + + if made, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: hash, SymbolId: "Cost::cheap"}); err != nil || made.Error != "" { + t.Fatalf("Instantiate(cheap): %v %q", err, made.GetError()) + } + resp = runAnalysis(t, srv, &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: kase}) + wantVerdicts(t, "RunAnalysis with two objects held", resp.VerificationVerdicts, kase+"=error") + if detail := resp.VerificationVerdicts[0].Detail; !strings.Contains(detail, "ambiguous subject") || !strings.Contains(detail, "cheap") || !strings.Contains(detail, "dear") { + t.Errorf("RunAnalysis with two objects held = %q, want the ambiguity naming both carriers", detail) + } + // Naming the object keeps today's answer about it. + resp = runAnalysis(t, srv, &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: kase, SubjectSymbolId: "Cost::cheap"}) + wantVerdicts(t, "RunAnalysis on cheap", resp.VerificationVerdicts, kase+"=pass") +} diff --git a/internal/frontend/grpc/robustness_held_population_test.go b/internal/frontend/grpc/robustness_held_population_test.go new file mode 100644 index 0000000000..082d3c5200 --- /dev/null +++ b/internal/frontend/grpc/robustness_held_population_test.go @@ -0,0 +1,59 @@ +package grpc + +import ( + "context" + "strings" + "testing" + + "connectrpc.com/connect" + pb "github.com/Open-MBEE/OpenSysML/api/proto" +) + +// TestGRPCRobustnessHeldPopulation puts the verification RPCs to the objects +// Instantiate holds, with no subject named, at the population's bound: a case run +// on a held object needs an object of its own, so a sweep that would pass the +// bound is RESOURCE_EXHAUSTED naming it, as Instantiate is, not an error verdict +// quoting the runtime; the population is left as it was, and a check about a +// named subject, made on a worker of its own, is unaffected. +func TestGRPCRobustnessHeldPopulation(t *testing.T) { + t.Setenv(HeldObjectsEnvVar, "3") + srv := mustNewService(t, 10) + hash := mustVerifyModel(t, srv, heldPopulationModel, "held-population-robustness") + ctx := context.Background() + if made, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: hash, SymbolId: "test::fleet"}); err != nil || made.Error != "" { + t.Fatalf("Instantiate(test::fleet): %v %q", err, made.GetError()) + } + exhausted := func(t *testing.T, rpc string, err error) { + t.Helper() + if connect.CodeOf(err) != connect.CodeResourceExhausted { + t.Fatalf("%s at the bound: code = %v, want RESOURCE_EXHAUSTED: %v", rpc, connect.CodeOf(err), err) + } + for _, text := range []string{"holds 3 objects", HeldObjectsEnvVar} { + if !strings.Contains(err.Error(), text) { + t.Errorf("%s error %q lacks %q", rpc, err.Error(), text) + } + } + } + + t.Run("requirement sweep at the bound", func(t *testing.T) { + _, err := srv.VerifyRequirement(ctx, &pb.VerifyRequirementRequest{ModelHash: hash, SymbolId: "test::costReq"}) + exhausted(t, "VerifyRequirement", err) + }) + t.Run("satisfaction sweep at the bound", func(t *testing.T) { + _, err := srv.VerifySatisfaction(ctx, &pb.VerifySatisfactionRequest{ModelHash: hash}) + exhausted(t, "VerifySatisfaction", err) + }) + t.Run("population unchanged", func(t *testing.T) { + cached, _ := srv.cache.Get(hash) + if got := srv.objects(cached).rt.InstanceCount(); got != 3 { + t.Errorf("held after the refused sweeps = %d, want 3", got) + } + }) + t.Run("named subject on its own worker", func(t *testing.T) { + resp, err := srv.VerifyRequirement(ctx, &pb.VerifyRequirementRequest{ModelHash: hash, SymbolId: "test::costReq", SubjectSymbolId: "test::fleet"}) + if err != nil { + t.Fatalf("VerifyRequirement on fleet: %v", err) + } + wantVerdicts(t, "VerifyRequirement on fleet", resp.VerificationVerdicts, "test::Definition::costTest=pass", "test::Definition::costTest=pass") + }) +} diff --git a/internal/frontend/grpc/validate.go b/internal/frontend/grpc/validate.go index b30c610e99..69de008864 100644 --- a/internal/frontend/grpc/validate.go +++ b/internal/frontend/grpc/validate.go @@ -60,7 +60,11 @@ func (s *Service) ValidateInstance(ctx context.Context, req *pb.ValidateInstance resp.Verdicts = append(resp.Verdicts, v.objectVerdict(ov, plan)) if req := ov.Requirement; req != nil && !verified[req] { verified[req] = true - resp.VerificationVerdicts = append(resp.VerificationVerdicts, v.requirementVerifications(req, root, nil)...) + verifications, err := v.requirementVerifications(req, root, nil) + if err != nil { + return nil, err + } + resp.VerificationVerdicts = append(resp.VerificationVerdicts, verifications...) } } return resp, nil diff --git a/internal/frontend/grpc/verify.go b/internal/frontend/grpc/verify.go index 62cb9390b5..c30058de55 100644 --- a/internal/frontend/grpc/verify.go +++ b/internal/frontend/grpc/verify.go @@ -57,6 +57,8 @@ type verifyContext struct { engine analysis.Selection // release gives the runtime's worker back once the request is answered; the RPC defers it. release func() + // held is the population the request evaluates over, nil on a worker of the request's own. + held *heldObjects } // newVerifyContext reads the request's engine, looks the model up and builds a @@ -86,6 +88,44 @@ func releaseNothing() { // The parent context releases the worker it borrowed; this one holds none. } +// overHeld is this request's context over the objects Instantiate holds for the model, +// under the population's lock, which the returned function releases: a request naming no +// subject is about those objects, as a REPL check is about the objects the session holds. +// A request naming its subject, or a model holding no object, keeps the request's own +// worker and releases nothing. +func (v *verifyContext) overHeld(ctx context.Context, subject *runtime.Instance) (*verifyContext, func()) { + if subject != nil { + return v, releaseNothing + } + held, ok := v.service.heldObjects(v.cached) + if !ok { + return v, releaseNothing + } + unlock := held.lock(ctx) + if held.empty() { + unlock() + return v, releaseNothing + } + return v.onHeld(held), unlock +} + +// onHeld is this request's context over a held population's runtime, which the +// caller holds the lock of; its failures at the population's bound are statuses. +func (v *verifyContext) onHeld(held *heldObjects) *verifyContext { + on := v.on(held.rt) + on.held = held + return on +} + +// exhausted is the RESOURCE_EXHAUSTED status of an evaluation over the held population +// that would pass its bound; nil for any other failure, and on a worker of the request's own. +func (v *verifyContext) exhausted(err error) error { + if v.held == nil { + return nil + } + return v.held.exhausted(err) +} + // sem is the semantic model the request's runtime evaluates against. func (v *verifyContext) sem() *semantics.Model { return v.runtime.Semantics() } @@ -297,6 +337,8 @@ func (s *Service) VerifyConstraint(ctx context.Context, req *pb.VerifyConstraint if err != nil { return &pb.VerifyConstraintResponse{Error: err.Error()}, nil } + v, unlock := v.overHeld(ctx, inst) + defer unlock() args, readErr, err := v.checkArgs(question, req.Arguments, req.NamedArguments) if err != nil { return nil, err @@ -314,6 +356,9 @@ func (s *Service) VerifyConstraint(ctx context.Context, req *pb.VerifyConstraint if err := callerGone(ctx, evalErr); err != nil { return nil, err } + if status := v.exhausted(evalErr); status != nil { + return nil, status + } subject := subjectOf(result, inst) return &pb.VerifyConstraintResponse{ Verdict: v.verdict(verdictConstraint, sym, "", subject, result.Holds, evalErr, plan), @@ -393,6 +438,8 @@ func (s *Service) VerifyRequirement(ctx context.Context, req *pb.VerifyRequireme if err != nil { return &pb.VerifyRequirementResponse{Error: err.Error()}, nil } + v, unlock := v.overHeld(ctx, inst) + defer unlock() args, readErr, err := v.checkArgs(question, req.Arguments, req.NamedArguments) if err != nil { return nil, err @@ -410,13 +457,21 @@ func (s *Service) VerifyRequirement(ctx context.Context, req *pb.VerifyRequireme if err := callerGone(ctx, evalErr); err != nil { return nil, err } + if status := v.exhausted(evalErr); status != nil { + return nil, status + } subject := subjectOf(result, inst) + // Beside the requirement's verdict: what the cases verifying it answered when + // their bodies ran, a type-owned one on each object of the type the model holds. + verifications, err := v.requirementVerificationRuns(sym, subject, nil) + if err != nil { + return nil, err + } return &pb.VerifyRequirementResponse{ - Verdict: v.verdict(verdictRequirement, sym, "", subject, result.Holds, evalErr, plan), - Instances: v.instanceGraph(subject), - // Beside the satisfaction verdict: what the cases verifying this - // requirement answered when their bodies ran. - VerificationVerdicts: v.requirementVerifications(sym, subject, nil), + Verdict: v.verdict(verdictRequirement, sym, "", subject, result.Holds, evalErr, plan), + // The subject's graph, and that of every object a case ran on. + Instances: v.instanceGraphs(v.runRoots(subject, verifications, nil, nil)), + VerificationVerdicts: v.verificationVerdicts(verifications, namedFQN(v.cached.Index, sym)), }, nil } @@ -525,7 +580,11 @@ func (v *verifyContext) satisfyVerdicts(ctx context.Context, a *runtime.SatisfyA if err != nil { return nil, nil, nil, err } - return []*pb.Verdict{verdict}, instances, v.assertionVerifications(a, subject, runs), nil + verifications, err := v.assertionVerifications(a, subject, runs) + if err != nil { + return nil, nil, nil, err + } + return []*pb.Verdict{verdict}, instances, verifications, nil } if a.StatingType() == nil { return one(v.satisfyVerdict(ctx, a)) @@ -539,7 +598,7 @@ func (v *verifyContext) satisfyVerdicts(ctx context.Context, a *runtime.SatisfyA if len(subjects) == 0 { return one(v.satisfyVerdict(ctx, a)) } - on := v.on(held.rt) + on := v.onHeld(held) var verdicts []*pb.Verdict var instances []*pb.Instance var verifications []*pb.VerificationVerdict @@ -556,7 +615,11 @@ func (v *verifyContext) satisfyVerdicts(ctx context.Context, a *runtime.SatisfyA on.associateRequirement(verdict, a) verdicts = append(verdicts, verdict) instances = append(instances, on.instanceGraph(subject)...) - verifications = append(verifications, on.assertionVerifications(a, subject, runs)...) + verified, err := on.assertionVerifications(a, subject, runs) + if err != nil { + return nil, nil, nil, err + } + verifications = append(verifications, verified...) } return verdicts, instances, verifications, nil } @@ -713,20 +776,35 @@ func (v *verifyContext) calcUsageOutputs(ctx context.Context, subject string, sy return pbOutputs, true, plan, nil } -// requirementVerifications are the body verdicts of the whole model's verification cases verifying -// req (the case need not share the requirement's document), type-owned ones run about subject. -func (v *verifyContext) requirementVerifications(req *symbols.Symbol, subject *runtime.Instance, runs *runtime.VerificationRuns) []*pb.VerificationVerdict { - return v.verificationVerdicts( - v.runtime.VerificationVerdictsOnce(v.cached.DocumentRoots(), req, subject, runs), - namedFQN(v.cached.Index, req)) +// requirementVerificationRuns runs the whole model's verification cases verifying req (the +// case need not share the requirement's document), type-owned ones about subject, and +// reports their body verdicts; a run over the held population that would pass its bound +// is the RESOURCE_EXHAUSTED status instead. +func (v *verifyContext) requirementVerificationRuns(req *symbols.Symbol, subject *runtime.Instance, runs *runtime.VerificationRuns) ([]runtime.VerificationVerdict, error) { + verdicts := v.runtime.VerificationVerdictsOnce(v.cached.DocumentRoots(), req, subject, runs) + for _, verdict := range verdicts { + if status := v.exhausted(verdict.Err); status != nil { + return nil, status + } + } + return verdicts, nil +} + +// requirementVerifications are requirementVerificationRuns' verdicts spelled for the wire. +func (v *verifyContext) requirementVerifications(req *symbols.Symbol, subject *runtime.Instance, runs *runtime.VerificationRuns) ([]*pb.VerificationVerdict, error) { + verdicts, err := v.requirementVerificationRuns(req, subject, runs) + if err != nil { + return nil, err + } + return v.verificationVerdicts(verdicts, namedFQN(v.cached.Index, req)), nil } // assertionVerifications are the body verdicts of the verification cases whose // objective verifies the requirement an assertion satisfies, run about subject. -func (v *verifyContext) assertionVerifications(a *runtime.SatisfyAssertion, subject *runtime.Instance, runs *runtime.VerificationRuns) []*pb.VerificationVerdict { +func (v *verifyContext) assertionVerifications(a *runtime.SatisfyAssertion, subject *runtime.Instance, runs *runtime.VerificationRuns) ([]*pb.VerificationVerdict, error) { req := a.AssertedRequirement() if req == nil { - return nil + return nil, nil } return v.requirementVerifications(req, subject, runs) } From 45b142323134e10616d6efd4e95dd6ddd62858bd 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:34:02 +0000 Subject: [PATCH 03/10] fix(repl): %satisfy labels a nested object by the indexed path %validate prints MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A definition's `satisfy r;` decided over the objects a session holds named a nested object by its feature alone (`fleet.cheap`) while %validate named the same object `fleet.cheap[1]`. The runtime now spells a carrier's path as the validation walk spells the object it reaches — one shared segment spelling, a collection's element indexed — and the REPL, the CLI's -satisfy and the gRPC satisfy verdict's instance_path label the object by it. Co-Authored-By: jason.han --- cmd/sysml/satisfy_label_test.go | 43 ++++++++++ internal/exec/runtime/condition.go | 83 +++++++++++++------ internal/exec/runtime/context.go | 2 +- internal/exec/runtime/satisfy.go | 2 +- internal/exec/runtime/validate.go | 2 +- internal/frontend/grpc/validate.go | 8 +- internal/frontend/grpc/verify.go | 1 + internal/frontend/repl/meta.go | 2 +- internal/frontend/repl/query.go | 18 ++-- internal/frontend/repl/satisfy_stated_test.go | 32 +++++++ internal/frontend/repl/validate.go | 6 +- 11 files changed, 152 insertions(+), 47 deletions(-) create mode 100644 cmd/sysml/satisfy_label_test.go diff --git a/cmd/sysml/satisfy_label_test.go b/cmd/sysml/satisfy_label_test.go new file mode 100644 index 0000000000..73124d0fba --- /dev/null +++ b/cmd/sysml/satisfy_label_test.go @@ -0,0 +1,43 @@ +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 same indexed path -validate +// prints for it, so the two reports agree on which object a verdict is about. +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()) + } +} diff --git a/internal/exec/runtime/condition.go b/internal/exec/runtime/condition.go index 111851320a..346d99de99 100644 --- a/internal/exec/runtime/condition.go +++ b/internal/exec/runtime/condition.go @@ -1068,8 +1068,8 @@ 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 @@ -1077,7 +1077,7 @@ func (ctx *Context) reachCarriers(roots []*Instance, carries func(*Instance) boo 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,19 @@ 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 feature's +// name, indexed for a collection's 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 +1254,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 { @@ -1298,17 +1330,14 @@ 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. -func (ctx *Context) carrierFeatures(c carrier) []string { - if len(c.features) == 0 || c.instance == nil { +// carrierFeatures is the path to a nested carrier as a verdict labels it: the +// segments walked from its root, a collection's element indexed, spelled as a +// validation walk spells the object it reaches. +func carrierFeatures(c carrier) []string { + if 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) + return c.segments } // definitionOf is the definition objects of sym are objects of: sym itself when diff --git a/internal/exec/runtime/context.go b/internal/exec/runtime/context.go index 3ac58b312f..7f649ae8a2 100644 --- a/internal/exec/runtime/context.go +++ b/internal/exec/runtime/context.go @@ -1351,7 +1351,7 @@ func (ctx *Context) checkResultOf(holds bool, subject carrier) CheckResult { Holds: holds, Subject: subject.instance, SubjectRoot: subject.root, - SubjectPath: ctx.carrierFeatures(subject), + SubjectPath: carrierFeatures(subject), } } diff --git a/internal/exec/runtime/satisfy.go b/internal/exec/runtime/satisfy.go index f295a994ad..279cf257a6 100644 --- a/internal/exec/runtime/satisfy.go +++ b/internal/exec/runtime/satisfy.go @@ -464,7 +464,7 @@ func (ctx *Context) SatisfactionSubjects(a *SatisfyAssertion, roots []*Instance) carriers := ctx.carriersWhere(roots, func(inst *Instance) bool { return ctx.statedOf(a, inst) }) out := make([]SatisfactionSubject, 0, len(carriers)) for _, c := range carriers { - out = append(out, SatisfactionSubject{Object: c.instance, Root: c.root, Path: ctx.carrierFeatures(c)}) + out = append(out, SatisfactionSubject{Object: c.instance, Root: c.root, Path: carrierFeatures(c)}) } return out } diff --git a/internal/exec/runtime/validate.go b/internal/exec/runtime/validate.go index 296fb8e931..67dd7a7afc 100644 --- a/internal/exec/runtime/validate.go +++ b/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 } diff --git a/internal/frontend/grpc/validate.go b/internal/frontend/grpc/validate.go index 69de008864..67a75d7e27 100644 --- a/internal/frontend/grpc/validate.go +++ b/internal/frontend/grpc/validate.go @@ -83,13 +83,19 @@ func (v *verifyContext) objectVerdict(ov runtime.ObjectVerdict, plan analysis.Pl kind = verdictBinding } out := v.verdict(kind, ov.Element, ov.Text, ov.Subject, ov.Status == runtime.ValidationHolds, ov.Err, plan) - out.InstancePath = strings.Join(ov.Path, ".") + out.InstancePath = instancePath(ov.Path) if ov.Requirement != nil { out.RequirementId = namedFQN(v.cached.Index, ov.Requirement) } return out } +// instancePath spells on a verdict the path from the object a request named to +// the nested object the verdict is about, as the REPL labels it: `cheap[2]`. +func instancePath(path []string) string { + return strings.Join(path, ".") +} + // summaryVerdict is the verdict about the object as a whole: it holds when every // assertion holds and the walk was complete, and is undecided with the reason otherwise. func (v *verifyContext) summaryVerdict(symbolID string, root *runtime.Instance, report runtime.ValidationReport, plan analysis.Plan) *pb.Verdict { diff --git a/internal/frontend/grpc/verify.go b/internal/frontend/grpc/verify.go index c30058de55..1caf1ae6fc 100644 --- a/internal/frontend/grpc/verify.go +++ b/internal/frontend/grpc/verify.go @@ -612,6 +612,7 @@ func (v *verifyContext) satisfyVerdicts(ctx context.Context, a *runtime.SatisfyA } subject := subjectOf(result, inst) verdict := on.verdict(verdictSatisfy, a.Symbol, a.Text(), subject, result.Holds, err, plan) + verdict.InstancePath = instancePath(held.Path) on.associateRequirement(verdict, a) verdicts = append(verdicts, verdict) instances = append(instances, on.instanceGraph(subject)...) diff --git a/internal/frontend/repl/meta.go b/internal/frontend/repl/meta.go index 7f9be46b5d..223b130779 100644 --- a/internal/frontend/repl/meta.go +++ b/internal/frontend/repl/meta.go @@ -2613,7 +2613,7 @@ func (s *Session) satisfyVerdictsOf(ctx *runtime.Context, a *runtime.SatisfyAsse func (s *Session) subjectLabel(subject runtime.SatisfactionSubject) string { if subject.Root != nil && subject.Root != subject.Object { if root := s.instanceName(subject.Root); root != "" { - return root + featurePath(subject.Path) + return objectPath(root, subject.Path) } } return s.objectLabel(subject.Object) diff --git a/internal/frontend/repl/query.go b/internal/frontend/repl/query.go index 1a10017dd2..52f8340c3f 100644 --- a/internal/frontend/repl/query.go +++ b/internal/frontend/repl/query.go @@ -10,7 +10,6 @@ import ( "github.com/Open-MBEE/OpenSysML/internal/exec/objref" "github.com/Open-MBEE/OpenSysML/internal/exec/runtime" "github.com/Open-MBEE/OpenSysML/internal/semantic/symbols" - "github.com/Open-MBEE/OpenSysML/internal/syntax/source" ) // VerdictStatus is what a checked condition answered. @@ -416,18 +415,17 @@ func (s *Session) reportedSubject(result runtime.CheckResult, inst *runtime.Inst // rather than reported under the wrong one. return inst, owner } - return result.Subject, root + featurePath(result.SubjectPath) + return result.Subject, objectPath(root, result.SubjectPath) } -// featurePath spells walked feature names as a label's tail, each after a `.` -// and quoted where its spelling needs it: `engine`, `mount` → `.engine.mount`. -func featurePath(names []string) string { - var out strings.Builder - for _, name := range names { - out.WriteString(".") - out.WriteString(source.NameText(name)) +// objectPath labels an object nested in the one labelled root by the segments +// walked to it, as the runtime spells them: `fleet.cheap[2]`. Every verdict about +// a nested object — %validate's, %satisfy's, a check's — labels it this way. +func objectPath(root string, path []string) string { + if len(path) == 0 { + return root } - return out.String() + return root + "." + strings.Join(path, ".") } // instanceName is the label the session holds inst under — its name as the diff --git a/internal/frontend/repl/satisfy_stated_test.go b/internal/frontend/repl/satisfy_stated_test.go index 3d2ee164c6..ae4187d43f 100644 --- a/internal/frontend/repl/satisfy_stated_test.go +++ b/internal/frontend/repl/satisfy_stated_test.go @@ -91,3 +91,35 @@ func TestSatisfyStatedByADefinitionSweepsItsObjects(t *testing.T) { "✓ satisfy costReq holds (on ProductPkg::product ID: "+again+")", "✗ satisfy costReq fails (on ProductPkg::costly ID: "+costly+")") } + +// TestSatisfyLabelsObjectsAsValidateDoes checks that %satisfy names each object a +// definition's `satisfy r;` is decided on by the indexed path %validate prints for +// it — `fleet.cheap[2]`, not `fleet.cheap` — so the two reports agree on the object. +func TestSatisfyLabelsObjectsAsValidateDoes(t *testing.T) { + s := loadSource(t, `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; +}`) + run(t, s, "%instantiate fleet") + labels := []string{ + "✓ satisfy costReq holds (on test::fleet.cheap[1] ID: 2)", + "✓ satisfy costReq holds (on test::fleet.cheap[2] ID: 3)", + } + satisfied := run(t, s, "%satisfy") + wants(t, satisfied, labels...) + wants(t, run(t, s, "%validate fleet"), labels...) + if strings.Contains(satisfied, "fleet.cheap ID") { + t.Errorf("%%satisfy labels an object by its feature alone:\n%s", satisfied) + } +} diff --git a/internal/frontend/repl/validate.go b/internal/frontend/repl/validate.go index 9d94928dda..5b1d45f38f 100644 --- a/internal/frontend/repl/validate.go +++ b/internal/frontend/repl/validate.go @@ -2,7 +2,6 @@ package repl import ( "fmt" - "strings" "github.com/Open-MBEE/OpenSysML/internal/exec/analysis" "github.com/Open-MBEE/OpenSysML/internal/exec/runtime" @@ -54,10 +53,7 @@ func (s *Session) validateVerdicts(ref string) []Verdict { // objectVerdict renders one assertion's verdict about one object, named by the // path it was reached along from the validated object. func objectVerdict(v runtime.ObjectVerdict, label string) Verdict { - owner := label - if len(v.Path) > 0 { - owner = label + "." + strings.Join(v.Path, ".") - } + owner := objectPath(label, v.Path) subject := v.Text + " on " + owner condition := "Required condition" switch v.Kind { From 6abe008364eafe8f9bab6e59bd250ca35db0e09b 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:34:02 +0000 Subject: [PATCH 04/10] test(grpc): pin VerifyRequirement over the held population as a conformance case Co-Authored-By: jason.han --- .../grpc/held_population_verify_test.go | 2 +- tests/grpc/conformance_docquery_test.go | 10 +-- tests/grpc/conformance_test.go | 10 ++- tests/grpc/conformance_verify_test.go | 69 +++++++++++++++++++ tests/grpc/testdata/conformance/README.md | 6 +- ..._requirement_held_population.expected.json | 10 +++ .../verify_requirement_held_population.sysml | 19 +++++ ...verify_requirement_no_object.expected.json | 8 +++ .../verify_requirement_no_object.sysml | 19 +++++ 9 files changed, 139 insertions(+), 14 deletions(-) create mode 100644 tests/grpc/conformance_verify_test.go create mode 100644 tests/grpc/testdata/conformance/verify_requirement_held_population.expected.json create mode 100644 tests/grpc/testdata/conformance/verify_requirement_held_population.sysml create mode 100644 tests/grpc/testdata/conformance/verify_requirement_no_object.expected.json create mode 100644 tests/grpc/testdata/conformance/verify_requirement_no_object.sysml diff --git a/internal/frontend/grpc/held_population_verify_test.go b/internal/frontend/grpc/held_population_verify_test.go index 98c0d3059c..50971f97b7 100644 --- a/internal/frontend/grpc/held_population_verify_test.go +++ b/internal/frontend/grpc/held_population_verify_test.go @@ -131,7 +131,7 @@ func TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier(t *testing.T) { // TestRunAnalysisWithoutASubjectRunsOnTheHeldObject verifies that a case a // definition owns, run with no subject, is a feature of the one held object of -// the definition, is ambiguous over two, and asks for one when the model holds +// the definition, reports the ambiguity over two, and asks for one when the model // holds none — as the REPL's %analysis decides it. func TestRunAnalysisWithoutASubjectRunsOnTheHeldObject(t *testing.T) { srv := mustNewService(t, 10) diff --git a/tests/grpc/conformance_docquery_test.go b/tests/grpc/conformance_docquery_test.go index a234c930b4..ac94b31b50 100644 --- a/tests/grpc/conformance_docquery_test.go +++ b/tests/grpc/conformance_docquery_test.go @@ -31,15 +31,7 @@ type expectedRow struct { func runRunDocumentQueryCase(t *testing.T, srv *grpc.Service, ctx context.Context, modelHash string, tc conformanceCase) { t.Helper() - for _, sym := range tc.Instantiate { - resp, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: modelHash, SymbolId: sym}) - if err != nil { - t.Fatalf("Instantiate %s: %v", sym, err) - } - if resp.Error != "" { - t.Fatalf("Instantiate %s: %s", sym, resp.Error) - } - } + instantiateAll(t, srv, ctx, modelHash, tc.Instantiate) bindings := make([]*pb.DocumentQueryBinding, 0, len(tc.Bindings)) for _, b := range tc.Bindings { values := make([]*pb.DocumentValue, 0, len(b.Values)) diff --git a/tests/grpc/conformance_test.go b/tests/grpc/conformance_test.go index 6b65023569..bdfe0b6047 100644 --- a/tests/grpc/conformance_test.go +++ b/tests/grpc/conformance_test.go @@ -138,8 +138,12 @@ type conformanceCase struct { Question string `json:"question,omitempty"` ExpectedNotes []expectedNote `json:"expected_notes"` - // RunDocumentQuery: the symbols Instantiate creates objects of first, in - // order, then the query and its bindings. + // VerifyRequirement: the body verdicts the cases verifying the requirement + // must answer, in order, each about the object it ran on. + ExpectedVerificationVerdicts []expectedVerificationVerdict `json:"expected_verification_verdicts"` + + // RunDocumentQuery, VerifyRequirement: the symbols Instantiate creates objects + // of first, in order, so the request is about the objects the model holds. Instantiate []string `json:"instantiate,omitempty"` QueryID string `json:"query_id,omitempty"` Bindings []expectedBinding `json:"bindings,omitempty"` @@ -401,6 +405,8 @@ func runGRPCConformanceCase(t *testing.T, dir, caseName string) { runCheckBehaviorCase(t, srv, ctx, parseResp.ModelHash, tc) case "VerifyConstraint": runVerifyConstraintCase(t, srv, ctx, parseResp.ModelHash, tc) + case "VerifyRequirement": + runVerifyRequirementCase(t, srv, ctx, parseResp.ModelHash, tc) default: t.Fatalf("unknown rpc %q", tc.RPC) } diff --git a/tests/grpc/conformance_verify_test.go b/tests/grpc/conformance_verify_test.go new file mode 100644 index 0000000000..a9744d307d --- /dev/null +++ b/tests/grpc/conformance_verify_test.go @@ -0,0 +1,69 @@ +package grpc_test + +import ( + "context" + "testing" + + pb "github.com/Open-MBEE/OpenSysML/api/proto" + "github.com/Open-MBEE/OpenSysML/internal/frontend/grpc" +) + +// expectedVerificationVerdict is the fixture encoding of a pb.VerificationVerdict: +// the case, the verdict kind its body answered, the detail of one that decided +// nothing, and the type of the object it ran on (empty for a run on none). +type expectedVerificationVerdict struct { + Case string `json:"case"` + Kind string `json:"kind"` + Detail string `json:"detail"` + InstanceType string `json:"instance_type"` +} + +// runVerifyRequirementCase instantiates the case's objects, verifies the requirement +// about the subject named (none when empty) and compares the requirement's status +// with the body verdicts of the cases verifying it, each about its own object. +func runVerifyRequirementCase(t *testing.T, srv *grpc.Service, ctx context.Context, modelHash string, tc conformanceCase) { + t.Helper() + instantiateAll(t, srv, ctx, modelHash, tc.Instantiate) + + resp, err := srv.VerifyRequirement(ctx, &pb.VerifyRequirementRequest{ + ModelHash: modelHash, + SymbolId: tc.SymbolID, + SubjectSymbolId: tc.SubjectSymbolID, + }) + if err != nil { + t.Fatalf("VerifyRequirement: %v", err) + } + if checkExpectedError(t, tc, resp.Error) { + return + } + if resp.Verdict.Status != tc.ExpectedStatus { + t.Errorf("status = %q (%s), want %q", resp.Verdict.Status, resp.Verdict.Error, tc.ExpectedStatus) + } + if len(resp.VerificationVerdicts) != len(tc.ExpectedVerificationVerdicts) { + t.Fatalf("verification verdicts = %v, want %d", resp.VerificationVerdicts, len(tc.ExpectedVerificationVerdicts)) + } + for i, want := range tc.ExpectedVerificationVerdicts { + got := resp.VerificationVerdicts[i] + if got.CaseId != want.Case || got.Kind != want.Kind || got.Detail != want.Detail || got.InstanceTypeId != want.InstanceType { + t.Errorf("verification verdict %d = %v, want %+v", i, got, want) + } + if (got.InstanceId != 0) != (want.InstanceType != "") { + t.Errorf("verification verdict %d names object #%d, want an object: %v", i, got.InstanceId, want.InstanceType != "") + } + } +} + +// instantiateAll creates an object of each symbol named, in order, so the +// request that follows is about the objects the model holds. +func instantiateAll(t *testing.T, srv *grpc.Service, ctx context.Context, modelHash string, symbols []string) { + t.Helper() + for _, sym := range symbols { + resp, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: modelHash, SymbolId: sym}) + if err != nil { + t.Fatalf("Instantiate %s: %v", sym, err) + } + if resp.Error != "" { + t.Fatalf("Instantiate %s: %s", sym, resp.Error) + } + } +} diff --git a/tests/grpc/testdata/conformance/README.md b/tests/grpc/testdata/conformance/README.md index 43db94de17..5675b7f9d2 100644 --- a/tests/grpc/testdata/conformance/README.md +++ b/tests/grpc/testdata/conformance/README.md @@ -22,7 +22,7 @@ in this directory, so adding a case is a data-only change. | `expected_assignments` | ImportData | the assignments' descriptions over every import, in order; `expected_content` is the edited model, `expected_error` a refusal that leaves it unchanged | | `results`, `actions`, `runs`, `seed`, `observe` | CompareResults | the results index as JSON, the configurations selected, the runs per configuration, the seed and stored-name → feature pairs | | `expected_configurations` | CompareResults | per configuration in index order: `name`, `status`, `runs`, `completed`, `stored_runs`, `observables` (stored name → compared), `unresolved` and `lines_contain` | -| `rpc` | all | `GetSymbol`, `Evaluate`, `Instantiate`, `ExecuteAction`, `ExecuteState`, `ApplyEdits`, `RunDocumentQuery`, `EvaluateCalc`, `CheckBehavior` or `VerifyConstraint` | +| `rpc` | all | `GetSymbol`, `Evaluate`, `Instantiate`, `ExecuteAction`, `ExecuteState`, `ApplyEdits`, `RunDocumentQuery`, `EvaluateCalc`, `CheckBehavior`, `VerifyConstraint` or `VerifyRequirement` | | `rpc` | all | `GetSymbol`, `Evaluate`, `Instantiate`, `ExecuteAction`, `ExecuteState`, `GetDiagnostics`, `ApplyEdits`, `RunDocumentQuery` or `EvaluateCalc` | `ApplyEdits` sequence operations may carry the recursive action-body fields @@ -59,7 +59,9 @@ empty else blocks are not authorable. | `expected_status`, `expected_notes` | VerifyConstraint | the verdict's `status`, and the notes its answer rests on, in order: `kind` (`assumed_one` or `uncovered`), `subject`, `text` | | `query` | Query | the standard's `Query` as protojson writes it (`scope`, `select`, `where`, `orderBy`) | | `expected_element_ids`, `expected_query_error` | Query | the ids the answer reports, in order; or text the refusal's status message must contain | -| `instantiate` | RunDocumentQuery | FQNs `Instantiate` creates objects of first, in order, so the query can bind and enumerate them | +| `instantiate` | RunDocumentQuery, VerifyRequirement | FQNs `Instantiate` creates objects of first, in order, so the query can bind and enumerate them, or the verification is about the objects the model holds | +| `subject_symbol_id` | VerifyRequirement | optional FQN of the part/usage instantiated as the requirement's subject; absent, the requirement is checked over the objects the model holds, as the REPL's `%requirement` is over a session's | +| `expected_status`, `expected_verification_verdicts` | VerifyRequirement | the requirement verdict's `status`, and the body verdicts of the cases verifying it, in order: `case`, `kind`, `detail` (empty for a decided verdict) and `instance_type`, the type of the object the case ran on (empty for a run on none) | | `query_id` | RunDocumentQuery | FQN of the document query to run | | `bindings` | RunDocumentQuery | list of `{parameter, values}`, each value a document value bound to the parameter | | `expected_columns` | RunDocumentQuery | full ordered projected-column name list | diff --git a/tests/grpc/testdata/conformance/verify_requirement_held_population.expected.json b/tests/grpc/testdata/conformance/verify_requirement_held_population.expected.json new file mode 100644 index 0000000000..39a47a8e0d --- /dev/null +++ b/tests/grpc/testdata/conformance/verify_requirement_held_population.expected.json @@ -0,0 +1,10 @@ +{ + "rpc": "VerifyRequirement", + "instantiate": ["test::fleet"], + "symbol_id": "test::costReq", + "expected_status": "undecided", + "expected_verification_verdicts": [ + {"case": "test::Definition::costTest", "kind": "pass", "instance_type": "test::Fleet::cheap"}, + {"case": "test::Definition::costTest", "kind": "pass", "instance_type": "test::Fleet::cheap"} + ] +} diff --git a/tests/grpc/testdata/conformance/verify_requirement_held_population.sysml b/tests/grpc/testdata/conformance/verify_requirement_held_population.sysml new file mode 100644 index 0000000000..1dbd8a4774 --- /dev/null +++ b/tests/grpc/testdata/conformance/verify_requirement_held_population.sysml @@ -0,0 +1,19 @@ +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; + verification costTest { + objective costObjective { verify costReq; } + return verdict = VerificationCases::PassIf(costReq(this)); + } + } + part def Fleet { part cheap : Definition [2] { attribute :>> cost = 80.0; } } + part fleet : Fleet; +} diff --git a/tests/grpc/testdata/conformance/verify_requirement_no_object.expected.json b/tests/grpc/testdata/conformance/verify_requirement_no_object.expected.json new file mode 100644 index 0000000000..1ff861b280 --- /dev/null +++ b/tests/grpc/testdata/conformance/verify_requirement_no_object.expected.json @@ -0,0 +1,8 @@ +{ + "rpc": "VerifyRequirement", + "symbol_id": "test::costReq", + "expected_status": "undecided", + "expected_verification_verdicts": [ + {"case": "test::Definition::costTest", "kind": "inconclusive", "detail": "needs an object of test::Definition: none is instantiated"} + ] +} diff --git a/tests/grpc/testdata/conformance/verify_requirement_no_object.sysml b/tests/grpc/testdata/conformance/verify_requirement_no_object.sysml new file mode 100644 index 0000000000..1dbd8a4774 --- /dev/null +++ b/tests/grpc/testdata/conformance/verify_requirement_no_object.sysml @@ -0,0 +1,19 @@ +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; + verification costTest { + objective costObjective { verify costReq; } + return verdict = VerificationCases::PassIf(costReq(this)); + } + } + part def Fleet { part cheap : Definition [2] { attribute :>> cost = 80.0; } } + part fleet : Fleet; +} From be643d9b6fbcab5df3a34d9440ed9e9c1c21e1d6 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:34:04 +0000 Subject: [PATCH 05/10] docs: verification RPCs over the held population and the shared object label Co-Authored-By: jason.han --- .../unreleased/grpc-verify-held-population.fixed.md | 1 + .../satisfy-indexed-object-labels.fixed.md | 1 + docs/project/spec-compliance.md | 4 ++-- docs/reference/wire-contract.md | 13 +++++++++++++ 4 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 changes/unreleased/grpc-verify-held-population.fixed.md create mode 100644 changes/unreleased/satisfy-indexed-object-labels.fixed.md diff --git a/changes/unreleased/grpc-verify-held-population.fixed.md b/changes/unreleased/grpc-verify-held-population.fixed.md new file mode 100644 index 0000000000..88f8e06199 --- /dev/null +++ b/changes/unreleased/grpc-verify-held-population.fixed.md @@ -0,0 +1 @@ +- 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. diff --git a/changes/unreleased/satisfy-indexed-object-labels.fixed.md b/changes/unreleased/satisfy-indexed-object-labels.fixed.md new file mode 100644 index 0000000000..c88cef150e --- /dev/null +++ b/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`. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 6b36cbe5f0..3c7f1b4b84 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -415,7 +415,7 @@ in place of them: a failing verification body does not make a satisfied requirem | A verification case's objective checks the case's **subject**, not its verdict (§7.24.1: "the objective of a verification case is to verify that the verification subject satisfies one or more specific requirements"; `VerificationCases::VerificationCase::obj` redefines the objective's subject as the case's): the library redefines the objective with a bound, not defaulted, subject — `VerificationCases::VerificationCase::obj :>> Case::obj { subject subj = VerificationCase::subj; }` — and the runtime honours the redefining feature's stated value over the redefined `Case::obj`'s `default Case::result`, as a language rule rather than a verification one: the stated `VerificationCase::subj` is resolved to the run's subject binding through the redefinition index (`subj :>> Case::subj`, the usage's own `subject lander` redefining it). So an objective typed by a requirement def whose subject has another name (`subject lander : Lander` against the library's `subj`) evaluates that requirement against the verification subject with no binding of its own — whether the usage restates the subject without a value (`subject :>> subj;` ahead of its inputs, the shape the pilot accepts since a usage's owned parameters redefine its definition's by position) or leaves it to the library — an objective whose requirement declares no subject is decided the same way, `in limit = limit;` still binds the requirement's parameter, and the objective is decided (`satisfied`/`not satisfied`) beside the body's `pass`/`fail` on every surface — `-analysis`, `-requirement`, `-satisfy`, `%analysis`, `%requirement`, `%satisfy`, gRPC `RunAnalysis`/`VerifyRequirement` — and in every row of a `-sweep`. A requirement subject the verification subject cannot be is `undecided` naming both (`subject rover is bound to the case's subject (VerificationCases::VerificationCase::obj): type mismatch: Lander #1 (scout) is not a Rover`); a verification whose own subject nothing binds is the case's `subjectUnboundError` naming *that* subject; a usage restating the objective's subject (`objective : R { subject lander = other; }`, `subject = other;`, `subject :>> subj = other;`) is refused as overriding the library's fixed `=` value | `runtime/analysis_run.go` `Context.objectiveBindings`, `Context.unboundObjectiveSubject`, `Context.statedSubjectValue`, `Context.statedCaseMember`, `statedAsDefault`, `calcShape.memberRole`; `runtime/calc_usage.go` `Context.calcMemberNames` (redefined features indexed under the run's name), `calcShape.memberName`; `runtime/subsetting.go` `Context.redefinedFeatures`; `runtime/condition.go` `Context.conditionFeatures` (the effective feature values along the chain); `runtime/library_functions.go` `Context.libraryDeclared`; `passes/feature_value_overriding.go` (the `=` refusal) | conformance `verification_objective_subject` (+ `.trace.golden`), `verification_objective_subject_violated`, `verification_objective_subject_unstated`, `verification_objective_subject_unbound`, `analysis_objective_subject_default_over_case_subject`; `robustness_verification_test.go:verification_objective_subject_of_another_type`, `:verification_objective_subject_left_unbound`, `:verification_objective_subject_rebound`; `cmd/sysml/verification_test.go:TestVerificationObjectiveDecidesOnEverySurface`, `cmd/sysml/sweep_test.go:TestSweepVerificationThroughCLI`, `repl/verification_verdict_test.go:TestVerificationObjectiveDecidesAgainstTheCaseSubject`, `grpc/verification_verdict_test.go:TestRunAnalysisDecidesAVerificationObjectiveAgainstTheCaseSubject` | ✅ Faithful | | A body binding `verdict` (or its result) to a `VerdictKind` literal reports that literal, recognized by the enumeration the value belongs to rather than by the spelling of the name. The verdict is read from the case's result parameter only — the name it declares, the library's `verdict`, or an unnamed `result` — so an `out` parameter of the same enumeration is not mistaken for the case's answer | `runtime/verification_run.go` `Context.bodyVerdict`, `verdictOutputNames`, `Context.verdictOf`, `Context.isVerdictKind`, `verdictKindName`, `verdictOutputName`; `runtime/analysis_run.go` `calcRun.resultName` | `runtime/verification_verdict_test.go:TestVerificationBodyVerdicts` (`test::stated`, `test::aux`) | ⚠️ Tool-defined — reported as the library declares the literal | | A body that produces no verdict value — no `PassIf`, no `verdict` binding — is `inconclusive`, saying so, rather than defaulted to a pass or a fail | `runtime/verification_run.go` `Context.bodyVerdict` (`VerdictInconclusive`) | conformance `verification_verdict_inconclusive`, `runtime/verification_verdict_test.go:TestVerificationBodyVerdicts` (`test::silent`) | ⚠️ Tool-defined | -| A verification case a part definition owns is a feature of every object of that definition (§7.24; §7.6.3, a usage nested in a definition; the static side is the nested-definition feature accessibility rule): `-validate=`, `-requirement`, `-satisfy` and the gRPC `ValidateInstance`/`VerifyRequirement`/`VerifySatisfaction` run it once per object of the definition the check is about — every object the run holds for a check about none, the objects a multiplicity repeats (`part cheap : Definition [2]`, a `[0..*]` collection's members, a part nested inside a repeated part) each on their own, so the verdict count is the object count rather than the usage count — with that object as the one it reads its owner's features from, and name the object on the verdict; a `satisfy` without `by` a definition states is checked on the object of that definition the same way. With no object of the definition instantiated the case has nothing to be a feature of, so every surface sweeping it (`-satisfy`, `-requirement`, `-analysis` without an object, the gRPC and JSON surfaces) reports it `inconclusive` — the library's `VerdictKind` for a run that decided nothing, not `error`, nothing being wrong with the model — with the detail `needs an object of : none is instantiated` the definition's `satisfy` line uses; an analysis case a definition owns is refused with the same message (`ErrNeedsObject`). A case a part usage owns is unaffected: it reads the usage's bound values, as a usage's `satisfy` instantiates the usage | `runtime/verification_cases.go` `Context.VerificationVerdictsOn`, `Context.caseCarriers` over `condition.go` `Context.objectsUnder` (every object, where a check's `carriersUnder` keeps one per declaration); `runtime/verification_cases.go` `Context.verificationResultOn`; `runtime/satisfy.go` `Context.SatisfactionSubjects` (every object a type-stated `satisfy` sweeps); `runtime/analysis_run.go` `Context.casePerformer` (`ErrNeedsObject`); `runtime/verification_run.go` `Context.RunVerification`, `VerificationVerdict.Subject`; `runtime/satisfy.go` `Context.CheckSatisfactionOn`; `repl/verification.go` `Session.withVerifications`, `verificationLine`; `grpc/verify.go` `verifyContext.requirementVerifications` | conformance `verification_definition_owned`, `verification_definition_owned_fail`, `verification_definition_owned_no_object`, `analysis_definition_owned_no_object`; `runtime/definition_owned_case_test.go`, `runtime/robustness_definition_owned_case_test.go`; `repl/definition_owned_case_test.go`; `grpc/definition_owned_case_test.go`; `cmd/sysml/verification_test.go:TestRunVerificationOnADefinitionOwnedCase`; conformance `validation_verification_definition_owned` (`_fail`, `_satisfy_holds_verification_fails`, `_satisfy_fails_verification_passes`, `_subject_owner_bound`, `_subject_unbound`), each satisfaction verdict pinned beside the verification runs of its requirement, and `cmd/sysml/verification_test.go:TestValidateAgreesWithConformanceFixtures` holding `-validate` to the same verdicts; conformance `requirement_verification_repeated_subjects` (`[2]` twice, two passing and two failing), `requirement_verification_open_multiplicity_subjects` (an empty `[0..*]` gives no run, a subset one a run per member), `requirement_verification_nested_repeated_subjects` (a bolt in each of four wheels), pinned about no object as `-requirement` reports them, `cmd/sysml/verification_test.go:TestRequirementAgreesWithConformanceFixtures` holding `-requirement` to the same runs, `robustness_verification_test.go:testVerificationRunsOncePerRepeatedObject`, `grpc/definition_owned_case_test.go:TestVerifyRunsADefinitionOwnedCaseOnEveryRepeatedObject` | ✅ Faithful | +| A verification case a part definition owns is a feature of every object of that definition (§7.24; §7.6.3, a usage nested in a definition; the static side is the nested-definition feature accessibility rule): `-validate=`, `-requirement`, `-satisfy` and the gRPC `ValidateInstance`/`VerifyRequirement`/`VerifySatisfaction` run it once per object of the definition the check is about — every object the run holds for a check about none (the gRPC `VerifyConstraint`, `VerifyRequirement` and `RunAnalysis` naming no `subject_symbol_id` evaluate over the population `Instantiate` holds for the model, under its lock, as `VerifySatisfaction` does and as a REPL check is about the objects the session holds: a type-owned constraint is checked on the held object carrying it, a case a definition owns runs as a feature of the held object of that definition, and a sweep that would pass the held-objects bound is `RESOURCE_EXHAUSTED` as `Instantiate` is; a named subject keeps a worker of its own), the objects a multiplicity repeats (`part cheap : Definition [2]`, a `[0..*]` collection's members, a part nested inside a repeated part) each on their own, so the verdict count is the object count rather than the usage count — with that object as the one it reads its owner's features from, and name the object on the verdict; a `satisfy` without `by` a definition states is checked on the object of that definition the same way. With no object of the definition instantiated the case has nothing to be a feature of, so every surface sweeping it (`-satisfy`, `-requirement`, `-analysis` without an object, the gRPC and JSON surfaces) reports it `inconclusive` — the library's `VerdictKind` for a run that decided nothing, not `error`, nothing being wrong with the model — with the detail `needs an object of : none is instantiated` the definition's `satisfy` line uses; an analysis case a definition owns is refused with the same message (`ErrNeedsObject`). A case a part usage owns is unaffected: it reads the usage's bound values, as a usage's `satisfy` instantiates the usage | `runtime/verification_cases.go` `Context.VerificationVerdictsOn`, `Context.caseCarriers` over `condition.go` `Context.objectsUnder`; `grpc/verify.go` `verifyContext.overHeld`, `verifyContext.requirementVerificationRuns` (`VerificationVerdict.Err` classifies the bound), `grpc/analysis.go` `verifyContext.scheduled` (every object, where a check's `carriersUnder` keeps one per declaration); `runtime/verification_cases.go` `Context.verificationResultOn`; `runtime/satisfy.go` `Context.SatisfactionSubjects` (every object a type-stated `satisfy` sweeps); `runtime/analysis_run.go` `Context.casePerformer` (`ErrNeedsObject`); `runtime/verification_run.go` `Context.RunVerification`, `VerificationVerdict.Subject`; `runtime/satisfy.go` `Context.CheckSatisfactionOn`; `repl/verification.go` `Session.withVerifications`, `verificationLine`; `grpc/verify.go` `verifyContext.requirementVerifications` | conformance `verification_definition_owned`, `verification_definition_owned_fail`, `verification_definition_owned_no_object`, `analysis_definition_owned_no_object`; `runtime/definition_owned_case_test.go`, `runtime/robustness_definition_owned_case_test.go`; `repl/definition_owned_case_test.go`; `grpc/definition_owned_case_test.go`, `grpc/held_population_verify_test.go`, `grpc/robustness_held_population_test.go:TestGRPCRobustnessHeldPopulation`, gRPC conformance `verify_requirement_held_population`, `verify_requirement_no_object`; `cmd/sysml/verification_test.go:TestRunVerificationOnADefinitionOwnedCase`; conformance `validation_verification_definition_owned` (`_fail`, `_satisfy_holds_verification_fails`, `_satisfy_fails_verification_passes`, `_subject_owner_bound`, `_subject_unbound`), each satisfaction verdict pinned beside the verification runs of its requirement, and `cmd/sysml/verification_test.go:TestValidateAgreesWithConformanceFixtures` holding `-validate` to the same verdicts; conformance `requirement_verification_repeated_subjects` (`[2]` twice, two passing and two failing), `requirement_verification_open_multiplicity_subjects` (an empty `[0..*]` gives no run, a subset one a run per member), `requirement_verification_nested_repeated_subjects` (a bolt in each of four wheels), pinned about no object as `-requirement` reports them, `cmd/sysml/verification_test.go:TestRequirementAgreesWithConformanceFixtures` holding `-requirement` to the same runs, `robustness_verification_test.go:testVerificationRunsOncePerRepeatedObject`, `grpc/definition_owned_case_test.go:TestVerifyRunsADefinitionOwnedCaseOnEveryRepeatedObject` | ✅ Faithful | | A body whose run fails with a typed error — an unbound subject, a failing step, a feature holding no value — is `error` carrying that error's own text, and the failure is a verdict rather than a refused request; a malformed *request* (a symbol of the wrong kind, an unknown named argument) stays a typed error from the call | `runtime/verification_run.go` `Context.RunVerification`, `badRequest`; `runtime/errors.go` `subjectUnboundError` (kind `verification`) | conformance `verification_verdict_error`, `robustness_verification_test.go:verification_body_that_cannot_run`, `:verification_body_step_that_fails`, `runtime/verification_verdict_test.go:TestVerificationBodyVerdicts` | ⚠️ Tool-defined | | A verification case performed as a step of another (`verification sub : Case;`, the library's `subVerificationCases :> subcases`) has its own verdict read from the step's performance and is reported **on its own**, marked as a subcase: the library declares the containment but states no roll-up rule — no calculation combining subcase verdicts into the parent's — so none is invented: a parent whose body binds no verdict of its own stays `inconclusive` beside its subcases' verdicts, and a parent whose own body passes still reports and exits as a pass beside a subcase that failed. A subcase the run did not perform — the case on the branch a decision did not select — answered nothing and is reported by neither, rather than being reported as an `error`. A subcase that could not run at all is a step that failed, which ends the performing case's run as any failed step does: that case's verdict is the `error` naming the subcase and the reason, and no verdict is reported for a body that did not finish | `runtime/verification_run.go` `Context.subcaseVerdicts`, `Context.subcaseVerdict`, `verdictOutputNames`; `runtime/case_step.go` `performances.performCase`; `VerificationVerdict.Subcase` | conformance `verification_verdict_subcases`, `verification_verdict_subcase_branch`, `runtime/verification_verdict_test.go:TestVerificationSubcaseVerdictsAreReportedOnTheirOwn`, `runtime/robustness_verification_test.go:verification_subcase_that_cannot_run`, `repl/verification_verdict_test.go:TestAnalysisKeepsACaseStatusApartFromItsSubcases` | ⚠️ Tool-defined — reported individually, with the reason stated here | | An objective stating only `verify r;` is `satisfied`, and the case is decided by its body's verdict alone: the objective is a `RequirementUsage` whose result is `allTrue(assumptions()) implies allTrue(constraints())` (`Requirements::RequirementConstraintCheck`), `verify` is a `RequirementVerificationMembership` naming a `verifiedRequirement` and no constraint of the objective, and the library's `VerificationCase::obj::requirementVerifications :> subrequirements` binds no value, so a check over no constraints is true; `-analysis` exits 0 for a passing body and 1 for a failing one, while an objective whose own condition cannot be evaluated stays `undecided` and the case unresolved | `runtime/analysis_run.go` `Context.analysisVerdict` | `verification_objective_verify_only.sysml`, `verification_objective_verify_only_fail.sysml`, `runtime/verification_verdict_test.go:TestVerifyOnlyObjectiveIsSatisfiedAndNoSatisfaction`, `repl/verify_only_objective_test.go:TestVerifyOnlyObjectiveIsDecidedByTheBody`, `cmd/sysml/verify_only_objective_test.go:TestVerifyOnlyObjectiveExitsByTheBodyVerdict`, `analysis_objective_undecided.sysml` (the undecided case kept), `analysis_objective_bare.sysml` (a bare `objective obj;` in an analysis case is `satisfied` by the same rule) | ✅ Faithful — the library's own result over no constraints | @@ -745,7 +745,7 @@ remain one-shot. | `validateAssertConstraintUsageReference` (`Must reference a constraint.`, SysML v2 §8.3.20.2 `AssertConstraintUsage`): `assert c`, `assert not c` and `assert constraint c` reference a constraint usage — a requirement usage included — the last feature of a feature chain deciding, an inherited constraint accepted, the reference stated as a usage or as a member of a constraint body alike; a definition, a package or an unresolved name is the earlier tier's error | `passes/typecheck.go` `referenceKindMessage` (the referent-kind query `satisfy` and `assert` share), `checkChainReferenceKind` for a chained referent, `checkBehaviorMember` for a constraint-body member | `passes/typecheck_assert_reference_test.go`; `semantic/s04-assert-references-non-constraint.sysml` is rejected by both tools | ✅ Faithful | | `validateAssignmentActionUsageReferent` (`An assignment must have a referent.`, SysML v2 §8.3.17.5 `AssignmentActionUsage::referent`): the target of `assign x := v` names a feature; a definition, a package, a datatype or another namespace is rejected with what it is declared as, an unresolved target stays the name-resolution error, and only a feature reaches the time-varying rule | `passes/w8d_assignment_referent.go` `assignmentReferentChecker.check` over `symbols.SymbolKind.IsFeature` | `passes/w8d_assignment_referent_test.go` (`TestAssignmentReferentNonFeatureRejected`, `TestAssignmentReferentFeatureOrUnresolvedIsNotReported`); `semantic/s43-assign-to-non-feature.sysml` is rejected by both tools | ✅ Faithful | | `assert satisfy by ;` is a verdict of its own: the assertion is evaluated as the requirement usage it is (`SatisfyRequirementUsage`, SysML v2 §8.3.21.10), with the requirement's subject parameter bound to the object the `by` feature supplies, so the conditions read that object's values; that object is held to the subject's declaration as an expression-bound one is (KerML §7.3.4.1) — classified by the subject's type (a `Ship` for a `Tanker` subject answers `t.cargo`), refused as a `type mismatch` where the type cannot hold it, or as a `multiplicity violation` where one object is too few (`Ship[2]`) | `runtime/satisfy.go` `SatisfyAssertionsIn`, `evaluateSatisfactionOn`; `runtime/context.go` `memberBindings`, `holdBound`; `repl/meta.go` `doSatisfy` | `satisfy_subject_binding.sysml`, `satisfy_inherited_conditions.sysml`, `satisfy_subject_classified.sysml`, `satisfy_subject_refused.sysml`, `runtime/satisfy_test.go`, `runtime/analysis_objective_binding_test.go:TestSuppliedSubjectIsHeldToItsDeclaration`, `repl/satisfy_test.go:TestSatisfyVerdicts` | ✅ Faithful | -| A `satisfy r;` stating no `by` is about the objects of the type stating it — the owner is the satisfying feature (SysML v2 §7.20.1), so a definition's assertion is decided once per object of that definition the session or the service holds, nested ones included, as `-validate=` decides it; a usage's instantiates the usage, as `by p` instantiates `p`; a definition's with no object asks for one (`needs an object of DefinitionPkg::Definition`, gRPC `no subject … an object of … is needed`) rather than reading the requirement's subject from nothing; with one object held the runtime answers about it by the subject rule, with several it is ambiguous. An objective's `verify r;` is a `RequirementVerificationMembership`, not a `SatisfyRequirementUsage`, so no satisfaction surface reports it (the verification surfaces do) | `runtime/satisfy.go` `SatisfyAssertion.StatingType`, `Context.SatisfactionSubjects`, `Context.SatisfySubject`, `Context.CheckSatisfactionOn` (the subject rule via `checkSubject`), `satisfyAssertionOf` (`Usage.IsVerifiedRequirement`); `repl/meta.go` `Session.satisfyVerdictsOf`, `Session.satisfyNeedsObject`; `grpc/verify.go` `verifyContext.satisfyVerdicts` (over the `Instantiate` population), `grpc/objects.go` `Service.heldObjects` | `satisfy_stated_by_definition.sysml`, `satisfy_stated_by_usage.sysml`, `satisfy_stated_by_usage_violated.sysml`, `satisfy_excludes_verify.sysml`, `runtime/satisfy_test.go:TestSatisfactionStatedByADefinitionIsAboutItsObjects`, `:TestSatisfactionStatedByAUsageIsAboutItsOwnObject`, `repl/satisfy_stated_test.go`, `grpc/satisfy_stated_test.go`, `cmd/sysml/satisfy_stated_test.go:TestSatisfyStatedByADefinition` | ✅ Faithful | +| A `satisfy r;` stating no `by` is about the objects of the type stating it — the owner is the satisfying feature (SysML v2 §7.20.1), so a definition's assertion is decided once per object of that definition the session or the service holds, nested ones included, as `-validate=` decides it; a usage's instantiates the usage, as `by p` instantiates `p`; a definition's with no object asks for one (`needs an object of DefinitionPkg::Definition`, gRPC `no subject … an object of … is needed`) rather than reading the requirement's subject from nothing; with one object held the runtime answers about it by the subject rule, with several it is ambiguous. An objective's `verify r;` is a `RequirementVerificationMembership`, not a `SatisfyRequirementUsage`, so no satisfaction surface reports it (the verification surfaces do) | `runtime/satisfy.go` `SatisfyAssertion.StatingType`, `Context.SatisfactionSubjects`, `Context.SatisfySubject`, `Context.CheckSatisfactionOn` (the subject rule via `checkSubject`), `satisfyAssertionOf` (`Usage.IsVerifiedRequirement`); `repl/meta.go` `Session.satisfyVerdictsOf`, `Session.satisfyNeedsObject`; `grpc/verify.go` `verifyContext.satisfyVerdicts` (over the `Instantiate` population), `grpc/objects.go` `Service.heldObjects`; every surface labels the object a type's assertion is decided on by the path `-validate=` prints for it, a collection's element indexed (`fleet.cheap[2]`): `condition.go` `heldSegments`, `indexedSegment`, `carrierFeatures` (the one spelling the validation walk's `heldChildren` shares), `repl/query.go` `objectPath`, `grpc/validate.go` `instancePath` | `satisfy_stated_by_definition.sysml`, `satisfy_stated_by_usage.sysml`, `satisfy_stated_by_usage_violated.sysml`, `satisfy_excludes_verify.sysml`, `runtime/satisfy_test.go:TestSatisfactionStatedByADefinitionIsAboutItsObjects`, `:TestSatisfactionStatedByAUsageIsAboutItsOwnObject`, `repl/satisfy_stated_test.go` (`TestSatisfyLabelsObjectsAsValidateDoes`), `grpc/satisfy_stated_test.go`, `cmd/sysml/satisfy_stated_test.go:TestSatisfyStatedByADefinition`, `cmd/sysml/satisfy_label_test.go` | ✅ Faithful | | An assertion may be negated (`assert not constraint { … }`, `assert not satisfy … by …`; `Invariant::isNegated`, SysML v2 §8.3.21.10), and holds exactly when the conditions it denies do not | `ast/defusage.go` `Usage.IsNegated`, `parser/defusage.go` `applyFeatureMods`, `runtime/condition.go` `evaluateConditions` | `tests/parser/testdata/parse/assert_negated.golden`, `satisfy_negated.sysml`, `runtime/negation_test.go` | ✅ Faithful | | A negated constraint states no condition it can deny when its body holds only assumptions, which are trusted rather than checked, so nothing binds its result and it reports no value (`constraint cneg: no value: the constraint declares no required condition, only assumptions`) rather than a violation naming none; the solver refuses its denial the same (`unboundConstraintResult`) | `runtime/condition.go` `evaluateConditions`, `conditionCheck.noResultValue`; `solve/translate.go` `unboundConstraintResult`, `translator.translate` | `runtime/condition_test.go` `TestNegatedConstraintWithOnlyAssumptionsIsNotAVerdict` | ✅ Faithful | | A negation denies the conditions of the constraint it is written on **together** — `not (a and b)`, not `not a and not b` — so it holds as soon as one of them fails | `runtime/condition.go` `appendConditions`, `conditionHolds` | `runtime/condition_test.go` `TestNegatedNestedConstraintNegatesTheConjunction`, `constraint_negated_group.sysml` | ✅ Faithful | diff --git a/docs/reference/wire-contract.md b/docs/reference/wire-contract.md index d46cc3efbb..430028aeee 100644 --- a/docs/reference/wire-contract.md +++ b/docs/reference/wire-contract.md @@ -1745,6 +1745,19 @@ 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, as the REPL answers), 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 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 From b47ba1621720e6fc3b457ec36e9282d9175862e4 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:51:03 +0000 Subject: [PATCH 06/10] fix(runtime): a carrier's label keeps the declaration a subsetting collection gathers The indexed path ends in the declaration the object materializes where it differs from the feature holding it, as carrierLabels names it; a repeated part keeps its indexed segment. Co-Authored-By: jason.han --- internal/exec/runtime/condition.go | 36 ++++++++++++++++++++++-------- internal/exec/runtime/context.go | 2 +- internal/exec/runtime/satisfy.go | 2 +- 3 files changed, 29 insertions(+), 11 deletions(-) diff --git a/internal/exec/runtime/condition.go b/internal/exec/runtime/condition.go index 346d99de99..5af31e8cd0 100644 --- a/internal/exec/runtime/condition.go +++ b/internal/exec/runtime/condition.go @@ -1309,14 +1309,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 @@ -1331,13 +1337,25 @@ func carrierPath(c carrier, definition string) []string { } // carrierFeatures is the path to a nested carrier as a verdict labels it: the -// segments walked from its root, a collection's element indexed, spelled as a -// validation walk spells the object it reaches. -func carrierFeatures(c carrier) []string { - if c.instance == nil { +// segments walked from its root, a collection's element indexed as a validation +// walk spells the object it reaches, ending in the declaration the carrier +// materializes where a collection gathers objects of several declarations, as +// carrierLabels names it. +func (ctx *Context) carrierFeatures(c carrier) []string { + if len(c.segments) == 0 || c.instance == nil { return nil } - return c.segments + name := "object" + if def := ctx.definitionOf(c.instance.Type); def != nil && def.Name != "" { + name = def.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 diff --git a/internal/exec/runtime/context.go b/internal/exec/runtime/context.go index 7f649ae8a2..3ac58b312f 100644 --- a/internal/exec/runtime/context.go +++ b/internal/exec/runtime/context.go @@ -1351,7 +1351,7 @@ func (ctx *Context) checkResultOf(holds bool, subject carrier) CheckResult { Holds: holds, Subject: subject.instance, SubjectRoot: subject.root, - SubjectPath: carrierFeatures(subject), + SubjectPath: ctx.carrierFeatures(subject), } } diff --git a/internal/exec/runtime/satisfy.go b/internal/exec/runtime/satisfy.go index 279cf257a6..f295a994ad 100644 --- a/internal/exec/runtime/satisfy.go +++ b/internal/exec/runtime/satisfy.go @@ -464,7 +464,7 @@ func (ctx *Context) SatisfactionSubjects(a *SatisfyAssertion, roots []*Instance) carriers := ctx.carriersWhere(roots, func(inst *Instance) bool { return ctx.statedOf(a, inst) }) out := make([]SatisfactionSubject, 0, len(carriers)) for _, c := range carriers { - out = append(out, SatisfactionSubject{Object: c.instance, Root: c.root, Path: carrierFeatures(c)}) + out = append(out, SatisfactionSubject{Object: c.instance, Root: c.root, Path: ctx.carrierFeatures(c)}) } return out } From 07ceba24440f5c342a976f2120de7a91e5ee355d Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 28 Oct 2026 04:59:16 +0000 Subject: [PATCH 07/10] fix(grpc): RunAnalysis of a held verification case at the bound is RESOURCE_EXHAUSTED A verification case run reports its own failure in the verdict rather than the call's error, so a run over the held population that passed the held-objects bound answered an error verdict; exhaustedRun reads the verdicts' errors as the call's, as the requirement sweep already did. Co-Authored-By: jason.han --- internal/frontend/grpc/analysis.go | 17 ++++++++++++++++- .../grpc/robustness_held_population_test.go | 4 ++++ 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/internal/frontend/grpc/analysis.go b/internal/frontend/grpc/analysis.go index 3b4a35cbd5..5e83fee97f 100644 --- a/internal/frontend/grpc/analysis.go +++ b/internal/frontend/grpc/analysis.go @@ -74,12 +74,27 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) ( if gone := callerGone(ctx, err); gone != nil { return nil, gone } - if status := v.exhausted(err); status != nil { + 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 run over the held population +// that would pass its bound, whether the call failed of it or a verification case's +// verdict carries the failure, as a case run reports its own; 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 a request leaves the held population's runtime as it // found it; a policy the runtime cannot be set to is the error. diff --git a/internal/frontend/grpc/robustness_held_population_test.go b/internal/frontend/grpc/robustness_held_population_test.go index 082d3c5200..5d99f6e6d8 100644 --- a/internal/frontend/grpc/robustness_held_population_test.go +++ b/internal/frontend/grpc/robustness_held_population_test.go @@ -39,6 +39,10 @@ func TestGRPCRobustnessHeldPopulation(t *testing.T) { _, err := srv.VerifyRequirement(ctx, &pb.VerifyRequirementRequest{ModelHash: hash, SymbolId: "test::costReq"}) exhausted(t, "VerifyRequirement", err) }) + t.Run("case run at the bound", func(t *testing.T) { + _, err := srv.RunAnalysis(ctx, &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: "test::Definition::costTest"}) + exhausted(t, "RunAnalysis", err) + }) t.Run("satisfaction sweep at the bound", func(t *testing.T) { _, err := srv.VerifySatisfaction(ctx, &pb.VerifySatisfactionRequest{ModelHash: hash}) exhausted(t, "VerifySatisfaction", err) From c1ab124e2a12c2a2470de61e62a53970e63bc588 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 28 Oct 2026 04:59:16 +0000 Subject: [PATCH 08/10] fix(grpc): a tool dry run leaves the runtime as it found it The preview's writes are restored from a snapshot and the runner the runtime had goes back on, as the REPL's preview does; over the held population both outlived the request. Co-Authored-By: jason.han --- .../grpc/held_population_preview_test.go | 66 +++++++++++++++++++ internal/frontend/grpc/tooldryrun.go | 17 +++-- 2 files changed, 79 insertions(+), 4 deletions(-) create mode 100644 internal/frontend/grpc/held_population_preview_test.go diff --git a/internal/frontend/grpc/held_population_preview_test.go b/internal/frontend/grpc/held_population_preview_test.go new file mode 100644 index 0000000000..270d68cf8c --- /dev/null +++ b/internal/frontend/grpc/held_population_preview_test.go @@ -0,0 +1,66 @@ +package grpc + +import ( + "context" + "fmt" + "slices" + "testing" + + pb "github.com/Open-MBEE/OpenSysML/api/proto" + "github.com/Open-MBEE/OpenSysML/internal/exec/analysis" +) + +// TestToolPreviewLeavesTheHeldPopulationAsItWas verifies that a tool dry run of a +// case naming no subject, made over the held population, leaves it as it found it: +// the objects the preview materialized are gone with it, and the runner the +// population's runtime had is back on it rather than the preview's. +func TestToolPreviewLeavesTheHeldPopulationAsItWas(t *testing.T) { + srv := mustNewService(t, 10) + hash := mustVerifyModel(t, srv, heldPopulationModel, "held-population-preview") + ctx := context.Background() + if made, err := srv.Instantiate(ctx, &pb.InstantiateRequest{ModelHash: hash, SymbolId: "test::fleet"}); err != nil || made.Error != "" { + t.Fatalf("Instantiate(test::fleet): %v %q", err, made.GetError()) + } + cached, _ := srv.cache.Get(hash) + rt := srv.objects(cached).rt + plain := &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: "test::Definition::costTest"} + first, err := srv.RunAnalysis(ctx, plain) + if err != nil || first.Error != "" { + t.Fatalf("RunAnalysis before the preview: %v %q", err, first.GetError()) + } + // A run keeps the performance it made, as the REPL's does; a preview keeps nothing. + before := rt.InstanceCount() + + resp, err := srv.RunAnalysis(ctx, &pb.RunAnalysisRequest{ModelHash: hash, SymbolId: "test::Definition::costTest", ToolDryRun: true}) + if err != nil { + t.Fatalf("RunAnalysis tool dry run: %v", err) + } + if resp.Error != msgNoToolReached { + t.Errorf("preview of a case calling no tool reported %q, want %q", resp.Error, msgNoToolReached) + } + if got := rt.InstanceCount(); got != before { + t.Errorf("held after the preview = %d objects, want the %d held before it", got, before) + } + if _, dry := rt.ToolRunner().(*analysis.DryRunner); dry { + t.Error("the preview's dry runner is still on the held population's runtime") + } + + // The run after the preview is the run before it: a run, not a preview, on the same objects. + run, err := srv.RunAnalysis(ctx, plain) + if err != nil { + t.Fatalf("RunAnalysis after the preview: %v", err) + } + if run.Error != "" || run.ToolDryRun != nil { + t.Errorf("run after the preview reported %q with preview %v, want a run of the case", run.Error, run.ToolDryRun) + } + spell := func(verdicts []*pb.VerificationVerdict) []string { + out := make([]string, len(verdicts)) + for i, v := range verdicts { + out[i] = fmt.Sprintf("%s=%s on #%d", v.CaseId, v.Kind, v.InstanceId) + } + return out + } + if got, want := spell(run.VerificationVerdicts), spell(first.VerificationVerdicts); !slices.Equal(got, want) { + t.Errorf("run after the preview = %v, want the run before it, %v", got, want) + } +} diff --git a/internal/frontend/grpc/tooldryrun.go b/internal/frontend/grpc/tooldryrun.go index 5ea441b11e..b6ff5f4248 100644 --- a/internal/frontend/grpc/tooldryrun.go +++ b/internal/frontend/grpc/tooldryrun.go @@ -4,6 +4,8 @@ import ( "context" "errors" + "connectrpc.com/connect" + pb "github.com/Open-MBEE/OpenSysML/api/proto" "github.com/Open-MBEE/OpenSysML/internal/exec/analysis" "github.com/Open-MBEE/OpenSysML/internal/exec/runtime" @@ -18,12 +20,19 @@ const msgNoToolReached = "no ToolExecution-annotated action was reached; nothing // The run's own results are not kept, so the response carries the preview, the // run's notes and, where the run failed otherwise, its error. func (s *Service) toolDryRun(ctx context.Context, v *verifyContext, sym *symbols.Symbol, args runtime.AnalysisArgs) (*pb.RunAnalysisResponse, error) { - // The preview runs on the request's own runtime, as the REPL's does: the - // dry runner is set on that context, and an engine's run of its own would - // not see it. + // The preview runs on the request's runtime, as the REPL's does, and leaves + // nothing of it there: its writes are restored from a snapshot and the runner + // the runtime had goes back on, since over the held population both outlive it. + snap, err := v.runtime.Snapshot() + if err != nil { + return nil, statusError(connect.CodeInternal, err.Error()) + } + defer func() { snap.Restore(); snap.Release() }() + prior := v.runtime.ToolRunner() runner := s.engines.DryRunner(v.engine) v.runtime.SetToolRunner(runner) - _, err := v.runCaseOn(sym, args) + defer v.runtime.SetToolRunner(prior) + _, err = v.runCaseOn(sym, args) if gone := callerGone(ctx, err); gone != nil { return nil, gone } From d88a0cac8dd76c3d1c9fd903bf52fe68fe0b8861 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 28 Oct 2026 04:59:16 +0000 Subject: [PATCH 09/10] docs: tool previews and the explore schedule over the held population Co-Authored-By: jason.han --- changes/unreleased/grpc-verify-held-population.fixed.md | 1 + docs/project/spec-compliance.md | 2 +- docs/reference/wire-contract.md | 8 ++++++-- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/changes/unreleased/grpc-verify-held-population.fixed.md b/changes/unreleased/grpc-verify-held-population.fixed.md index 88f8e06199..96a6a3c537 100644 --- a/changes/unreleased/grpc-verify-held-population.fixed.md +++ b/changes/unreleased/grpc-verify-held-population.fixed.md @@ -1 +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. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 3c7f1b4b84..b18b5f66a8 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -415,7 +415,7 @@ in place of them: a failing verification body does not make a satisfied requirem | A verification case's objective checks the case's **subject**, not its verdict (§7.24.1: "the objective of a verification case is to verify that the verification subject satisfies one or more specific requirements"; `VerificationCases::VerificationCase::obj` redefines the objective's subject as the case's): the library redefines the objective with a bound, not defaulted, subject — `VerificationCases::VerificationCase::obj :>> Case::obj { subject subj = VerificationCase::subj; }` — and the runtime honours the redefining feature's stated value over the redefined `Case::obj`'s `default Case::result`, as a language rule rather than a verification one: the stated `VerificationCase::subj` is resolved to the run's subject binding through the redefinition index (`subj :>> Case::subj`, the usage's own `subject lander` redefining it). So an objective typed by a requirement def whose subject has another name (`subject lander : Lander` against the library's `subj`) evaluates that requirement against the verification subject with no binding of its own — whether the usage restates the subject without a value (`subject :>> subj;` ahead of its inputs, the shape the pilot accepts since a usage's owned parameters redefine its definition's by position) or leaves it to the library — an objective whose requirement declares no subject is decided the same way, `in limit = limit;` still binds the requirement's parameter, and the objective is decided (`satisfied`/`not satisfied`) beside the body's `pass`/`fail` on every surface — `-analysis`, `-requirement`, `-satisfy`, `%analysis`, `%requirement`, `%satisfy`, gRPC `RunAnalysis`/`VerifyRequirement` — and in every row of a `-sweep`. A requirement subject the verification subject cannot be is `undecided` naming both (`subject rover is bound to the case's subject (VerificationCases::VerificationCase::obj): type mismatch: Lander #1 (scout) is not a Rover`); a verification whose own subject nothing binds is the case's `subjectUnboundError` naming *that* subject; a usage restating the objective's subject (`objective : R { subject lander = other; }`, `subject = other;`, `subject :>> subj = other;`) is refused as overriding the library's fixed `=` value | `runtime/analysis_run.go` `Context.objectiveBindings`, `Context.unboundObjectiveSubject`, `Context.statedSubjectValue`, `Context.statedCaseMember`, `statedAsDefault`, `calcShape.memberRole`; `runtime/calc_usage.go` `Context.calcMemberNames` (redefined features indexed under the run's name), `calcShape.memberName`; `runtime/subsetting.go` `Context.redefinedFeatures`; `runtime/condition.go` `Context.conditionFeatures` (the effective feature values along the chain); `runtime/library_functions.go` `Context.libraryDeclared`; `passes/feature_value_overriding.go` (the `=` refusal) | conformance `verification_objective_subject` (+ `.trace.golden`), `verification_objective_subject_violated`, `verification_objective_subject_unstated`, `verification_objective_subject_unbound`, `analysis_objective_subject_default_over_case_subject`; `robustness_verification_test.go:verification_objective_subject_of_another_type`, `:verification_objective_subject_left_unbound`, `:verification_objective_subject_rebound`; `cmd/sysml/verification_test.go:TestVerificationObjectiveDecidesOnEverySurface`, `cmd/sysml/sweep_test.go:TestSweepVerificationThroughCLI`, `repl/verification_verdict_test.go:TestVerificationObjectiveDecidesAgainstTheCaseSubject`, `grpc/verification_verdict_test.go:TestRunAnalysisDecidesAVerificationObjectiveAgainstTheCaseSubject` | ✅ Faithful | | A body binding `verdict` (or its result) to a `VerdictKind` literal reports that literal, recognized by the enumeration the value belongs to rather than by the spelling of the name. The verdict is read from the case's result parameter only — the name it declares, the library's `verdict`, or an unnamed `result` — so an `out` parameter of the same enumeration is not mistaken for the case's answer | `runtime/verification_run.go` `Context.bodyVerdict`, `verdictOutputNames`, `Context.verdictOf`, `Context.isVerdictKind`, `verdictKindName`, `verdictOutputName`; `runtime/analysis_run.go` `calcRun.resultName` | `runtime/verification_verdict_test.go:TestVerificationBodyVerdicts` (`test::stated`, `test::aux`) | ⚠️ Tool-defined — reported as the library declares the literal | | A body that produces no verdict value — no `PassIf`, no `verdict` binding — is `inconclusive`, saying so, rather than defaulted to a pass or a fail | `runtime/verification_run.go` `Context.bodyVerdict` (`VerdictInconclusive`) | conformance `verification_verdict_inconclusive`, `runtime/verification_verdict_test.go:TestVerificationBodyVerdicts` (`test::silent`) | ⚠️ Tool-defined | -| A verification case a part definition owns is a feature of every object of that definition (§7.24; §7.6.3, a usage nested in a definition; the static side is the nested-definition feature accessibility rule): `-validate=`, `-requirement`, `-satisfy` and the gRPC `ValidateInstance`/`VerifyRequirement`/`VerifySatisfaction` run it once per object of the definition the check is about — every object the run holds for a check about none (the gRPC `VerifyConstraint`, `VerifyRequirement` and `RunAnalysis` naming no `subject_symbol_id` evaluate over the population `Instantiate` holds for the model, under its lock, as `VerifySatisfaction` does and as a REPL check is about the objects the session holds: a type-owned constraint is checked on the held object carrying it, a case a definition owns runs as a feature of the held object of that definition, and a sweep that would pass the held-objects bound is `RESOURCE_EXHAUSTED` as `Instantiate` is; a named subject keeps a worker of its own), the objects a multiplicity repeats (`part cheap : Definition [2]`, a `[0..*]` collection's members, a part nested inside a repeated part) each on their own, so the verdict count is the object count rather than the usage count — with that object as the one it reads its owner's features from, and name the object on the verdict; a `satisfy` without `by` a definition states is checked on the object of that definition the same way. With no object of the definition instantiated the case has nothing to be a feature of, so every surface sweeping it (`-satisfy`, `-requirement`, `-analysis` without an object, the gRPC and JSON surfaces) reports it `inconclusive` — the library's `VerdictKind` for a run that decided nothing, not `error`, nothing being wrong with the model — with the detail `needs an object of : none is instantiated` the definition's `satisfy` line uses; an analysis case a definition owns is refused with the same message (`ErrNeedsObject`). A case a part usage owns is unaffected: it reads the usage's bound values, as a usage's `satisfy` instantiates the usage | `runtime/verification_cases.go` `Context.VerificationVerdictsOn`, `Context.caseCarriers` over `condition.go` `Context.objectsUnder`; `grpc/verify.go` `verifyContext.overHeld`, `verifyContext.requirementVerificationRuns` (`VerificationVerdict.Err` classifies the bound), `grpc/analysis.go` `verifyContext.scheduled` (every object, where a check's `carriersUnder` keeps one per declaration); `runtime/verification_cases.go` `Context.verificationResultOn`; `runtime/satisfy.go` `Context.SatisfactionSubjects` (every object a type-stated `satisfy` sweeps); `runtime/analysis_run.go` `Context.casePerformer` (`ErrNeedsObject`); `runtime/verification_run.go` `Context.RunVerification`, `VerificationVerdict.Subject`; `runtime/satisfy.go` `Context.CheckSatisfactionOn`; `repl/verification.go` `Session.withVerifications`, `verificationLine`; `grpc/verify.go` `verifyContext.requirementVerifications` | conformance `verification_definition_owned`, `verification_definition_owned_fail`, `verification_definition_owned_no_object`, `analysis_definition_owned_no_object`; `runtime/definition_owned_case_test.go`, `runtime/robustness_definition_owned_case_test.go`; `repl/definition_owned_case_test.go`; `grpc/definition_owned_case_test.go`, `grpc/held_population_verify_test.go`, `grpc/robustness_held_population_test.go:TestGRPCRobustnessHeldPopulation`, gRPC conformance `verify_requirement_held_population`, `verify_requirement_no_object`; `cmd/sysml/verification_test.go:TestRunVerificationOnADefinitionOwnedCase`; conformance `validation_verification_definition_owned` (`_fail`, `_satisfy_holds_verification_fails`, `_satisfy_fails_verification_passes`, `_subject_owner_bound`, `_subject_unbound`), each satisfaction verdict pinned beside the verification runs of its requirement, and `cmd/sysml/verification_test.go:TestValidateAgreesWithConformanceFixtures` holding `-validate` to the same verdicts; conformance `requirement_verification_repeated_subjects` (`[2]` twice, two passing and two failing), `requirement_verification_open_multiplicity_subjects` (an empty `[0..*]` gives no run, a subset one a run per member), `requirement_verification_nested_repeated_subjects` (a bolt in each of four wheels), pinned about no object as `-requirement` reports them, `cmd/sysml/verification_test.go:TestRequirementAgreesWithConformanceFixtures` holding `-requirement` to the same runs, `robustness_verification_test.go:testVerificationRunsOncePerRepeatedObject`, `grpc/definition_owned_case_test.go:TestVerifyRunsADefinitionOwnedCaseOnEveryRepeatedObject` | ✅ Faithful | +| A verification case a part definition owns is a feature of every object of that definition (§7.24; §7.6.3, a usage nested in a definition; the static side is the nested-definition feature accessibility rule): `-validate=`, `-requirement`, `-satisfy` and the gRPC `ValidateInstance`/`VerifyRequirement`/`VerifySatisfaction` run it once per object of the definition the check is about — every object the run holds for a check about none (the gRPC `VerifyConstraint`, `VerifyRequirement` and `RunAnalysis` naming no `subject_symbol_id` evaluate over the population `Instantiate` holds for the model, under its lock, as `VerifySatisfaction` does and as a REPL check is about the objects the session holds: a type-owned constraint is checked on the held object carrying it, a case a definition owns runs as a feature of the held object of that definition, and a sweep that would pass the held-objects bound is `RESOURCE_EXHAUSTED` as `Instantiate` is; a named subject keeps a worker of its own), the objects a multiplicity repeats (`part cheap : Definition [2]`, a `[0..*]` collection's members, a part nested inside a repeated part) each on their own, so the verdict count is the object count rather than the usage count — with that object as the one it reads its owner's features from, and name the object on the verdict; a `satisfy` without `by` a definition states is checked on the object of that definition the same way. With no object of the definition instantiated the case has nothing to be a feature of, so every surface sweeping it (`-satisfy`, `-requirement`, `-analysis` without an object, the gRPC and JSON surfaces) reports it `inconclusive` — the library's `VerdictKind` for a run that decided nothing, not `error`, nothing being wrong with the model — with the detail `needs an object of : none is instantiated` the definition's `satisfy` line uses; an analysis case a definition owns is refused with the same message (`ErrNeedsObject`). A case a part usage owns is unaffected: it reads the usage's bound values, as a usage's `satisfy` instantiates the usage | `runtime/verification_cases.go` `Context.VerificationVerdictsOn`, `Context.caseCarriers` over `condition.go` `Context.objectsUnder`; `grpc/verify.go` `verifyContext.overHeld`, `verifyContext.requirementVerificationRuns` (`VerificationVerdict.Err` classifies the bound), `grpc/analysis.go` `verifyContext.scheduled`, `verifyContext.exhaustedRun`, `grpc/tooldryrun.go` `Service.toolDryRun` (snapshot and runner restored) (every object, where a check's `carriersUnder` keeps one per declaration); `runtime/verification_cases.go` `Context.verificationResultOn`; `runtime/satisfy.go` `Context.SatisfactionSubjects` (every object a type-stated `satisfy` sweeps); `runtime/analysis_run.go` `Context.casePerformer` (`ErrNeedsObject`); `runtime/verification_run.go` `Context.RunVerification`, `VerificationVerdict.Subject`; `runtime/satisfy.go` `Context.CheckSatisfactionOn`; `repl/verification.go` `Session.withVerifications`, `verificationLine`; `grpc/verify.go` `verifyContext.requirementVerifications` | conformance `verification_definition_owned`, `verification_definition_owned_fail`, `verification_definition_owned_no_object`, `analysis_definition_owned_no_object`; `runtime/definition_owned_case_test.go`, `runtime/robustness_definition_owned_case_test.go`; `repl/definition_owned_case_test.go`; `grpc/definition_owned_case_test.go`, `grpc/held_population_verify_test.go`, `grpc/held_population_preview_test.go:TestToolPreviewLeavesTheHeldPopulationAsItWas`, `grpc/robustness_held_population_test.go:TestGRPCRobustnessHeldPopulation`, gRPC conformance `verify_requirement_held_population`, `verify_requirement_no_object`; `cmd/sysml/verification_test.go:TestRunVerificationOnADefinitionOwnedCase`; conformance `validation_verification_definition_owned` (`_fail`, `_satisfy_holds_verification_fails`, `_satisfy_fails_verification_passes`, `_subject_owner_bound`, `_subject_unbound`), each satisfaction verdict pinned beside the verification runs of its requirement, and `cmd/sysml/verification_test.go:TestValidateAgreesWithConformanceFixtures` holding `-validate` to the same verdicts; conformance `requirement_verification_repeated_subjects` (`[2]` twice, two passing and two failing), `requirement_verification_open_multiplicity_subjects` (an empty `[0..*]` gives no run, a subset one a run per member), `requirement_verification_nested_repeated_subjects` (a bolt in each of four wheels), pinned about no object as `-requirement` reports them, `cmd/sysml/verification_test.go:TestRequirementAgreesWithConformanceFixtures` holding `-requirement` to the same runs, `robustness_verification_test.go:testVerificationRunsOncePerRepeatedObject`, `grpc/definition_owned_case_test.go:TestVerifyRunsADefinitionOwnedCaseOnEveryRepeatedObject` | ✅ Faithful | | A body whose run fails with a typed error — an unbound subject, a failing step, a feature holding no value — is `error` carrying that error's own text, and the failure is a verdict rather than a refused request; a malformed *request* (a symbol of the wrong kind, an unknown named argument) stays a typed error from the call | `runtime/verification_run.go` `Context.RunVerification`, `badRequest`; `runtime/errors.go` `subjectUnboundError` (kind `verification`) | conformance `verification_verdict_error`, `robustness_verification_test.go:verification_body_that_cannot_run`, `:verification_body_step_that_fails`, `runtime/verification_verdict_test.go:TestVerificationBodyVerdicts` | ⚠️ Tool-defined | | A verification case performed as a step of another (`verification sub : Case;`, the library's `subVerificationCases :> subcases`) has its own verdict read from the step's performance and is reported **on its own**, marked as a subcase: the library declares the containment but states no roll-up rule — no calculation combining subcase verdicts into the parent's — so none is invented: a parent whose body binds no verdict of its own stays `inconclusive` beside its subcases' verdicts, and a parent whose own body passes still reports and exits as a pass beside a subcase that failed. A subcase the run did not perform — the case on the branch a decision did not select — answered nothing and is reported by neither, rather than being reported as an `error`. A subcase that could not run at all is a step that failed, which ends the performing case's run as any failed step does: that case's verdict is the `error` naming the subcase and the reason, and no verdict is reported for a body that did not finish | `runtime/verification_run.go` `Context.subcaseVerdicts`, `Context.subcaseVerdict`, `verdictOutputNames`; `runtime/case_step.go` `performances.performCase`; `VerificationVerdict.Subcase` | conformance `verification_verdict_subcases`, `verification_verdict_subcase_branch`, `runtime/verification_verdict_test.go:TestVerificationSubcaseVerdictsAreReportedOnTheirOwn`, `runtime/robustness_verification_test.go:verification_subcase_that_cannot_run`, `repl/verification_verdict_test.go:TestAnalysisKeepsACaseStatusApartFromItsSubcases` | ⚠️ Tool-defined — reported individually, with the reason stated here | | An objective stating only `verify r;` is `satisfied`, and the case is decided by its body's verdict alone: the objective is a `RequirementUsage` whose result is `allTrue(assumptions()) implies allTrue(constraints())` (`Requirements::RequirementConstraintCheck`), `verify` is a `RequirementVerificationMembership` naming a `verifiedRequirement` and no constraint of the objective, and the library's `VerificationCase::obj::requirementVerifications :> subrequirements` binds no value, so a check over no constraints is true; `-analysis` exits 0 for a passing body and 1 for a failing one, while an objective whose own condition cannot be evaluated stays `undecided` and the case unresolved | `runtime/analysis_run.go` `Context.analysisVerdict` | `verification_objective_verify_only.sysml`, `verification_objective_verify_only_fail.sysml`, `runtime/verification_verdict_test.go:TestVerifyOnlyObjectiveIsSatisfiedAndNoSatisfaction`, `repl/verify_only_objective_test.go:TestVerifyOnlyObjectiveIsDecidedByTheBody`, `cmd/sysml/verify_only_objective_test.go:TestVerifyOnlyObjectiveExitsByTheBodyVerdict`, `analysis_objective_undecided.sysml` (the undecided case kept), `analysis_objective_bare.sysml` (a bare `objective obj;` in an analysis case is `satisfied` by the same rule) | ✅ Faithful — the library's own result over no constraints | diff --git a/docs/reference/wire-contract.md b/docs/reference/wire-contract.md index 430028aeee..92e500b0af 100644 --- a/docs/reference/wire-contract.md +++ b/docs/reference/wire-contract.md @@ -1748,7 +1748,8 @@ one per assertion. All three return the `instances` they built, in the same shap 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, as the REPL answers), a +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 @@ -1756,7 +1757,10 @@ from the root it was instantiated under (`cheap[2]`), as `ValidateInstance` spel `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. +`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 From 76204f8fb723d492f1d38f38d75772a6164bb35a Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 28 Oct 2026 15:02:49 +0000 Subject: [PATCH 10/10] refactor: keep the comments of the held-population change to two lines Co-Authored-By: jason.han --- cmd/sysml/satisfy_label_test.go | 5 ++--- internal/exec/runtime/condition.go | 12 ++++-------- internal/frontend/grpc/analysis.go | 10 ++++------ .../grpc/held_population_preview_test.go | 6 ++---- .../grpc/held_population_verify_test.go | 19 ++++++------------- .../grpc/robustness_held_population_test.go | 8 ++------ internal/frontend/grpc/tooldryrun.go | 5 ++--- internal/frontend/grpc/verify.go | 13 ++++--------- internal/frontend/repl/query.go | 5 ++--- internal/frontend/repl/satisfy_stated_test.go | 3 +-- tests/grpc/conformance_verify_test.go | 10 ++++------ 11 files changed, 33 insertions(+), 63 deletions(-) diff --git a/cmd/sysml/satisfy_label_test.go b/cmd/sysml/satisfy_label_test.go index 73124d0fba..9e75e6f347 100644 --- a/cmd/sysml/satisfy_label_test.go +++ b/cmd/sysml/satisfy_label_test.go @@ -23,9 +23,8 @@ const repeatedPartModel = `package test { part fleet : Fleet; }` -// TestSatisfyLabelsObjectsAsValidateDoes checks that -satisfy names each object -// a definition's `satisfy r;` is decided on by the same indexed path -validate -// prints for it, so the two reports agree on which object a verdict is about. +// 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} diff --git a/internal/exec/runtime/condition.go b/internal/exec/runtime/condition.go index 5af31e8cd0..c53b749ecf 100644 --- a/internal/exec/runtime/condition.go +++ b/internal/exec/runtime/condition.go @@ -1240,9 +1240,8 @@ type heldSegment struct { 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 feature's -// name, indexed for a collection's element. +// 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 []heldSegment{{segment: name, id: id}} @@ -1336,11 +1335,8 @@ func carrierPath(c carrier, definition string) []string { return walked } -// carrierFeatures is the path to a nested carrier as a verdict labels it: the -// segments walked from its root, a collection's element indexed as a validation -// walk spells the object it reaches, ending in the declaration the carrier -// materializes where a collection gathers objects of several declarations, as -// carrierLabels names it. +// 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.segments) == 0 || c.instance == nil { return nil diff --git a/internal/frontend/grpc/analysis.go b/internal/frontend/grpc/analysis.go index 5e83fee97f..d50162f001 100644 --- a/internal/frontend/grpc/analysis.go +++ b/internal/frontend/grpc/analysis.go @@ -80,9 +80,8 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) ( return v.caseResponse(run, plan, err), nil } -// exhaustedRun is the RESOURCE_EXHAUSTED status of a run over the held population -// that would pass its bound, whether the call failed of it or a verification case's -// verdict carries the failure, as a case run reports its own; nil for any other run. +// 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 @@ -95,9 +94,8 @@ func (v *verifyContext) exhaustedRun(run caseRun, err error) error { return nil } -// scheduled sets the runtime's schedule for this request and returns what puts -// back the one it had, so a request leaves the held population's runtime as it -// found it; a policy the runtime cannot be set to is the error. +// 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 { diff --git a/internal/frontend/grpc/held_population_preview_test.go b/internal/frontend/grpc/held_population_preview_test.go index 270d68cf8c..5b1f95c5c7 100644 --- a/internal/frontend/grpc/held_population_preview_test.go +++ b/internal/frontend/grpc/held_population_preview_test.go @@ -10,10 +10,8 @@ import ( "github.com/Open-MBEE/OpenSysML/internal/exec/analysis" ) -// TestToolPreviewLeavesTheHeldPopulationAsItWas verifies that a tool dry run of a -// case naming no subject, made over the held population, leaves it as it found it: -// the objects the preview materialized are gone with it, and the runner the -// population's runtime had is back on it rather than the preview's. +// TestToolPreviewLeavesTheHeldPopulationAsItWas verifies that a subjectless tool dry run +// leaves the held population as it found it: no preview object held, the prior runner back on. func TestToolPreviewLeavesTheHeldPopulationAsItWas(t *testing.T) { srv := mustNewService(t, 10) hash := mustVerifyModel(t, srv, heldPopulationModel, "held-population-preview") diff --git a/internal/frontend/grpc/held_population_verify_test.go b/internal/frontend/grpc/held_population_verify_test.go index 50971f97b7..ef5e50969f 100644 --- a/internal/frontend/grpc/held_population_verify_test.go +++ b/internal/frontend/grpc/held_population_verify_test.go @@ -30,11 +30,8 @@ const heldPopulationModel = `package test { part fleet : Fleet; }` -// TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation verifies that -// VerifyRequirement naming no subject answers over the objects Instantiate holds, -// as the REPL's %requirement does after %instantiate: the requirement's own verdict -// is undecided, its subject being unbound, and the definition-owned case runs once -// on each held object of the definition — the same verdicts VerifySatisfaction reports. +// TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation verifies that a subjectless +// VerifyRequirement runs the definition-owned case once per held object, as %requirement does. func TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation(t *testing.T) { srv := mustNewService(t, 10) hash := mustVerifyModel(t, srv, heldPopulationModel, "held-population-requirement") @@ -74,10 +71,8 @@ func TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation(t *testing.T) { } } -// TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier verifies that a -// constraint a definition owns, asked about with no subject, is checked on the -// one held object carrying it, is ambiguous over two, and reads declared defaults -// when the model holds none — as the REPL's %constraint decides it. +// TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier verifies a subjectless constraint +// check is about the one held carrier, ambiguous over two, on defaults with none, as %constraint. func TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier(t *testing.T) { srv := mustNewService(t, 10) hash := mustVerifyModel(t, srv, `package Tanks { @@ -129,10 +124,8 @@ func TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier(t *testing.T) { } } -// TestRunAnalysisWithoutASubjectRunsOnTheHeldObject verifies that a case a -// definition owns, run with no subject, is a feature of the one held object of -// the definition, reports the ambiguity over two, and asks for one when the model -// holds none — as the REPL's %analysis decides it. +// TestRunAnalysisWithoutASubjectRunsOnTheHeldObject verifies a subjectless definition-owned +// case runs on the one held object, is ambiguous over two, and asks for one with none. func TestRunAnalysisWithoutASubjectRunsOnTheHeldObject(t *testing.T) { srv := mustNewService(t, 10) hash := mustVerifyModel(t, srv, definitionOwnedCaseModel, "held-definition-owned-analysis") diff --git a/internal/frontend/grpc/robustness_held_population_test.go b/internal/frontend/grpc/robustness_held_population_test.go index 5d99f6e6d8..f2c5fba2c2 100644 --- a/internal/frontend/grpc/robustness_held_population_test.go +++ b/internal/frontend/grpc/robustness_held_population_test.go @@ -9,12 +9,8 @@ import ( pb "github.com/Open-MBEE/OpenSysML/api/proto" ) -// TestGRPCRobustnessHeldPopulation puts the verification RPCs to the objects -// Instantiate holds, with no subject named, at the population's bound: a case run -// on a held object needs an object of its own, so a sweep that would pass the -// bound is RESOURCE_EXHAUSTED naming it, as Instantiate is, not an error verdict -// quoting the runtime; the population is left as it was, and a check about a -// named subject, made on a worker of its own, is unaffected. +// TestGRPCRobustnessHeldPopulation: a subjectless sweep that would pass the held-objects +// bound is RESOURCE_EXHAUSTED, the population unchanged, a named-subject check unaffected. func TestGRPCRobustnessHeldPopulation(t *testing.T) { t.Setenv(HeldObjectsEnvVar, "3") srv := mustNewService(t, 10) diff --git a/internal/frontend/grpc/tooldryrun.go b/internal/frontend/grpc/tooldryrun.go index b6ff5f4248..5b657e03bc 100644 --- a/internal/frontend/grpc/tooldryrun.go +++ b/internal/frontend/grpc/tooldryrun.go @@ -20,9 +20,8 @@ const msgNoToolReached = "no ToolExecution-annotated action was reached; nothing // The run's own results are not kept, so the response carries the preview, the // run's notes and, where the run failed otherwise, its error. func (s *Service) toolDryRun(ctx context.Context, v *verifyContext, sym *symbols.Symbol, args runtime.AnalysisArgs) (*pb.RunAnalysisResponse, error) { - // The preview runs on the request's runtime, as the REPL's does, and leaves - // nothing of it there: its writes are restored from a snapshot and the runner - // the runtime had goes back on, since over the held population both outlive it. + // The preview leaves the runtime as it found it, as the REPL's does: the held + // runtime outlives the request, so its writes are restored and its runner put back. snap, err := v.runtime.Snapshot() if err != nil { return nil, statusError(connect.CodeInternal, err.Error()) diff --git a/internal/frontend/grpc/verify.go b/internal/frontend/grpc/verify.go index 1caf1ae6fc..aaf259c60c 100644 --- a/internal/frontend/grpc/verify.go +++ b/internal/frontend/grpc/verify.go @@ -88,11 +88,8 @@ func releaseNothing() { // The parent context releases the worker it borrowed; this one holds none. } -// overHeld is this request's context over the objects Instantiate holds for the model, -// under the population's lock, which the returned function releases: a request naming no -// subject is about those objects, as a REPL check is about the objects the session holds. -// A request naming its subject, or a model holding no object, keeps the request's own -// worker and releases nothing. +// overHeld is this request's context over the objects Instantiate holds, under the population's +// lock the returned function releases; a named subject or an empty population keeps the worker. func (v *verifyContext) overHeld(ctx context.Context, subject *runtime.Instance) (*verifyContext, func()) { if subject != nil { return v, releaseNothing @@ -777,10 +774,8 @@ func (v *verifyContext) calcUsageOutputs(ctx context.Context, subject string, sy return pbOutputs, true, plan, nil } -// requirementVerificationRuns runs the whole model's verification cases verifying req (the -// case need not share the requirement's document), type-owned ones about subject, and -// reports their body verdicts; a run over the held population that would pass its bound -// is the RESOURCE_EXHAUSTED status instead. +// requirementVerificationRuns runs every verification case verifying req, type-owned ones about +// subject, and reports their body verdicts; past the held-objects bound it is RESOURCE_EXHAUSTED. func (v *verifyContext) requirementVerificationRuns(req *symbols.Symbol, subject *runtime.Instance, runs *runtime.VerificationRuns) ([]runtime.VerificationVerdict, error) { verdicts := v.runtime.VerificationVerdictsOnce(v.cached.DocumentRoots(), req, subject, runs) for _, verdict := range verdicts { diff --git a/internal/frontend/repl/query.go b/internal/frontend/repl/query.go index 52f8340c3f..7f1e251861 100644 --- a/internal/frontend/repl/query.go +++ b/internal/frontend/repl/query.go @@ -418,9 +418,8 @@ func (s *Session) reportedSubject(result runtime.CheckResult, inst *runtime.Inst return result.Subject, objectPath(root, result.SubjectPath) } -// objectPath labels an object nested in the one labelled root by the segments -// walked to it, as the runtime spells them: `fleet.cheap[2]`. Every verdict about -// a nested object — %validate's, %satisfy's, a check's — labels it this way. +// objectPath labels an object nested in the labelled root by the segments walked to it, +// `fleet.cheap[2]`, the one spelling every verdict about a nested object uses. func objectPath(root string, path []string) string { if len(path) == 0 { return root diff --git a/internal/frontend/repl/satisfy_stated_test.go b/internal/frontend/repl/satisfy_stated_test.go index ae4187d43f..fc71605f55 100644 --- a/internal/frontend/repl/satisfy_stated_test.go +++ b/internal/frontend/repl/satisfy_stated_test.go @@ -93,8 +93,7 @@ func TestSatisfyStatedByADefinitionSweepsItsObjects(t *testing.T) { } // TestSatisfyLabelsObjectsAsValidateDoes checks that %satisfy names each object a -// definition's `satisfy r;` is decided on by the indexed path %validate prints for -// it — `fleet.cheap[2]`, not `fleet.cheap` — so the two reports agree on the object. +// definition's `satisfy r;` is decided on by the indexed path %validate prints for it. func TestSatisfyLabelsObjectsAsValidateDoes(t *testing.T) { s := loadSource(t, `package test { private import ScalarValues::Real; diff --git a/tests/grpc/conformance_verify_test.go b/tests/grpc/conformance_verify_test.go index a9744d307d..f4c87f7b55 100644 --- a/tests/grpc/conformance_verify_test.go +++ b/tests/grpc/conformance_verify_test.go @@ -8,9 +8,8 @@ import ( "github.com/Open-MBEE/OpenSysML/internal/frontend/grpc" ) -// expectedVerificationVerdict is the fixture encoding of a pb.VerificationVerdict: -// the case, the verdict kind its body answered, the detail of one that decided -// nothing, and the type of the object it ran on (empty for a run on none). +// expectedVerificationVerdict is the fixture encoding of a pb.VerificationVerdict: case, +// kind, the detail of one deciding nothing, and the type of the object it ran on. type expectedVerificationVerdict struct { Case string `json:"case"` Kind string `json:"kind"` @@ -18,9 +17,8 @@ type expectedVerificationVerdict struct { InstanceType string `json:"instance_type"` } -// runVerifyRequirementCase instantiates the case's objects, verifies the requirement -// about the subject named (none when empty) and compares the requirement's status -// with the body verdicts of the cases verifying it, each about its own object. +// runVerifyRequirementCase instantiates the case's objects, verifies the requirement about +// the subject named (none when empty) and compares the status and body verdicts expected. func runVerifyRequirementCase(t *testing.T, srv *grpc.Service, ctx context.Context, modelHash string, tc conformanceCase) { t.Helper() instantiateAll(t, srv, ctx, modelHash, tc.Instantiate)