[devin-ai-integration]

What and why

A requirement usage a definition owns — part def P1 { attribute sub : Integer = 3; requirement rq : R1 { subject s :>> s = sub; } } — held an object of its definition (R1) when its body only restated the subject: declaresFeatures counted body members that are *ast.Usage nodes but not an *ast.SubjectMember, so CompositeTypeOf fell back to the def. The object's shape was then R1's, whose s binds nothing, and p1.rq.s read <undetermined> with p1.rq.result undetermined through it — while -validate on p1 (which evaluates the usage's body bindings against the object through memberBindings) decided the requirement. The read and the check disagreed about the same object.

The fix is in the shape/materialisation layer, not in the read path:

• runtime/instance.go declaresFeatures: a body restating the subject (named, redefining, or a bare subject = x;) declares a feature, so the usage is the type of the object it holds, as any body declaring a feature already made it. CompositeTypeOf treats a satisfy usage's by the same way, since by x is the subject's feature value (SysML.xtext SatisfactionSubjectMember).
• runtime/shape.go effectiveFeature → new roleRedefiningDefault: when neither the inherited subject nor anything it redefines by name binds a value, the value of a body member redefining it under no name of its own (subject = sub;, an implicit role redefinition) or of the satisfy usage's by operand becomes the feature's value, evaluated in the scope it was written in.
• runtime/context.go memberBindings + new subjectParameterNames: a satisfy usage's by operand is bound under its subject's names before the body's members are read, unless an object is supplied from outside (the check path's by object) — so the result read of a satisfy usage sees the same subject the check does.
• runtime/return_parameters.go statesConditions: a satisfy requirement usage is a requirement usage (SysML v2 §7.21.4), so its result is its conditions' verdict.
• runtime/satisfy.go CheckSatisfactionOn: satisfy requirement r : R by x; is checked against the conditions R states (new statesAnyCondition) instead of being refused as satisfying no requirement; satisfiedBy reads the by operand through semantics.SatisfyEndsOf.
• runtime/shape.go new satisfiedByValue and runtime/context.go memberBindings: the by operand is the subject's most specific value, over a value or default the satisfied requirement's subject declares or inherits; only a subject written default (valueIsDefault) yields to an empty or undetermined source.
• solve/differential_test.go newNodeValues: the differential gate reads a satisfaction's references through ReadInSatisfaction, with the assertion's bindings, so its node values name the by object as the evaluator does (the gate now agrees on 131 elements, 0 disagreed; the production pin reader, SatisfactionReader, already read them so).
• runtime/return_parameters.go conditionResultValue + new conditionSelf (used by checkRequirementOn and action_holds.go holds): a nested usage's subject and actor bindings are read against the owning object, its conditions against the object it holds — the usage's own v over the owner's v.

Specification basis

SysML v2 §7.21.2 Requirements (the subject is a parameter the usage's body redefines and binds), §8.3.21.11 SubjectMembership (a bare subject = x; implicitly redefines the definition's subject), §7.21.4 Satisfy Requirement Usages (by binds the subject; isNegated asserts the requirement false, §8.3.21.10), §7.22.2 Cases (an objective is a requirement usage whose subject defaults to the case's result); KerML 1.0 §7.4.11 Feature Values (a value in a nested feature's body is evaluated in that feature's context; a default applies when nothing else values the feature), §7.3.4.5 (the more specific declaration governs the object's type). Adds a row to docs/project/spec-compliance.md (⚠️ Approximate, naming the open subrequirement and no-by items below).

Behaviour changes

Before	After	Spec
p1.rq.s → <undetermined>, p1.rq.result → <undetermined> for requirement rq : R1 { subject s :>> s = sub; } in P1, at model level and on an instantiated p1; -validate=p1 held	p1.rq.s → 3, p1.rq.result → true (false for a failing value), equal to -validate=p1	SysML v2 §7.21.2 (the subject is a parameter the usage's body redefines and binds); KerML 1.0 §7.4.11 (a feature value in a nested feature's body is evaluated in that feature's context)
subject s = sub; and the bare subject = sub; likewise undetermined	both read 3/true	§7.21.2, §8.3.21.11 SubjectMembership (a subject member implicitly redefines the definition's subject)
satisfy requirement sat : RP by pa; nested in a definition: -validate refused it ("no requirement to satisfy"), p1.sat.s/p1.sat.result undetermined	checked against RP's conditions; p1.sat.s is the pa object, p1.sat.result its verdict; same at package level (satisfy requirement satPkg : RP by p1.pa;)	§7.21.4 Satisfy Requirement Usages (by binds the subject; the declared requirement states its type's conditions)
not satisfy requirement n : R by x; (nested or package-level): -validate/-satisfy refused it; n.result undetermined	n.result is R's verdict (true when R holds) while the assertion's standing is violated — no inversion of the read	§8.3.21.10 (isNegated: the requirement is asserted false); Constraints.sysml negatedConstraintChecks :> falseEvaluations
An object held by such a usage was typed by the definition (object:Probe::R1; the library's Cases::Case::obj holder by Requirements::RequirementCheck)	typed by the usage (object:Probe::P1::rq, object:UseCases::UseCase::obj), as a usage whose body declares any other feature already was	KerML 1.0 §7.3.4.5 (the more specific declaration governs)
requirement rqDefault : R1 { subject s :>> s default sub; }: p1.rqDefault.s/.result <undetermined>	3/true — the default applies since nothing else values s	KerML 1.0 §7.4.11 (a default feature value applies when no other value is given)
ca2.obj.subj for case ca2 : Ca2 { return rr : Integer = 7; } → <undetermined> (the library's subject subj default Case::result; read as the declaration)	7: the default is evaluated in the owning case's context, Case::result being that case's own result; ca2.obj.result stays true (RequirementConstraintCheck::result states no condition on subj); a use case's u1.obj.subj, its case stating no result, stays <undetermined> with u1.obj.result true	SysML v2 §7.22.2 Cases (the objective's subject defaults to the case's result), KerML 1.0 §7.4.11
A use case's obj.result whose objective condition reads a subject that fails it (use case u3 : U3 { subject s = bad0; }, w = −1): true on develop, vacuously — the holder was typed RequirementCheck and the objective's condition never evaluated	false: the objective's condition is evaluated against the bound subject	SysML v2 §7.22.2 Cases (the objective is a requirement usage checked on its subject), Requirements.sysml RequirementCheck::result
satisfy requirement sat : RG by bad; where RG declares subject s : PA default good;: -satisfy refused it; sat.s read good (the inherited default)	checked on bad; sat.s is bad, sat.result false — the by operand supersedes the subject's declared value or default, in the result read and in the object's shape alike	§7.21.4 (by binds the satisfy usage's subject); KerML 1.0 §7.4.11 (the redefining feature's value governs)
A nested usage's conditions read the owning object: requirement rq : RV { attribute extra = 1; } in a part with attribute v = -1 (RV states v > 0 on its own v) — -validate reported rq fails on the owner's v; p.rq.result <undetermined>	the conditions read the usage's own object: rq is undecided (no value for feature v) and p.rq.result <undetermined>; requirement rqOwnV : RV { attribute v :>> v = 5; } is true in both	KerML 1.0 §7.4.11 (a feature value is read on the feature's own object); §7.3.4.5
subject s :>> s = P1::optional; with optional : Integer[0..1] empty and the subject declared default 1: -validate refused it for its multiplicity, but p1.r.s read 1	the read is refused as the check is (multiplicity violation: 0 value(s) bound to a feature with multiplicity lower bound 1); only a subject written default yields to an empty or undetermined source	KerML 1.0 §7.4.11, §7.3.4.4 (a value written with = is the feature's value and must meet its multiplicity)
A subject nothing binds (subject s :>> s;, or a bodiless requirement rq : R1;)	unchanged: <undetermined> at model level, uninitialized on an object, the check refuses it; never true	—

Verification usages were already right (RunVerification binds the body's subject) and still agree: p1.ver.verdict = pass/fail for verification ver : VD { subject s :>> s = sub; }.

Measured fallout

• docs/project/library-and-prefix-sweep-outcomes.txt re-recorded, 17 rows moved, all in the systems sweep's Probe model:
  • object type of a requirement usage whose body values the subject, and of a satisfy usage with a by (Probe::p1.rq, Probe::p1.sr, new Probe::P1().rq/.sr, their .self, the object rows, and the two checkedConstraints collections listing them): object:Probe::R1 → object:Probe::P1::rq / ::sr — 10 rows.
  • Probe::p1.rq.s: undetermined → object:Probe::P2 — the subject now holds what subject s :>> s = sub#(1) binds — 1 row.
  • Probe::p1.sr.s / .sr.result for the probe satisfy requirement sr : R1 by sub; (rewritten from by sub#(1), a syntax error: SysML.xtext SatisfactionReferenceExpression is a FeatureChainMember, and the pilot 0.62.0 validator refuses it too): undetermined / constant true → multiplicity violation: 2 value(s) bound to a feature with multiplicity upper bound 1, since sub : P2[2] is bound to subject s : P2. The row now pins that refusal (KerML 1.0 §7.4.11 binding, §7.3.4.4 multiplicity); before, the by never reached a read and the result was vacuously true — 2 rows.
  • object type of a use case's library objective (Probe::u1.obj, Probe::p1.uq.obj, Probe::p1.iu.obj, new Probe::U1().obj): object:Requirements::RequirementCheck → object:UseCases::UseCase::obj — 4 rows; their obj.result stays true (pinned in the fixture for a case, a use case, both nested in a part, and on an instantiated object).
• testdata/kernel_member_reads.golden (TestKernelLibraryMembersReadable): no rows moved.
• Solver differential gate (internal/exec/solve TestDifferentialConformanceCorpus): 131 agreed, 0 disagreed (129 before); satisfy_chain_unresolved's satisfy r by config.nope moves from "without values" to "unreadable-read", since the by operand is now the subject's value and does not evaluate — no verdict either way.
• No conformance fixture, golden trace, parser golden or corpus baseline moved; training_examples_expected.txt untouched.

Left open

• A subrequirement's verdict does not reach its container's result (§7.21.2, Requirements.sysml subrequirements :> constraints), and a satisfy stating no by inside a part does not bind the containing part as its subject (§7.21.4); both pre-existing, named in the compliance row (⚠️).
• A read of a verification usage's subject at package level (verPkg.s) goes through the case-usage output path and is refused as unknown output; its verdict reads correctly.

How it was verified

On the branch head (fix commit, docs commit, review-fix commit, merges of origin/develop up to 188f222):

• go build ./..., go vet ./... — ok; gofmt -l . — empty; make lint (staticcheck + gosec) — ✓ Lint passed
• go test -count=1 ./internal/exec/runtime -run 'TestReturnParameter|TestExecutionConformance|TestNestedRequirementUsageShapeBindsItsSubject|TestRuntimeRobustnessNestedSubjectBinding|TestKernelLibraryMembersReadable|TestLibraryAndPrefixSweep' — ok (two conformance fixtures, sweep re-recorded: 13 rows, kernel golden unchanged)
• OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_PILOT_LIBRARY_XMI=1 go test -count=1 ./... with the corpora from scripts/download-training-examples.sh, scripts/download-pilot-corpora.sh, scripts/download-pilot-library-xmi.sh — 119 packages ok, exit 0 (tests/codegen, cmd/sysml, internal/check included)
• python3 scripts/changelog.py check, python3 scripts/check-doc-ids.py — ok
• CLI probes on the built binary: the model in the first section reads p1.rq.s = 3, p1.rq.result = true with -e, on -instantiate p1, and -instantiate p1 -validate=p1 reports requirement rq holds; not satisfy requirement nsrHolds : R1 by one; reads nsrHolds.result = true while -validate reports it violated (Required condition evaluated to false: not s.w > 0); ca2.obj.subj <undetermined>, ca2.obj.result/u1.obj.result/h.uq.obj.result/new Holder().cq.obj.result true; package OccurrencesTest { part def P1 { part pa; part pb; attribute v : ScalarValues::Integer = self.suboccurrences->SequenceFunctions::size(); } part p1 : P1; } reads p1.v = 2.

On the head with the defaulted-subject rule (ac4865890): go build ./..., go vet ./..., gofmt -l . empty, make lint passed; TestReturnParameter*, TestExecutionConformance, TestLibraryAndPrefixSweep (re-recorded), TestKernelLibraryMembersReadable (no rows moved), TestNestedRequirementUsageShapeBindsItsSubject, TestRuntimeRobustnessNestedSubjectBinding, TestAnalysis*/TestObjective* green; go test ./... with the three corpora and their REQUIRE variables: 119 packages ok; python3 scripts/changelog.py check and python3 scripts/check-doc-ids.py clean.

On the merge head over origin/develop a270e66 (#1302, #1305, #1313, #1315–#1318, #1323, #1325; clean merge, no golden or fixture row moved by the merged work): go build ./..., go vet ./..., gofmt -l . empty, make lint; the runtime gates above; ./internal/exec/... ./internal/check/... ./cmd/sysml/... with the three corpora and their REQUIRE variables; OccurrencesTest p1.v = 2 at model level and on an instantiated object; changelog and doc-id checks clean.

On the head with the review fixes merged over origin/develop 43a831e (#1306): go build ./..., go vet ./..., gofmt -l . empty, make lint; the runtime gates above (fixture extended with the own-feature, empty-subject and by-over-default reads; sweep and kernel golden unchanged); ./internal/exec/... ./internal/check/... ./cmd/sysml/... with the three corpora and their REQUIRE variables; OccurrencesTest p1.v = 2 at model level and on an instantiated object; changelog and doc-id checks clean.

On the merge head over origin/develop e3ec3c2 (PRs #1299–#1304 merged in; no conflicts, no sweep or kernel golden row moved by the merged work): go build ./..., go vet ./..., gofmt -l . empty; the runtime gates above, ./internal/exec/... ./internal/check/... ./cmd/sysml/... with the three corpora and their REQUIRE variables all ok; OccurrencesTest p1.v = 2; changelog and doc-id checks clean.

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

[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