[devin-ai-integration]

What and why

On develop, part-usage-part-definition ("A part must be typed by at least one part definition.") is reported on a part usage typed only by an item definition — package P { item def I; part p : I; } — and so on four lines of the OMG pilot example corpus (Geometry Examples/SimpleQuadcopter.sysml:14 and :114, Simple Tests/IndividualTest.sysml:12, Simple Tests/ItemTest.sysml:11). The pinned pilot reports nothing there, but its silence is not the argument: the pilot never evaluates the constraint (checkPartUsage is commented out), so the question is what the specification's own derivation says. This PR settles the reading first (below) and then brings the check and every record that cites it into line with that reading.

Closes nothing by itself; it revisits the behaviour #647 asked for.

Spec decision

Verdict: partDefinition->notEmpty() cannot fail for a part usage typed only by an item definition. The check on develop is stricter than the specification.

Clauses (SysML v2.1 Beta 2 and KerML 1.1 Beta 2 at the pin of scripts/pilot-pin.sh, rendered by scripts/download-spec-examples.sh into build/spec-docs/):

• SysML §8.3.11.3 PartUsage: /partDefinition : PartDefinition [0..*] {subsets itemDefinition}; derivePartUsagePartDefinition — partDefinition = itemDefinition->selectByKind(PartDefinition); validatePartUsagePartDefinition — partDefinition->notEmpty(); checkPartUsageSpecialization — specializesFromLibrary('Parts::parts').
• SysML §8.3.10.3 ItemUsage, deriveItemUsageItemDefinition — itemDefinition = occurrenceDefinition->selectByKind(Structure); §8.3.9.3 /occurrenceDefinition : Class {redefines definition}; §8.3.8.3 Usage /definition : Classifier {redefines type}. §8.3.1 (derivation constraints, note): a derived property that redefines a derived property takes the redefined property's derivation — so definition, occurrenceDefinition, itemDefinition and partDefinition are all filters over KerML Feature::type.
• KerML §8.3.3.3.4 deriveFeatureType: type = closure(typingFeatures()).typing.type with redundant supertypes removed; typingFeatures() (§8.3.3.3.4) is all subsetted features except CrossSubsetting (plus the last chaining feature). Nothing in it distinguishes an implied Subsetting from an owned one.
• SysML §8.4.7.2 and the §8.4.3 implied-relationships table: checkPartUsageSpecialization is satisfied by an implied Subsetting of Parts::parts, whose type is Parts::Part (§9.2.4). KerML §8.4.2 omits an implied specialization only when an owned specialization has the same general or a subtype of it; a FeatureTyping by an item definition is neither, so the implied subsetting stays.
• SysML §8.3.1 / KerML §8.3.1 (validation constraints): "They are written presuming that all semantic constraints are satisfied." With checkPartUsageSpecialization satisfied, type(p) ⊇ {Parts::Part}, itemDefinition(p) ⊇ {Parts::Part} (a PartDefinition is a Structure), partDefinition(p) ⊇ {Parts::Part}. §8.3.1 also notes that derived values "may depend on whether implied relationships are included in the model or not", which is exactly why the validation constraints are read under the presumption above rather than against a model missing its implied relationships.
• SysML §7.10 (Parts overview), note: "Because the base usage of a part usage is the part usage parts defined by the base part definition Part, every part usage is always directly or indirectly defined by at least one part definition, implicitly if not explicitly, in addition to any other item definitions." This is the authors stating the consequence of the derivation in prose.

So the constraint is not self-contradictory and admits one reading: it is satisfied for every part usage once the semantic constraints are, and the only part usage it can ever report is one whose derived partDefinition is empty — i.e. one for which the implied Parts::parts subsetting cannot be formed (no Parts library in scope). The reading in docs/project/spec-pilot-gap-register.md §19 (27 Sep) was right; the issue's reading, which counted only the owned typings, was not.

Corroboration, not grounds:

• The pilot's own metamodel agrees with the derivation. Its JSON export (scripts/pilot-json-exporter, isImpliedIncluded = false) of package P { item def I; part p : I; } gives type = [P::I, Parts::Part], occurrenceDefinition = [P::I, Parts::Part], itemDefinition = [P::I, Parts::Part], partDefinition = [Parts::Part].
• The pilot authors' fixture validation/valid/PartUsage.sysml.xt:41 annotates part f :> i; under item i : I; with // also typed by part def Part.

What the code did on develop: internal/check/passes/part_usage_definition.go read semantics.Model.FeatureTypeSet, which excludes the implied generals whenever the feature states any typing of its own, so on part p : I it saw {I} and reported. The tree's own reflective layer already disagreed with it: Model.reflectiveFeatureTypes added Parts::parts' type for a PartUsage (pinned since 2 Oct by TestReflectivePartUsageIncludesImplicitPartDefinition: type = [ItemType, Parts::Part], partDefinition = [Parts::Part]). Our API JSON export writes type = [I] for the part usage (isImpliedIncluded = false) and no partDefinition at all, so it neither agreed nor disagreed with the check; that export gap (the pilot writes partDefinition = [Parts::Part]) is noted, not changed here.

The specification's own example drew the rule too: examples/spec-examples/sysml/7.6.5/1.sysml (part cylinders : Cylinder[2..*]; with Cylinder an item definition from ShapeItems) carried three only-ours kind-mismatch rows in the differential baseline.

Behaviour changes

• part-usage-part-definition is withdrawn. A part usage typed only by an item definition (or by any non-part definition) is no longer reported, and the diagnostic code leaves the catalogue. Spec-compliance note: SysML v2.1 Beta 2 §8.3.11.3 validatePartUsagePartDefinition holds for every part usage whose semantic constraints hold, through the implied Parts::parts subsetting (§7.10, §8.3.1, §8.4.7.2; KerML §8.3.3.3.4, §8.4.2), so no textual model violates it. The pass could not be kept as a vacuous check: the census (tools/census/validation) requires every faithful validate* row to be backed by a probe that draws its diagnostic, and no library-loaded model can, so the row moves to deliberate on the precedent of validateDefinitionVariationIsAbstract and validateEnumerationDefinitionIsVariation (unobservable in text, held as derived truth).
• Reflective type joins the implied generals' types for every usage kind. New semantics.Model.FeatureTypeSetWithImplied = FeatureTypeSet ∪ the types of the kind's implied generals and base feature, most-specific only; Model.reflectiveFeatureTypes reads it in place of the PartUsage-only Parts::parts lookup. For a typed usage whose declared type conforms to its kind's base (attribute a : Real, part r : PD) nothing changes; for a part typed by an item definition reflective type is [I, Parts::Part] and partDefinition is [Parts::Part], as the pilot derives them. A subject s : T; is indexed as a part usage here, so the join also takes the base feature of the symbol's kind (Parts::parts) and TestReflectivePartUsageIncludesImplicitPartDefinition keeps type = [ItemType, Parts::Part] for it; the join is confined to SysML usages so KerML end features keep their declared types (TestSelfCheckReflectiveRelationshipConstraints).
• derivePartUsagePartDefinition moves from unknown to faithful in the census, citing the reflective derivation.

Records moved

Record	Before	After
tests/corpus/testdata/pilot_corpora_expected.txt	SimpleQuadcopter.sysml 2, IndividualTest.sysml 1, ItemTest.sysml 1	rows removed (clean)
tests/corpus/testdata/spec_examples_expected.txt	sysml/7.6.5/1.sysml 3	row removed (clean)
docs/project/pilot-differential-baseline.json	517 fully agreeing / 366 only ours / 1475 ours; pilot-examples 88 / 261, spec-examples 150 / 50	521 / 359 / 1468; pilot-examples 91 / 257, spec-examples 151 / 47 (the 4 OMG lines and the 3 spec-example lines; nothing else moved)
docs/project/pilot-xpect-baseline.json	1293 agree / 33 disagree; sysml 345 / 13; noErrors 262 / 276	1296 / 30; sysml 348 / 10; noErrors 265 / 276 (IndividualTest.sysml.xt, ItemTest.sysml.xt, validation/valid/PartUsage.sysml.xt)
docs/project/pilot-rejection-baseline.json	semantic/variant-kind-inconsistent-with-variation.sysml oursErrors 6	5 (still both-reject; 347 cases, 335 both reject, 12 only ours — unchanged)
docs/project/constraint-manifest.json / validation-constraints.md	validatePartUsagePartDefinition faithful (164 reported, 4 deliberate); derivePartUsagePartDefinition unknown	deliberate (163 reported, 5 deliberate); faithful
docs/reference/diagnostics.md	part-usage-part-definition entry	removed (make diagnostics-catalogue)
examples/self-model/pipeline.sysml	passCount = 67, a PartUsageDefinitionPass row	66, row removed; this moves the examples root digest in pilot-differential-baseline.json (digest only, no figure) and in api-json-differential-baseline.json (one self-model element fewer: matched 91774 → 91766, pilot-only 37351 → 37349, with the api-json-differential.md figures re-typed to match)
Prose	gap register §19 (said both accept — stale), pilot-differential.md S10 row (Ours, pilot-following reason), pilot-xpect.md row + open reading, pilot-rejection.md rows, constraint-census-triage.md observation + row 127 (#1232 is merged), spec-compliance.md row, the four testing-pilot-* skills' headline figures	spec-over-pilot adjudication throughout; make docs-counts and make docs-check pass

The differential baseline rows for the four OMG lines are gone rather than kept: the pilot still lacks the check, but there is no longer a diagnostic on our side to record against it — both tools are clean on those lines, which is the spec-over-pilot outcome.

Specification basis

SysML v2.1 Beta 2 §8.3.11.3 validatePartUsagePartDefinition / derivePartUsagePartDefinition, §8.3.10.3 deriveItemUsageItemDefinition, §8.4.7.2, §7.10; KerML 1.1 Beta 2 §8.3.3.3.4 deriveFeatureType, §8.4.2, §8.3.1. The validatePartUsagePartDefinition row in docs/project/spec-compliance.md is rewritten (census deliberate, ✅ faithful: the derivation is held, no diagnostic).

How it was verified

Re-run on the head with bin/sysml: Geometry Examples/SimpleQuadcopter.sysml, Simple Tests/IndividualTest.sysml, Simple Tests/ItemTest.sysml and package P { item def I; part p : I; } all analyse clean (no diagnostic of any severity).

New tests: semantics/feature_type_implied_test.go (part p : I → FeatureTypeSet = [I], FeatureTypeSetWithImplied = [I, Parts::Part]; a part owned by an item def, a part typed by a part def, an untyped part and a typed attribute), passes/item_typed_part_test.go (the issue's model, the OMG shapes and part f :> i; draw no error). TestReflectivePartUsageIncludesImplicitPartDefinition keeps pinning type/partDefinition for the part usage.

Gate (local): go build ./... clean; go vet ./... clean; gofmt -l . empty; make lint ✓ (staticcheck + gosec, main module and tools); make docs-counts ✓; make docs-check ✓; go run -C tools ./cmd/validation-census -check ✓; pilot-diff / pilot-xpect / pilot-reject re-recorded and reproducing; go test ./... with OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SPEC_EXAMPLES=1 OPENSYSML_REQUIRE_PILOT_LIBRARY_XMI=1 OPENSYSML_REQUIRE_PSSM_SUITE=1: first run 120 packages ok, 2 failing — examples (TestSelfModelPassRegistryMatchesImplementation: the self-model still listed the withdrawn pass) and internal/frontend/repl (TestSelfCheckPartUsageDefinitionForObjectivesAndVariants: a subject is indexed as a part usage and lost Parts::Part when the special case went). Both fixed in the second commit (the kind's base joins a SysML usage's implied types; confined to SysML so KerML end features keep their declared types), then internal/semantic/..., internal/check/..., internal/frontend/repl, examples, internal/doc/..., internal/exec/runtime, internal/translate/export, tests/corpus, tests/export, tests/resolve, internal/workspace/... re-run with the require variables: 36 packages ok, 0 failing.

Review round on the merged head: a bare variant a; referencing an action (placeholder kind part usage, metaclass ReferenceUsage) had gained Parts::Part in its reflective type; FeatureTypeSetWithImplied now returns the plain FeatureTypeSet for a variant reference, pinned by TestReflectiveVariantReferenceTakesNoKindBaseType. Probed and unchanged: attribute x : I (item def) derives [I, Base::DataValue] on both the parsed and recorded paths (the implied attributeValues edge exists when the declared type does not conform); part :> Parts::parts, part : PD :> Parts::parts, part :> explicitTyped, port : ~PortD, item : PD keep their declared type only, so a suppressed implied edge changes nothing. After the fix pilot-apijson-diff -update re-recorded byte-identical, the four provenance tests pass, make docs-counts is current, and the four OMG files plus the minimal model validate with zero diagnostics.

Follow-ups

• The recorder stores Parts::Part among a recorded variant reference's own types (FeatureTypeSet returns [P::AD Parts::Part] for the recorded fixture before any implied join), so the recorded path of a variant reference still shows the part base; the regression test pins the parsed path only.

Checklist

• make lint passes locally; go test ./... with the require variables set: see above
• 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

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