Skip to article frontmatterSkip to article content
Site not loading correctly?

This may be due to an incorrect BASE_URL configuration. See the MyST Documentation for reference.

Checked: What the record proves

Authors
Affiliations
Dynamical Systems Group
Humane Intelligence

This page runs the checks that the Checked block of the guarantees chapter claims. The executor ogc/executor.py walks the process as the model graph states it and emits a record; the checks run over that record, over the parameter variants and over each mutation of the first run, and the two tables the chapter shows are produced here by the same code. A reader need not take the chapter’s word for it. Every line of output below is produced by the code above it, the gate re-executes this notebook and fails if the committed outputs differ, and each claim is an assert that stops the notebook when it does not hold. The asserts are those of tests/test_executor.py.

import sys; sys.path[:0] = ["notebooks", "."]  # the shared module lives beside this notebook
import checked

sys.path.insert(0, str(checked.ROOT))
from ogc import executor

model = checked.model_graph()                       # model/og-caie.model.ttl
shapes = checked.load("shapes/epo.shapes.ttl")      # all of S0 to S9
epo = checked.load("vocabulary/epo.ttl")
demo = executor.demonstrate(model, shapes, epo)     # the run, the variants and the mutations, each with its checks


def show(name, c):
    cov = c["coverage"]
    print(f"{name}: conforms={c['conforms']} fired={c['fired']} missing={c['missing']} "
          f"coverage={cov['coverage']} (pass {cov['passRate']} / fail {cov['failRate']} / cantTell {cov['cantTellRate']}) traceback={c['traceback']}")

1The first run conforms, is complete and traces

One requirement, three criteria, a plan that exercises two of them with the third’s deviation recorded, one session that applies every probe once. The record must conform to every shape S0 to S9 with none firing, lack no item kind the process produces, have a coverage of two thirds whose pass, fail and cannot-tell rates sum to one, and return one traceback row per determination an attestation aggregates: three, since the operator’s determination is paired with the domain expert’s (sheet 10-15).

run = demo["run"]
show("run", run)
assert run["conforms"] and not run["fired"] and not run["missing"]
assert abs(run["coverage"]["coverage"] - 2 / 3) < 1e-4
assert abs(run["coverage"]["passRate"] + run["coverage"]["failRate"] + run["coverage"]["cantTellRate"] - 1) < 1e-6
assert run["traceback"] == 3
checked.passed("the first run conforms, is complete, has coverage two thirds and three traceback rows")
run: conforms=True fired=[] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
ok: the first run conforms, is complete, has coverage two thirds and three traceback rows

2The variants

The parameters change and the checks run again: planning all three criteria brings coverage to one and four traceback rows; two sessions over two requirements of two criteria, all planned, bring twelve rows; five criteria judged with the five combinations of outcome, sufficiency and appropriateness the shapes allow (sheet 10-12) conform, with the inapplicable one uncovered.

v = demo["variants"]
for name, c in v.items():
    show(name, c)
assert v["planned 3 of 3"]["conforms"] and abs(v["planned 3 of 3"]["coverage"]["coverage"] - 1) < 1e-6
assert v["planned 3 of 3"]["traceback"] == 4
big = v["two sessions, two requirements"]
assert big["conforms"] and not big["missing"] and abs(big["coverage"]["coverage"] - 1) < 1e-6 and big["traceback"] == 12
five = v["the five judgments"]
assert five["conforms"] and not five["missing"] and abs(five["coverage"]["coverage"] - 0.8) < 1e-6
checked.passed("planned 3 of 3 has coverage one and four rows; two sessions, two requirements has coverage one and twelve rows; the five judgments conform")
planned 2 of 3: conforms=True fired=[] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
planned 3 of 3: conforms=True fired=[] missing=[] coverage=1.0 (pass 0.3333 / fail 0.6667 / cantTell 0.0) traceback=4
two sessions, two requirements: conforms=True fired=[] missing=[] coverage=1.0 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=12
the five judgments: conforms=True fired=[] missing=[] coverage=0.8 (pass 0.25 / fail 0.25 / cantTell 0.5) traceback=7
ok: planned 3 of 3 has coverage one and four rows; two sessions, two requirements has coverage one and twelve rows; the five judgments conform

3Every mutation is caught by a named check

Each mutation breaks one thing in the first run. EXPECTED is the table tests/test_executor.py pins: which shapes fire, which item kinds go missing, and where the traceback empties. A mutation is caught when the record does not conform, or lacks an item kind, or returns no traceback row. The assert says that every mutation matches its expected row and that every one is caught.

EXPECTED = {
    "skip-assessment": {"fired": ["S2-RequirementSet"], "missing": ["AppropriatenessAssessment"]},
    "skip-approval": {"fired": [], "missing": ["PlanApproval"]},
    "skip-access": {"fired": ["S2-RequirementSet"], "missing": ["TestItemAccess"], "traceback": 0},
    "unwire-evidence": {"fired": ["S5-Evidence", "S6-Attestation"], "traceback": 0},
    "executive-attests": {"fired": ["S6-Attestation"]},
    "attest-without-determination": {"fired": ["S6-Attestation", "S8-Recommendation"], "traceback": 0},
    "requirements-before-agreement": {"fired": ["S0-Layers", "S0-Parties"]},
    "engagement-mismatch": {"fired": ["S0-Population"]},
    "skip-report-approval": {"fired": ["S8-Delivery", "S8-Recommendation", "S9-Acceptance"], "missing": ["ReportApproval"]},
    "pad-pass-rate": {"fired": ["S7-Report"]},
    "one-person-team": {"fired": ["S0-Roles"]},
    "cherry-pick": {"fired": ["S6-Attestation"], "traceback": 2},
}
assert set(demo["mutations"]) == set(EXPECTED)
for name, exp in EXPECTED.items():
    got = demo["mutations"][name]
    show(name, got)
    for k, v in exp.items():
        assert got[k] == v, (name, k, got[k], v)
    assert (not got["conforms"]) or got["missing"] or got["traceback"] == 0, f"{name} was not caught"
checked.passed("all twelve mutations match the expected rows and each is caught by a named check")
skip-assessment: conforms=False fired=['S2-RequirementSet'] missing=['AppropriatenessAssessment'] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
skip-approval: conforms=True fired=[] missing=['PlanApproval'] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
skip-access: conforms=False fired=['S2-RequirementSet'] missing=['TestItemAccess'] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=0
unwire-evidence: conforms=False fired=['S5-Evidence', 'S6-Attestation'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=0
executive-attests: conforms=False fired=['S6-Attestation'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
attest-without-determination: conforms=False fired=['S6-Attestation', 'S8-Recommendation'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=0
requirements-before-agreement: conforms=False fired=['S0-Layers', 'S0-Parties'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
engagement-mismatch: conforms=False fired=['S0-Population'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
skip-report-approval: conforms=False fired=['S8-Delivery', 'S8-Recommendation', 'S9-Acceptance'] missing=['ReportApproval'] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
pad-pass-rate: conforms=False fired=['S7-Report'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
one-person-team: conforms=False fired=['S0-Roles'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
cherry-pick: conforms=False fired=['S6-Attestation'] missing=[] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=2
ok: all twelve mutations match the expected rows and each is caught by a named check

4The one the shapes accept

The chapter states one finding rather than hiding it: skipping the plan approval leaves a record the shapes accept, because no shape yet requires that item to exist (concern C-43, open); completeness against the model catches it. Skipping the access grant was the second such finding until the envelope was bound to the test item an access grant names (sheet 10-17): now S2-RequirementSet fires, and completeness and the empty traceback catch it too. The asserts say exactly that.

approval, access = demo["mutations"]["skip-approval"], demo["mutations"]["skip-access"]
show("skip-approval", approval)
show("skip-access", access)
assert approval["conforms"] and approval["missing"] == ["PlanApproval"]
checked.passed("skip-approval conforms to the shapes and is caught by completeness (PlanApproval missing)")
assert not access["conforms"] and access["fired"] == ["S2-RequirementSet"] and access["missing"] == ["TestItemAccess"] and access["traceback"] == 0
checked.passed("skip-access is refused by S2-RequirementSet, by completeness (TestItemAccess missing) and by the empty traceback")
skip-approval: conforms=True fired=[] missing=['PlanApproval'] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=3
skip-access: conforms=False fired=['S2-RequirementSet'] missing=['TestItemAccess'] coverage=0.6667 (pass 0.5 / fail 0.5 / cantTell 0.0) traceback=0
ok: skip-approval conforms to the shapes and is caught by completeness (PlanApproval missing)
ok: skip-access is refused by S2-RequirementSet, by completeness (TestItemAccess missing) and by the empty traceback

5The two tables the chapter shows

The walkthrough of the chapter includes generated/executor.md. That fragment is rendered by scripts/render.py’s render_executor, which calls the same demonstrate. It is rendered again here, shown, and compared with the committed fragment byte for byte.

from IPython.display import Markdown, display

sys.path.insert(0, str(checked.ROOT / "scripts"))
from render import render_executor

rendered = render_executor()
print(rendered)
committed = (checked.ROOT / "generated" / "executor.md").read_text()
assert rendered == committed
checked.passed("generated/executor.md, the tables the chapter shows, equals what render_executor produces now")
**The executed runs.**

| Run | Shapes S0 to S9 | Item kinds missing | Coverage (pass / fail / cannot tell) | Traceback rows |
|---|---|---|---|---|
| planned 2 of 3 | conforms | none | 0.6667 (0.50 / 0.50 / 0.00) | 3 |
| planned 3 of 3 | conforms | none | 1.0000 (0.33 / 0.67 / 0.00) | 4 |
| two sessions, two requirements | conforms | none | 1.0000 (0.50 / 0.50 / 0.00) | 12 |
| the five judgments | conforms | none | 0.8000 (0.25 / 0.25 / 0.50) | 7 |

**The mutations of the first run.**

| Mutation | Shapes S0 to S9 | Item kinds missing | Coverage (pass / fail / cannot tell) | Traceback rows | Caught by |
|---|---|---|---|---|---|
| skip-assessment: skip the appropriateness assessment (a step's output missing) | fails S2-RequirementSet | AppropriatenessAssessment | 0.6667 (0.50 / 0.50 / 0.00) | 3 | shapes S2-RequirementSet; completeness (AppropriatenessAssessment missing) |
| skip-approval: skip the plan approval | conforms | PlanApproval | 0.6667 (0.50 / 0.50 / 0.00) | 3 | completeness (PlanApproval missing) |
| skip-access: skip the access grant (a contracting step missing) | fails S2-RequirementSet | TestItemAccess | 0.6667 (0.50 / 0.50 / 0.00) | 0 | shapes S2-RequirementSet; completeness (TestItemAccess missing); traceback (no row) |
| unwire-evidence: cut the wire binding evidence to its plan | fails S5-Evidence, S6-Attestation | none | 0.6667 (0.50 / 0.50 / 0.00) | 0 | shapes S5-Evidence, S6-Attestation; traceback (no row) |
| executive-attests: the authorized representative attests instead of the domain expert | fails S6-Attestation | none | 0.6667 (0.50 / 0.50 / 0.00) | 3 | shapes S6-Attestation |
| attest-without-determination: attestations aggregate no determination | fails S6-Attestation, S8-Recommendation | none | 0.6667 (0.50 / 0.50 / 0.00) | 0 | shapes S6-Attestation, S8-Recommendation; traceback (no row) |
| requirements-before-agreement: the requirement set dated before the agreement | fails S0-Layers, S0-Parties | none | 0.6667 (0.50 / 0.50 / 0.00) | 3 | shapes S0-Layers, S0-Parties |
| engagement-mismatch: the statement of work decides an interview for a population the record only speaks for | fails S0-Population | none | 0.6667 (0.50 / 0.50 / 0.00) | 3 | shapes S0-Population |
| skip-report-approval: the report delivered without a domain expert's approval of its contents | fails S8-Delivery, S8-Recommendation, S9-Acceptance | ReportApproval | 0.6667 (0.50 / 0.50 / 0.00) | 3 | shapes S8-Delivery, S8-Recommendation, S9-Acceptance; completeness (ReportApproval missing) |
| pad-pass-rate: the report's pass rate padded to one while every attestation stands | fails S7-Report | none | 0.6667 (0.50 / 0.50 / 0.00) | 3 | shapes S7-Report |
| one-person-team: the domain expert also holds the evaluation operator's role | fails S0-Roles | none | 0.6667 (0.50 / 0.50 / 0.00) | 3 | shapes S0-Roles |
| cherry-pick: an attestation drops one of its determinations without saying why | fails S6-Attestation | none | 0.6667 (0.50 / 0.50 / 0.00) | 2 | shapes S6-Attestation |

ok: generated/executor.md, the tables the chapter shows, equals what render_executor produces now

6Two executions produce identical graphs

Same model, same parameters, same graph: the two records are isomorphic and of the same size.

from rdflib.compare import isomorphic

a, b = executor.execute(model), executor.execute(model)
print(f"first execution: {len(a)} triples; second: {len(b)} triples; isomorphic: {isomorphic(a, b)}")
assert len(a) == len(b) and isomorphic(a, b)
checked.passed("two executions of the model produce isomorphic graphs")
first execution: 547 triples; second: 547 triples; isomorphic: True
ok: two executions of the model produce isomorphic graphs

7The executor refuses a model whose step signature drifted

The templates in the executor declare what each step emits; the model declares what each step’s out parameters are. A copy of the model graph loses the approval out parameter of the evaluation’s plan step, so the step’s signature no longer matches its template, and execute must raise rather than emit a record. The message it raises with is printed.

from rdflib import Graph, Namespace

SYS = Namespace("https://www.omg.org/spec/SysML#")
drifted = Graph()
for t in model:
    drifted.add(t)
approval = next(p for p in drifted.subjects(SYS.declaredName, None)
                if str(drifted.value(p, SYS.qualifiedName)) == "OGCAIE::EvaluationProcess::plan::approval")
drifted.remove((approval, None, None))
print(f"triples removed from the plan step: {len(model) - len(drifted)}")
refused = None
try:
    executor.execute(drifted)
except RuntimeError as e:
    refused = str(e)
print(f"refused: {refused}")
assert refused is not None and refused.startswith("step plan")
checked.passed("execute refuses a model whose plan step lost its approval output")
triples removed from the plan step: 6
refused: step plan: template emits ['PlanApproval', 'PlanDeviation', 'Probe', 'TestPlan'] but the model declares ['PlanDeviation', 'Probe', 'Strategy', 'TestPlan']
ok: execute refuses a model whose plan step lost its approval output

8Verdict

One line for the reader and for the gate. It is printed only when every cell above ran and every assert held.

checked.verdict()
claims checked: 8
  the first run conforms, is complete, has coverage two thirds and three traceback rows
  planned 3 of 3 has coverage one and four rows; two sessions, two requirements has coverage one and twelve rows; the five judgments conform
  all twelve mutations match the expected rows and each is caught by a named check
  skip-approval conforms to the shapes and is caught by completeness (PlanApproval missing)
  skip-access is refused by S2-RequirementSet, by completeness (TestItemAccess missing) and by the empty traceback
  generated/executor.md, the tables the chapter shows, equals what render_executor produces now
  two executions of the model produce isomorphic graphs
  execute refuses a model whose plan step lost its approval output
NOTEBOOK: PASS
Appendix C: computational proofs
Checked: A nested lifecycle
Appendix C: computational proofs
Appendix D: the rulings