[devin-ai-integration]

What and why

KerML §7.3.4 implicit specialization is a property of every type and feature, but the runtime derived the Kernel/library memberships of an object only from the features of its shape (its user-declared type), and only through implicit subsettings of non-library features. Performances the executor itself creates from library actions — the anonymous LoopAction node, each iteration body, the start/done shots — therefore lacked the memberships the Kernel library derives for them: k.loopy.loops#(1).enclosedPerformances read [] and timeEnclosedOccurrences omitted the bodies.

Measured on develop (0cf906f3d) for the reproducer perform action loopy { … loop action body { … } until n >= 3; … }:

object	member	develop	now
loop node	enclosedPerformances	missing []	the 3 bodies
loop node	timeEnclosedOccurrences	missing [loop, start, done]	[loop, body×3, start, done]
loop node	subperformances, suboccurrences	fine []	[] (body is not composite)
loop node	snapshots	fine	unchanged
body	enclosedPerformances, subperformances, suboccurrences	fine [inc]	unchanged
body	snapshots, timeSlices, superoccurrence	fine	unchanged
shots (start/done)	timeEnclosedOccurrences, snapshots, portions	fine	unchanged
performed action loopy	enclosedPerformances, subperformances, timeEnclosedOccurrences	fine [loop]	unchanged
performed action's start	timeEnclosedOccurrences, portions	fine	unchanged

Root causes, each fixed generally (no name or loop special-casing):

1. runtime/kernel_collections.go shapeSubsettersOf walked only the shape features; a member the object holds outside its shape (a library parameter the run filled, such as LoopAction::body) now contributes like any other subsetter.
2. runtime/subsetting.go subsetsTransitively/implicitSubsettingNames skipped every library-tier feature, so an implicit subsetting a library feature states (LoopAction::body is a step of a Performance, hence :> enclosedPerformances) was never followed.
3. semantics/nested.go nestedRuleFQN gave a non-composite step no implicit subsetting at all; per the pilot (isBehaviorOwnedComposite → subperformances, else isBehaviorOwned → enclosedPerformances) a composite step is a subperformance and a non-composite one (ref action, a parameter such as body) an enclosed performance. Compositeness of a KerML feature is its declaration's; of a SysML usage its kind's (usageIsComposite, which now also knows a body parameter is not composite).
4. semantics/roles.go: a state's entry/do/exit action redefines States::StateAction::entryAction/doAction/exitAction by its role (SysML checkActionUsageStateActionRedefinition; the pilot's isComputeRedefinitions "for state and transition actions, always add implicit redefinition"), so the state's entryAction and its declared entry action are one performance instead of two. This surfaced once the StateAction subactions entered subperformances.
5. runtime/shape.go implicitFeatureBases: a feature redefining an item (ShapeItems item :>> vertices) holds Items as well as what its type says, so the Geometry library's subitems now derive their edges and vertices.

Specification basis

KerML 1.0 §7.3.4 (implicit specialization), Performances.kerml (enclosedPerformances :> timeEnclosedOccurrences, subperformances :> enclosedPerformances), Occurrences.kerml; KerML checkStepEnclosedPerformanceSpecialization; SysML v2 checkActionUsageStateActionRedefinition; SysML.xtext UsagePrefix (ref before use case). New row in docs/project/spec-compliance.md (after the nested-usage implicit-subsetting row).

Behaviour changes

• A loop's enclosedPerformances/timeEnclosedOccurrences list its iteration bodies; its subperformances/suboccurrences stay empty.
• A ref action owned by a behavior is one of its enclosedPerformances (semantics/nested_test.go:TestImplicitSubsettingsRefStep previously asserted none — stricter than the spec and the pilot).
• A state's entry/exit action is a subperformance of the state but not one of its subactions (States.sysml action :>> subactions :> middle; StatePerformances.kerml entry then middle then exit, do :> middle; the pilot's isActionOwnedComposite excludes isEntryExitAction): semantics/nested.go NestedUsage.EntryExitAction sends such an action to the step fallback (subperformance) instead of Actions::Action::subactions. sm.subactions: develop [en], 738defa [en, doAction, exitAction], now [doAction]; sm.subperformances/enclosedPerformances: develop [en], 738defa and now [en, doAction, exitAction]; sm.middle <undetermined> throughout (an abstract [1..*] step no value binds). Pinned by k.smSubactionCount = 1, k.smSubperformanceCount = 3, k.smSubactionIsDoAction.
• A state's entryAction/doAction/exitAction is the declared entry/do/exit action, and the library name stays resolvable beside it: semantics/roles.go splits ImplicitRoleRedefinitions into libraryRoleRedefinitions (state actions, a view's render; identity at run time, no masking) and caseRoleRedefinitions (subject/objective/actor/stakeholder; masked by masking.go maskingRedefinedFeatures as on develop — TradeStudy objective evaluation depends on it). The pinned pilot validator resolves sm.entryAction beside entry action en; pinned by k.entryActionIsEn in the conformance fixture.
• Library subitems derive their library-declared members: a Rectangle's edges and vertices, an Ellipsoid's faces, a SpatialItem's originPoint; Box.subitems now reports the same unresolved tflv binding Box.vertices already reported (pinned in instance_library_geometry_box). Reading a Box in full now costs more than the 1000 feature-value reads maxMaterializeBudget allowed (its 8 vertices, 12 edges and 6 faces each carry their Item collections: 80 objects); the budget -instantiate and -validate walk under is 4000, which reads both box fixtures to the end (materialization: {} stays a complete, clean read) — a recursive type is still cut by maxMaterializeDepth and the on-path rule (instance_validate_bounded unchanged).
• checkedConstraints of a view lists its viewpointConformance requirement.
• A ref use case written in a body is a reference usage: the body-member parser applied a ref before a one-word kind keyword only, so part def A { ref use case x; } was composite (one of the part's ownedActions, so refused nonunique); the top-level form already kept the ref. The standard library's UseCase::self/start/done/includedUseCases are the ref use cases they are written as (stdlib snapshot regenerated), pinned by parser/ref_use_case_test.go.
• semantics.ImplicitSubsettingCandidates (what the v1 migrator consults before writing nonunique) follows the same compositeness rule as the model: a non-composite step in a part, item or port owner subsets nothing; in a performance or occurrence owner enclosedPerformances. The migrator's owner table judged a v1 «Viewpoint» as a viewpoint def while writing it as a view def; it now judges the view def it writes (migrate/uniqueness_test.go:TestImplicitlyUniqueAgreesWithTheChecker, which caught both).

Golden movement (every row)

• kernel_member_reads_running/state_machine.golden (9 rows): enclosedPerformances, suboccurrences, subperformances of sm at three points gain the StateAction doAction/exitAction performances the runtime materializes for a state declaring no do/exit (they existed before — sm.doAction was readable on develop — and are now listed where subactions :> subperformances puts them).
• kernel_member_reads.golden (4 rows): enclosedPerformances/suboccurrences/subperformances empty → collection of 3; predecessors 11 → 13 (the same objects).
• docs/project/library-and-prefix-sweep-outcomes.txt (9 rows): vw1/vwq/Vw1().checkedConstraints empty → the viewpointConformance object; sph.subitems → its face; spat.subitems +originPoint; box.subitems → the tflv binding error; st/es/S1().subactions empty → the three StateAction default performances.
• docs/project/library-and-prefix-sweep-outcomes.txt (3 more rows, entry/exit fix): p1.st/p1.es/S1().subactions collection(3) [entryAction, doAction, exitAction] → collection(1) [doAction]; state_machine.golden and kernel_member_reads.golden do not move (they list sub-/enclosedPerformances, which keep all three).
• library_shape_test.go:TestInheritedLibraryFeaturesMaterializeNoObjects no longer reads subitems of a Box: the library itself puts the box's faces in it.

Cost

10 000-iteration loop, 3 runs each: develop 0.68/0.91/0.87 s, 202–216 MB RSS; this branch 0.65/0.91/1.03 s, 204–214 MB RSS — within noise, no new per-iteration path (the held-member walk is per read, over the object's own feature values).

Follow-ups (not this PR)

• A case's u.subj beside subject s is unresolved (as on develop) while the pilot validator resolves it; un-masking case roles breaks TradeStudy objective evaluation (tradeStudyObjective: require condition … evaluationFunction has no return expression), so the evaluator's objective lookup must stop relying on masking first.

• The on-disk library index cache (libs/cache.go) served records derived by an earlier local build: with the same source, a binary built in the main tree resolved u.subj (no masking, from an experiment build) until ~/.cache/sysml-ls was cleared, while a worktree build of the same commit refused it. The key carries a build identity meant to prevent exactly this (buildid.go: clean revision, else executable size and mtime), so the stale hit needs a reproducer and a fix of its own.

• A state declaring no do/exit still materializes a default doAction/exitAction performance; the pilot holds none for an unset [0..1].

How it was verified

• conformance implicit_specialization_runtime_objects (loop node, bodies, shots, a Rectangle's subitems), robustness_implicit_specialization_test.go:TestRuntimeRobustnessImplicitSpecialization (reading the derived collections creates no objects under a tight object bound; a state's entry/do action is its entryAction/doAction)
• TestKernelLibraryMembersReadableWhileRunning, TestKernelLibraryMembersReadable, TestLibraryAndPrefixSweep re-recorded as accounted above
• Tim's model OccurrencesTest::p1.v and new OccurrencesTest::P1().v both still 2
• Gates run locally on the final head: go build ./..., go vet ./..., gofmt -l . (empty), make lint (staticcheck + gosec pass), go test ./internal/exec/runtime/... (ok), go test -count=1 -timeout 30m ./cmd/sysml/... alone (ok), go test ./tests/corpus/... with the training, pilot, spec-example and PSSM corpora downloaded and their OPENSYSML_REQUIRE_* set (ok), tests/identity with the pilot library XMI (ok), internal/exec/smt (ok), the parser, semantics, check, migrate, libs and ir packages (ok), python3 scripts/changelog.py check, python3 scripts/check-doc-ids.py
• TestEmbeddedSnapshotIsCurrent/TestSnapshotIndexMatchesFreshLoad pass against the regenerated stdlib snapshot

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

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/d3ecda1e7b624c9facc77be02738785c
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/d3ecda1e7b624c9facc77be02738785c?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

[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 found 1 potential issue.

⚠️ 1 issue in files not directly in the diff

⚠️ Box materialization checks accept incomplete walks

For the box fixtures, bounded: true accepts materialization checks that stop at the read budget. Errors in unread values can now go undetected.

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

[devin-ai-integration]

Re the Devin Review finding on instance_library_geometry_box.expected.json (bounded: true accepting an incomplete walk): agreed, it recorded a stopped walk, not a contract. Fixed in 8a44a9a — a Box's 8 vertices, 12 edges and 6 faces now each carry their Item collections (80 objects), more than the 1000 feature-value reads maxMaterializeBudget allowed, so the walk stopped with values unread. The budget -instantiate and -validate walk under is now 4000; both box fixtures read to the end again (materialization: {}, a complete clean read), and a recursive type is still cut by maxMaterializeDepth and the on-path rule (instance_validate_bounded unchanged). Runtime and cmd/sysml suites pass.

[devin-ai-integration]

738defa fixes a regression this PR had introduced at 8a44a9a: the new role redefinition of a state's entry/do/exit action onto States::StateAction::entryAction/doAction/exitAction had entered maskingRedefinedFeatures, so a static read of sm.entryAction beside entry action en became unresolved member: entryAction — develop resolves it (sm.entryAction->size() = 1), 8a44a9a refused it, and now it resolves again (= 1), as the pinned pilot validator accepts the same model with no diagnostic. semantics/roles.go now splits ImplicitRoleRedefinitions into libraryRoleRedefinitions (state actions, a view's render: run-time identity, sm.entryAction == sm.en, no name masking) and caseRoleRedefinitions (subject/objective/actor/stakeholder: masked exactly as on develop, which TradeStudy objective evaluation depends on), and masking.go masks only the latter. The conformance fixture implicit_specialization_runtime_objects gains an exhibit state sm { entry action en {} then idle; state idle; } and the slot k.entryActionIsEn = true pinning both the resolution and the identity. Unchanged and not this PR: sm.subactions/subperformances listing the doAction/exitAction performances the runtime still materializes for an undeclared [0..1] state action is the first follow-up in the description.

[devin-ai-integration]

2573e8d corrects sm.subactions. The library says StateAction::subactions :>> subactions :> middle (States.sysml) with entry then middle then exit and do :> middle (StatePerformances.kerml), and the pilot's UsageAdapter.isActionOwnedComposite excludes isEntryExitAction, so a state's entry/exit action is a subperformance of the state but not one of its subactions. semantics/nested.go marks such a usage NestedUsage.EntryExitAction and sends it to the step fallback (subperformances) instead of Actions::Action::subactions. For state def SM { entry action en {} then s1; state s1; }:

member	develop	738defa	now
sm.subactions	[en]	[en, doAction, exitAction]	[doAction]
sm.subperformances	[en]	[en, doAction, exitAction]	[en, doAction, exitAction]
sm.enclosedPerformances	[en]	[en, doAction, exitAction]	[en, doAction, exitAction]
sm.middle	<undetermined>	<undetermined>	<undetermined>

Golden movement: docs/project/library-and-prefix-sweep-outcomes.txt, 3 rows (Probe::p1.st, Probe::p1.es, new Probe::S1() .subactions: collection(3) [entryAction, doAction, exitAction] → collection(1) [doAction]); state_machine.golden and kernel_member_reads.golden do not move (they list sub-/enclosedPerformances, which keep all three). The conformance fixture gains k.smSubactionCount = 1, k.smSubperformanceCount = 3 and k.smSubactionIsDoAction = true. That [doAction] is a default performance for an undeclared [0..1] do remains the first follow-up in the description, not this PR.