satisfaction claims

This notebook introduces the assert satisfy / assert not satisfy idiom; after running it you can record, inside a usage’s own context, whether it meets a requirement, and evaluate that claim against the model.

The previous notebook applied TimelyToast to the model as timely : TimelyToast. slow, from Chapter 2, is a deliberately injected fault: cycleTime fixed at 200 seconds, built to fail timely’s 180-second bound. This notebook folds a negated satisfaction claim into slow’s own body and evaluates it against the model’s own values.

from pathlib import Path
import opensysml
from toaster.report import format_diagnostics

conn = opensysml.connect(version="v0.9.0")

# editor.add_assert_satisfy(owner='ToasterDemo::slow', req='timely', by='slow', negated=True) when API ships
# assert satisfy not yet supported by the Editor API - https://github.com/Open-MBEE/toaster/issues/12 / https://github.com/Open-MBEE/OpenSysML/issues/598
# spec: SysML v2 formal/2026-03-02 section 7.19 (SatisfyRequirementUsage)
SLOW_NOT_SATISFY = "    assert not satisfy timely by slow;"
print(SLOW_NOT_SATISFY)

    assert not satisfy timely by slow;

The claim is folded into slow’s own body: slow names itself as the usage the claim is about, so no separate container is needed. slow’s full usage, restated with this new line, is what the cumulative model now carries.

SLOW_WITH_CLAIM = (
    "part slow : Toaster {\n"
    "    attribute :>> cycleTime = 200.0 [SI::s];\n"
    f"{SLOW_NOT_SATISFY}\n"
    "}"
)
TOASTER_INCREMENT = SLOW_WITH_CLAIM

source = Path("../../models/ch03-cumulative.sysml").read_text()
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}"

The reopened slow usage loads without diagnostics, restating its Chapter 2 override with the injected-fault claim added. The next cell checks what happens when an assert satisfy names a usage that does not resolve.

# Negative control: assert satisfy naming an undeclared usage raises
# "unresolved reference" at the assert-satisfy site.
bad_source = """
package Bad {
    private import ScalarValues::*;
    private import SI::*;
    private import ISQ::*;
    part def Toaster { attribute cycleTime : ISQ::DurationValue; }
    requirement def TimelyToast {
        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 undefinedUsage;
    }
}
"""
bad = conn.load_from_content(bad_source, strict=False)
assert not bad.ok
print("Expected error:", bad.diagnostics[0].message)

Expected error: unresolved reference: undefinedUsage

With the negative control confirmed, the next cell evaluates the claim slow now carries against the model’s own values.

from toaster.query import satisfy_relationships

# TimelyToastTest's verify timely; also exports as a SatisfyRequirementUsage,
# with no subject: it names no usage and is not itself a claim about one.
claims = [c for c in satisfy_relationships(model) if c["subject"]]
assert len(claims) == 1
claim = claims[0]
print(f"satisfy claim: {claim}")

expression = f"{claim['requirement']}({claim['subject']})"
holds = model.eval(expression)
print(f"{expression} = {holds}")
conn.close()

satisfy claim: {'id': 'ToasterDemo::slow::@1', 'requirement': 'ToasterDemo::timely', 'subject': 'ToasterDemo::slow', 'is_negated': True}
ToasterDemo::timely(ToasterDemo::slow) = False

timely(slow) evaluates to False: slow’s 200-second cycleTime does not meet the 180-second bound. The model’s claim is assert not satisfy, so this result confirms the claim rather than contradicting it. This demonstrates the deliberately negated claim applied to an injected fault value: a real, evaluable claim about a fixture built to fail. It does not yet demonstrate a check catching a failure that traces back to a design choice, since deriving a cycle time from an actual mechanism is not yet possible; slow’s fixed value is the measured quantity itself, typed in directly, not a result computed from anything.

assert not satisfy timely by slow;, printed above, loaded without error; model.eval() confirms the negated claim holds against slow’s own values, shown by the False result above.

Try the chapter exercise in exercises/ch03/exercise.ipynb: fold a negated satisfaction claim into your hot usage of BrewUnit, following the pattern above; do not assert anything about nominal, whose brewTemp is unbound.