[devin-ai-integration]

What and why

Follow-up to #1542. The model's default multiplicity is 0..* everywhere it is judged, but the constraint solver still read a feature that states no multiplicity as exactly one value (StatedMultiplicityOf reported nothing for it, so no refusal and no note). The solver now takes the multiplicity from the model alone (Model.GoverningMultiplicityOf: declared, inherited by redefinition, or DefaultMultiplicityOf; StatedMultiplicityOf tells a stated bound from the default) and derives no rule of its own:

• A stated, inherited or implicit multiplicity that admits several values refuses the read, as before (c.wheels.radius through wheels : Wheel[4]; a redefinition inheriting [0..*]).
• A feature that declares and inherits none, which the default 0..* governs, is read as one value under an assumption the query records (Query.AssumedOne) and the REPL's solver reports print: Assuming test::Tank::level holds one value: it declares no multiplicity, so the default [0..*] governs it. No count is asserted, so no [1..1] is smuggled in. The verdict is about the case where the feature holds one value, which is also the only case the evaluator answers about: over none or two values, level >= 0.0 is a type-mismatch refusal, not a verdict (the new _none/_two fixtures pin that).
• %check <part> walks a defaulted object-holding feature through its one representative object, as %validate does, and reports the same assumption once (Assuming spare holds one object: …), merged with the value read through it; the assumption is carried by the held group and reported only when that group is translated, so a part left in Uncovered assumes nothing.

Why not a plain refusal: the default 0..* governs more than KerML features. A bare in a : Integer parameter of a constraint or calc def is a ReferenceUsage, which SysML v2 §7.6.3 leaves out of the implicit [1..1], and EffectiveParameterRange answers 0..* for it too (probed: test::C::a governing 0..*, stated none). Refusing it rejects every constraint def { in x : Real; … }: 65 tests in internal/exec/solve and the gRPC verify tests fail, and %check, %solve, %configure, %optimize and the gRPC verify questions become unusable on ordinary models. The runtime holds such a parameter to 0..* as well (two bound values are held, not refused). Reading it as one value and saying so keeps the solver sound about the model and useful.

Audit of the other count-dependent paths: quantify.go already reads GoverningMultiplicityOf for the variation point (unchanged); no AtMostOne/size read exists in internal/exec/solve; counterexample and witness rendering is per variable and unchanged; the gRPC verify verdict has no field for notes (as for Query.Uncovered), so the assumption reaches gRPC only through the shared Query for now; %check, %solve, %explain, %configure and %optimize all print through solveReports, which appends the assumption lines.

The solve differential now also runs over the .kerml conformance cases (it skipped them by extension, and mentionsConditions did not know KerML inv).

Specification basis

• KerML 1.1 Beta 2 §7.4.12 Multiplicities and §7.4.5.2 ("the usual default of 0..*"): a feature declaring and inheriting no multiplicity.
• SysML v2.1 Beta 2 §7.6.3: the implicit [1..1] for an attribute, item, part or port usage owned by a definition or usage with no owned subsetting or redefinition; a reference usage (a bare in x) and a package-owned attribute are left at 0..*.
• KerML 1.1 Beta 2 §7.3.4.5 / §8.4.4.12.1: a redefinition declaring no multiplicity inherits the redefined declaration's.

docs/project/spec-compliance.md: new row in the Constraint Solving table (the multiplicity rule, Query.AssumedOne), the translatable-subset text and the collections limitation reworded, and the #1542 default-multiplicity row's solver mention. docs/reference/repl-commands.md %check describes the Assuming … holds one value line.

How it was verified

New fixtures under internal/exec/runtime/testdata/conformance/ (runtime conformance and the solve differential):

fixture	runtime	solver
solve_default_multiplicity_kerml_none.kerml (feature level : Real = ())	type-mismatch error (null)	translated, level assumed one; differential: without values
solve_default_multiplicity_kerml_one.kerml (= 2.0)	satisfied	translated, assumed one; differential: agreed
solve_default_multiplicity_kerml_two.kerml (= (2.0, 3.5))	type-mismatch error (sequence)	translated, assumed one; differential: without values
solve_implicit_multiplicity_usage.sysml (§7.6.3 attribute)	satisfied	translated, nothing assumed; agreed
solve_redefinition_inherits_multiplicity.sysml	levelNonNegative satisfied	:>> level under [1]: translated, nothing assumed, agreed; :>> readings under [0..*]: refused it may hold more than one value

Unit tests: internal/exec/solve/default_multiplicity_test.go (the five fixtures plus a bare in a : Integer parameter assumed once), internal/frontend/repl/check_default_multiplicity_test.go (%check prints the assumption for a KerML feature, nothing for an implicit [1..1] usage, and the one-object assumption once for part spare : Tank :> main).

Solve differential movement (z3 4.8.12), conformance corpus, before → after: 246 → 251 files, 550 → 556 elements, 342 → 347 translated, 208 → 209 skipped-by-refusal (+1: readings), 171 → 174 agreed (+3: kerml_one, implicit_multiplicity_usage, levelNonNegative), 147 → 149 without values (+2: kerml_none, kerml_two), 0 disagreed; the standard-library, training-corpus and randomized gates are byte-identical to develop. No oracle baseline (pilot-diff, pilot-exec, xpect, reject, training expectations) moved.

Gates (all with OPENSYSML_REQUIRE_SMT=1 OPENSYSML_SMT=/usr/bin/z3 and the training, pilot, spec-example, pilot-library-XMI and PSSM corpora required): go build ./... ok, go vet ./... ok, gofmt -l . empty, python3 scripts/changelog.py check ok, mkdocs build --strict ok; go test -count=1 ./... ok (every package; cmd/sysml and tests/codegen re-run with -timeout 40m after hitting the local 10-minute default, 257 s and 290 s).

Merged origin/develop at 48f60b4 (after #1550 landed): the only conflict was the default-multiplicity row of spec-compliance.md, resolved by keeping #1550's closing sentence and representative-object row and appending this PR's solver clause; doc gates re-run on the merged tree (mkdocs build --strict, changelog.py check), solve/REPL/runtime suites green. Against #1529 (chore/pilot-pin-2026-09, head 9ca600a) the merge conflicts in docs/project/spec-compliance.md and docs/project/validation-constraints.md, but every conflict hunk is between #1529 and develop's own later commits (the pilot 2026-08 → 2026-09 prose and the validation census counts); #1529 conflicts with bare origin/develop in the same two files without this branch. This branch's rows merge cleanly outside those hunks. The only file both touch is spec-compliance.md; #1529 touches nothing under internal/exec/solve, internal/frontend/repl or the conformance corpus.

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 (no gate count moved)
• 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/d98944611f3940a3aed28854fad06251
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/d98944611f3940a3aed28854fad06251?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