feat(runtime): apply nested redefinition chains below composite features - #634
Merged
Merged
Conversation
A chain redefinition written as a member of a type or usage (attribute :>> mid.leaf.value = 99.0;) now applies below every composite feature the chain walks, exactly as the nested-body form does: declared values (= and default =), types, multiplicities and redefining bodies, evaluated in the declaring body's scope, per element of a multi-valued intermediate. A redefinition the object's own type declares wins over a chain reaching the same feature, and a chain crossing a ref, port or subject owns nothing below it and is never applied. Each chain is reported as a nonstandard-semantics warning (an error in strict mode, and in every mode when the chain crosses a reference): the pinned pilot accepts the notation but applies no redefinition below the first segment. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
…definition change The self-model edit moved the examples/ input digest, and the new nonstandard-semantics warnings account for every added openSysMLOnly finding; no other movement. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…tion Re-recording the baseline moved the headline counts (344 fully agreeing, 46 only ours); regenerate the gated doc-count lines and update the quoted figures and the adjudication record to match. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Order the chains reaching one feature most-specific first — the tails carried down, then each type before its member sources — and let the first win rather than the last. Carry an object's pending tails through a held image so a member materialized after the restore is redefined all the same. When a classifier is added to an object, apply its nested redefinitions to the children already materialized, refining their feature values as the classifier's direct features do. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…d's own redefinition A redefined member shares one feature value under every name it reads as, so a chain's first segment matches any name of the value being materialized, not only the name read. And a child's own redefinition wins over a chain a classifier applies to it, the same precedence the materialize path gives it. Co-Authored-By: jason.han <hanhuijun@gmail.com>
6 tasks
… extension The feature chain in a redefinition target parses to a feature hosting the chain, and the host is redefinable (KerML 1.0 §7.3.4, §8.3.3.3): applying it below the chain's segments is the specification's reading, which the pinned pilot evaluator simply does not implement. Drop the nonstandard-semantics advisory and its strict escalation, name the through-reference error redefinition-through-reference, and restore the corpora ratchet, differential baseline and quoted figures the advisory had moved. Co-Authored-By: jason.han <hanhuijun@gmail.com>
… and stay within owned objects A chain counts as a redefinition written in the body declaring it, so it ranks exactly as the nested-body form does: a redefinition declared by the chain's context or a type specializing it wins, and the child's own type's redefinition, a base type's chain and unrelated bodies lose. The classify path decides by the same rule before installing the feature, and it refines only objects the owner holds — a reference, port or subject's is not the owner's to redefine. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ing object Co-Authored-By: jason.han <hanhuijun@gmail.com>
6 tasks
…as a body does Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ank its value among aliases Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ning feature Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…baseline Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ery alias of a bound part Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…efinition Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # internal/exec/runtime/classify_test.go # internal/semantic/semantics/model.go
…ge governed features Co-Authored-By: jason.han <hanhuijun@gmail.com>
…r chains Co-Authored-By: jason.han <hanhuijun@gmail.com>
…typed parameters Co-Authored-By: jason.han <hanhuijun@gmail.com>
…efinition Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/pilot-differential-baseline.json
…feature Co-Authored-By: jason.han <hanhuijun@gmail.com>
…he develop merge Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
6 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What and why
A chain redefinition written on a usage —
part top : Top { attribute :>> mid.leaf.value = 99.0; }— is legal SysML v2 and resolves cleanly, but neither the pinned pilot nor OpenSysML gave it any effect:top.mid.leaf.valuestill read the definition default. Modelers were writing the shorthand and silently getting nothing. Only the nested-body formpart :>> mid { part :>> leaf { attribute :>> value = 99.0; } }worked.This makes the shorthand behave exactly like the nested-body form:
semantics.NestedRedefinitionsOf(sym)(side table) lists the members ofsymwhose:>>target is a ≥2-segment feature chain that resolves.materialize(sym, id, owner, feature)creates a nested object, it collects the chains ofowner's types (and their member sources) whose first segment isfeature(or any alias sharing its*FeatureValue), plus tails carried onowner. A one-segment tail replaces that feature'sEffectiveFeatureon a cloned shape witheffectiveFeature(name, redefiningMember, sym)— so value (=/default =), declared type, multiplicity and a redefining body all take effect andCompositeTypeOfpicks them up unchanged; longer tails are stored onInstance.nestedand applied when the next level materializes.materializeMembersgoes through the same path, so a multi-valued intermediate (:>> wheels.radius) applies per element.redefinitionContext: the enclosing definition, or the topmost usage). Between chains, a chain whose context specializes another's wins (so a classifierSport :> Baseadded later beatsBase's chain, for children materialized before or after the classification); carried tails and unrelated contexts keep first-wins. Against a standard redefinition already standing on the feature, the chain yields only when that redefinition's context conforms to the chain's — the same body, or a subtype's nested body (blocksChain); the child's type's own:>>and bodies in types the chain owner specializes lose, as they do topart :>> wheel { :>> radius = 3.0 }.classify) applies the new classifier's chains to already-materialized descendants transactionally (installFeatureValue) and leaves them pending for lazy ones; it only walks objects the parent owns, so a populatedref/port/subject never has its target mutated. Held images (Image/Restore) round-tripInstance.nested.part :>> mid = existing; attribute :>> mid.leaf.value = 99.0;) is rejected with the existingErrValuedFeatureRestated; a valued chain from a body that specializes the binding's (Top { part mid : Mid = existing; },Sport :> Top { attribute :>> mid.leaf.value = 99.0; }) governs the inherited binding —EffectiveFeature.GovernedByChainmakesvalueBindsfalse, so a fresh object is materialized (also on classify) and the bound object is never touched; a chain declaring only a type or multiplicity conflicts with nothing.DefaultDecl= the redefining member), so:>> mid.leaf.value = factor * 2.0readsfactorfromTop, as the nested-body form does.NestedRedefinitionPassreports an error,redefinition-through-reference, when a non-final segment is aref/port/subject — there is no owned object to redefine below it, so the chain would silently not apply. A plain chain gets no diagnostic.=vsdefault =fixed-binding rule is unchanged and still applies to the chain's last feature.Specification basis
A feature chain in a redefinition target parses to a feature that hosts the chain; the chain determines the host's featuring type (first segment) and featured type (last segment), and the host is redefinable — KerML 1.0 §7.3.4 (feature chains) and §8.3.3.3 (redefinition), as confirmed with the spec lead. Applying the redefinition below the chain is therefore the specification's reading, recorded as ✅ Faithful in
docs/project/spec-compliance.md(redefinition section) and described under "Chain redefinitions" indocs/reference/grammar/conformance-audit.md. The pinned pilot evaluator (0.62.0) accepts the notation but reads the original value; that is noted as a pilot-evaluator gap indocs/project/pilot-differential.md. No corpus ratchet or differential baseline moves.How it was verified
nested_redefinition_chain(3- and 2-level chains, chain with a body, outer-scope value, collection intermediate),nested_redefinition_chain_equiv(shorthand and nested-body forms read identically) andnested_redefinition_precedence(subtype over base, carried over intermediate).TestRuntimeRobustnessNestedRedefinition: chain through arefevaluates to the default without panic; unresolvable chain returnsErrNoSuchFeature; chain below a value-bound feature returnsErrValuedFeatureRestatedand leaves the bound object untouched.NestedRedefinitionsOf(1-level excluded, 2/3-level included, unresolved excluded), the pass (ref error; silent on plain chains and the standard forms, in default and strict mode), aliased names in both read orders, held-image round-trip of pending tails, and classify: chains reach materialized and lazy children, a later classifier's chain outranks the base type's (both read orders), the chain outranks the child's type's own redefinition while a subtype's nested body keeps its value, and a chain through arefleaves the referenced object alone.bin/sysmlREPL (recording in the session): shorthand and nested-body forms both → 99.0 / 4.0, outer-scope expression → 14.0, collection →[0.4, 0.4], 4-level chain, inherited chains, fixed-binding protection, ref/port/subject errors.gofmt -l .,go vet ./...,make lint,make docs-check,go test ./...all clean.Checklist
make testandmake lintpass locallychanges/unreleased/<slug>.<section>.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (compliance rows need nothing: the census is counted at docs build)F4,K5) in the body, docs, or changelogLink to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/14f60f720c2d4586b28ed46025fa9f83
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/14f60f720c2d4586b28ed46025fa9f83?variant=devin
Requested by: @HuiJun