Skip to content

fix(instance): a refined subcomponent replaces the one it refines, as OSATE does (#496) - #517

Merged
avrabe merged 3 commits into
mainfrom
fix/refined-subcomponent-496
Oct 27, 2026
Merged

avrabe merged 3 commits into
mainfrom
fix/refined-subcomponent-496

Conversation

@avrabe

@avrabe avrabe commented Oct 22, 2026

Copy link
Copy Markdown
Contributor

hw : refined to system platform.single in an extending implementation
instantiated BESIDE the inherited hw : system platform instead of
replacing it. On main, DigitalControlSystem DCS.dualtier2 has three app
and three hw, one per extends level, where OSATE's own instance model
has one of each. 61 of the 2086 corpus files refine a subcomponent. Every
analysis that walks children saw the phantoms, and REQ-AADL-REF-CONTEXT-001
needed a resolver allowance to step around them.

Semantics, from OSATE source at osate2 @ 87468992:

  • ComponentImplementationOperations.getAllSubcomponents removes the
    refined original and appends the refinement, which takes the end
    position;
  • SubcomponentImpl.getAllClassifier: a refinement without a classifier
    keeps the original's;
  • SubcomponentImpl.getPropertyValueInternal: the refinement's values,
    then each refined original's, the first found winning.

collect_impl_chain_recursive now does the first two. The builder records
each refinement's refined-away originals, and one helper,
push_subcomponent_associations, used by all three property-map builders,
applies the originals' associations before the refinement's own.

Oracles:

  • OSATE instance models (test-data/osate2/instances, 11 *.aaxl2),
    comparing component counts: main matches 7 of 11 and DCS.dualtier2 has
    6 against OSATE's 2. The fix matches 8 of 11 and DCS.dualtier2 has 2.
    The other three rows are unchanged and out of scope.
  • unit tests: replacement (one hw, classified Plat.single, with its
    cpu); inherited and overriding properties; a refinement without a
    classifier keeps the original's. Hand mutants (no replacement, a plain
    replace without the property chain, no classifier fallback) are all
    caught.
  • corpus, main b883cac vs this build: the 61 refining files plus 15
    controls, 285 runs, 283 instantiating, 106 differing, every line
    classified. Removed: 264 subcomponent_rules, 112 completeness and 66
    binding_rules ERRORs plus their warnings, all from the phantoms. Added
    ERRORs are confined to two models. resourcebudgets: deadline misses and
    overloads that are TRUE findings from its own timing (47 ms / 20 ms =
    235% on hw.cpu; 34/20 = 170% on pc2), masked while the phantoms broke
    resolution. CasePositionControl: "not computed" becomes a below-minimum
    ERROR on an incomplete best case, filed as Latency below-minimum Error fires on an incomplete best case (components without timing) — '0.000 ms is below the declared minimum' asserted from missing data #516. weight_power on
    resourcebudgets SCS: 3.20 kg becomes 1.70 kg, because the phantoms were
    weighed twice.
  • workspace: 3334 passed, 0 failed.

The resolver's latest-first same-name sibling allowance (#497) is
removed. With it still in place, every test passed under a first-match
walk, so nothing exercised it once phantoms stopped existing. Its test
now checks that a reference resolves THROUGH a refinement, and
REQ-AADL-REF-CONTEXT-001's text is corrected.

rivet: REQ-AADL-SUBCOMPONENT-REFINE-001 (v0.47.0, verified), traces-to
REQ-AADL-REF-CONTEXT-001.

NOT CLAIMED: refined connections, flows or features; in_modes and
array-dimension inheritance across a refinement; a diagnostic for a
non-refined same-name redeclaration (still appended, as before);
SCS.Phys's component count, which is lower than OSATE's.

Refs #496, #516

🤖 Generated with Claude Code

https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z

@avrabe

avrabe commented Oct 22, 2026

Copy link
Copy Markdown
Contributor Author

Count correction: 107 runs differ, not 106. One run, multi-core/arinc653-p4080.aadl arinc_example.error, contains a NUL from #507's wrpc message (fixed in #518), so diff -r reported it as Binary files … differ and my header count missed it. Read with diff -a, it is the same phantom-removal class as the rest: the duplicate cpu and its diagnostics are gone, 13 → 12 components. The added-ERROR classification is unchanged.

@github-actions

Copy link
Copy Markdown

Rivet verification gate

✅ 20/20 passed

count
Passed 20
Failed 0
Skipped (no steps) 0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.

@codecov

codecov Bot commented Oct 22, 2026 •

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 99.25373% with 1 line in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/spar-hir-def/src/instance.rs 99.24% 1 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe
avrabe force-pushed the fix/refined-subcomponent-496 branch 3 times, most recently from 9eeac77 to 6a14860 Compare October 27, 2026 05:52
avrabe added a commit that referenced this pull request Oct 27, 2026
…ps turning every mutant unviable (#400) (#524)

#522's per-PR gate ran `cargo mutants --in-diff` under the workflow-wide
RUSTFLAGS "-D warnings". A mutant that replaces a function body leaves
its parameters unused, and -D warnings makes that a compile error
("unused variable: `inst`"). On #517 all 9 selected mutants were
therefore UNVIABLE, nothing was caught, and the gate's "none caught"
rule failed the PR with no test ever having run. Same diff measured
locally under RUSTFLAGS="-D warnings": 9 unviable, reproduced exactly.

`--cap-lints=true` makes cargo-mutants cap lint levels for mutated
builds. Same diff, same RUSTFLAGS, with the flag: 9 selected, 6 caught,
3 unviable, 0 missed, matching the local run without -D warnings.

Only the in-diff step changes. The full-crate run keeps -D warnings,
because its 292 ratchet was measured under it and capping would change
which mutants compile.

The "none caught → FAIL" rule did its job here. It refused to read "0
missed" from a run in which no test executed.

Refs #400, #496


Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
avrabe and others added 3 commits October 27, 2026 20:47
…heriting its classifier and property values as OSATE does (#496)

`hw : refined to system platform.single` in an extending implementation
instantiated BESIDE the inherited `hw : system platform` instead of
replacing it. On main, DigitalControlSystem DCS.dualtier2 has three `app`
and three `hw`, one per extends level, where OSATE's own instance model
has one of each. 61 of the 2086 corpus files refine a subcomponent. Every
analysis that walks children saw the phantoms, and REQ-AADL-REF-CONTEXT-001
needed a resolver allowance to step around them.

Semantics, from OSATE source at osate2 @ 87468992:
- ComponentImplementationOperations.getAllSubcomponents removes the
  refined original and appends the refinement, which takes the end
  position;
- SubcomponentImpl.getAllClassifier: a refinement without a classifier
  keeps the original's;
- SubcomponentImpl.getPropertyValueInternal: the refinement's values,
  then each refined original's, the first found winning.

collect_impl_chain_recursive now does the first two. The builder records
each refinement's refined-away originals, and one helper,
push_subcomponent_associations, used by all three property-map builders,
applies the originals' associations before the refinement's own.

Oracles:
- OSATE instance models (test-data/osate2/instances, 11 *.aaxl2),
  comparing component counts: main matches 7 of 11 and DCS.dualtier2 has
  6 against OSATE's 2. The fix matches 8 of 11 and DCS.dualtier2 has 2.
  The other three rows are unchanged and out of scope.
- unit tests: replacement (one hw, classified Plat.single, with its
  cpu); inherited and overriding properties; a refinement without a
  classifier keeps the original's. Hand mutants (no replacement, a plain
  replace without the property chain, no classifier fallback) are all
  caught.
- corpus, main b883cac vs this build: the 61 refining files plus 15
  controls, 285 runs, 283 instantiating, 106 differing, every line
  classified. Removed: 264 subcomponent_rules, 112 completeness and 66
  binding_rules ERRORs plus their warnings, all from the phantoms. Added
  ERRORs are confined to two models. resourcebudgets: deadline misses and
  overloads that are TRUE findings from its own timing (47 ms / 20 ms =
  235% on hw.cpu; 34/20 = 170% on pc2), masked while the phantoms broke
  resolution. CasePositionControl: "not computed" becomes a below-minimum
  ERROR on an incomplete best case, filed as #516. weight_power on
  resourcebudgets SCS: 3.20 kg becomes 1.70 kg, because the phantoms were
  weighed twice.
- workspace: 3334 passed, 0 failed.

The resolver's latest-first same-name sibling allowance (#497) is
removed. With it still in place, every test passed under a first-match
walk, so nothing exercised it once phantoms stopped existing. Its test
now checks that a reference resolves THROUGH a refinement, and
REQ-AADL-REF-CONTEXT-001's text is corrected.

rivet: REQ-AADL-SUBCOMPONENT-REFINE-001 (v0.47.0, verified), traces-to
REQ-AADL-REF-CONTEXT-001.

NOT CLAIMED: refined connections, flows or features; in_modes and
array-dimension inheritance across a refinement; a diagnostic for a
non-refined same-name redeclaration (still appended, as before);
SCS.Phys's component count, which is lower than OSATE's.

Refs #496, #516

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z
… associations (#496)

The in-diff mutation gate from #400 (run locally, cargo-mutants 27.1.0,
workspace test scope) found one survivor on this PR:
`build_anon_property_map` replaced with `()`. This PR routed it
through push_subcomponent_associations, and no test gave a property
to a subcomponent that names no classifier (`x : system { Code_Size =>
4 KByte; };`). The test pins that the property reaches the instance.
Re-run of the in-diff gate: 11 selected, 6 caught, 5 unviable,
0 missed.

Refs #496, #400

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z
… walk (spar#517)

#496 is fixed, so walk_children no longer tries every same-named child
latest-first — it takes the first match, which is all a legal model needs
(sibling names are unique). total_load_counts_only_threads_on_the_target_itself
built a synthetic instance with two processors both named "cpu" and relied on
the old latest-first walk to bind t2 to the second one. List cpu_b first so
the first-match walk binds t2 to it; the test's purpose is unchanged — two
same-named processors, t2 on one, t1 moved to the other, and the load counts
only t1 by identity.

spar-solver: 70/70 lib tests pass; spar-hir-def: 494/494; fmt clean.
@avrabe
avrabe force-pushed the fix/refined-subcomponent-496 branch from 6a14860 to faad797 Compare October 27, 2026 19:47
@avrabe
avrabe merged commit bdd0366 into main Oct 27, 2026
22 checks passed
@avrabe
avrabe deleted the fix/refined-subcomponent-496 branch October 27, 2026 21:47
@avrabe avrabe mentioned this pull request Oct 27, 2026
avrabe added a commit that referenced this pull request Oct 27, 2026
* chore(release): scope v0.47.0 — the property-semantics release; defer nine unstarted requirements to v0.48.0

DEC-RELEASE-V047-SCOPE-001 (accepted). v0.47.0 ships how AADL property
values are found and applied: references resolve from their declarer
(REF-CONTEXT), inline connection properties reach the instance
(CONNECTION-INLINE-PROPS), and every analysis resolves a binding by
identity (BINDING-CONSUMERS-001). The refined-subcomponent fix
(SUBCOMPONENT-REFINE, #517) and property inheritance (PROPERTY-INHERIT)
join if verified before the cut. Guard and robustness fixes also ship.

- REQ-AADL-BINDING-CONSUMERS-001 -> verified, its scope reduced to the
  consumers merged in #500, #503, #505, #506, #507/#518, #509, #511 and
  #514. Three remain as REQ-AADL-BINDING-CONSUMERS-002 (v0.48.0):
  ARINC 653 partitions (blocked on #504), move-ranking response time
  (RTA message text), and per-connection bus bindings in bus_bandwidth.
- Nine requirements that were never started move to v0.48.0: render x3,
  TSN CLI/YANG, SysML2 flows/modes, findings layer, DBC cycle time,
  claim ledger.
- REQ-CI-MUTANTS-IN-DIFF-001 had lost its `release: v0.47.0` on main,
  for a reason not established; it is restored here.

Refs #498, #460, #400

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z

* chore(release): move property inheritance to v0.47.1, beside the Priority-order fix it depends on

REQ-AADL-PROPERTY-INHERIT-001 is implemented and independently verified
(#527), but binding threads makes RTA reachable on models where spar
orders Priority backwards (#526). It ships with that fix in v0.47.1.
Recorded in DEC-RELEASE-V047-SCOPE-001.

Refs #460, #526

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z

* chore(release): v0.47.0 — promote REQ-CI-MUTANTS-IN-DIFF-001 on CI evidence and bump to 0.47.0

The v0.47.0 scope (DEC-RELEASE-V047-SCOPE-001) is now all verified, 8 of 8:
REF-CONTEXT, SUBCOMPONENT-REFINE, BINDING-CONSUMERS-001,
CONNECTION-INLINE-PROPS, SOM-COUNT-CHECKED, WCTT-PMOO-SKIP-VISIBLE,
CLOSING-KEYWORD-CROSSLINE, CI-MUTANTS-IN-DIFF.

REQ-CI-MUTANTS-IN-DIFF-001 is promoted on the PR-path run of #517 (run
40572309089): 9 selected over 249 changed lines, 6 caught, 3 unviable,
0 missed. That is the first nonzero selection observed in CI, and it
matches the local measurement on the same tree.

Version 0.46.0 -> 0.47.0 in Cargo.toml, Cargo.lock (workspace members
only, `cargo update -w --offline`) and vscode-spar/package.json;
`spar --version` prints `spar 0.47.0`.

Refs #460, #496, #498, #400

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
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.

1 participant