[devin-ai-integration]

What and why

Follow-up to #1537, which made an unbound calculation result read as ErrNoValue. One path stayed distinct: a constraint carrying no condition (and a negated constraint stating only assumptions) yielded its own ErrNoConditions — "no verdict". A constraint is a BooleanEvaluation whose result : Boolean[1] only its body expression binds; with no body nothing binds the result, which is the same unbound-result case #1537 settled as no value. "No conditions" is not a notion the specification has, so this folds it:

• A condition-less constraint definition or usage, and a negated constraint stating only assumptions, now report ErrNoValue on every surface that reports a check — REPL -constraint/-requirement/-satisfy/%check/%configure, LSP, gRPC VerifyConstraint/VerifyRequirement, MCP verify_constraint/verify_requirement, the solver (solve.Constraint/Satisfaction/Asserted), the smt engine and the validation report all go through evaluateConditions or solve/translate.go, so the one change covers them. The cause stays as the diagnostic detail through conditionCheck.noResultValue, which reuses unboundResultHint from fix(runtime): report an unbound calc result as no value, like an unassigned out #1537 (no second detail mechanism): constraint empty: no value: the constraint declares no condition; constraint cneg: no value: the constraint declares no required condition, only assumptions; and for a return r; the body never binds, the calc's own hint (result parameter r binds no value; write the result as the trailing expression …).
• runtime.ErrNoConditions and solve.ErrNoConditions are removed with every reference. Two callers were not about conditions at all — a missing assertion symbol (action_holds.go, sequence_executor.go, statements.go, smt/property.go) — and now wrap ErrNotAConstraint; the smt engine's refusal list carries ErrNoValue in place of the removed sentinel.
• Requirement vacuity (fix(runtime): count a nested requirement as a required constraint of its container #1539) is kept apart: a requirement, satisfaction or viewpoint over no required constraint still holds vacuously, an assume r0; subrequirement that requires nothing included (it is a satisfied check with nothing required, not a condition-less constraint). The solver's vacuousSubject became requirementSubject (the Requirement-rule subjects) and a denial of a vacuous requirement is now (not true) — unsatisfiable, agreeing with the evaluator, which reports assert not satisfy of it violated — instead of refusing with the removed sentinel; the assumptions of such a requirement are not read whether it is denied or violated, as the evaluator does not read them, so a false or untranslatable assumption cannot turn the denial's violation query unsatisfiable (translator.translate, Translator.Conditions). %configure of a family whose only assertion holds vacuously now answers with the existing "no variation point is read" diagnostic instead of the removed one.
• A model-level read of such a constraint's value (attribute b : Boolean = p3.cneg;) is now undetermined, as any unbound result is (read_return_parameters cnegNoCondition, previously the error).

Not touched: repl/view.go errNoConcernCondition ("states no condition to evaluate") is a different sentinel for a concern that resolves to no requirement (ErrNoRequirement), not for a condition-less check, so it stays. Historical CHANGELOG.md entries naming ErrNoConditions are history and are not edited.

Specification basis

KerML 1.1 Beta 2 §7.4.8.2 (a BooleanExpression's result : Boolean[1] is bound by its body) and SysML v2.1 Beta 2 §7.20.2 (a constraint is a BooleanEvaluation); requirement vacuity from Requirements::RequirementConstraintCheck (allTrue(assumptions()) implies allTrue(constraints()), SysML v2 §9.2.14). docs/project/spec-compliance.md: the constraint row ("A constraint carrying no condition …") and the negated-assumptions row are rewritten to ErrNoValue with the clauses; the requirement-vacuity row gains the denial-is-false semantics, the new fixtures and requirementSubject; the constraint-body-statements row (steps-only body) and the inherited-result-parameter row drop their ErrNoConditions claims. Status stays ✅ on all of them.

Changed assertions (intentional semantics change, not a weakening)

Each previously asserted ErrNoConditions; now:

Test	Now asserts
runtime/action_holds_test.go Holds(nil, nil)	ErrNotAConstraint (no assertion named — never about conditions)
runtime/condition_test.go:TestNegatedConstraintWithOnlyAssumptionsIsNotAVerdict	ErrNoValue + "no required condition"
runtime/constraint_test.go:TestConstraintWithoutConditionsIsNotAVerdict	ErrNoValue + "declares no condition"
runtime/owned_constraint_value_test.go:TestOwnedConstraintValueIsNotACondition	ErrNoValue
runtime/robustness_constraint_body_steps_test.go (empty body steps)	ErrNoValue
runtime/robustness_referenced_requirement_binding_test.go (the require wagonSpec cycle)	ErrNoValue + "names the requirement being checked"
runtime/robustness_subrequirement_test.go (constraint over nothing)	ErrNoValue
runtime/robustness_vacuous_requirement_test.go (alpha constraint ×2, condition-less constraints)	ErrNoValue (+ "the constraint declares no condition")
runtime/testdata/conformance/read_return_parameters.expected.json cnegNoCondition	{"type": "Undetermined"} (was the error string)
solve/asserted_vacuous_test.go affirmed	translates to a query with no assertion (vacuous); emptyConstraint → runtime.ErrNoValue
solve/differential_test.go refusal filter	runtime.ErrNoValue
solve/expression_test.go vacuous (negated constraint, nothing required)	runtime.ErrNoValue
solve/satisfy_test.go:TestSatisfactionWithoutConditionsIsVacuous denial	translates to (not true) instead of refusing
solve/translate_test.go (×2, TestNoConditions)	runtime.ErrNoValue
solve/vacuous_requirement_test.go (constraint assuming, requiring nothing)	runtime.ErrNoValue; new TestDeniedVacuousRequirementIgnoresItsAssumptions (denial (not true), its violation true, a false and an untranslatable assumption unread)
solve/violation_test.go:TestViolationWithoutClaimRefuses	runtime.ErrNoValue
repl/configure_family_test.go:TestConfigureAFamilyWhoseAssertionsStateNoCondition	the existing "no variation point is read" diagnostic
repl/satisfy_vacuous_test.go	output no longer contains "no value" (was "no condition to evaluate")

How it was verified

• New: conformance condition_less_constraint_def, condition_less_constraint_usage (error), condition_less_requirement_def, condition_less_requirement_usage, condition_less_subrequirement (assume r0; requiring nothing — satisfied); golden tests/parser/testdata/parse/condition_less_check; runtime/robustness_condition_less_check_test.go (def, usage, unbound return r; hint, requirement def/usage vacuous, assumed subrequirement vacuous).
• go build ./..., go vet ./..., gofmt -l . empty; go test -count=1 ./... with the training, pilot, spec-example, pilot-library-XMI and PSSM corpora fetched and required: all packages ok (cmd/sysml and tests/codegen hit the 10-minute default timeout only under the full parallel run on this VM and pass alone, 251s/286s). python3 scripts/changelog.py check ok; mkdocs build --strict ok.
• Oracle baselines: none moved (no pilot-diff/xpect/reject/referee baseline changed; tests/corpus ok as committed).
• Dry-merge in a detached worktree: against origin/develop (0286c98) clean; against fix(runtime): follow the library body of SequenceFunctions::excludingAt #1540 (87d5670) clean, and internal/exec/runtime, internal/exec/solve, internal/exec/smt, internal/frontend/repl on the merged tree: runtime, solve, smt and repl all ok. Against chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529 (9ca600a) the merge conflicts in docs/project/spec-compliance.md and docs/project/validation-constraints.md, but those conflicts already exist between bare origin/develop and chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529 and none of the hunks touch the rows this PR edits.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/c245709a88bb406696146e243581dfc7
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/c245709a88bb406696146e243581dfc7?variant=devin
Requested by: @HuiJun

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring