This notebook introduces asserted_inference; after running it you can record a functional-completeness judgment tying child claims to a parent claim, following Hawkins §3.1.
The Chapter 4 model now nests ApplyHeat inside ToastBread, with typed flows for bread and energy and a balance constraint bounding delivered energy and loss by the energy supplied. The question this notebook asks is narrower than whether the toaster’s functional architecture is complete: it is whether the flows this one worked example names are accounted for, honestly scoped to what one action out of Douglas’s roughly fifteen verb-noun functions can show.
from pathlib import Path
import opensysml
from toaster.evidence import ReviewRecord, hash_content, validate_record
from toaster.judgment_store import save_record
from toaster.report import format_diagnostics
conn = opensysml.connect(version="v0.9.0")
source = Path("../../models/ch04-cumulative.sysml").read_text()
lines = source.splitlines()
new_this_chapter = "\n".join(lines[16:32] + lines[37:47] + lines[107:116])
print(new_this_chapter)
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}"
action def ApplyHeat {
in bread : Bread;
in energy : ISQ::EnergyValue[0..*];
in duration : ISQ::DurationValue[0..*] {
doc /* Signal from a control function: how long to apply heat.
* No control function is modeled in this chapter, so this input
* is declared and typed but not yet connected to a value. */
}
out toast : Toast;
out delivered : ISQ::EnergyValue;
out loss : ISQ::EnergyValue;
assert constraint balance {
delivered >= 0.0 [SI::J] and loss >= 0.0 [SI::J] and delivered + loss <= energy
}
}
action def ToastBread {
doc /* Transform bread into toast acceptable to its user. */
in bread : Bread;
out toast : Toast;
first start;
then action applyHeat : ApplyHeat {
in bread = ToastBread::bread;
}
then done;
}
item def Start {
doc /* Signal marking the start of a toasting cycle, not the bread itself. */
}
item def Finish {
doc /* Signal marking the finish of a toasting cycle, not the toast itself. */
}
item def Cancel {
doc /* Signal requesting cancellation of an in-progress toasting cycle. */
}
The composed Toaster so far, drawn directly from the model that just loaded: the same part structure as before, confirmed unchanged without re-reading the dump above.
from toaster.render import model_to_dot, render_dot, containment_subgraph
from IPython.display import SVG
dot = model_to_dot(
model,
title="Ch4",
elements=containment_subgraph(model, "ToasterDemo::Toaster", depth=2),
)
out_path = Path("../../figures/ch04-structure.svg")
out_path.parent.mkdir(exist_ok=True)
render_dot(dot, out_path)
SVG(filename=str(out_path))The cumulative model prints above: ApplyHeat with its balance constraint, nested inside ToastBread, and the three signal item definitions from the previous notebook. The next cell checks what happens when a constraint references a feature the action definition does not declare.
# Negative control: an asserted constraint referencing a feature the action
# definition does not declare raises "unresolved reference".
bad_source = """
package Bad {
private import ScalarValues::*;
action def BadHeat {
in energy : Real;
out delivered : Real;
out loss : Real;
assert constraint balance { delivered + loss <= notAFeature }
}
}
"""
bad = conn.load_from_content(bad_source, strict=False)
assert not bad.ok
print("Expected error:", bad.diagnostics[0].message)
Expected error: unresolved reference: notAFeature
With the negative control confirmed, the next cells build AI-C04: an asserted_inference record about ApplyHeat’s own flow accounting, following the construction zone Hawkins’ taxonomy uses (anchor, claim, frame, premises, evidence, challenge, assemble).
Before AI-C04 states its claim, the next cells give it a real anchor in the model: a ReviewRecordRef tag naming ApplyHeat as what AI-C04 is about.
# what is being claimed, and what, specifically, it is about
subject_ref = "ToasterDemo::ApplyHeat"
AI_C04_TAG = """\
metadata aiC04Tag : ReviewRecordRef about ApplyHeat {
identifier = "AI-C04";
}
"""
print(AI_C04_TAG)
metadata aiC04Tag : ReviewRecordRef about ApplyHeat {
identifier = "AI-C04";
}
This fragment is the same text now committed in models/ch04-cumulative.sysml onward, alongside the ReviewRecordRef definition (carried forward from Chapter 2); loading the cumulative model (the model.ok cell above, unchanged) is what makes this a real, checkable tag rather than an assertion the reader has to trust.
TOASTER_INCREMENT = AI_C04_TAG
AI-C04 states the claim next: what is being claimed, and about which model element.
claim = ("ApplyHeat's typed flows account for bread, energy and duration in, and "
"toast, delivered energy and loss out; the asserted balance constraint "
"(delivered and loss each non-negative, their sum bounded by energy) is a "
"real, evaluable relation, not merely declared syntax. ApplyHeat is a step "
"of ToastBread, its bread input bound to ToastBread's own bread.")
model_ref = "ToasterDemo::ApplyHeat"
print(claim)
ApplyHeat's typed flows account for bread, energy and duration in, and toast, delivered energy and loss out; the asserted balance constraint (delivered and loss each non-negative, their sum bounded by energy) is a real, evaluable relation, not merely declared syntax. ApplyHeat is a step of ToastBread, its bread input bound to ToastBread's own bread.
The standard the claim is checked against: what would make this flow accounting complete, at the scope this one worked example claims (Hawkins’ appropriateness).
scope = "ToasterDemo::ApplyHeat, nested inside ToasterDemo::ToastBread"
criteria = ("Every declared flow (bread, energy, duration in; toast, delivered, loss "
"out) is named and typed, and the asserted balance constraint (delivered "
"and loss each non-negative, their sum bounded by energy) evaluates against "
"concrete values, holding or failing as conservation requires. This is not "
"the criterion for the toaster's full functional architecture (about "
"fifteen verb-noun functions, index.md); it is the criterion for this one "
"worked example.")
print(criteria)
Every declared flow (bread, energy, duration in; toast, delivered, loss out) is named and typed, and the asserted balance constraint (delivered and loss each non-negative, their sum bounded by energy) evaluates against concrete values, holding or failing as conservation requires. This is not the criterion for the toaster's full functional architecture (about fifteen verb-noun functions, index.md); it is the criterion for this one worked example.
What the claim takes as given: the prior chapter’s satisfaction judgment, and one modeling choice this chapter itself makes.
premises = ["AS-C03"]
assumption_refs = [
"duration is declared as a typed input but plays no role in the balance "
"constraint: this chapter does not derive delivered energy from duration, "
"so duration's own denotation as a signal from a control function is stated "
"but not yet connected to any computation.",
]
print(assumption_refs)
["duration is declared as a typed input but plays no role in the balance constraint: this chapter does not derive delivered energy from duration, so duration's own denotation as a signal from a control function is stated but not yet connected to any computation."]
Sufficiency needs real evidence too for notebook 01’s fix: writing energy and duration with an explicit [0..*] keeps the whole model evaluable, not just ApplyHeat in isolation. The next cell checks this directly against the model already loaded above.
slow_cycle_time = model.eval("ToasterDemo::slow.cycleTime")
print(f"slow.cycleTime: {slow_cycle_time}")
slow.cycleTime: 200 [SI::s]
slow.cycleTime evaluates to the 200-second value Chapter 2 gave it, unrelated to ApplyHeat entirely: the explicit [0..*] keeps the model fully evaluable, exactly the claim evidence_refs cites below.
Sufficiency also needs evidence for the balance constraint itself, not just a description of what it would do. The next cell builds three usages of ApplyHeat: one plausible, one that overdraws the energy budget, and one with a negative loss, in a small model that mirrors ApplyHeat’s own declaration rather than the toaster’s own model, since nominal and slow carry no concrete energy, delivered or loss values to check the constraint against.
PROBE_SOURCE = """
package Probe {
private import ScalarValues::*;
private import SI::*;
private import ISQ::*;
item def Bread;
item def Toast;
action def ApplyHeat {
in bread : Bread;
in energy : ISQ::EnergyValue[0..*];
in duration : ISQ::DurationValue[0..*];
out toast : Toast;
out delivered : ISQ::EnergyValue;
out loss : ISQ::EnergyValue;
assert constraint balance {
delivered >= 0.0 [SI::J] and loss >= 0.0 [SI::J] and delivered + loss <= energy
}
}
action plausibleHeat : ApplyHeat {
:>> energy = 1000.0 [SI::J];
:>> delivered = 700.0 [SI::J];
:>> loss = 200.0 [SI::J];
}
action implausibleHeat : ApplyHeat {
:>> energy = 1000.0 [SI::J];
:>> delivered = 900.0 [SI::J];
:>> loss = 300.0 [SI::J];
}
action negativeLossHeat : ApplyHeat {
:>> energy = 1000.0 [SI::J];
:>> delivered = 1500.0 [SI::J];
:>> loss = -600.0 [SI::J];
}
}
"""
probe_model = conn.load_from_content(PROBE_SOURCE, strict=False)
assert probe_model.ok
probe_verdicts = {}
for name in ("Probe::plausibleHeat", "Probe::implausibleHeat", "Probe::negativeLossHeat"):
probe_verdicts[name] = probe_model.verify_constraint(
"Probe::ApplyHeat::balance", subject=name
)
print(f"{name}: {probe_verdicts[name]}")
Probe::plausibleHeat: ✓ constraint Probe::ApplyHeat::balance holds (on Probe::plausibleHeat ID: 1) — observed by run
Probe::implausibleHeat: ✗ constraint Probe::ApplyHeat::balance fails (on Probe::implausibleHeat ID: 1): condition evaluated to false: delivered >= 0.0 [SI::J] and loss >= 0.0 [SI::J] and delivered + loss <= energy — witnessed by run
Probe::negativeLossHeat: ✗ constraint Probe::ApplyHeat::balance fails (on Probe::negativeLossHeat ID: 1): condition evaluated to false: delivered >= 0.0 [SI::J] and loss >= 0.0 [SI::J] and delivered + loss <= energy — witnessed by run
The constraint holds for the plausible usage and fails for both faulty ones: the implausible split that overdraws the energy budget, and the negative-loss usage that satisfies the sum bound alone only by letting loss go negative. Asserting non-negativity alongside the sum bound is what catches this second case; evidence_refs and rationale cite all three results directly.
evidence_refs = [
f"ToasterDemo::slow.cycleTime: {slow_cycle_time}, evaluated directly against "
"the loaded model above.",
f"balance constraint probe: {probe_verdicts['Probe::plausibleHeat']}",
f"balance constraint probe: {probe_verdicts['Probe::implausibleHeat']}",
f"balance constraint probe: {probe_verdicts['Probe::negativeLossHeat']}",
"ToasterDemo::ToastBread::applyHeat: ApplyHeat resolves as a nested action "
"usage with its bread input bound to ToastBread::bread, confirmed by "
"model.find() in the previous notebook.",
]
rationale = ("Every parameter ApplyHeat declares is named in the claim above, and the "
"explicit [0..*] on energy and duration keeps the whole model evaluable: "
"slow.cycleTime, unrelated to ApplyHeat, evaluates cleanly above. The "
"asserted balance constraint is not merely stated either: the probe above "
"shows it holds for values consistent with conservation and fails for both "
"an overdrawn split and a negative-loss split, so the non-negativity bounds "
"are doing real work, not just the sum bound. ApplyHeat is reachable from "
"ToastBread's own sequence, so it is a step of a decomposition, not a "
"definition nothing composes.")
print(rationale)
Every parameter ApplyHeat declares is named in the claim above, and the explicit [0..*] on energy and duration keeps the whole model evaluable: slow.cycleTime, unrelated to ApplyHeat, evaluates cleanly above. The asserted balance constraint is not merely stated either: the probe above shows it holds for values consistent with conservation and fails for both an overdrawn split and a negative-loss split, so the non-negativity bounds are doing real work, not just the sum bound. ApplyHeat is reachable from ToastBread's own sequence, so it is a step of a decomposition, not a definition nothing composes.
The challenge: what this does not demonstrate, and what stays open (Hawkins’ trustworthiness).
counterevidence = ("bread is wired from ToastBread's own bread parameter, but energy "
"is not: no energy source exists anywhere in the model yet, so leaving it "
"unbound is honest, not an omission. duration is declared but unconnected "
"to the balance constraint or to any other computation in this chapter, so "
"it does not yet participate in the flow accounting it claims to name. "
"ApplyHeat is the only function modeled; Douglas's functional architecture "
"names roughly fifteen, so this is a complete accounting for one worked "
"example, not a complete functional decomposition of the toaster. The "
"probe above checks a small model mirroring ApplyHeat's declaration, not "
"nominal or slow themselves, which give ApplyHeat no concrete energy "
"value.")
residual_uncertainties = ("Start, Finish and Cancel are declared as signals (their own "
"doc states this) but are not wired as accepted or produced items of "
"ApplyHeat in this chapter; whether they should be is left open for "
"whichever chapter models the cycle's event handling. efficiency and a "
"characterized conversion belong to a logical component this chapter does "
"not build; this record makes no claim about them.")
print(counterevidence)
print(residual_uncertainties)
bread is wired from ToastBread's own bread parameter, but energy is not: no energy source exists anywhere in the model yet, so leaving it unbound is honest, not an omission. duration is declared but unconnected to the balance constraint or to any other computation in this chapter, so it does not yet participate in the flow accounting it claims to name. ApplyHeat is the only function modeled; Douglas's functional architecture names roughly fifteen, so this is a complete accounting for one worked example, not a complete functional decomposition of the toaster. The probe above checks a small model mirroring ApplyHeat's declaration, not nominal or slow themselves, which give ApplyHeat no concrete energy value.
Start, Finish and Cancel are declared as signals (their own doc states this) but are not wired as accepted or produced items of ApplyHeat in this chapter; whether they should be is left open for whichever chapter models the cycle's event handling. efficiency and a characterized conversion belong to a logical component this chapter does not build; this record makes no claim about them.
With every part named above, the record assembles from them directly.
from toaster.query import get_review_record_refs
inference_record = ReviewRecord(
identifier="AI-C04",
kind="asserted_inference",
claim=claim,
subject_ref=subject_ref,
model_ref=model_ref,
content_hash=hash_content(source),
scope=scope,
criteria=criteria,
premises=premises,
assumption_refs=assumption_refs,
evidence_refs=evidence_refs,
rationale=rationale,
counterevidence=counterevidence,
residual_uncertainties=residual_uncertainties,
disposition="pending",
dependency_freshness="current",
engineering_conclusion="supported",
record_kind="worked_example",
)
errors = validate_record(inference_record, model=model)
save_record(inference_record)
tag = next((t for t in get_review_record_refs(model) if t["identifier"] == inference_record.identifier), None)
print(f"Model tag: {tag}")
print(f"Validation errors: {errors}")
print(f"Record kind: {inference_record.kind}")
conn.close()
Model tag: {'tag': 'ToasterDemo::aiC04Tag', 'identifier': 'AI-C04', 'annotated_element': 'ToasterDemo::ApplyHeat'}
Validation errors: []
Record kind: asserted_inference
The tag printed above is now part of the loaded model, and validate_record confirms the Python record and the model’s own tag agree about what AI-C04 is actually about. The Hawkins §3.1 schema fields named above are what the assembled record satisfies: an empty error list confirms the required fields, including a non-empty premises, are present, not merely printed.
Try the chapter exercise in exercises/ch04/exercise.ipynb: write an asserted_inference record (AI-C04-EX) claiming that your new nested action’s own flows are accounted for and its balance constraint is real and evaluable — honestly scoped the same way AI-C04 is scoped for ApplyHeat, not that brewing as a whole is functionally decomposed — referencing AS-C03-EX in premises.