This notebook introduces a judgment ledger over three real ReviewRecords already built earlier in this tutorial; after running it you can see what each one claims, which of Hawkins’ three judgment kinds it represents, and what its own residual_uncertainties says is not yet resolved.
This tutorial has no central registry of every ReviewRecord it has ever built, the same finding Chapter 9 made when it searched for one: each chapter’s judgment is authored once, in Python, at the chapter where it is made, per the construction-zone pattern; what Chapter 9 found missing was the other half of that design, a persisted store a later chapter could query -- toaster.judgment_store now supplies it, so a record built once is saved with save_record() and loaded elsewhere with load_record(), never reconstructed. So this notebook does not scan “every record the tutorial has ever produced”; instead it loads three real records from that store: AS-C06 and AS-C08, already loaded the same way in Chapter 9, plus one more, AI-C06 (Chapter 6’s own stopping judgment over the level-2 heat-generation branch, an asserted_inference, alongside the two asserted_solution records Chapter 9 already carried forward). What follows demonstrates the mechanics of a judgment ledger on a small, representative sample, not an exhaustive audit of every judgment record this tutorial has ever produced.
from pathlib import Path
import opensysml
from toaster.report import format_diagnostics
from toaster.judgment_store import load_record
conn = opensysml.connect(version="v0.9.0")
source = Path("../../models/ch10-cumulative.sysml").read_text()
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}"
Before reconstructing the three records, the negative control fitting this notebook’s own new record, AI-C06: Hawkins SS3.1 requires an asserted_inference to name at least one premise, since a bare assertion with nothing supporting it is not an inference at all. validate_record() already enforces this.
from toaster.evidence import ReviewRecord, hash_content, validate_record
incomplete_inference = ReviewRecord(
identifier="AI-BAD",
kind="asserted_inference",
claim="The judgment ledger is complete.",
subject_ref="ToasterDemo::HeatingAssembly::heatGen",
model_ref="ToasterDemo",
content_hash=hash_content(source),
scope="ToasterDemo",
criteria="Every real ReviewRecord this tutorial has built is included.",
premises=[], # intentionally empty
rationale="Chapter 10 built a ledger.",
counterevidence="No central registry exists to check completeness against.",
record_kind="worked_example",
)
errors = validate_record(incomplete_inference, model=model)
assert errors == ["asserted_inference requires at least one premise (Hawkins \u00a73.1)"], errors
print(f"Negative control ok: errors={errors}")
Negative control ok: errors=['asserted_inference requires at least one premise (Hawkins §3.1)']
AS-C06, loaded below via load_record() from the record Chapter 6 notebook 02 persisted with save_record(), the same record Chapter 9 already carries forward: a mechanism-selection judgment, argued from a domain premise about how a resistive element and a combustion burner each respond to a discrete timing signal. Its content_hash was computed against models/ch06-cumulative.sysml when that record was built and persisted, the real model it was actually written against.
as_c06 = load_record("AS-C06")
errors = validate_record(as_c06, model=model)
print(f"AS-C06 validation errors: {errors}")
AS-C06 validation errors: []
AS-C08, loaded the same way, via load_record(), from the record Chapter 8 notebook 02 persisted with save_record(): the record grounded in that chapter’s real Z3 proof of deliveredEnergyBoundedBySupply, the same one notebook 01 of this chapter found disconnected from any requirement usage and then tied, by subsetting, to energyConservationReq. Its content_hash was computed against models/ch08-cumulative.sysml when that record was built and persisted, the model it was actually written against.
as_c08 = load_record("AS-C08")
errors = validate_record(as_c08, model=model)
print(f"AS-C08 validation errors: {errors}")
AS-C08 validation errors: []
AI-C06, the third record, is genuinely different in kind: an asserted_inference about the level-2 heat-generation branch’s own stopping judgment, loaded below via load_record() from the record Chapter 6 notebook 03 persisted with save_record(). Its premises field names four earlier judgment identifiers directly (AC-C06, AS-C06, AS-C03, AI-C04), the clearest example in this tutorial of Hawkins’ own “child claims supporting a parent” idea. Its evidence_refs cites the same real analysis results Chapter 6 notebook 03 gathered against that chapter’s own model, rather than recomputed or restated by hand here. Its content_hash was also computed against that same file when the record was persisted, since both AI-C06 and AS-C06 above were written against Chapter 6’s own model.
HeatGenerator performs GenerateHeat, heatGenAllocation points from applyHeat.generateHeat to heatGen, declared inside HeatingAssembly where both resolve, and the requirement evaluates True on rated and False on weak -- the same three real results Chapter 6 notebook 03 gathered, carried forward in ai_c06’s own evidence_refs below rather than reprinted here. The record below is loaded via load_record(), the same pattern now used for AS-C06 and AS-C08 above.
ai_c06 = load_record("AI-C06")
errors = validate_record(ai_c06, model=model)
print(f"AI-C06 validation errors: {errors}")
AI-C06 validation errors: []
All three validate cleanly. The ledger below reports each record’s kind (Hawkins’ three sites: asserted_context, asserted_inference, asserted_solution), its disposition and record_kind (by this tutorial’s standing rule: always pending, always worked_example, never the forbidden alternatives), and its engineering_conclusion, next to what its own residual_uncertainties says is NOT yet resolved.
ledger = {"AS-C06": as_c06, "AS-C08": as_c08, "AI-C06": ai_c06}
for identifier, record in ledger.items():
print(f"{identifier}:")
print(f" kind: {record.kind}")
print(f" disposition: {record.disposition}")
print(f" record_kind: {record.record_kind}")
print(f" engineering_conclusion: {record.engineering_conclusion}")
print(f" residual_uncertainties: {record.residual_uncertainties}")
print()
assert all(r.disposition == "pending" for r in ledger.values())
assert all(r.record_kind == "worked_example" for r in ledger.values())
conn.close()
AS-C06:
kind: asserted_solution
disposition: pending
record_kind: worked_example
engineering_conclusion: undetermined
residual_uncertainties: Once a supply and a control policy are modeled together, this selection could be revisited against a real trade study rather than a domain premise alone.
AS-C08:
kind: asserted_solution
disposition: pending
record_kind: worked_example
engineering_conclusion: supported
residual_uncertainties: Whether efficiency, power and duration ever take values outside the bound in a real candidate is not addressed by this proof; it establishes only that the restated lemma respects conservation wherever its own bound is honored. If HeatGenerator's own efficiencyBounded or deliveredEnergy is ever edited, this record's content_hash (computed from the whole model file) does go stale, which forces a re-review, but nothing automatically re-checks that the restated copy still matches the edited original; that check would be manual. No physical heat generator has been checked against this property; HeatGenerator remains an abstract carrier with no concrete realization of its own.
AI-C06:
kind: asserted_inference
disposition: pending
record_kind: worked_example
engineering_conclusion: undetermined
residual_uncertainties: Whether GenerateHeat needs further decomposition of its own, whether HeatingAssembly is ever composed into a real Toaster candidate, and whether ApplyHeat's other flows (duration, bread, toast) get their own level-2 branches, are open for whichever chapter takes them up.
The ledger above lists the three records one at a time. The figure below shows how they depend on each other. Each record carries a premises field; wherever a premise is the identifier of another stored record, the figure draws an arrow from that record to the one citing it. It leaves out premises that are free-text statements, which are not records.
from toaster.render import render_dot
from IPython.display import SVG
def stored(identifier):
"""The stored record for `identifier`, or None when the store has none (a free-text premise has none)."""
try:
return load_record(identifier)
except OSError: # FileNotFoundError, or a free-text premise too long to be a file name
return None
nodes = dict(ledger)
for record in ledger.values():
for premise in record.premises:
if premise not in nodes and (upstream := stored(premise)):
nodes[premise] = upstream
edges = [(premise, identifier) for identifier, record in nodes.items() for premise in record.premises if premise in nodes]
dot_lines = [
'digraph "record dependencies" {',
" rankdir=LR;",
' graph [fontname="Helvetica" bgcolor=white labelloc=b label="shaded: the three ledger records; white: upstream records\\narrow: cited as a premise of"];',
' node [shape=box fontname="Helvetica" style=filled fillcolor=white];',
' edge [fontname="Helvetica"];',
]
for identifier, record in nodes.items():
fill = "#cfe3f7" if identifier in ledger else "white"
dot_lines.append(f' "{identifier}" [label="{identifier}\\n{record.kind}" fillcolor="{fill}"];')
for premise, identifier in edges:
dot_lines.append(f' "{premise}" -> "{identifier}";')
dot_lines.append("}")
out_path = Path("../../figures/ch10-record-dependencies.svg")
out_path.parent.mkdir(exist_ok=True)
render_dot("\n".join(dot_lines), out_path)
SVG(filename=str(out_path))Records are nodes and arrows are record-to-record premise links, read from each record’s premises field in the store; an arrow means “is cited as a premise of”, not “has been approved”. Omitted: free-text premises, links from records to model elements, the evidence each record cites, and records reachable only through an upstream record’s own premises.
Three real records, three different points of confidence. AS-C06 stays undetermined: its own residual admits the mechanism selection could be revisited against a real trade study once a supply and control policy are modeled together, not settled by the domain premise alone. AS-C08 is supported, but narrowly: its own residual is explicit that the restated lemma is not automatically re-checked against the real elements it mirrors if either is edited, and that no physical heat generator has ever been checked against it. AI-C06 stays undetermined too: its own residual leaves open whether GenerateHeat needs further decomposition, whether HeatingAssembly is ever composed into a real Toaster candidate, and whether ApplyHeat’s other flows get their own branches. Two records out of three stay undetermined, and the one supported record is supported only for a claim already narrowed to a hand-restated copy, not the real elements it mirrors. That is what a ledger is for: not a tally of how many records exist, but a reading of how much of that count is actually load-bearing.
Building three real judgment records side by side, reading their own kind, disposition and residual uncertainty rather than just their count, is what turns “this tutorial has produced some ReviewRecords” into a ledger an accountable engineer could actually use: what follows next, in notebook 03, synthesizes this ledger together with notebook 01’s own traceability graph.
Try the chapter exercise in exercises/ch10/exercise.ipynb: it asks you to build this same traceability graph and judgment ledger over your own coffee-maker model, then synthesize both into one honestly-scoped sign-off record.