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..96a6a3c537 --- /dev/null +++ b/changes/unreleased/grpc-verify-held-population.fixed.md @@ -0,0 +1,2 @@ +- gRPC `VerifyConstraint`, `VerifyRequirement` and `RunAnalysis` naming no `subject_symbol_id` now evaluate over the objects `Instantiate` holds for the model, as `VerifySatisfaction` already did and as the REPL's checks are about the objects a session holds: a verification case a definition owns runs once per held object of the definition and its `verification_verdicts` name each object, a constraint or requirement a definition owns is checked on the held object carrying it (ambiguous over several), and a case a definition owns runs as a feature of the held object of that definition. Before, `VerifyRequirement` after `Instantiate` answered a definition-owned case `inconclusive: needs an object … none is instantiated` while `VerifySatisfaction` on the same model reported it `pass` per object. A named subject keeps a worker of its own. A sweep over the population that would pass the `OPENSYSML_GRPC_MAX_HELD_OBJECTS` bound is `RESOURCE_EXHAUSTED`, as `Instantiate` is, rather than an error verdict quoting the runtime; `runtime.VerificationVerdict` carries the error an error verdict reports, and a `this` read keeps its cause in the error chain. +- A `RunAnalysis` run of a verification case over the held population that would pass the held-objects bound is `RESOURCE_EXHAUSTED` too, and a `RunAnalysis` tool dry run over the population undoes the preview's writes and puts the runtime's tool runner back, as the REPL's preview does. 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/cmd/sysml/satisfy_label_test.go b/cmd/sysml/satisfy_label_test.go new file mode 100644 index 0000000000..9e75e6f347 --- /dev/null +++ b/cmd/sysml/satisfy_label_test.go @@ -0,0 +1,42 @@ +package main + +import ( + "strings" + "testing" +) + +// repeatedPartModel holds two objects of a definition stating a satisfaction +// under one usage with a multiplicity. +const repeatedPartModel = `package test { + private import ScalarValues::Real; + requirement def CostRequirement { + subject product : Definition; + attribute maximumCost : Real; + require constraint costOk { product.cost <= maximumCost } + } + requirement costReq : CostRequirement { :>> maximumCost = 100.0; } + part def Definition { + attribute cost : Real; + satisfy costReq; + } + part def Fleet { part cheap : Definition [2] { attribute :>> cost = 80.0; } } + part fleet : Fleet; +}` + +// TestSatisfyLabelsObjectsAsValidateDoes checks that -satisfy names each object a +// definition's `satisfy r;` is decided on by the indexed path -validate prints for it. +func TestSatisfyLabelsObjectsAsValidateDoes(t *testing.T) { + binary := buildCLI(t) + files := map[string]string{"fleet.sysml": repeatedPartModel} + labels := []string{ + "✓ satisfy costReq holds (on test::fleet.cheap[1] ID: 2)", + "✓ satisfy costReq holds (on test::fleet.cheap[2] ID: 3)", + } + satisfied := checkFiles(t, binary, files, "-instantiate", "test::fleet", "-satisfy") + wantReport(t, satisfied, 0, labels...) + validated := checkFiles(t, binary, files, "-instantiate", "test::fleet", "-validate=test::fleet") + wantReport(t, validated, 0, labels...) + if strings.Contains(satisfied.output(), "fleet.cheap ID") { + t.Errorf("-satisfy labels an object by its feature alone, not its indexed path:\n%s", satisfied.output()) + } +} diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index aa831d037b..822f4e5f7a 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` (`runtime/errors.go` `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`, `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` (`runtime/errors.go` `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`; `runtime/verification_run.go` `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` (`ast/defusage.go` `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` (`ast/defusage.go` `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..92e500b0af 100644 --- a/docs/reference/wire-contract.md +++ b/docs/reference/wire-contract.md @@ -1745,6 +1745,23 @@ never both. one per assertion. All three return the `instances` they built, in the same shape as `Instantiate`. +With no `subjectSymbolId`, the three — and `RunAnalysis` — evaluate over the objects +`Instantiate` holds for the model, as the REPL's `%constraint`, `%requirement`, `%satisfy` and +`%analysis` are about the objects a session holds: a constraint or requirement a definition owns +is checked on the one held object carrying it (ambiguous over several of distinct declarations, as +the REPL answers; one declaration instantiated twice is checked on its newest object), a +verification case a definition owns runs once per held object of that definition and reports a +`verificationVerdicts` entry about each, naming the object by `instanceId`, and a `satisfy` +a definition states is decided per held object with `instancePath` spelling the object's path +from the root it was instantiated under (`cheap[2]`), as `ValidateInstance` spells it. The +`instances` carry every object a verdict is about. With nothing held, the answer is about +declared defaults, and a definition-owned case is `inconclusive` asking for an object. A +sweep that would make one more object than `OPENSYSML_GRPC_MAX_HELD_OBJECTS` allows is +`RESOURCE_EXHAUSTED`, as `Instantiate` is, and leaves the population as it was. A `RunAnalysis` +tool dry run over the held population leaves it as it was too: the preview's writes are undone +and the runner it previewed with is taken off. An `explore` schedule is the exception: its runs +are made on runtimes of their own, one per linearization, holding nothing, as the REPL's are. + A constraint or requirement whose condition reads `in` parameters takes their values on the request: `arguments` is a positional list bound in declaration order, `namedArguments` binds by parameter name, and the two may be mixed, as `RunAnalysis` binds a case's inputs; the values are diff --git a/internal/exec/runtime/condition.go b/internal/exec/runtime/condition.go index 111851320a..c53b749ecf 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,18 @@ func objectFeature(sym *symbols.Symbol) bool { return objectUsageKind(usage.Kind) || usage.Kind == ast.UsagePort } -// heldObjects returns the identities a feature value denotes, a collection's -// elements included. -func heldObjects(val Value) []int64 { +// heldSegment is the identity of an object a feature value holds and the segment +// naming it there. +type heldSegment struct { + segment string + id int64 +} + +// heldSegments returns the identities a feature value denotes, a collection's elements +// included, each under the segment a path names it by: the name, indexed for an element. +func heldSegments(val Value, name string) []heldSegment { if id, ok := val.Object(); ok { - return []int64{id} + return []heldSegment{{segment: name, id: id}} } var elements []Value switch { @@ -1239,15 +1253,32 @@ func heldObjects(val Value) []int64 { case val.Kind == ValSet && val.Set() != nil: elements = val.Set().Elements() } - var out []int64 - for _, element := range elements { + var out []heldSegment + for i, element := range elements { if id, ok := element.Object(); ok { - out = append(out, id) + out = append(out, heldSegment{segment: indexedSegment(name, i), id: id}) } } return out } +// heldObjects returns the identities a feature value denotes, a collection's +// elements included. +func heldObjects(val Value) []int64 { + held := heldSegments(val, "") + out := make([]int64, len(held)) + for i, h := range held { + out[i] = h.id + } + return out +} + +// indexedSegment names a collection's element in a path: the feature's name +// indexed from 1, `wheels[2]`, as every surface reporting an object spells it. +func indexedSegment(name string, i int) string { + return fmt.Sprintf("%s[%d]", name, i+1) +} + // carrierLabels names carriers as a diagnostic can quote them: the definition // each is an object of, its identity, and the feature path telling two apart. func (ctx *Context) carrierLabels(carriers []carrier) []string { @@ -1277,14 +1308,20 @@ func qualifiedText(names []string) string { return strings.Join(parts, "::") } +// carrierDeclaration is the name of the declaration a carrier materializes where +// it is not the definition it is an object of; empty where it is. +func carrierDeclaration(c carrier, definition string) string { + if c.instance.Type != nil && c.instance.Type.Name != definition { + return c.instance.Type.Name + } + return "" +} + // carrierPath names a carrier apart from its siblings: the features walked to // it, ending in the declaration it materializes — which differs from the feature // holding it when a collection gathers objects of several declarations. func carrierPath(c carrier, definition string) []string { - decl := "" - if c.instance.Type != nil && c.instance.Type.Name != definition { - decl = c.instance.Type.Name - } + decl := carrierDeclaration(c, definition) if len(c.features) == 0 { if decl == "" { return nil @@ -1298,17 +1335,23 @@ func carrierPath(c carrier, definition string) []string { return walked } -// carrierFeatures is the feature path to a nested carrier, one name a segment, -// corrected the way carrierLabels names an ambiguity's carriers. +// carrierFeatures is a verdict's path to a nested carrier: the segments walked from its root, +// a collection's element indexed as validation spells it, ending in the declaration it materializes. func (ctx *Context) carrierFeatures(c carrier) []string { - if len(c.features) == 0 || c.instance == nil { + if len(c.segments) == 0 || c.instance == nil { return nil } name := "object" if def := ctx.definitionOf(c.instance.Type); def != nil && def.Name != "" { name = def.Name } - return carrierPath(c, name) + decl := carrierDeclaration(c, name) + if decl == "" || c.features[len(c.features)-1] == decl { + return c.segments + } + walked := append([]string(nil), c.segments...) + walked[len(walked)-1] = source.NameText(decl) + return walked } // definitionOf is the definition objects of sym are objects of: sym itself when diff --git a/internal/exec/runtime/eval.go b/internal/exec/runtime/eval.go index efcd8dbf18..83155bb02b 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/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/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..d50162f001 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,39 @@ func (s *Service) RunAnalysis(ctx context.Context, req *pb.RunAnalysisRequest) ( if gone := callerGone(ctx, err); gone != nil { return nil, gone } + if status := v.exhaustedRun(run, err); status != nil { + return nil, status + } return v.caseResponse(run, plan, err), nil } +// exhaustedRun is the RESOURCE_EXHAUSTED status of a held-population run that passed +// its bound, in the call's error or in a verification verdict's; nil for any other run. +func (v *verifyContext) exhaustedRun(run caseRun, err error) error { + if status := v.exhausted(err); status != nil { + return status + } + for _, verdict := range run.verdicts() { + if status := v.exhausted(verdict.Err); status != nil { + return status + } + } + return nil +} + +// scheduled sets the runtime's schedule for this request and returns what puts back +// the one it had, so the held population's runtime is left as found; unsettable is the error. +func (v *verifyContext) scheduled(policy runtime.SchedulePolicy) (func(), error) { + was := v.runtime.Schedule() + if err := v.runtime.SetSchedule(policy); err != nil { + return nil, err + } + return func() { + // The policy the runtime held was set once already, so it is settable. + _ = v.runtime.SetSchedule(was) + }, nil +} + // caseResponse reports one run of a case: its outputs, verdicts, evaluations // and instances, or the failure that stopped it, with the plan's standing. func (v *verifyContext) caseResponse(run caseRun, plan analysis.Plan, err error) *pb.RunAnalysisResponse { 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..5b1f95c5c7 --- /dev/null +++ b/internal/frontend/grpc/held_population_preview_test.go @@ -0,0 +1,64 @@ +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 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") + 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/held_population_verify_test.go b/internal/frontend/grpc/held_population_verify_test.go new file mode 100644 index 0000000000..ef5e50969f --- /dev/null +++ b/internal/frontend/grpc/held_population_verify_test.go @@ -0,0 +1,159 @@ +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 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") + 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) + } + } +} + +// 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 { + 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 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") + 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..f2c5fba2c2 --- /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: 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) + 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("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) + }) + 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/tooldryrun.go b/internal/frontend/grpc/tooldryrun.go index 5ea441b11e..5b657e03bc 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,18 @@ 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 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()) + } + 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 } diff --git a/internal/frontend/grpc/validate.go b/internal/frontend/grpc/validate.go index b30c610e99..67a75d7e27 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 @@ -79,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 62cb9390b5..aaf259c60c 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,41 @@ 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, 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 + } + 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 +334,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 +353,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 +435,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 +454,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 +577,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 +595,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 @@ -553,10 +609,15 @@ 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)...) - 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 +774,33 @@ 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 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 { + 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) } 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..7f1e251861 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,16 @@ 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 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 } - 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..fc71605f55 100644 --- a/internal/frontend/repl/satisfy_stated_test.go +++ b/internal/frontend/repl/satisfy_stated_test.go @@ -91,3 +91,34 @@ 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. +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 { 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..f4c87f7b55 --- /dev/null +++ b/tests/grpc/conformance_verify_test.go @@ -0,0 +1,67 @@ +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: 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"` + 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 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) + + 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; +}