Pass 1 (harness alignment) + Pass 4 (Chapters 1-10 didactic content) - #20
Merged
Merged
Conversation
Content push-back from independent review (Opus 5.5, round 2). Text-only fix to DEFERRED.md/decisions/gap-issue-drafts.md plus two small notebook prose fixes; no model or notebook construct change. F1 (blocking): SysML v2.0 formal/2026-03-02 section 7.6.3 was cited backwards. Its tighter [1..1] default applies only to a usage declared with a kind keyword (attribute usage, item usage, port usage); `in bread : Bread;` has none, so per the grammar it is a DefaultReferenceUsage : ReferenceUsage (section 8.2.2.6.3), and section 7.6.4 defines a reference usage as exactly "a usage that is declared without any kind keyword." So bread/energy/duration do not meet section 7.6.3's condition for [1..1]; the spec's own default is the general, unbounded [0..*] (KerML 1.1 Beta 2 agrees). Rewrote both documents' framing: the trigger is an in parameter with no declared multiplicity, which OpenSysML treats as required though the spec's own default for it is [0..*] - a sharper bug report than before, since the tool imposes a requirement the model text does not even ask for. Fixed the table headers and conclusion accordingly. Added the tool's own kind-vs-@type disagreement as corroborating evidence (model.find(...).kind reports attributeUsage for these parameters; the API-JSON export types them ReferenceUsage - confirmed directly against the real fixture). While probing this, confirmed by direct test (not assumed) that an explicit [1..1] fails identically to the undeclared case - the tool already applies a [1..1]-shaped requirement whenever no multiplicity is stated. This refines the orchestrator's own ruling text (which assumed [1..1] would be "the spec-accurate way to state the real intent" without asserting it also resolves the evaluability gap): [1..1] is the spec-accurate fix for the model's honesty, but does not fix this gap either way. D-026 states this distinction explicitly rather than conflating the two. Q1 ruling applied: kept the model exactly as built, no multiplicity annotation added. D-026's rejection of [0..1] restated on its actual, default-independent rationale (the model's real intent is exactly one value, not yet known - neither [0..*] nor [0..1] states that) rather than the "loosens vs tightens" framing that the corrected default direction invalidated. N1: D-026's opening paragraph now matches the current (Q2-fixed) model, where the error names "energy," and notes the earlier "bread" message was from the pre-Q2 minimal probe, not a live contradiction. N2: "Six variants" corrected to "Seven variants" (both documents; the table has seven rows). N3: "not any reference to a separate definition" now cites the only-out row (a reference that does not fail) as the actual refutation, not the abstract/[0..*] rows (which fail, and so don't refute that hypothesis at all - they're consistent with it). Abstract/[0..*] reframed as evidence that abstractness and usage-level multiplicity don't rescue the case, a distinct claim. N4: "either spec citation" corrected to "this citation" (only one citation appears at that point). N5: nb03's "satisfies the old `delivered + loss <= energy` bound" reworded to "satisfies the sum bound alone," removing the authoring-history framing. N6: nb01's demo cell prints `balance constraint kind: constraintUsage` right next to prose about the asserted constraint; added one sentence to the seam cell noting model.find(...).kind reports the general constraint kind, not the asserted subtype, so this isn't a contradiction. N7: no action (informational only, per the review). Re-verified: full test suite 289 passed (unchanged); glossary lint 0 ch04 hits, 145 total (unchanged, text-only round); glossary check clean; both touched notebooks execute fresh with real, non-empty output and no errors; em-dashes zero in both touched notebooks (DEFERRED.md/gap-issue-drafts.md retain their pre-existing convention, unchanged from prior rounds).
…m PASS4-004 round 2; add item 12 logging the deferred-figures pattern across every chapter re-derived so far (Ch2, Ch4, and Ch5 will make three), recommending a dedicated diagram pass once the sequence stabilizes rather than piecemeal per-chapter rendering
Content push-back from independent review (Opus 5.5, round 3). F3 changes
the plan: an explicit, spec-identical [0..*] multiplicity resolves the
D-026 evaluation gap entirely, applied here as the fix rather than
documented as a rejected option.
F2: Draft 10's two remaining passages that still argued from the pre-F1
premise ("relaxing to [0..1]", "mandatory... not optional") rewritten to
match the corrected [0..*]-is-the-real-default premise consistently.
F3 (the important one): models/ch04-cumulative.sysml's ApplyHeat now
declares `in energy : ISQ::EnergyValue[0..*]` and `in duration :
ISQ::DurationValue[0..*]` (bread stays unannotated, already bound to
ToastBread::bread per Q2). This is the spec's own implicit default for a
bare in/out reference usage (SysML v2.0 formal/2026-03-02 7.6.3/7.6.4),
written out explicitly rather than left implicit, which is all OpenSysML
v0.9.0 needs to keep the model evaluable. DL-030/DL-031's requirement
(typed, unit-bearing, no value) is completely unaffected: the parameters
are exactly as valueless and exactly as not-yet-bound as before, and
nothing about what the model means has changed.
Verified: model.ok == True; predecessor containment ch03->ch04 clean;
ToasterDemo::slow.cycleTime evaluates to 200 [SI::s] and
ToasterDemo::timely(ToasterDemo::slow) evaluates to False, both matching
Chapter 3's own established result; the balance constraint still evaluates
correctly against energy[0..*] (plausible holds, implausible fails,
negative-loss fails) - re-run in full since the reviewer's finding didn't
check this.
Rewrote the ch04 notebook content and the conformance test to match the
fixed reality:
- tests/test_conformance.py: renamed and rewrote the execution-error test
to assert status == "passed" with zero findings, mirroring ch03's own
test exactly (same pattern, same assertions).
- nb01: IN_PARAMS fragment and narration updated to the explicit [0..*]
form. The cell that previously narrated "this attribute access fails,
here's why, see D-026" now tells the true, better story: a bare,
unstated multiplicity and its explicit spelling-out should mean the same
thing per spec, but OpenSysML v0.9.0 treats them differently, so the
model states the multiplicity explicitly, both as honest and as what
keeps the model evaluable. Added a live demonstration
(model.eval("ToasterDemo::slow.cycleTime")) to the closing demo cell as
real evidence, not just narrated.
- nb03: added a dedicated evidence step evaluating slow.cycleTime directly
against the already-loaded real model (new sufficiency evidence for
AI-C04, cited in evidence_refs/rationale); the probe-justification cell
no longer cites a gap workaround, since nominal/slow are now fully
evaluable - the standalone mirror model is needed only because nominal/
slow carry no concrete energy/delivered/loss values to check the
constraint against, an ordinary reason unrelated to any tool gap. The
mirror's own ApplyHeat declaration updated to match the real model's
[0..*] shape.
- index.md/conclusion.md: "Expected result"/"What we built" updated to the
new signature; both mention the explicit-multiplicity fix and cite
slow.cycleTime's restored evaluability as part of what the chapter
establishes.
Rewrote DEFERRED.md D-026 and decisions/gap-issue-drafts.md Draft 10 around
the new headline finding (an implicit and an explicit-but-spec-identical
[0..*] multiplicity are treated differently, not "an unbound mandatory
parameter fails") in both documents' opening summary, added the explicit
[0..*] isolation-table row next to the implicit row it contrasts with, and
rewrote the Workaround section: explicit [0..*] is the applied fix, not a
rejected option; [0..1] stays documented-and-rejected (narrows the
multiplicity and misstates these inputs as optional); the [1..1]-also-
fails finding kept as supporting evidence that the tool's behavior tracks
"a multiplicity token is present" rather than any coherent multiplicity
semantics. Draft 10's Request section reframed around the inconsistency
as the bug, with the workaround stated as evidence of it, not as an
unsolved blocker.
decisions/next-passes.md item 11 (broader Ch1-Ch8 multiplicity question) is
on the base branch, not touched here, per the orchestrator's own note that
they will update it on integration.
Re-verified: full test suite 289 passed; check_construction.py --check
--chapter 4 consistent (--check full: only ch05, 15 issues, same expected
non-goal ripple); glossary lint 0 ch04 hits, 145 total unchanged; glossary
check clean; local book build clean (58 pages); all three notebooks execute
fresh with real, non-empty output and no errors; em-dashes zero in every
touched notebook/md/model file (DEFERRED.md/gap-issue-drafts.md retain
their pre-existing convention; tests/test_conformance.py's 12 pre-existing
hits are all outside the lines this round added, confirmed by diff).
…D-026/Draft 10's repro and mechanism claims were wrong Reviewer (round 4) found two real defects in the gap-tracking text itself, both confined to DEFERRED.md and decisions/gap-issue-drafts.md, no model/notebook/test change needed: - The repro and isolation table conflated experiments across ApplyHeat's three separate unbound parameters (bread, energy, duration), so changing only one line as shown would not actually reproduce the claimed result (bread or duration would still block). Split into two clean experiments (which construction reaches the parameter; what the parameter's own multiplicity does) and rebuilt the repro isolated to a single parameter so it reproduces exactly as described. - Both documents claimed the tool 'keys on whether a multiplicity token is present in the text, full stop' - contradicted by their own evidence (explicit [1..1] fails identically to the bare form). Replaced with the mechanism the evidence actually supports: OpenSysML gives a bare in parameter the [1..1]-shaped default reserved for attribute/item/port usages (not what a keyword-less reference usage should get per spec), then raises on a nested step's unbound parameter with effective lower bound >= 1 - a coherent, if wrong, rule. Applied directly rather than through another builder/reviewer round: this was the third consecutive round where D-026/Draft 10's text was the only defect, the reviewer's own report already specified the exact corrected mechanism and evidence table, and the risk of a text-only correction to two non-learner-facing internal documents is low. Flagging this deviation from the normal process explicitly.
Rebases models/ch04-cumulative.sysml onto the current ch03 fixture and executes the layer audit's rulings: ApplyHeat rebuilt with typed flows only (bread, energy, duration in; toast, delivered, loss out) plus an asserted, bounded balance constraint, removing the efficiency-parameterized DeliveredEnergy invocation entirely (DL-030) - calc def DeliveredEnergy does not return to this chapter, deferred to whichever chapter builds HeatingSystem's actual conversion; ApplyHeat nested as a real step of ToastBread rather than free-floating (F-4); Start/Finish/Cancel documented as signals, not material (DL-036); duration kept as a valueless functional input slot, denotation fixed as a control-function signal (DL-031); nb03's missing ReviewRecord import fixed and AI-C04 rebuilt with the new judgment-record construction zone. Structurally the largest chapter yet: nesting ApplyHeat surfaced a genuine, previously undiscovered OpenSysML v0.9.0 gap (D-026) - a bare, unstated 'in' parameter's multiplicity and its explicit, spec-identical [0..*] spelling-out are treated differently by the tool's evaluator, breaking model.eval on attributes with no relation to ApplyHeat at all. Isolated precisely across two controlled experiments (which construction reaches the parameter; what the parameter's own declared multiplicity does), confirmed against both spec text (SysML formal/2026-03-02, KerML 1.1 Beta 2) and the tool's own internal inconsistencies (a top-level unbound parameter is tolerated, a nested one is not; model.find(...).kind disagrees with the API-JSON export's own typing). Fixed with a spec-neutral change (explicit [0..*] on energy and duration, which states nothing the implicit default did not already mean) rather than accepted as a permanent limitation - Chapter 3's established evaluability is fully restored, not merely documented as broken. Drafted, held-for-review gap report (D-026, DEFERRED.md; Draft 10, gap-issue-drafts.md) not filed upstream. Five independent review rounds (Opus 5.5, different model than the Sonnet 5 author): round 1 FAIL (co-author trailers, DL-032-forbidden narration, an inverted DL-032/DL-049 reading, a pacing gap); round 2 FAIL (a backwards spec citation in the gap report, seven bundled polish items); round 3 FAIL (the gap report's own core technical claim was itself wrong on re-derivation - explicit [0..*] turned out to be a real fix, not just a documented workaround, prompting the model change described above); round 4 FAIL (the gap report's repro and stated mechanism, after that fix, no longer held up under independent re-verification, and this round's correction was applied directly rather than through a further builder round, given how narrowly it was already scoped by the reviewer's own findings); round 5 PASS, confirmed clean by independent re-probing of the core multiplicity-vs-evaluability claim, not just a read-through. Chapter 5's own predecessor-containment gap against the new ch04 (14-15 elements, mostly the functional constructs this chapter adds plus the constraint's type change) is expected and recorded, not fixed here - an explicit non-goal. Chapter 5's own contract inherits it, along with the DeliveredEnergy/HeatingSystem placement this chapter deferred and Chapter 5's pre-existing misuse of Start/Finish as material part-types.
…isolated/fixed across five review rounds, what shipped and what's carried forward
…t HeatingSystem, port interface
F-1: replace the invalid definition-level 'allocate ApplyHeat to HeatingSystem;' with a
named, usage-level allocation usage: 'allocation heatAllocation allocate
ToastBread::applyHeat to Toaster::heating;', visible to model.query().
F-2: HeatingSystem becomes 'abstract part def HeatingSystem :> ToastingSystem { perform
action applyHeat : ApplyHeat; }', a genuine logical carrier for the allocated function.
F-3/F-4/F-5/F-6: BreadLoader, BreadEjector, BreadHandling and the bread item-typed part
usage flow are removed entirely. They traced to no function, used item defs as part
types (invalid SysML), and were never composed into the system of interest.
New content: a real port-typed interface between ControlSystem and HeatingSystem,
carrying the duration signal ApplyHeat has declared unconnected since Chapter 4.
'port def DurationPort' with an 'out duration' attribute, a conjugated port usage on
HeatingSystem and a matching port usage on ControlSystem, connected by
'flow control.durationOut to heating.durationIn;' inside Toaster.
Probed directly against OpenSysML v0.9.0 before committing: the named allocation
usage, the abstract HeatingSystem with Toaster::heating still resolving cleanly, and
the port/flow idiom all parse and load with model.ok == True and zero language-gap
findings (previously two: allocate-between-definitions, part-typed-only-by-item-def).
nb01 (kept filename 01-concept-selection.ipynb, F-8): retitled to model navigation, the notebook's actual content; removed all 'concept selection' language, which named a construct (selection among alternatives) the notebook never taught. Elements navigated now exist in the rebased model (HeatingSystem, ApplyHeat), not the removed Heater/DeliveredEnergy. nb02 (Allocate): builds the abstract HeatingSystem (perform ApplyHeat) and the named allocation usage. Demonstrates model.query() seeing the allocation directly and perform_relationships confirming the performer, replacing the old JSON-only readback. nb03 (Interfaces): builds the DurationPort interface and the flow between ControlSystem and HeatingSystem, replacing the removed BreadHandling content entirely. Runs the port-type conformance check (empty, non-vacuous: two real ports). Renders the interconnection diagram to figures/ch05-interconnection.svg and displays it inline via IPython.display.SVG, with a two-sentence caption stating what it shows (the control-heating port connection) and does not show (ApplyHeat's own flows) -- the figure was previously rendered to a tempdir and never shown (F-9). index.md and conclusion.md: rewritten to describe the real content. F-7 fixes throughout: 'functional-to-physical assignment' -> function-to-logical-component allocation; 'structural layer' removed (not a tutorial layer); 'hardware component' -> logical component; 'HeatingSystem realizes ApplyHeat' -> performs (allocation is not realization, AGENTS.md 1.5); the diagram no longer described as 'confirming' connectivity (a diagram is a view, not independent evidence, AGENTS.md 1.7). Spec citations corrected to the architecture-layers skill's confirmed sections (7.15.2 for AllocationUsage; the 7.12-7.14 range for port/flow, since the skill does not confirm a narrower number). Exercise pointers checked against exercises/ch05/exercise.ipynb's real, unfixed content and left accurate to it, per PASS4-002/003/004 precedent.
…tainment gap scripts/check_construction.py: CONSTRUCTION_NOTEBOOKS[5]'s context_stubs updated to match the rebased model. nb02's fragment declares HeatingSystem itself (abstract, performing ApplyHeat), so it is not stubbed; stubs now cover ToastingSystem, ApplyHeat, ToastBread::applyHeat and Toaster::heating, the cross-chapter names the allocation references. nb03's fragment declares DurationPort, HeatingSystem, ControlSystem and Toaster completely, so only ToastingSystem and ApplyHeat remain stubbed. tests/test_predecessor_containment.py: ch04->ch05 is now clean (rebased fixture), so chapter 5 moves from its own dedicated dropped-elements test into the parametrized clean-pairs list. ch05->ch06 opens the same gap one chapter further down (ch06 was not touched, a stated non-goal): a new dedicated test replaces the old one, asserting the 21 named elements ch06 is missing (Chapter 1/4 functional constructs plus Chapter 5's own allocation and interface constructs), matching the exact rhythm PASS4-002/003/004 each established.
src/toaster/conformance.py: REGISTRY's 'port-type' entry sets applies_from=(5, 3), mirroring DL-048's exact precedent for satisfaction-claims-evaluated. This is the model's first port-typed connection, so the check has something to test for the first time; confirmed passed with zero findings against the real ch05 fixture. tests/test_conformance.py: adds a ch05 fixture and two tests -- one confirming ch05 carries neither of the two DL-039 language-gap findings ch04-ch08 have (the removed definition-level allocate and item-typed part usage), one confirming the scheduled port-type check reports passed with a real, non-vacuous port pair (two PortUsage elements), not ch08's vacuous empty-list pass. Updates test_registry_port_type_entry and the two tests that asserted the old, unscheduled applies_from=None behavior against the real REGISTRY entry, which is now correctly 'failed' past its stage against a genuine mismatch fixture.
chapters/ch04-functional-decomp/conclusion.md: 'What comes next' re-checked against what Chapter 5 actually builds (the standing SOP, decisions/next-passes.md item 10). Rewritten from the old 'allocate for assignment relationships and flow for item flows between parts' to name the real constructs: a named, usage-level allocate and a port-typed flow carrying the duration signal. docs/index.md: Chapter 5's curriculum row question column no longer says 'realized' (allocation is not realization, AGENTS.md 1.5); constructs column adds perform and port, both now genuinely taught.
…pertype, use interface not flow
Finding 1 (regression): abstract part def HeatingSystem no longer specializes
ToastingSystem. DL-019/DL-020 already ruled this out (ToastingSystem is the
subject all layers describe, not something a logical component specializes;
PASS4-001 removed the identical pattern from Chapter 1). The rebase onto ch04
had reintroduced it, which made HeatingSystem inherit ToastingSystem's own
perform action toastBread : ToastBread, i.e. the heating component performing
the whole system's function. HeatingSystem now carries no supertype at all,
matching Chapter 1's corrected shape.
OQ-1: replaced the port-typed 'flow' with 'interface', the construct SysML v2
formal/2026-03-02 7.14.1 actually names for a connection whose ends are all
ports. Probed both bare-port ends (control.durationOut to heating.durationIn)
and directed-feature ends (...durationOut.duration to ...durationIn.duration,
the form the reviewer cited from the spec's own FuelInterface example) before
choosing: bare-port ends is what shipped, because it matches the glossary's
own confirmed interface definition (ends are ports, not features within
them) and keeps port_type_mismatches comparing real PortUsage ends instead of
becoming vacuous again. Named ('durationInterface') so model.query() sees it.
…fix duplicate node bug OQ-1 explicitly widens this contract's blast zone to src/toaster/render.py. build_interconnection_intent now recognizes InterfaceUsage and ConnectionUsage alongside FlowUsage when extracting the diagram's connections (a connection whose ends are all ports is an interface, SysML v2 formal/2026-03-02 7.14.1); query.py needed no change, since port_type_mismatches already handled InterfaceUsage ends. Finding 9 (node-identity bug, confirmed against the actual shipped SVG: it drew both a 'heating' box from the owned-part extraction and a separate 'Toaster::heating' box from the allocation edge, the same model element drawn twice). render_sysmld now normalizes a qualified reference's leading segment to a known part's short name before drawing an edge, so 'Toaster::heating' reuses the same node 'heating' already has. Verified against the real ch05 model: the rendered SVG now has exactly one 'heating' node and one 'control' node, plus 'ToastBread::applyHeat' (correctly not merged, a different kind of thing: the allocated function, not a part). tests/test_interconnection.py: two new regression tests, one for the InterfaceUsage recognition and one for the node-identity fix, both against a small synthetic model (not the ch05 fixture, since this file is general- purpose, predating this chapter).
…s and add page headings Finding 1: nb02's cell claiming ToastingSystem/toastBread as 'the logical idiom Chapter 1 already established' for a component is removed (false per DL-019: ToastingSystem is the subject, not a logical component); grounded instead in AGENTS.md's own stated logical idiom (an abstract part def that performs an action). Every HeatingSystem fragment across nb02/nb03 drops ':> ToastingSystem'. Finding 2: added a markdown heading to the first cell of all three notebooks (matching Chapter 1's and Chapter 4's own established convention, which this chapter's notebooks had never carried), so the built page title reflects the real content instead of a filename-derived fallback. Verified directly against _build/html/config.json after a local book build: nb01's page title is now 'model navigation', not 'Concept Selection' or any variant of the filename. Finding 3: 'gives ApplyHeat::duration a modeled source' and 'closing a gap Chapter 4 left open' are removed everywhere (conclusion.md, index.md, nb03): false, since ApplyHeat::duration is not bound to the port and nb03's own doc already said so. Reworded to state what actually changed: a connection point now exists showing where the signal would flow, once something produces it. Finding 4: 'confirms the two ports are compatible' is reworded everywhere to state precisely what port_type_mismatches checks (declared type relatedness) and does not check (conjugation correctness). Finding 9: the figure's caption now states the conclusion it supports (a single, type-checked connection point now joins the two components) rather than only an omission. Finding 10: nb02's exercise pointer no longer suggests the exact 'allocate Brew to BrewUnit;' syntax (the invalid, definition-level form F-1 fixed) or 'confirm model.ok stays True' (the proxy DL-039 warns is not the real conformance criterion); it now describes the exercise step in general terms, since this contract introduced that specific guidance and PASS4-005 is the one responsible for it, unlike the untouched exercise content itself. OQ-2: no policy action invented for ControlSystem; it stays a concrete, port-bearing 'logical, not yet built' component exactly as DL-020 describes. OQ-3: 'decomposing HeatingSystem into its physical parts' (conclusion.md) reworded to 'one level deeper into HeatingSystem', not presupposing a direct logical-to-physical jump per DL-043. OQ-4: 'the same kind of action, allocated and performed by type' replaces language that could be read as claiming the allocation's ToastBread::applyHeat and HeatingSystem's own perform action applyHeat are the same occurrence.
…orrected model figures/ch05-interconnection.svg: regenerated against the corrected model (HeatingSystem with no supertype, the interface construct, the node-identity fix), confirmed via a local book build to still render and display correctly in the built page. scripts/check_construction.py: nb02's context_stubs no longer stub ToastingSystem (HeatingSystem's fragment no longer specializes it). nb03's still needs it (Toaster's own, unchanged ':> ToastingSystem'). Comments updated to describe the corrected shape.
…redecessor-containment names Finding 5: test_port_type_check_passes_on_ch05_real_port_connection now asserts the InterfaceUsage's actual connector ends resolve to the two declared, named ports (durationOut, durationIn), not just a raw PortUsage count (which included the interface's own two synthetic end features, found while fixing this: 4 PortUsage elements total, 2 of them unnamed). Added test_port_type_check_catches_a_real_conjugated_port_mismatch: a genuinely mismatched pair (DurationPort's conjugate on one side, an unrelated PressurePort's conjugate on the other) connected through the same interface/conjugated-port idiom this chapter introduces, confirming port_type_mismatches is not vacuous in either direction. tests/test_predecessor_containment.py: the ch05->ch06 dropped-elements test gains ToasterDemo::Toaster::durationInterface (now named, so it appears in the NAMED-only predecessor-containment comparison, unlike the unnamed flow it replaced).
…raft 11) Widened blast zone (push-back's own explicit instruction) to DEFERRED.md and decisions/gap-issue-drafts.md, same pattern as PASS4-004's D-026: a held, not filed, draft. D-027 documents what the reviewer independently reproduced: a second declaration reopening an existing namespace member's name loads with model.ok == True and two name-conflict warnings, then model.to_api_json() raises ConversionError. Every helper this repo uses beyond model.query()/model.find() depends on to_api_json(), so this is a real, if narrow, hazard for any future builder tempted to spread one type's construction-zone declaration across two notebooks by reopening it (a pattern PASS4-005 considered and designed around entirely, not shipped). Recorded as a candidate, not a settled bug claim: two different readings of what the actual defect is (to_api_json() too strict, or load_from_content's warning-only severity too lenient) are named and left open, since no KerML namespace/membership constraint was checked against the spec text directly to settle which. Draft 11 in decisions/gap-issue-drafts.md carries the same reproduction and the same open framing, held for Z's review per the exact precedent D-026/Draft 10 already set.
…roduces
The reviewer ran the exact given source (package P { part def X; part def X
{ attribute a : Real; } }) and got ok=False (unresolved: Real), not the
ok=True-with-warnings-then-ConversionError behavior the entry documents:
Real needs ScalarValues::* imported, which the repro omitted.
Added the missing import, re-verified directly: ok == True, two
severity='warning'/code='name-conflict' diagnostics, model.find resolves,
model.to_api_json() raises ConversionError exactly as described. Fixed both
DEFERRED.md D-027 and decisions/gap-issue-drafts.md Draft 11 to the corrected
source, with a note on what was wrong and that it was re-verified.
…nterface' Three spots never touched when the construct switched from flow to interface (a prior push-back round): - chapters/ch04-functional-decomp/conclusion.md: 'a port-typed flow carrying the duration signal between components' was wrong on both halves (it's an interface, and duration stays unbound, nothing carries the signal yet). Reworded to 'a named interface giving duration a connection point... without yet binding it to a value.' - docs/index.md's Chapter 5 construct list: 'port, flow' -> 'port, interface'. - src/toaster/conformance.py's port-type scheduling comment: 'DurationPort flow' -> 'DurationPort interface'.
… ends B4: cells claimed 'the allocation and the performer relationship both point at HeatingSystem' without ever printing the allocation's own ends, blurring exactly the usage-versus-definition distinction this notebook exists to teach (F-1: allocation is usage-level). The demo cell now calls find_allocations(model) directly and prints its result; the narration states precisely what it shows: heatAllocation goes from ToastBread::applyHeat to Toaster::heating (a usage), and perform_relationships shows HeatingSystem (the definition that usage is typed by) performing ApplyHeat. Re-executed the notebook fresh to confirm the printed output matches the narration exactly. Bundled minor fixes: - The negative control now uses a usage-level malformed form (an undefined step on a real, declared action, allocated by a named usage-level allocation) instead of the old bare, definition-level shape F-1 removed from the real model, so it no longer visually contradicts the positive content next to it. Re-verified: still produces the expected unresolved- reference diagnostic. - 'the component now built to perform it' (implying HeatingSystem is a finished component) reworded to 'the usage that is typed by HeatingSystem and now allocated to perform it', consistent with DL-020's 'logical, not yet built'. - index.md's 'Expected result': 'a DurationPort connecting ControlSystem and HeatingSystem' reworded (a port def does not connect anything itself) to 'a DurationPort typing a new port on each of ControlSystem and HeatingSystem', with the interface stated as what joins them.
…t corrections the reviewer specified precisely Round 3 found three remaining defects, all confined to learner-facing prose, no model/test change needed: - conclusion.md still claimed a port def 'connects' two components, the exact defect item 4 had already fixed in index.md but missed here - nb03 falsely cross-referenced ControlSystem to 'Ch5 nb02', which never mentions it (ControlSystem is Chapter 1's) - nb03's demo printed the interface connection under a stale 'Flows:' label (the dict key itself, intent['flows'], is unchanged - it's render.py's real return-value name, used elsewhere too) Bundled two related non-blocking notes from the reviewer's open questions since they were equally narrow and precisely specified: reworded a sentence implying DurationPort literally carries ApplyHeat's duration value (it carries a value of the same type, not that value); removed an AGENTS.md citation from learner-facing prose (an internal instruction file, not a tutorial source - same rule already applied against DL-number citations). Applied directly rather than a fourth builder/review round: three consecutive rounds have now found only small, precisely-specified text issues, all narrower in scope each time. Verified independently before committing: JSON validity, zero em-dashes, full test suite (294 passed), both touched notebooks re-executed fresh with clean real output.
Rebases models/ch05-cumulative.sysml onto the current ch04 fixture and executes a real structural redesign, not a patch: the audit found the chapter's central content (BreadLoader/BreadEjector/BreadHandling and a flow between them) was invalid SysML tracing to no function, never composed into the system of interest - removed entirely. Replaced with content built from what Chapter 4 actually established: a named, usage-level allocation (allocate ToastBread::applyHeat to Toaster::heating, resolving F-1's definition-level language-tier gap now that a real usage of ApplyHeat exists to allocate); HeatingSystem made a genuine abstract logical carrier that performs ApplyHeat (F-2); and this model's first real port-typed interface, connecting ControlSystem to HeatingSystem and carrying the duration signal Chapter 4 left explicitly unconnected - conjugate ports (~DurationPort) verified against the actual SysML v2.0 spec text (Annex A's FuelInterface example) before committing to the idiom. The port-type conformance check (DL-038) is scheduled for the first time, against a real two-port connection, not vacuously. The interconnection figure is actually rendered and shown in the built book, not deferred - the first chapter in this sequence to do so, using tooling the chapter's own stale notebook had already called but never displayed. Four independent review rounds (Opus 5.5, different model than the Sonnet 5 author): round 1 FAIL, most seriously a real regression (HeatingSystem :> ToastingSystem reintroduced, exactly what DL-019/DL-020 ruled out and Chapter 1's own re-derivation had already removed), plus a retitle that never reached the published book, two claims contradicted by the model itself, and a new test that couldn't distinguish a real port comparison from a vacuous one; round 2 FAIL (a gap-tracking document's own repro didn't reproduce as written, three stale forward references to a construct the chapter no longer uses, and one notebook's claim about the allocation's own evidence that its output didn't show); round 3 FAIL, down to three small precisely-specified text issues, applied directly by the orchestrator rather than a fourth builder round; round 4 PASS, confirmed clean. Co-author trailers were stripped by the orchestrator three times across the five build/review cycles (mechanical, tree-hash verified each time, never touching content). Chapter 6's own predecessor-containment gap against the new ch05 is expected and recorded, not fixed here - an explicit non-goal. Chapter 6's own contract inherits HeatingSystem's corrected shape (abstract, no ToastingSystem supertype, performs ApplyHeat) and the new interface idiom this chapter establishes.
… DL-019/020 regression caught and fixed, the first real port/interface content, four review rounds
…GenerateHeat Rebases models/ch06-cumulative.sysml onto the current, merged ch05-cumulative.sysml (the stale predecessor still had Heater/HeatingElement/PowerWire, un-abstracted HeatingSystem, and none of Chapter 4/5's functional and interface constructs). Adds a complete function/logical/physical chain one level below HeatingSystem: - GenerateHeat, nested inside ApplyHeat the same way ApplyHeat nests in ToastBread - EnergyPort and HeatGenerator, the abstract logical carrier (perform + port + an unbound power slot, the same design-space idiom as Toaster::cycleTime) - HeatingAssembly :> HeatingSystem, composing heatGen : HeatGenerator - heatGenAllocation, a named usage-level allocation (ApplyHeat::generateHeat to HeatingAssembly::heatGen), mirroring Chapter 5's heatAllocation - ResistanceCoil :> HeatGenerator, a concrete realization with a properly ISQ/SI-typed resistance attribute and a redefined power rating - HeatGenerationReq, a logical requirement on HeatGenerator (not a concrete part), and rated/weak, two realizations checked against it, weak's failure folded into its own context as assert not satisfy rather than a false positive assert satisfy Removes PowerWire and the old Heater-based requirement wholesale rather than repairing them (no function drives a power-delivery branch in this model). model.ok == True with zero language-gap findings; both staged conformance checks (port-type, satisfaction-claims-evaluated) report passed, non-vacuously, for the first time on this chapter's own fixture.
…, judgments Rebuilds all three ch06 notebooks against the re-derived model, keeping the existing filenames (Chapter 5's own precedent) but retitling to match the new content: - 01-subsystem-requirements.ipynb: level-2 function and logical carrier (GenerateHeat, EnergyPort, HeatGenerator, HeatingAssembly, heatGenAllocation) - 02-second-level.ipynb: level-2 physical realization (ResistanceCoil, HeatGenerationReq, rated/weak) plus AS-C06 (selection among alternatives: resistive Joule heating over a combustion-based alternative, argued from interface compatibility with what the model already declares) and AC-C06 (the requirement is a measure of performance, not effectiveness; its 600 W threshold is honestly recorded as not yet derived from any stated MoE) - 03-stopping-judgment.ipynb: AI-C06 rebuilt from scratch, checked against real analysis gathered from the loaded model (perform_relationships, find_allocations, two real satisfy evaluations), not the model's own declaration cited back at itself; fixes the missing-import NameError; honest about what the branch does not yet establish (no producer wired to energyIn, no full toaster candidate, the threshold still underived) index.md and conclusion.md rewritten to match; docs/index.md's Chapter 6 row and ch05's own conclusion.md 'What comes next' updated to match what actually shipped. Zero em-dashes, zero Tall-world labels, zero glossary lint hits in every touched file (was 20, now 0). All three notebooks executed fresh and clean, real non-empty output in every code cell.
…tests CONSTRUCTION_NOTEBOOKS[6] adds nb01 and nb02 (the two construct-introducing notebooks; nb03 is a judgment notebook with no TOASTER_INCREMENT), confirmed required against HEAD (Chapter 6 was not previously registered). test_predecessor_containment.py: ch05->ch06 is now clean (PASS4-006 rebased ch06-cumulative.sysml onto ch05-cumulative.sysml's current content), so the known-gap test moves one chapter down to ch06->ch07 (not touched by this contract, still built against the old, stale ch06 fixture). Parametrize list updated accordingly (6 added to the clean list, 7 removed). Test count unchanged at 294 (one known-gap test swapped for another, one chapter later).
…tanceCoil
The previous phrasing ('two candidates that realize ResistanceCoil') had the
realization relationship backwards; rated/weak are usages typed by
ResistanceCoil, the concrete part that realizes the abstract HeatGenerator.
…: what's pinned (uv.lock, the OpenSysML binary version, Node lockfile/nvmrc), what CI actually checks today vs. what's still manual (notebook execution and the book build aren't in CI yet), how ReviewRecord's content_hash makes a judgment's evidence checkable rather than making the judgment itself a computation to rerun, and three honest limits: cited sources are pinned by hash but not distributed (copyright), a gap fixed upstream doesn't silently change this tutorial until someone deliberately re-pins, and the rendered book isn't auto-rebuilt on every notebook change
…e, ordering, exercise pointers B3 (contract wording defect, corrected here): removed 'electrical' from GenerateHeat's and EnergyPort's own docs. Neither the function nor the port commits to an energy form now, so GenerateHeat genuinely passes the same substitution test ApplyHeat itself does (a resistive coil and a gas flame both take some energy input and deliver heat). AS-C06 is rewritten to be the actual, non-circular selection: it argues from ControlSystem's real, already-modeled discrete duration signal (confirmed by model.find(), not assumed) pairing naturally with an electrically-switched mechanism, not from 'no fuel port exists' once the port was already generic. ResistanceCoil's electrically-specific name and Joule-heating doc are admissible only after this record, not before. B4: reordered models/ch06-cumulative.sysml and nb02 so HeatGenerationReq (and AC-C06, its measure-framing judgment) come before AS-C06's selection, which comes before ResistanceCoil, matching DL-042's own stated order: state the requirement, select the mechanism against it, then build the realization the selection licenses. B1/B2: removed every 'complete'/'stopping rule satisfied' claim from conclusion.md, index.md, ch05's own forward reference, and AI-C06 itself. AI-C06's claim, criteria, rationale and engineering_conclusion (now 'undetermined', not 'supported') state precisely, condition by condition, what DL-043's stopping rule actually shows at this level and what it does not: energyIn has no producer wired to it, HeatingAssembly is composed into no full Toaster candidate, the threshold is underived, and ApplyHeat's other flows (bread, duration, toast, delivered, loss) are not accounted for at this level at all. This chapter builds one honest, complete-in-itself worked-example branch of ApplyHeat's own decomposition, explicitly not a full accounting of every flow, matching Chapter 4's own precedent for ApplyHeat itself. B5: fixed two evidence citations that pointed at something never gathered. AS-C06 now cites a real model.find() call made in this same notebook, not a fictitious one in 'the previous notebook'. AI-C06's assumption_refs now describes what notebook 01 actually did (printed and loaded APPLY_HEAT_INCREMENT), not a model.find() call that was never made there. B6: fixed nb01/nb02's exercise pointers to describe only what exercises/ch06/exercise.ipynb actually asks (BrewComponent/Impeller/FilterBasket decomposition; a BrewReq requirement with an underSpec variant) rather than a nested sub-function or a selection/framing judgment the real exercise does not ask for. N7 (bundled, same class of defect as B1/B2): fixed an inaccurate 'exactly how Chapter 5 treated duration' cross-reference in nb01 to state precisely what Chapter 5 did (built and connected durationIn/durationOut) versus what this chapter leaves undone for energyIn (no such connection built). All acceptance checks re-run clean: model.ok == True, both conformance checks passed non-vacuously, 294 tests passing (no delta), 0 ch06 lint hits, all three notebooks executed fresh with real non-empty output, local book build succeeds (58 pages).
…ties One test per relationship shape the round-3 review found missing: the chapter's own assert-satisfy-by idiom, dependency, allocate, bind, metadata, an invocation expression, a concern definition as owner, a viewpoint definition as owner, a requirement requiring a requirement, a list-shaped multi-subsets field, and frame concern. Each is confirmed detected with the correct owning requirement. Also adds the one case that must still NOT be detected: a transitive chain through an intermediate constraint that is not itself owned by any requirement, confirmed to remain the honest, named scope limit after the redesign, and confirmed separately that the same intermediate IS found when it is itself the query target (a one-hop-at-a-time property, not a blind spot on the intermediate element). Every existing round-1/round-2 test still passes unchanged against the new implementation. Corrects the negative-control test's own docstring, which still described the old, narrower field-list design.
Both main-chapter notebooks and the exercise mirror still described the round-2 design (a fixed list of subsets/redefines/references/referent fields, and every DIRECT way SysML v2 lets a requirement tie to a constraint) after query.py was redesigned as a field-agnostic scan. Reworded every such claim to describe the actual design: a scan of every field of every element, excluding only containment/self-identity bookkeeping and the KerML relationship-object family, checked against a type-hierarchy-aware requirement-owner test. The one honest scope limit (a transitive chain through a non-requirement-owned intermediate) is named in every rewritten passage, unchanged. Also fixes two leftover round-2 occurrences in 03-engineering-signoff.ipynb of "tied to no requirement usage" that should have read "tied to no requirement" (to cover RequirementDefinition and its subtypes too), missed when that fix was applied elsewhere in the same file. Both main-chapter notebooks re-executed end to end via nbclient with zero errors; their stored outputs and execution metadata are refreshed accordingly. The exercise notebook's cells were normalized through nbformat read/write (no execution: its own model is a learner-supplied placeholder) to restore the repo's own list-of-lines source formatting after an editing tool wrote single-string source.
…70's stale test count DL-071 records the round-3 fix-and-reverify: a third independent review found the round-2 fix still missed real ties (most seriously the chapter's own assert-satisfy-by idiom), and this entry documents the field-agnostic redesign, the javap-confirmed metaclass evidence behind both exclusion sets, the full reproduction of every round-3 finding as a committed test, the re-verification against all three pinned tools, and the honest adversarial attempt made to find a further gap before closing this out. next-passes.md item 29 gets a SUPERSEDED note pointing to DL-071, since its prior RESOLVED note (DL-070) described a design this round replaced. Also corrects DL-070's own "eight tests" claim, which was already stale by the time round 3 found the search incomplete: restated qualitatively (one test per relationship/owner shape) rather than re-hardcoded, with a note that a live count should be computed (pytest --collect-only), not read off this log.
…eld-agnostic scan Replace the open-ended field-agnostic scan (plus its type-hierarchy-aware owner walk) with two small, explicitly-named checks: satisfy-by-subject, built on the existing satisfy_relationships helper, and a direct subsets/redefines/references/referent reference from within a RequirementDefinition/RequirementUsage's own body (exact-type owner only, the original owner-chain walk). Delete _dict_refs, _STRUCTURAL_FIELDS, _LINK_BOOKKEEPING_TYPES, _is_requirement_owner_type and _REQUIREMENT_METACLASS_PARENTS entirely. Tests: keep/adapt the round-1/round-2 direct-reference tests; convert the now-out-of-scope round-3 tests (connection-end, dependency, allocate, bind, metadata, concern/viewpoint ownership, invocation expression, transitive chain) into explicit negative tests proving the narrow scope is genuinely narrow; add a new satisfy-by-subject positive test and a new connection-end negative test.
…esign State plainly what the orphan-evidence search checks (satisfy-by-subject; a direct reference from within a requirement's own body) and what it does not (connection-ends, sibling dependency/allocate/metadata relationships, Concern/Viewpoint ownership, a transitive chain through an unowned intermediate), with a brief, honest note on the history of broadening that led here. Remove every "exhaustive"/"field-agnostic" claim about the current design. Re-executed end to end via nbclient; the real model's own finding is unchanged.
…esign Same scope statement as the main chapter's own corrected cells, for the coffee domain. Smoke-tested separately with a real assert-satisfy-by fixture, confirming the same, unmodified library helper detects a satisfy-by-subject tie in this domain too.
This branch is still unmerged, so DL-071's own text is corrected directly rather than superseded again: describes the full history (vacuous -> broadened three times, each broadening finding a real gap -> a genuine scope question escalated to Z -> Z decided to narrow rather than keep broadening) and the final design Z settled on. Marks next-passes.md item 29 resolved with the final, accurate description. Flags a new, unrelated tool-gap finding (sysml-toolkit and the OMG pilot both reject a bare named connector declaration that OpenSysML accepts) for the ACE/orchestrator.
…t/pilot, accepted by OpenSysML Found while building a connection-end fixture for the ch10 tie-search fix. Same one-of-three-tools shape as D-034, but which tool(s) are actually correct per the grammar is not yet determined -- KerML.xtext's own Connector rule appears to permit this shape on a direct reading.
…isfy, fix invalid connection-end fixture
…cific issue A nested connector is rejected by sysml-toolkit/the pilot too, not only a top-level one -- the real pattern is that connector is a KerML surface keyword SysML's own grammar doesn't use (connection/connect is the SysML form), and OpenSysML is likely the one being too permissive, not the other two having a gap. Found during the ch10 widget-search fix's final review.
Replaces a structurally vacuous check (could never return True for any loadable model) with two small, explicitly-named, honestly-bounded checks: satisfy-by-subject (the tutorial's own idiom, reusing the existing satisfy_relationships helper) and a direct subsets/redefines/references/ referent reference from within a requirement's own body. Went through five rounds of independent review. Rounds 1-3 progressively broadened the search and each found a real, new gap (a missed require/assume reference; the tutorial's own satisfy idiom; a connection-end tie only round 3's own exclusion-list design still missed), plus a genuine scope question with no clean answer from the existing design -- escalated to Z, who decided to stop chasing an open-ended completeness search and narrow instead. Round 4 built the narrowed, two-check design (a real 99-line reduction). Round 5 found one residual overclaim plus two small correctness issues (a negated satisfy wrongly counted as a tie; an invalid test fixture), fixed directly. Also flagged a new, unrelated tool gap along the way (DEFERRED.md D-036: a KerML-only connector keyword accepted by OpenSysML in .sysml content, correctly rejected by the other two tools). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…t scoped to one constraint Found during the ch10 tie-remediation work: verify_holds's line parser fails on the FIRST satisfies-annotated line anywhere in a file, not just a specific constraint, so a targeted lookup of an unrelated constraint's own verdict still hits this gap if any assert satisfy appears earlier in the same file.
Add requirement def EnergyConservationReq (subject HeatGenerator, own require constraint subsetting deliveredEnergyBoundedBySupply), its usage energyConservationReq, and verification def EnergyConservationTest to models/ch08-cumulative.sysml, mirroring the existing TimelyToast / TimelyToastTest pattern exactly. Sync models/ch10-cumulative.sysml's body to stay byte-identical, per that file's own header comment. Register the two new construction notebooks in check_construction.py's CONSTRUCTION_STAGES[8] with minimal context_stubs; confirmed with --check (exit 0, all 10 chapters).
04-energy-conservation-req.ipynb introduces requirement def EnergyConservationReq and its usage energyConservationReq, and demonstrates toaster.query.tied_to_any_requirement() flipping from False to True for deliveredEnergyBoundedBySupply. 05-verification-case.ipynb introduces the matching verification def EnergyConservationTest, mirroring chapters/ch03-measures/04-verification-case.ipynb's own cell shape for TimelyToastTest. Both notebooks executed top to bottom via jupyter nbconvert --execute with no errors. index.md and conclusion.md updated: Ingredients table, Method, Expected result, and What we built.
Syncing ch10-cumulative.sysml (previous commit) gives the base model a real, unconditional tie via EnergyConservationReq, which every fixture in this file builds on top of. A constant, ENERGY_CONSERVATION_TIE, names that fixed entry; roughly twenty existing exact-equality assertions (discovered by running the suite, not by inspection alone) are extended to account for it while preserving each test's own original point (several 'finds nothing at all' scope-boundary tests now assert 'finds nothing beyond the base tie' instead, still correctly demonstrating their own construct contributes no additional entry). One requirement_coverage test (against ch08) also gained energyConservationReq in its expected requirement set, since it is a real, named RequirementUsage that function is correctly supposed to list. Full suite green after every edit.
Chapter 10's own notebooks 01 and 03 now fail their hardcoded 'assert not tied_to_a_requirement' when run against the synced ch10-cumulative.sysml -- expected and already deferred to Chapter 10's own follow-on contract by ENERGY-TIE-08's own text, confirmed here by actually executing them rather than assumed. Chapter 9's 01-requirement-coverage.ipynb and index.md now understate the model by one requirement and one satisfy relationship each -- a genuinely new finding this contract's own text did not anticipate, flagged for whoever owns ch09 next, not fixed here (out of this contract's blast zone).
…h coverage Round-1's own test fix (previous commit) kept every tests/test_query.py fixture on top of the real, now-tied ch10-cumulative.sysml and patched each expected result with a fixed ENERGY_CONSERVATION_TIE entry. That silently turned every tied_to_any_requirement(...) is False assertion in the file (12 of them) into is True, since the always-present base tie satisfies the boolean regardless of what any given fixture's own construct does -- independent review (claude-opus-5-5) caught this, named all 12, and showed a concrete mutant (bool(requirement_ties(...)) in place of the real any(t["requirement"] is not None for t in ...)) now survives 5 of them where it used to fail them on pass1/harness-alignment. Fixed properly instead, src/toaster/query.py untouched: a new _strip_energy_conservation_tie helper and ch10_pre_tie_source fixture remove the EnergyConservationReq/energyConservationReq/ EnergyConservationTest block back out of ch10-cumulative.sysml's own text, and every fixture-building test now concatenates that tie-free source instead of the real one -- restoring every one of those tests to its own original, pre-ENERGY-TIE-08 assertions verbatim. The real, current, tied model is checked in exactly one place now, test_requirement_ties_real_model_now_tied_via_energy_conservation_req (renamed from test_requirement_ties_negative_control_real_model), the only genuinely new semantic claim this contract makes. Re-ran the reviewer's exact mutant: the same 5 tests fail again. The self-contradicting docstring the round-1 fix left on test_requirement_ties_does_not_detect_transitive_chain_by_design is gone (that test is restored verbatim). DL-072 corrected in place to describe this design instead of the superseded one, and to restate the ch09 coverage finding precisely (energyConservationReq itself reports covered: False, a second uncovered requirement ch09's own narrative never mentions).
Records the full judgment process behind choosing Approach B over Approach A and the probed hybrid, and the direct spec reading (SysML v2 formal/2026-03-02 SS7.20-7.21) that found assert-satisfy-by-a-constraint to be legal but semantically vacuous here, and unnecessary given Check B's subsetting alone already satisfies both the spec's own satisfaction criterion and the project's finalized tie-detection checker.
…ent alone verify_satisfaction() errors identically on assert satisfy energyConservationReq by X regardless of X (the lemma, an unrelated part, or heatGenCheck itself) -- "require condition evaluation failed: no value for feature heatGenCheck.efficiency" in all three cases. Sharper than the earlier semantic- vacuity argument: the construct doesn't just add no information, it errors when exercised the way its own siblings (heatGenerationReq's real satisfy claims) are legitimately exercised. Records the steelman for keeping it, why it's outweighed, and the resolution (drop it, add one doc-comment sentence making the omission legible instead).
Approach A's EnergyConservationReq declared an unused subject (heatGen : HeatGenerator) that its own require-constraint never referenced, violating SysML v2 SS7.21.1's subject-conformance rule (confirmed independently against a parallel branch, fix/ch10-tie-remediation, whose author hit this as a live tool diagnostic and fixed it). Its verification def added spec ceremony without fixing that defect. Reverts, cleanly, exactly to ae6f40e: b6d48a4, 59276aa, 84df9b8, c8a2a88, ca5dbf7. Full rationale in docs/case-studies/2026-09-30-energy-conservation- requirement-tie.md. Approach B, revised (no assert-satisfy-by-constraint, per that same case study), is being reconciled on top of this next.
Independent review of the reconciliation contract found this document wrongly attributed the OMG pilot's "Bound features should have conforming types" warning to Approach A. Confirmed directly (git log -S and a fresh pilot run against each commit's own model): Approach A never had an assert-satisfy line at all, so the pilot had no live binding to flag and reports 0 issues on it. The warning belongs to Approach B's own first draft (26e184e), which paired a typed subject with an assert-satisfy line; B's author fixed it two commits later (56100bb). Approach A's own, different defect (a declared but unused subject) was found by direct spec reading, not by any tool.
…nergyConservationReq by subsetting, no assert satisfy Reconciles Approach A (reverted, subject-type violation) and Approach B (unmerged, kept an assert-satisfy line found by direct test to make model.verify_satisfaction() error identically regardless of binding). Final design: subject-less EnergyConservationReq/energyConservationReq, tied to the lemma only via require constraint c :> deliveredEnergyBoundedBySupply from within the requirement's own body (Check B). requirement_ties() now reports exactly one entry, attributed to the definition; requirement_coverage() reports the new requirement as covered=False by design; satisfy_relationships() stays at 4. Adapts every requirement_ties fixture test in test_query.py to filter out this new permanent base-model tie via _ties_for_fixture, and replaces test_requirement_ties_negative_control_real_model with test_requirement_ties_real_model_now_tied_via_remediation. See docs/case-studies/2026-09-30-energy-conservation-requirement-tie.md for the full working.
…add negative control Notebook 01: reconstructs the before-remediation state to show the honest "untied" finding, builds EnergyConservationReq (no declared subject, no assert satisfy), adds a negative-control demonstration that attempting assert satisfy energyConservationReq by deliveredEnergyBoundedBySupply makes model.verify_satisfaction() error identically regardless of binding, confirms sysmlv2 verify --solve emits no check at all for the bare subsetting reference, and revises AC-C10 to drop every Check-A-dependent claim while keeping its own core circularity finding. Notebook 03: updates the coverage/tie recheck to expect the new requirement (covered=False, tied via Check B on the definition), cites AC-C10, and revises AI-C10's claim/premises/rationale/counterevidence accordingly. Notebook 02: fixes one stale sentence claiming the lemma "is not tied to any requirement usage" (now true only before remediation). index.md/conclusion.md: narrate the one new model element, the no-assert- satisfy decision, and AC-C10's own honest framing.
… timely's real gap Chapter 10's own new requirement (added this contract) also reports covered=False under this chapter's requirement_coverage() helper, but for a structurally different reason than timely's: a deliberate design choice (tied by subsetting an already-proved lemma, not by assert satisfy), not an omission a learner could still close by more querying. Adds a forward- pointing clarification to notebook 01 and index.md so a reader reaching Chapter 10 does not misread the new requirement as a second, undiscovered instance of this chapter's own finding.
…rop Check A Mirrors the real chapter's own remediation in the coffee-maker domain: a new Step 2 right after the traceability search asks the learner to build their own MassConservationReq-style requirement, subject-less, tied to deliveredMassBoundedBySupply by subsetting only (explicitly warning against repeating the real chapter's own reverted subject-type mistake), with no assert satisfy line. Renumbers the former Step 2/3 to Step 3/4, updates the coverage/tie assertions to expect the tie now holds, and adds a blank- scaffold AC-C10-EX judgment record following the same structural-fields- real/argued-fields-hinted split every other record in this exercise uses.
…es item 29 DL-072 records the reconciliation of Approach A and Approach B into the final design, pointing to the case study document for the full rationale. next-passes.md item 29 is now fully closed: the search DL-070/DL-071 fixed had nothing real to find until this contract added the tie it was built to detect.
…olver wording, exercise NameError, check_construction guard, stale-wording cleanup F1: restore real tied_to_any_requirement()/requirement_ties() calls in every TieFixture test, replacing the local _ties_for_fixture/_fixture_tied_to_any_requirement reimplementation with a pre-tie reconstruction of models/ch10-cumulative.sysml (CH10_SOURCE_WITHOUT_TIE) so the real functions can be called directly without the base model's own permanent tie contaminating the result. Confirmed with the reviewer's own mutant (tied_to_any_requirement returning bool(requirement_ties(...))): 5 tests fail with the mutant, 0 without it. F2: fix AC-C10/AI-C10's overclaim that assert-satisfy 'generates no separate verdict at all' under sysmlv2 verify --solve -- false: adding it back makes the solver emit a real 'undecided' verdict, just not a satisfied one. Replaced the prose-only solver contrast with a real, executed cell (energy-tie scratch file, subprocess, assert on the undecided line). Extended the verify_satisfaction() negative control to three real bindings (the lemma itself, its own free-standing usage, an unrelated candidate) so the 'regardless of what is bound' claim in AC-C10's evidence_refs is actually earned, not inferred from one binding. F3: exercises/ch10/exercise.ipynb's AC-C10-EX cell used ReviewRecord/hash_content/ validate_record before their own import (first introduced two cells later, in what is now Step 3) -- NameError at Step 2 for a learner running top to bottom. Moved the import to AC-C10-EX's own cell. Confirmed via a static use-before-def AST scan (no coffee model is committed to execute this notebook directly): the import-related NameError is gone; the remaining flags are pre-existing, unrelated comprehension-traversal-order false positives in untouched cells, confirmed by direct inspection. N1: register chapters/ch10-traceability-signoff/01-traceability-graph.ipynb's own TOASTER_INCREMENT in scripts/check_construction.py's CONSTRUCTION_NOTEBOOKS[10] (a real guard gap, not just a stale comment -- confirmed the stub passes and its absence fails). N2/Q1: reworded the 'no subject' justification everywhere it was repeated (doc comment, models/ch10-cumulative.sysml, notebook 01's cells 22/24/38/40) to state the real reason -- the required constraint never references any subject at all -- instead of the leftover Approach-B framing about a satisfying feature conforming to a subject type, which no longer applies once assert satisfy is gone. N3: tidied cell 24's pilot-check wording to be clearly about this branch's own model, not implicitly about Approach B's. N5: cited DEFERRED.md D-029 as the reason cell 42 shells out to sysmlv2 directly rather than through toaster.modelcheck's own wrapper. N6: fixed stale 'Step 2' references (now Step 3) in the exercise's own cell-43, renamed the _s3 variable suffix to _s4 to match the actual renumbering, fixed notebook 03's 'not a fourth gap' miscounted phrasing, and index.md's 'Trace both requirements' table row (now two of three).
…e pilot's subject-type warning G1: this round's own expanded cells had conflated two distinct earlier drafts' own defects. Approach A (reverted at 85b7778) never added an assert satisfy line at all -- its own defect was a declared, unused subject, found by direct spec reading, not by any tool diagnostic. The real OMG pilot warning ('Bound features should have conforming types') belongs to Approach B's own first commit (26e184e), which paired a typed subject with a real assert satisfy line; Approach B's own author fixed that by dropping the subject two commits later (56100bb), before this reconciliation began. Corrected in notebook 01 (cell 22, AC-C10 premise 2), models/ch10-cumulative.sysml's own header comment, and decisions/log.md DL-072 (amended in place, since it has not landed on pass1/harness-alignment yet). N2: fixed the three remaining occurrences of the stale 'satisfying feature conforms to subject type' framing (index.md, conclusion.md, exercise.ipynb Step 2) to state the real reason instead -- the required constraint never references a subject at all.
mzargham
added a commit
that referenced
this pull request
Oct 1, 2026
Pass 1 (harness alignment) + Pass 4 (Chapters 1-10 didactic content)
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
1 participant
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 this is
Pass 1 (harness alignment) and Pass 4 (didactic content, Chapters 1-10) of the toaster SysML v2 tutorial rebuild, squashed into a single branch for review.
Pass 1 rewrote AGENTS.md into a Foundations document (what/how/where layering, MoE/MoP/TPM, the judgment taxonomy), built a local glossary knowledge graph (
glossary/) as the source of truth for terms, and aligned the skills, decision log and role definitions to it.Pass 4 re-derived or authored all ten chapters against that aligned Foundations:
ApplyHeat)decisions/pass4-run-004.mddecisions/pass4-run-005.mddecisions/pass4-run-006.mdCyclestate machine,deliveredEnergy)decisions/pass4-run-007.mddecisions/pass4-run-008.mddecisions/pass4-run-009.mddecisions/pass4-run-010.mdEach chapter went through an independent builder/reviewer pipeline (different models for author and reviewer), with review rounds logged in the run log above.
Since the last description update: closing the one open gap Chapter 10 itself found
Chapter 10's own traceability search correctly, honestly reported that Chapter 8's Z3-proved conservation lemma (
deliveredEnergyBoundedBySupply) was tied to no stated requirement — originally treated as deliberate pedagogy (the inverse of an "unjustified widget"). On review, using something that plausibly should be tied as the worked example of "not tied" was judged confusing, so a real tie was added instead, with the pedagogy preserved via a separate, deliberately-untied fixture.Two independently-built designs for the tie were attempted the same day (discovered mid-session, not planned redundancy), reconciled into one final design after a full spec-letter-vs-spec-intent interrogation of SysML v2 §7.20–7.21 and §7.24 and two rounds of independent review. The full working — including a design that was built, reviewed twice, merged, and then reverted after a deeper defect was found — is recorded in
docs/case-studies/2026-09-30-energy-conservation-requirement-tie.md, kept because the reasoning is as much the point as the final construct.decisions/log.mdDL-072 anddecisions/next-passes.mditem 29 record the closure.Verification
uv run pytest -q→ 411 passed, 7 deselected;uv run pytest -q -m checkpoint→ 7 passed (418/418 total).uv run python scripts/check_construction.py --check→ all 10 chapters consistent.uv run python -m glossary check→ 0 errors (7 pre-existing source-PDF-absent warnings).build) green on this head; every notebook executes cleanly with real, non-empty output.Open items for review
decisions/next-passes.mdtracks everything flagged along the way that wasn't fixed in-place (29 items; none block this merge — each is scoped as input to a later pass: exercise-track follow-ups, upstream issue filing, a couple of recorded-but-not-acted-on tooling ideas).DEFERRED.mdhas the toolchain gaps found (D-001 through D-036), each with a workaround recorded, a citation, and a drafted (unfiled, where relevant) upstream issue.🤖 Generated with Claude Code