This notebook introduces the asserted_solution judgment record; after running it you can record which satisfaction claims the model’s evaluated values support, and which remain open.
The previous notebook evaluated assert not satisfy timely by slow and confirmed it holds. Before treating that evaluation as settled, we record the judgment as a Hawkins-style asserted_solution: what the evaluation supports, and what it does not yet decide about nominal.
from pathlib import Path
import opensysml
from toaster.report import format_diagnostics
conn = opensysml.connect(version="v0.9.0")
source = Path("../../models/ch03-cumulative.sysml").read_text()
lines = source.splitlines()
excerpt = "\n".join(lines[35:47] + [" ..."] + lines[61:65] + [" ..."] + lines[66:80])
print(excerpt)
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}" requirement def TimelyToast {
doc /*
* The toaster shall complete a toasting cycle in at most 180 seconds.
* Rationale: kitchen workflows typically span 5-15 minutes; a cycle
* exceeding 3 minutes delays meal preparation and falls outside where
* and how a user prepares a meal.
*/
subject toaster : Toaster;
require constraint { toaster.cycleTime <= 180.0 [SI::s] }
}
requirement timely : TimelyToast;
...
part slow : Toaster {
attribute :>> cycleTime = 200.0 [SI::s];
assert not satisfy timely by slow;
}
...
verification def TimelyToastTest {
doc /*
* Verification method: timed test of three consecutive toasting cycles at
* nominal input power; all must complete within 180 seconds.
* Method type: test (VerificationMethodKind::test, SysML v2 §7.24 Table 22).
* Note: formal #verificationMethod metadata not yet supported in OpenSysML v0.9.0;
* tracked at toaster#19 / OpenSysML#608.
* spec: SysML v2 formal/2026-03-02 §7.24.2 (VerificationCaseDefinition).
*/
subject toaster : Toaster;
objective {
verify timely;
}
}
The part skeleton underneath the requirement and judgment content below -- unchanged since Chapter 2, drawn here to orient before reading the satisfy claim in detail.
from toaster.render import model_to_dot, render_dot
from IPython.display import SVG
dot = model_to_dot(model, title="Ch3")
out_path = Path("../../figures/ch03-structure.svg")
out_path.parent.mkdir(exist_ok=True)
render_dot(dot, out_path)
SVG(filename=str(out_path))The ch03-cumulative.sysml file applies TimelyToast to the model as timely : TimelyToast, folds assert not satisfy timely by slow into slow’s own body, and adds TimelyToastTest, a verification case that declares how timely will be checked (notebook 04). Its doc comment’s note not yet supported in OpenSysML v0.9.0 predates this tutorial’s component naming and refers to the OpenSysML runtime v0.9.0, which does not accept the formal #verificationMethod metadata; notebook 04 explains (toaster#19).
# Negative control: a require constraint referencing an attribute the
# subject's type does not declare raises "unresolved member" at the point
# of use.
bad_source = """
package Bad {
private import ScalarValues::*;
part def Toaster { attribute cycleTime : Real default = 120.0; }
requirement def BadReq {
subject t : Toaster;
require constraint { t.notAnAttribute <= 180.0 }
}
}
"""
bad = conn.load_from_content(bad_source, strict=False)
assert not bad.ok
print("Expected error:", bad.diagnostics[0].message)Expected error: unresolved member: notAnAttribute
With the negative control confirmed, the next cell rebuilds the threshold judgment: what the evaluated claim on slow supports, and what remains unclaimed about nominal.
The evaluation itself comes first: model.eval checks the negated claim on slow against the model’s own values. claim states what that evaluation is being read as supporting, and model_ref names the requirement it concerns.
from toaster.evidence import ReviewRecord, validate_record, hash_content
slow_holds = model.eval("ToasterDemo::timely(ToasterDemo::slow)")
print(f"ToasterDemo::timely(ToasterDemo::slow) = {slow_holds}")
claim = ("The negated claim on slow (assert not satisfy timely by slow) "
"evaluates True: slow's cycleTime (200 s) fails timely's 180 s "
"bound, as intended for the injected fault. No corresponding claim is made for nominal.")
model_ref = ("ToasterDemo::timely")
print(claim)ToasterDemo::timely(ToasterDemo::slow) = False
The negated claim on slow (assert not satisfy timely by slow) evaluates True: slow's cycleTime (200 s) fails timely's 180 s bound, as intended for the injected fault. No corresponding claim is made for nominal.
Before moving to scope and criteria, the next cells give this claim a real anchor in the model: a ReviewRecordRef tag naming timely as what AS-C03 is about.
# what is being claimed, and what, specifically, it is about
subject_ref = "ToasterDemo::timely"
AS_C03_TAG = """\
metadata asC03Tag : ReviewRecordRef about timely {
identifier = "AS-C03";
}
"""
print(AS_C03_TAG)metadata asC03Tag : ReviewRecordRef about timely {
identifier = "AS-C03";
}
This fragment is the same text now committed in models/ch03-cumulative.sysml onward, alongside the ReviewRecordRef definition (carried forward from Chapter 2) and acC03Tag (notebook 01); 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 = AS_C03_TAGscope and criteria state the standard the claim is judged against: exactly which evaluation, on which usage, counts as this claim holding.
scope = ("ToasterDemo")
criteria = ("assert not satisfy timely by slow holds when "
"ToasterDemo::timely(ToasterDemo::slow) evaluates False.")
print(criteria)assert not satisfy timely by slow holds when ToasterDemo::timely(ToasterDemo::slow) evaluates False.
premises names what makes slow a legitimate fixture for this claim in the first place: a deliberately injected value, not a derived one.
premises = ([
"slow.cycleTime is fixed at 200.0 [SI::s], a deliberately injected "
"fault value (Chapter 2), not a value derived from any mechanism.",
])
print(premises)['slow.cycleTime is fixed at 200.0 [SI::s], a deliberately injected fault value (Chapter 2), not a value derived from any mechanism.']
AC-C03’s framing judgment is the assumption this record rests on; evidence_refs points at the evaluation above, and rationale connects that evidence to the claim.
assumption_refs = ([
"AC-C03: timely is framed as a measure of effectiveness "
"(notebook 01).",
])
evidence_refs = ([
"assert not satisfy timely by slow (ToasterDemo::slow::@1), "
"evaluated by model.eval('ToasterDemo::timely(ToasterDemo::slow)') "
"= False, above.",
])
rationale = ("slow's fixed cycleTime exceeds the bound, and the model's own "
"evaluation confirms the negated claim holds. This demonstrates "
"the deliberately negated satisfaction claim applied to an "
"injected fault value: a real, evaluable claim about a fixture "
"built to fail, not a check that traces a failure back to a "
"design choice, since deriving a cycle time from an actual "
"mechanism is not yet possible. Toaster::cycleTime carries no "
"default value, so nominal.cycleTime has no value and "
"ToasterDemo::timely(ToasterDemo::nominal) cannot be evaluated "
"at all; claiming nominal satisfies timely would assert a "
"result that was never computed.")
print(rationale)slow's fixed cycleTime exceeds the bound, and the model's own evaluation confirms the negated claim holds. This demonstrates the deliberately negated satisfaction claim applied to an injected fault value: a real, evaluable claim about a fixture built to fail, not a check that traces a failure back to a design choice, since deriving a cycle time from an actual mechanism is not yet possible. Toaster::cycleTime carries no default value, so nominal.cycleTime has no value and ToasterDemo::timely(ToasterDemo::nominal) cannot be evaluated at all; claiming nominal satisfies timely would assert a result that was never computed.
The challenge: counterevidence states plainly what this result does not demonstrate, and residual_uncertainties says what stays genuinely open about nominal (Hawkins’ trustworthiness again: an evaluated True is not the same as a settled question).
counterevidence = ("This only demonstrates that a chosen fault value fails. It does "
"not demonstrate that a derived cycle time can pass; that "
"demonstration needs a chapter that derives cycle time from the "
"mechanism and the energy balance.")
residual_uncertainties = ("Whether timely is best framed as a measure of effectiveness or a "
"measure of performance stays a contestable judgment (AC-C03, "
"notebook 01), independent of this result. nominal's status under "
"timely is genuinely open, not merely deferred.")
print(counterevidence)
print(residual_uncertainties)This only demonstrates that a chosen fault value fails. It does not demonstrate that a derived cycle time can pass; that demonstration needs a chapter that derives cycle time from the mechanism and the energy balance.
Whether timely is best framed as a measure of effectiveness or a measure of performance stays a contestable judgment (AC-C03, notebook 01), independent of this result. nominal's status under timely is genuinely open, not merely deferred.
With every part named above, the solution record assembles from them directly.
from toaster.query import get_review_record_refs
from toaster.judgment_store import save_record
solution_record = ReviewRecord(
identifier="AS-C03",
kind="asserted_solution",
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(solution_record, model=model)
save_record(solution_record)
tag = next((t for t in get_review_record_refs(model) if t["identifier"] == solution_record.identifier), None)
print(f"Model tag: {tag}")
print(f"Validation errors: {errors}")
print(f"Record kind: {solution_record.kind}")
conn.close()Model tag: {'tag': 'ToasterDemo::asC03Tag', 'identifier': 'AS-C03', 'annotated_element': 'ToasterDemo::timely'}
Validation errors: []
Record kind: asserted_solution
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 AS-C03 is actually about.
Try the chapter exercise in exercises/ch03/exercise.ipynb: write an asserted_solution record for your satisfaction claim.