fix(check): conformance of an implicit subsetting (#726)

[someshSandbox]

Fixes #726.

validateSubsettingUniquenessConformance is a constraint on a Subsetting, and an implied Subsetting is a Subsetting too. Model.ConformanceViolations checked only the written :>/:>> relationships, so a feature that implicitly subsets a unique library feature could be declared nonunique unnoticed.

model	develop	this PR
action def A { action b[*] nonunique; } (implicitly subsets Actions::Action::subactions, Action[0..*], unique)	no errors	3:9: error: Subsetting/redefining feature cannot be nonunique if subsetted/redefined feature is unique
action def A { action b[*] nonunique :> subactions; }	that error at :> subactions	the same, once
part def A { part b[*] nonunique; } (implicitly subsets Items::Item::subitems, Item[0..*], unique)	no errors	the same error at the declaration
abstract flow def F; part def C { message m : F[*] nonunique; } (a message is an action; in a part it implicitly subsets Parts::Part::ownedActions, Action[0..*], unique)	no errors	the same error at the declaration
action def A { action b[*]; }, part def A { ref part b[*] nonunique; }, part def A { attribute b[*] nonunique; }	no errors	no errors

Change:

• ConformanceViolations also runs the restriction checks (uniqueness, and constancy with it) against each feature ImplicitSubsettings gives the usage. The finding is at the declaration, since nothing is written to point at.
• A feature the usage already subsets or redefines explicitly is checked once, at the written reference.
• validation-constraints.md records the implicit case.
• tests/migrate: a SysML v1 composite property with isUnique="false" still migrates as written, to part n : A[2] nonunique; in a part. That part implicitly subsets Item::subitems, so TestCollectionModifiersAreWritten now expects that one uniqueness finding at n, where it expected none.
• examples/parser_features_demo_messages_events.sysml declares its two messages in MessageChannel nonunique, which the constraint forbids, since a message in a part implicitly subsets the unique Part::ownedActions. The example is left as it is, so the pilot-differential baseline's examples digest doesn't move, and it is listed in examplesKnownFailures with that reason. Fixing the example and re-recording the baseline is Example parser_features_demo_messages_events.sysml declares nonunique messages that subset a unique feature #758.

Tests:

• passes/w8b_redefinition_conformance_test.go:TestW8BUniquenessConformanceOfAnImplicitSubsetting covers every row above.
• internal/semantic/..., internal/check/..., internal/exec/runtime/..., internal/translate/..., tests/corpus/..., tests/export/..., tests/identity/..., internal/frontend/grpc/..., internal/workspace/... and cmd/sysml/... pass. The bundled library raises no new finding, and the one example that does is listed above.

🤖 Generated with Claude Code

[devin-ai-integration]

Note

Newer findings are available below. Devin Review posted a newer report on this PR, in addition to the findings presented here.

🔍 Devin Review: 1 flag

Not posted on this PR by your GitHub settings — view it in Devin Review. (Configure)

[devin-ai-integration]

Devin Review found 1 new potential issue.

⚠️ 1 issue in files not directly in the diff

⚠️ Shipped messages demo fails validation

Both nonunique messages implicitly subset the unique Part::ownedActions, so -validate rejects the shipped demo. The examplesKnownFailures entry only suppresses the test failure.

1 flag not posted on this PR by your GitHub settings — view it in Devin Review. (Configure)

[HuiJun]

This one took a bit of review, especially when this points out a gap in the pilot implementation. After review, I think I agree with you on this, though #758 would only fix the test. We'll have to update some migration mapping as well. Thanks Somesh!