Skip to content

fix(migrate): write no nonunique where the v2 usage must be unique; messages demo validates clean - #795

Merged
HuiJun merged 3 commits into
developfrom
fix/758-nonunique-composites
Oct 1, 2026
Merged

HuiJun merged 3 commits into
developfrom
fix/758-nonunique-composites

Conversation

@devin-ai-integration

@devin-ai-integration devin-ai-integration Bot commented Oct 1, 2026 •

Copy link
Copy Markdown
Contributor

What and why

Fixes #758

Follows #748 (fix(check): conformance of an implicit subsetting), which is on develop already (5fb9a8434); this branch is cut from it, so no landing-order constraint remains. #748 made subsetting-uniqueness-conformance hold of the feature a usage implicitly subsets, which exposed two things this PR corrects:

1. examples/parser_features_demo_messages_events.sysml (fe28318f3). The two channel messages were declared message incoming: Message[*] nonunique; / message outgoing: Message[*] nonunique;; a message in a part implicitly subsets the unique Parts::Part::ownedActions, so the modifier is dropped and nothing else in the demo changes (no prose in the demo or examples/PARSER_FEATURES_DEMOS.md described the messages as nonunique). The examplesKnownFailures entry goes, and with it the map and the known/unknown switch in TestExamplesAnalyseCleanly — it held only this file, so a plain if len(errs) > 0 remains.

2. The SysML v1 migrator (7a60fd2de). collection(p) wrote nonunique for every isUnique="false" property and typeModifier.shape() wrote ordered nonunique for every []/[n] MagicDraw type modifier, regardless of the usage the property becomes. For a composite part/item/action/… whose v2 usage implicitly subsets a unique library feature, that is now invalid notation. Before/after for the fixture in TestCollectionModifiersAreWritten:

// before                                   // after
part n : A[2] nonunique;                    part n : A[2];
ref part b : A ordered nonunique :> n;      ref part b : A ordered :> n;
attribute o : ScalarValues::Real[0..*] ordered nonunique;   (unchanged — Base::dataValues is nonunique)
ref part u : A;                             (unchanged — a reference subsets nothing implicitly)

and the report, where the drop is never silent:

_n  approximated  nonunique is not written: a part in a part def implicitly subsets Items::Item::subparts, which is unique
_b  approximated  nonunique is not written: it subsets n, which is written unique

How the decision is made — derived from the semantics, no name table in the migrator:

  • internal/semantic/semantics/nested.go is refactored so the rule chains run over declaration kinds alone: NestedUsage{Kind, Composite, Portion, Performed, Exhibited, Included, RequirementConstraint} × NestedOwner{Usage | Def} → nestedRuleFQN, with the model-dependent KerML step fallback (subperformances / ownedPerformances / enclosedPerformances, chosen by what the owner conforms to) split off behind a step flag. Model.implicitSubsettingFQN is the same function as before over a symbol; the new exported ImplicitSubsettingCandidates(u, owner) []string is the kind-only view (one feature, or the three step-fallback features under an occurrence owner).
  • internal/translate/migrate/uniqueness.go: implicitlyUnique(kw, prefix, dir, owner) maps the written keyword (part, item, action, … ref → a default reference usage, which the parser reads as an attribute) and owner category to those kinds, asks for the candidates, and reads each one's uniqueness from the bundled library through semantics.Model.IsUnique over libs.SharedBase() (built once). A directed usage is a parameter and is exempt, as IsParameter exempts it in the checker.
  • migration.writtenUnique adds the explicit case the fixture itself shows: a usage that redefines or subsets (:>>/:>, incl. the shadow redefinition) a feature that is written unique — declared so in v1, or forced unique by this same rule — must be unique too, else the written :> n fails the same conformance. Cycles settle on what is declared.
  • collection(p, unique), shaped(…, unique) and typeModifier.shape(unique) take the verdict; association ends, metadata tag attributes, behavior parameters and activity pins pass false (none of them is a composite nested usage). feature() appends the nonunique is not written: … note, so report.add marks the entry approximated per the existing convention.
  • slotConflict (38abe5f12, from review) judges a repeated slot value by the same written uniqueness rather than the v1 isUnique flag: a slot repeating an instance on a composite property that is now written unique is unmapped as a slot conflict, as on any unique feature, and a repeat on a feature an array type modifier writes nonunique is admitted.

Decision taken, flagged for the maintainer: the modifier is dropped (and recorded) rather than the usage converted to a ref, since a ref would change composition semantics, and the cascade to an explicit subsetter (b above) follows from the same rule. Say so if you would rather have b handled differently.

Docs: docs/reference/sysml-v1-migration.md gains a row for isOrdered/isUnique="false" properties describing the rule and the note, the type-modifier paragraph says []/[n] write ordered alone on a usage that must be unique, and the slot-conflict row says "a feature written unique". docs/project/spec-compliance.md has no row covering the migrator's uniqueness handling (its uniqueness rows are the value-level and collection ones), so it is untouched; docs/project/validation-constraints.md already covers the checker side from #748.

Specification basis

SysML v2 1.0 §7.9.3.2 / KerML 1.0 §8.3.3.3.4 Feature::isUnique and the subsetting-uniqueness-conformance constraint (a subsetting/redefining feature cannot be nonunique if the subsetted/redefined feature is unique); the implicit subsettings of SysML v2 §8.3.x as implemented in nested.go. No spec-compliance.md row moves.

How it was verified

Tests:

  • tests/migrate/relations_test.go TestCollectionModifiersAreWritten: fix(check): conformance of an implicit subsetting (#726) #748 changed it to expect the one uniqueness finding at part n : A[2] nonunique;, pinning the broken output. It now expects the notation above, no diagnostics, _n/_b approximated with the exact notes, and _o/_u/_e1 mapped. The fixture's o is made isUnique="false" so a legal nonunique (an attribute) stays in the output and the Turtle isNonunique check remains load-bearing.
  • New internal/translate/migrate/uniqueness_test.go TestImplicitlyUniqueAgreesWithTheChecker: for every usage keyword the migrator writes × ref/composite × every owner category, builds <owner> O { <usage> x[*] nonunique; }, skips combinations the owner does not admit at all, and asserts the migrator writes nonunique exactly when the checker accepts it. Plus the parameter/ref/attribute exemptions and libraryUnique on subparts (unique) / dataValues (nonunique) / an unknown name.
  • New tests/migrate/values_test.go TestPartSlotRepeatingOnAForcedUniquePartIsUnmapped: a nonunique composite spares is written part spares : MCS[0..*]; (approximated) and its slot holding 'mcs 2' twice is unmapped with the slot-conflict note.
  • go test -count=1 ./internal/semantic/semantics ./internal/check/... green after the nested.go refactor (behaviour-preserving; semantics/nested_test.go and the implicit-subsetting conformance goldens unchanged).

Baselines, adjudicated:

  • Pilot differential (./scripts/download-pilot-sysml-validator.sh, go run -C tools ./cmd/pilot-diff -update): the only movement is the examples root digest (69a73dac… → 4a51ae18…), from the demo edit. Aggregate unchanged: 380 files, 345 fully agreeing, 38 agreed / 40 ours-only / 1616 pilot-only. The baseline records no per-file verdict for the demo (it was not a disagreeing file), so no verdict line moves. Reproduced: rm -rf build/pilot-diff && go run -C tools ./cmd/pilot-diff then diff <(jq -S . docs/project/pilot-differential-baseline.json) <(jq -S . build/pilot-diff/pilot-diff.json) differs only in the committed "recorded" date line. go test -C tools ./referee/diff -run TestCommittedBaselineStatesThisRepositorysProvenance passes.
  • PSSM migration gate (./scripts/download-pssm-suite.sh, go test -count=1 ./tests/corpus -run TestPSSMSuiteMigration): passes with the ratchet unchanged (14512 approximated / 23544 mapped / 6 skipped / 9660 unmapped / 13 validation-errors) — the suite has no composite isUnique="false" property that the rule touches. Re-run green after the slot change.
  • go test ./tests/migrate/... ./internal/translate/migrate/...: green, migration goldens unchanged.
  • Training/pilot corpus gates ran inside go test ./... with OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 set; no expectation file moves.

Definition of done (corpora provisioned per AGENTS.md §2):

$ make build && bin/sysml -validate examples/parser_features_demo_messages_events.sysml
✓ package MessagesAndEvents
✓ examples/parser_features_demo_messages_events.sysml: no errors
$ go build ./...        # ok
$ go vet ./...          # ok
$ gofmt -l .            # (empty)
$ make lint             # ✓ Lint passed
$ python3 scripts/changelog.py check   # ok
$ go test -count=1 ./...               # 91 packages ok, 0 FAIL

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 (messages-demo-nonunique.fixed.md, migrate-nonunique-composites.fixed.md)
  • baselines regenerated and make docs-counts run if a gate count moved (only the pilot-differential examples digest moved; no counted gate 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/e321310cad9c411eabb8c8aebfc18c4d
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/e321310cad9c411eabb8c8aebfc18c4d?variant=devin
Requested by: @HuiJun

devin-ai-integration Bot and others added 2 commits October 1, 2026 15:33
A message in a part implicitly subsets the unique Parts::Part::ownedActions,
so the two channel messages cannot be nonunique. The example validates clean,
leaves the known-failure list (which held only it), and the pilot-differential
baseline re-records the examples digest.

Fixes #758

Co-Authored-By: jason.han <hanhuijun@gmail.com>
A v1 property with isUnique=false, or a MagicDraw [] / [n] type modifier,
that becomes a usage implicitly subsetting a unique library feature, or that
redefines or subsets a feature written unique, is written without nonunique;
the report notes the dropped modifier and marks the entry approximated.

The decision reuses the checker's implicit-subsetting rules: semantics now
exposes ImplicitSubsettingCandidates over declaration kinds alone, and the
migrator reads the candidates' uniqueness from the bundled library.

Co-Authored-By: jason.han <hanhuijun@gmail.com>
@devin-ai-integration

Copy link
Copy Markdown
Contributor Author

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

@devin-ai-integration
devin-ai-integration Bot marked this pull request as ready for review October 1, 2026 15:57
devin-ai-integration[bot]

This comment was marked as resolved.

…iqueness

slotConflict read the v1 isUnique flag, so a repeated instance in a slot of a
nonunique composite property passed although the part is now written unique.
It asks featureWrittenUnique instead, which also admits a repeat on a feature
an array type modifier writes nonunique.

Co-Authored-By: jason.han <hanhuijun@gmail.com>
@devin-ai-integration devin-ai-integration Bot reopened this Oct 1, 2026
@HuiJun
HuiJun merged commit 341aa21 into develop Oct 1, 2026
44 of 46 checks passed
@HuiJun
HuiJun deleted the fix/758-nonunique-composites branch October 1, 2026 18:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Example parser_features_demo_messages_events.sysml declares nonunique messages that subset a unique feature

1 participant