This notebook states one new SysML construct, deliveredEnergyBoundedBySupply, a real-arithmetic lemma of the same shape as HeatGenerator’s own conservation entailment; after running it you can confirm the construct is really in the loaded model.
Chapter 7 built efficiencyBounded (0 <= efficiency <= 1) and deliveredEnergy (power * duration * efficiency) on HeatGenerator, then checked the relation only at rated’s own efficiency (0.7). This notebook adds a construct with the same shape as what those two together would imply: delivered energy never exceeds supplied energy, for every value of efficiency in its bound. Ch8-02 explains why this is a hand-restated lemma, not a solver-checked reference to efficiencyBounded and deliveredEnergy themselves (DEFERRED.md D-030, D-031). See Ch7-01 delivered energy for efficiencyBounded and deliveredEnergy themselves.
from pathlib import Path
import opensysml
from toaster.report import format_diagnostics
conn = opensysml.connect(version="v0.9.0")
# A fresh, unbound usage of HeatGenerator: no efficiency, no power. Its own two
# features stay free so the lemma below is about every value they could take,
# not one candidate's fixed choice.
HEAT_GEN_CHECK_USAGE = " part heatGenCheck : HeatGenerator;"
print(HEAT_GEN_CHECK_USAGE) part heatGenCheck : HeatGenerator;
heatGenCheck adds nothing to the model but an unbound usage of HeatGenerator. It is not a design candidate the way rated or weak are; it exists only so the lemma below has a subject whose efficiency and power are still free.
heatGenCheck is typed directly by HeatGenerator, the unbound usage the lemma below needs. rated and weak are typed by ResistanceCoil, itself a specialization of HeatGenerator. All three usages are declared at package scope, so none carries an owner edge below. That specialization is drawn as a solid, hollow-triangle edge, distinct from the dashed typing edges.
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)}"
from toaster.render import model_to_dot, render_dot
from IPython.display import SVG
dot = model_to_dot(model, title="Ch8")
out_path = Path("../../figures/ch08-structure.svg")
out_path.parent.mkdir(exist_ok=True)
render_dot(dot, out_path)
SVG(filename=str(out_path))heatGenCheck, rated, and weak carry no owner edge, each declared at package scope. ResistanceCoil’s specialization of HeatGenerator is the solid, hollow-triangle edge between them, unlike the dashed typing edges.
Back to the construction: heatGenCheckDuration is next.
# duration is deliveredEnergy's other free parameter; a fresh unbound attribute
# stands in for it the same way heatGenCheck stands in for efficiency and power.
CHECK_DURATION_ATTR = " attribute heatGenCheckDuration : ISQ::DurationValue;"
print(CHECK_DURATION_ATTR) attribute heatGenCheckDuration : ISQ::DurationValue;
heatGenCheckDuration is not owned by HeatGenerator: deliveredEnergy’s duration is only ever a calc parameter, not a feature of the carrier, so a separate top-level attribute stands in for some duration the same way heatGenCheck stands in for some heat generator.
DELIVERED_ENERGY_BOUND = """\
assert constraint deliveredEnergyBoundedBySupply {
doc /* A real-arithmetic lemma of the same shape as the relation
* efficiencyBounded (0 <= efficiency <= 1) and deliveredEnergy's own
* definition (power * duration * efficiency) together would imply:
* given efficiency in [0,1] and non-negative power and duration,
* power * duration * efficiency never exceeds power * duration.
* Restated by hand on a fresh, unbound usage (heatGenCheck) rather
* than a solver-checked reference to HeatGenerator's own
* efficiencyBounded and deliveredEnergy: this toolchain's Z3 backend
* does not compose two separately declared assert constraints,
* whether sibling or inherited (D-030), and cannot reason through a
* chained calc invocation such as heatGenCheck.deliveredEnergy(...)
* (D-031). Proved by Z3 over the unbound heatGenCheck.efficiency,
* heatGenCheck.power and heatGenCheckDuration features
* (verify --solve): this restated lemma holds for all such values,
* but the proof does not track HeatGenerator's own efficiencyBounded
* or deliveredEnergy if either changes; a content-hash-based record
* against this file does go stale when either changes (any edit to
* the file changes the hash), which is a partial safeguard, not a
* check that the restated copy stays in sync. */
(heatGenCheck.efficiency >= 0.0 and heatGenCheck.efficiency <= 1.0
and heatGenCheck.power >= 0.0 [SI::W] and heatGenCheckDuration >= 0.0 [SI::s])
implies (heatGenCheck.power * heatGenCheckDuration * heatGenCheck.efficiency)
<= heatGenCheck.power * heatGenCheckDuration
}"""
print(DELIVERED_ENERGY_BOUND) assert constraint deliveredEnergyBoundedBySupply {
doc /* A real-arithmetic lemma of the same shape as the relation
* efficiencyBounded (0 <= efficiency <= 1) and deliveredEnergy's own
* definition (power * duration * efficiency) together would imply:
* given efficiency in [0,1] and non-negative power and duration,
* power * duration * efficiency never exceeds power * duration.
* Restated by hand on a fresh, unbound usage (heatGenCheck) rather
* than a solver-checked reference to HeatGenerator's own
* efficiencyBounded and deliveredEnergy: this toolchain's Z3 backend
* does not compose two separately declared assert constraints,
* whether sibling or inherited (D-030), and cannot reason through a
* chained calc invocation such as heatGenCheck.deliveredEnergy(...)
* (D-031). Proved by Z3 over the unbound heatGenCheck.efficiency,
* heatGenCheck.power and heatGenCheckDuration features
* (verify --solve): this restated lemma holds for all such values,
* but the proof does not track HeatGenerator's own efficiencyBounded
* or deliveredEnergy if either changes; a content-hash-based record
* against this file does go stale when either changes (any edit to
* the file changes the hash), which is a partial safeguard, not a
* check that the restated copy stays in sync. */
(heatGenCheck.efficiency >= 0.0 and heatGenCheck.efficiency <= 1.0
and heatGenCheck.power >= 0.0 [SI::W] and heatGenCheckDuration >= 0.0 [SI::s])
implies (heatGenCheck.power * heatGenCheckDuration * heatGenCheck.efficiency)
<= heatGenCheck.power * heatGenCheckDuration
}
The lemma’s antecedent restates what efficiencyBounded already guarantees, plus non-negative power and duration; its consequent restates the same arithmetic deliveredEnergy’s own definition computes. Both are copied by hand, not referenced: Ch8-02 shows directly that neither the model’s own bound nor its own calc definition can actually move this lemma’s verdict, because sysml-toolkit’s solver never reaches through to either one.
TOASTER_INCREMENT = f"{HEAT_GEN_CHECK_USAGE}\n{CHECK_DURATION_ATTR}\n\n{DELIVERED_ENERGY_BOUND}\n"
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)}"ch08-cumulative.sysml already carries this construct forward: it is not assembled from the fragments above at runtime, it is the chapter’s own committed fixture. model.find() and model.query() below confirm deliveredEnergyBoundedBySupply is really part of the loaded model, not only in the strings printed above.
sym = model.find("ToasterDemo::deliveredEnergyBoundedBySupply")
assert sym is not None, "deliveredEnergyBoundedBySupply not found in the loaded model"
print(f"model.find(): {sym}")
constraint_names = []
for e in model.query():
d = e.as_dict()
if d.get("@type") == "ConstraintUsage":
constraint_names.append(d["qualifiedName"])
assert "ToasterDemo::deliveredEnergyBoundedBySupply" in constraint_names
print(f"model.query() sees it too, among {len(constraint_names)} named ConstraintUsage elements.")model.find(): deliveredEnergyBoundedBySupply (constraintUsage)
model.query() sees it too, among 3 named ConstraintUsage elements.
A require constraint referencing an undefined attribute still fails to load, exactly as it always has: this checks the language tier before the chapter’s own genuinely new negative controls appear in Ch8-02, which shows the model-checking loop itself catching both a fully broken entailment and a merely weakened one.
# A require constraint referencing an undefined attribute fails.
bad_source = """
package P {
private import ScalarValues::*;
part def Thing { attribute x : Real default = 5.0; }
requirement def Check {
subject t : Thing;
require constraint { t.undeclared <= 10.0 }
}
}
"""
bad = conn.load_from_content(bad_source, strict=False)
assert not bad.ok, "Expected failure for undeclared attribute in constraint"
print(f"Negative control ok: bad.ok={bad.ok}")
conn.close()Negative control ok: bad.ok=False
The definitions printed above loaded without error, and both model.find() and model.query() confirmed deliveredEnergyBoundedBySupply is now part of the model, shown by the symbol and the qualified name printed earlier in this notebook.
Try the chapter exercise in exercises/ch08/exercise.ipynb: it works through the same verify_satisfaction() and stale-detection pattern on its own, separate coffee-maker exercise model.