This notebook introduces a real requirement-coverage report, built by joining every named RequirementUsage against every SatisfyRequirementUsage the model actually carries; after running it you can see which requirements have a real claim of satisfaction against them, which candidates were checked and with what polarity, and which have none at all.
Chapters 3 through 8 declared satisfy claims one at a time, each notebook adding or checking a single candidate against a single requirement. This chapter asks a different question across the whole model at once: for every requirement usage the model declares, has anyone actually claimed a candidate satisfies it, and of which polarity? This notebook adds no new model element: models/ch08-cumulative.sysml, the real, current cumulative model Chapter 8 committed, already has everything this query needs, so this chapter queries it directly rather than growing a models/ch09-cumulative.sysml file that would carry nothing new (a design choice recorded in this chapter’s own Overview).
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)}"
The model loads cleanly. Before querying it, the same language-tier control every chapter carries: a satisfy naming a requirement that was never declared still fails to load, which matters directly for a chapter about what has and has not been claimed -- a broken reference can never silently count as a claim.
# A satisfy claim naming a requirement that doesn't exist fails to load; it can
# never silently show up as a "claim" this chapter's coverage query would count.
bad_source = """
package Bad {
private import ScalarValues::*;
part def Widget { attribute x : Real default = 1.0; }
part w : Widget;
assert satisfy missingReq by w;
}
"""
bad = conn.load_from_content(bad_source, strict=False)
assert not bad.ok, "Expected failure for an undeclared requirement"
print(f"Negative control ok: bad.ok={bad.ok}")
Negative control ok: bad.ok=False
With the model loaded, the coverage report starts from the same two surfaces every chapter’s own satisfy claim already used: every named RequirementUsage from model.query(), and every SatisfyRequirementUsage, named or not, from get_satisfy_relationships() (D-001: model.query() returns none of these directly). Each raw satisfy element carries subsets (the requirement it claims against), subject (the candidate, when there is one), isNegated (a positive or a negative claim) and sysx:declaredKeyword ("verify" for a verification-case objective).
from toaster.query import find_requirements, get_satisfy_relationships, ApiIndex
idx = ApiIndex(model)
requirements = sorted(r.id for r in find_requirements(model))
raw_satisfies = get_satisfy_relationships(model)
claims = []
for s in raw_satisfies:
claims.append({
"id": s.get("qualifiedName"),
"requirement": idx.qn(s["subsets"]) if "subsets" in s else None,
"subject": idx.qn(s["subject"]) if "subject" in s else None,
"is_verify": s.get("sysx:declaredKeyword") == "verify",
"is_negated": bool(s.get("isNegated", False)),
})
print(f"requirements: {requirements}")
for c in claims:
print(c)
requirements: ['ToasterDemo::heatGenerationReq', 'ToasterDemo::timely']
{'id': 'ToasterDemo::slow::@1', 'requirement': 'ToasterDemo::timely', 'subject': 'ToasterDemo::slow', 'is_verify': False, 'is_negated': True}
{'id': 'ToasterDemo::TimelyToastTest::@2::@0', 'requirement': 'ToasterDemo::timely', 'subject': None, 'is_verify': True, 'is_negated': False}
{'id': 'ToasterDemo::rated::@1', 'requirement': 'ToasterDemo::heatGenerationReq', 'subject': 'ToasterDemo::rated', 'is_verify': False, 'is_negated': False}
{'id': 'ToasterDemo::weak::@1', 'requirement': 'ToasterDemo::heatGenerationReq', 'subject': 'ToasterDemo::weak', 'is_verify': False, 'is_negated': True}
Four SatisfyRequirementUsage relationships in total, over two requirements -- but not four claims in the sense this report cares about. Three are real claims about a specific candidate, positive or negative: slow fails timely, rated satisfies heatGenerationReq, weak fails it. The fourth, TimelyToastTest’s own verify timely; objective, is a verification-case objective, not a claim about any subject: TimelyToastTest (the verification case) does declare its own subject toaster : Toaster, but that is a type-level placeholder, not a binding to a specific candidate like nominal, and the objective relationship itself, the one this query actually sees, carries no subject at all in the exported model. Joining the three real claims by requirement, split by polarity, is the actual coverage report; the fourth is reported separately, since it names a requirement without claiming anything about a subject.
from collections import defaultdict
coverage = {r: {"positive": [], "negative": [], "verify_objectives": []} for r in requirements}
dropped = []
for c in claims:
if c["requirement"] not in coverage:
dropped.append(c)
continue
if c["is_verify"]:
coverage[c["requirement"]]["verify_objectives"].append(c["id"])
elif c["is_negated"]:
coverage[c["requirement"]]["negative"].append(c["subject"])
else:
coverage[c["requirement"]]["positive"].append(c["subject"])
print(f"claims dropped (requirement not in the named list above): {len(dropped)}")
assert dropped == [], f"Unexpected dropped claims: {dropped}"
for r in requirements:
cov = coverage[r]
positive, negative, verify_objectives = cov["positive"], cov["negative"], cov["verify_objectives"]
covered = bool(positive)
print(f"{r}:")
print(f" positive satisfy claims: {positive}")
print(f" negative satisfy claims: {negative}")
print(f" verify objectives (no subject): {verify_objectives}")
print(f" covered (has >=1 positive claim): {covered}")
assert coverage["ToasterDemo::heatGenerationReq"]["positive"] == ["ToasterDemo::rated"]
assert coverage["ToasterDemo::heatGenerationReq"]["negative"] == ["ToasterDemo::weak"]
assert coverage["ToasterDemo::timely"]["positive"] == []
claims dropped (requirement not in the named list above): 0
ToasterDemo::heatGenerationReq:
positive satisfy claims: ['ToasterDemo::rated']
negative satisfy claims: ['ToasterDemo::weak']
verify objectives (no subject): []
covered (has >=1 positive claim): True
ToasterDemo::timely:
positive satisfy claims: []
negative satisfy claims: ['ToasterDemo::slow']
verify objectives (no subject): ['ToasterDemo::TimelyToastTest::@2::@0']
covered (has >=1 positive claim): False
heatGenerationReq is covered on both sides: rated was checked and found to satisfy it, weak was checked and found not to. timely has never had a positive satisfy claim at all. The only claim against it is negative (slow does not satisfy it), and the only other reference is TimelyToastTest’s own objective, which claims nothing about a subject. This is a real, present gap in the tutorial’s own accumulated model, not a scratch example built to fail on purpose: nominal, the usage meant to represent the toaster actually meeting its timing requirement, has no assert satisfy timely by nominal anywhere in models/ch08-cumulative.sysml. This does not mean nominal fails timely: Toaster::cycleTime is still a settable attribute, not derived from anything (unchanged since Chapter 2), so no one has ever actually checked whether nominal satisfies timely in the first place. The gap this query finds is an absence of a claim, not evidence of a failed one.
Is this join trustworthy, or could a differently-written join reach a different answer? src/toaster/query.py already ships a requirement_coverage() helper for exactly this kind of question, so the natural check is not to invent a second mechanism but to see whether it agrees. First, though, a genuine wrong way to join the same data, one this repository’s own helper actually had until this chapter’s own work found and fixed it: a join that counts ANY claim, positive or negative, as coverage.
# A polarity-blind join: exactly the mistake of counting a FAILING claim as coverage.
naive_covered = defaultdict(list)
for c in claims:
if c["requirement"] and c["subject"]:
naive_covered[c["requirement"]].append(c["subject"])
print("A polarity-blind join would report:")
for r in requirements:
claimants = naive_covered.get(r, [])
print(f" {r}: covered={bool(claimants)} claimed by={claimants}")
assert naive_covered["ToasterDemo::timely"] == ["ToasterDemo::slow"]
A polarity-blind join would report:
ToasterDemo::heatGenerationReq: covered=True claimed by=['ToasterDemo::rated', 'ToasterDemo::weak']
ToasterDemo::timely: covered=True claimed by=['ToasterDemo::slow']
A polarity-blind join reports timely as covered, using slow’s own FAILING claim as the evidence -- exactly backwards. This was not a hypothetical risk: src/toaster/query.py’s requirement_coverage() carried this exact bug until this chapter found and fixed it, ignoring isNegated entirely and reporting weak’s failing claim against heatGenerationReq as coverage too. The fixed version now splits by polarity the same way this notebook’s own join always has, and also excludes TimelyToastTest’s own auto-generated, unnamed requirement usage (the objective’s own bookkeeping wrapper, not a design requirement) from the requirement list it reports on.
from toaster.query import requirement_coverage
repo_coverage = {c["requirement"]: c for c in requirement_coverage(model)}
for r in requirements:
print(repo_coverage[r])
assert repo_coverage["ToasterDemo::timely"]["covered"] is False
assert repo_coverage["ToasterDemo::timely"]["satisfied_by"] == []
assert repo_coverage["ToasterDemo::timely"]["failed_by"] == ["ToasterDemo::slow"]
assert repo_coverage["ToasterDemo::heatGenerationReq"]["covered"] is True
assert repo_coverage["ToasterDemo::heatGenerationReq"]["satisfied_by"] == ["ToasterDemo::rated"]
assert repo_coverage["ToasterDemo::heatGenerationReq"]["failed_by"] == ["ToasterDemo::weak"]
conn.close()
{'requirement': 'ToasterDemo::heatGenerationReq', 'satisfied_by': ['ToasterDemo::rated'], 'failed_by': ['ToasterDemo::weak'], 'covered': True}
{'requirement': 'ToasterDemo::timely', 'satisfied_by': [], 'failed_by': ['ToasterDemo::slow'], 'covered': False}
Two independently-written joins over the same raw data, one built cell by cell in this notebook and one already living in the repository’s own query module, now agree exactly: timely is not covered, heatGenerationReq is. They agree only because both actually track polarity; a join that does not, as shown above, reaches the opposite, wrong answer for timely. That is what “coverage” has to mean for this check to be worth anything at all: a positive claim someone actually made, not merely a claim of any kind.
One honest caveat about what covered=False means, since this tutorial keeps building on this same model after this chapter: Chapter 10 later adds a third named requirement, energyConservationReq, tied to Chapter 8’s own Z3-proved conservation lemma (deliveredEnergyBoundedBySupply) by subsetting from within the requirement’s own body, not by any instance-level assert satisfy (see that chapter’s own AC-C10 judgment record for the full account). requirement_coverage() -- this same helper, confirmed against the same two independently-written joins above -- reports covered=False for it too, with satisfied_by=[], exactly as empty as timely’s own. But the two Falses mean structurally different things: timely’s is a real, present gap, because nominal has never been positively checked against it at all, and could be; energyConservationReq’s is False by design, because this helper only counts a positive assert satisfy declaration, and that construct was deliberately not used for it (a direct test in Chapter 10 shows it would not do real evaluative work here). A reader who reaches Chapter 10 should not read energyConservationReq’s own covered=False as a second, undiscovered version of this chapter’s timely finding.
The requirement usages and satisfy relationships declared in models/ch08-cumulative.sysml, queried above through two differently-written joins, produced the same coverage gap both times, and a third, deliberately wrong join showed exactly what goes missing when polarity is dropped -- confirming the finding is a property of the model itself, not an artifact of how it was asked.
Try the chapter exercise in exercises/ch09/exercise.ipynb: it asks you to produce a coverage report over your own coffee-maker model, using the query-and-join pattern this notebook builds.