This notebook introduces check_stale() applied across a small set of tracked records at once, not just one; after running it you can tell, for each of two real records, whether it is still current against the real, committed model, and watch what a real model edit actually does to each one.
Chapter 8 notebook 03 already showed check_stale() on one record against one lemma. This notebook keeps the chapter’s original filename (03-stale-detection.ipynb): the content is genuinely about scale -- checking several tracked records against the real, current model in one pass -- but “at scale” over two records is still a small, honestly-scoped demonstration, not a claim that every record this tutorial has ever produced is being tracked (notebook 02’s own scope note applies here too). It reuses notebook 02’s own two records, AS-C06 and AS-C08, rebuilt verbatim below (the exact same field strings notebook 02 uses) since each notebook in this tutorial loads and runs independently.
from pathlib import Path
import opensysml
from toaster.report import format_diagnostics
conn = opensysml.connect(version="v0.9.0")
source = Path("../../models/ch08-cumulative.sysml").read_text()
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}"
A record with an empty identifier fails validation outright, distinct from staleness: it was never a valid record to begin with, regardless of which model it references (the same control Chapter 8 notebook 03 used).
from toaster.evidence import ReviewRecord, hash_content, validate_record
broken = ReviewRecord(
identifier="", # intentionally empty
kind="asserted_solution",
claim="Some claim",
subject_ref="ToasterDemo::deliveredEnergyBoundedBySupply",
model_ref="ToasterDemo",
content_hash=hash_content(source),
scope="Some scope",
criteria="Some criteria",
rationale="Some rationale",
counterevidence="Some counterevidence",
record_kind="worked_example",
)
errors = validate_record(broken, model=model)
assert errors == ["identifier is empty"], f"Expected exactly one error, got {errors}"
print(f"Negative control ok: errors={errors}")
Negative control ok: errors=['identifier is empty']
AS-C06 and AS-C08, loaded below via load_record(), the exact same records notebook 02 loads (see notebook 02 for the narration behind each field): AS-C06’s content_hash against models/ch06-cumulative.sysml, the model it was actually written against; AS-C08’s against models/ch08-cumulative.sysml, the real, current model this notebook also loads above.
from toaster.judgment_store import load_record
ch06_source = Path("../../models/ch06-cumulative.sysml").read_text()
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, the record Chapter 8’s own Z3 proof grounds, loaded the same way, via load_record().
as_c08 = load_record("AS-C08")
errors = validate_record(as_c08, model=model)
print(f"AS-C08 validation errors: {errors}")
AS-C08 validation errors: []
Checked against models/ch08-cumulative.sysml before any edit: AS-C06 was written against models/ch06-cumulative.sysml, and is already stale, but not from mere unrelated bookkeeping. AS-C08 was written against this exact file, so it is still current.
from toaster.evidence import check_stale
tracked = {"AS-C06": as_c06, "AS-C08": as_c08}
print("Before any edit:")
for identifier, record in tracked.items():
print(f" {identifier}: stale={check_stale(record, source)}")
assert check_stale(as_c06, source) is True
assert check_stale(as_c08, source) is False
Before any edit:
AS-C06: stale=True
AS-C08: stale=False
AS-C06’s own counterevidence names something specific as still missing: “Joule heating’s own relation ... is still not modeled, so efficiency and response-time comparisons remain out of reach either way.” A direct diff between models/ch06-cumulative.sysml and the current model shows that gap partly overtaken, not exactly closed: Chapter 7 added efficiency, efficiencyBounded and deliveredEnergy to HeatGenerator, squarely inside the scope AS-C06 itself declares (ToasterDemo::HeatGenerator and its realizations), so an efficiency comparison can now at least be started. The Joule-heating relation the same counterevidence names, and any response-time comparison, are still not modeled. AS-C06 is not just formally stale, a hash mismatch; its own stated uncertainty has been substantively overtaken by real, subsequent model growth -- a record that could now, at least in part, actually be re-checked against something that did not previously exist.
import difflib
ch06_lines = ch06_source.splitlines()
ch08_lines = source.splitlines()
added = [
line for line in difflib.unified_diff(ch06_lines, ch08_lines, lineterm="")
if line.startswith("+") and not line.startswith("+++")
]
efficiency_lines = [line for line in added if "efficiency" in line.lower()]
print(f"{len(efficiency_lines)} added lines mention efficiency, including:")
for line in efficiency_lines[:3]:
print(f" {line.strip()}")
assert efficiency_lines, "Expected efficiency-related growth between ch06 and the current model"
18 added lines mention efficiency, including:
+ attribute efficiency : DimensionOneValue;
+ assert constraint efficiencyBounded {
+ doc /* Efficiency is the fraction of supplied energy delivered as
AS-C08’s own residual_uncertainties names a different, specific risk: editing HeatGenerator’s own efficiencyBounded or deliveredEnergy would stale this record. The edit applied next is NOT that: it loosens deliveredEnergyBoundedBySupply’s own bound (the companion lemma copy the record is actually about), a different part of the same file. check_stale() still reports the record stale, for a reason its own text is explicit about: content_hash is computed from the WHOLE model file, so any edit anywhere in it, not only to the specific elements a record’s own residual names, invalidates the hash -- a real, partial safeguard, honestly not a check that the specifically-named risk is what actually happened.
# Loosen the lemma's own bound (the companion copy AS-C08 is actually about), not
# HeatGenerator's efficiencyBounded/deliveredEnergy (the elements its own residual
# names as a risk) -- a different part of the same file.
revised_source = source.replace(
"heatGenCheck.efficiency <= 1.0",
"heatGenCheck.efficiency <= 1.2",
)
assert revised_source != source, "Expected the replacement to change the source"
assert "0.0 <= efficiency and efficiency <= 1.0" in revised_source, (
"efficiencyBounded's own bare-`efficiency` bound must be untouched by this edit"
)
revised_model = conn.load_from_content(revised_source, strict=False)
assert revised_model.ok, "Revised model should still parse"
print("After loosening deliveredEnergyBoundedBySupply's own bound (1.0 -> 1.2):")
for identifier, record in tracked.items():
print(f" {identifier}: stale={check_stale(record, revised_source)}")
assert check_stale(as_c06, revised_source) is True
assert check_stale(as_c08, revised_source) is True
conn.close()
After loosening deliveredEnergyBoundedBySupply's own bound (1.0 -> 1.2):
AS-C06: stale=True
AS-C08: stale=True
Both records now report stale, but the two histories are genuinely different. AS-C06 was stale before this edit too, and for a reason this specific edit has nothing to do with: real growth (Chapter 7) partly overtook the gap its own counterevidence named, without closing it (the Joule relation and response-time comparisons are still unmodeled). AS-C08 newly went stale from an edit to a different construct than the one its own residual specifically warned about, caught only because the hash covers the whole file. Reading each record’s own fields against the real model diff, not just its stale/current status, is what surfaces why each one changed: checking either record alone, at either point, would only have reported “stale” or “current,” not the reason.
Two records, tracked and checked together against the same file before and after one real edit, reported two different histories: one substantively overtaken by real growth, the other caught by a coarse, whole-file safeguard rather than a targeted one.
Try the chapter exercise in exercises/ch09/exercise.ipynb: it asks you to check your own two records for staleness, at scale, the same way this notebook checks AS-C06 and AS-C08 together.