Checked: A nested lifecycle - CAIE as an executable specification

This page runs the checks that the Checked block of the nested lifecycle chapter claims: the authoring view validates strictly under the pinned converter; the canonical graph regenerates byte for byte within its budget; the four M4 shapes hold over it; S0-Layers holds over the record and the counterexample of a requirement set declared before the agreement fails it. 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.

import sys; sys.path[:0] = ["notebooks", "."]  # the shared module lives beside this notebook
import json
import subprocess
import tempfile
from pathlib import Path

import checked

sys.path.insert(0, str(checked.ROOT / "scripts"))
from prune_model import TRIPLE_BUDGET, build  # the one pipeline that writes the canonical graph

SYSML = checked.toolchain()  # toolchain/bin/sysml, OpenSysML v0.4.3 pinned by digest

1The authoring view validates strictly¶

model/caie.sysml is the authoring view (R-22). The pinned converter is run from the repository root as a subprocess, exactly as the gate runs it, with -validate -strict. The claim is its exit code; its output lines are printed as they come.

r = subprocess.run([str(SYSML), "model/caie.sysml", "-validate", "-strict"], cwd=checked.ROOT, capture_output=True, text=True)
print("$ sysml model/caie.sysml -validate -strict")
print((r.stdout + r.stderr).rstrip())
print(f"(exit {r.returncode})")
assert r.returncode == 0 and "no errors" in r.stdout
checked.passed("model/caie.sysml validates under sysml -validate -strict with exit 0")

$ sysml model/caie.sysml -validate -strict
✓ package CAIE
✓ model/caie.sysml: no errors
(exit 0)
ok: model/caie.sysml validates under sysml -validate -strict with exit 0

2The canonical graph regenerates byte for byte within its budget¶

scripts/prune_model.py converts the authoring view with the pinned converter, prunes the result to the term map and serialises it deterministically. Its build is called here into a temporary path and the bytes are compared with the committed model/caie.model.ttl; the fresh manifest is compared with model/model_manifest.json (only the artifact’s path differs, since the fresh file has a temporary name); and the triple count is held against TRIPLE_BUDGET, the parsimony gate whose rationale the manifest carries.

committed = checked.ROOT / "model" / "caie.model.ttl"
manifest = json.loads((checked.ROOT / "model" / "model_manifest.json").read_text())
with tempfile.TemporaryDirectory() as tmp:
    out, fresh_manifest_path = Path(tmp) / "caie.model.ttl", Path(tmp) / "model_manifest.json"
    graph = build(checked.ROOT / "model" / "caie.sysml", out, fresh_manifest_path)
    identical = out.read_bytes() == committed.read_bytes()
    fresh_manifest = json.loads(fresh_manifest_path.read_text())
fresh_manifest["artifact"]["path"] = manifest["artifact"]["path"]
print(f"raw conversion: {manifest['raw']['triples']} triples; pruned: {len(graph)} triples; budget: {TRIPLE_BUDGET}; headroom: {TRIPLE_BUDGET - len(graph)}")
print(f"fresh bytes equal the committed graph: {identical}")
print(f"fresh manifest equals the committed manifest: {fresh_manifest == manifest}")
assert identical and fresh_manifest == manifest
checked.passed("model/caie.model.ttl regenerates byte for byte, with its manifest")
assert len(graph) <= TRIPLE_BUDGET and manifest["artifact"]["triples"] == len(graph) and manifest["triple_budget"]["value"] == TRIPLE_BUDGET
checked.passed("the graph is within the triple budget and the manifest records both")

raw conversion: 18976 triples; pruned: 5712 triples; budget: 6600; headroom: 888
fresh bytes equal the committed graph: True
fresh manifest equals the committed manifest: True
ok: model/caie.model.ttl regenerates byte for byte, with its manifest
ok: the graph is within the triple budget and the manifest records both

3The process shapes hold over the graph¶

The four M4 shapes are copied from shapes/model.shapes.ttl: the steps in fixed succession (M4-Steps), the evaluation process nested in the contracting lifecycle by typing, its inputs fed by contracting steps and its outputs feeding one (M4-Nesting), the successions forming a DAG (M4-ProcessDag), and every item kind produced by some step (M4-EveryItemProduced).

model = checked.model_graph()
M4 = checked.shapes("shapes/model.shapes.ttl", ["M4-Steps", "M4-Nesting", "M4-ProcessDag", "M4-EveryItemProduced"])
conforms, fired = checked.report("model/caie.model.ttl", model, M4)
assert conforms and not fired
checked.passed("the model graph conforms to M4-Steps, M4-Nesting, M4-ProcessDag and M4-EveryItemProduced")

model/caie.model.ttl: conforms = True
  M4-EveryItemProduced pass
  M4-Nesting           pass
  M4-ProcessDag        pass
  M4-Steps             pass
ok: the model graph conforms to M4-Steps, M4-Nesting, M4-ProcessDag and M4-EveryItemProduced

4The two layers of the record¶

S0-Layers holds the layers apart: every item pinned at the contract is generated no later than the requirement set, and every item pinned within the evaluation no earlier than the agreement (R-32). It is run alone over the measles evaluation, loaded with the model graph as the test suite loads it.

record = checked.record()
S = checked.shapes("shapes/epo.shapes.ttl", ["S0-Layers"])
conforms, fired = checked.report("track/measles-evaluation.ttl", record, S)
assert conforms and not fired
checked.passed("the measles evaluation conforms to S0-Layers")

track/measles-evaluation.ttl: conforms = True
  S0-Layers            pass
ok: the measles evaluation conforms to S0-Layers

5A requirement set declared before the agreement¶

counterexamples/requirements-before-agreement.ttl dates the requirement set before the agreement was signed. The chapter says it fails S0-Layers. S0-Parties fires as well when it is in the shapes graph, since that shape carries its own ordering constraint, that the agreement precedes the requirement set (R-21); both are run here so the reader sees both, and the assert is about S0-Layers.

cx = checked.counterexample("requirements-before-agreement.ttl")
S = checked.shapes("shapes/epo.shapes.ttl", ["S0-Layers", "S0-Parties"])
conforms, fired = checked.report("counterexamples/requirements-before-agreement.ttl", cx, S)
assert not conforms and "S0-Layers" in fired
checked.passed("requirements-before-agreement.ttl does not conform and fails S0-Layers")

counterexamples/requirements-before-agreement.ttl: conforms = False
  S0-Layers            FAIL
  S0-Parties           FAIL
  S0-Layers at ev:service-agreement:
    S0 two layers (R-32): every item of the record pinned at the contract is generated no later than the requirement set, and every item pinned within the evaluation no earlier than the agreement.
  S0-Parties at ev:service-agreement:
    S0: the agreement precedes the requirement set: requirements are agreed under the contract, not before it (R-21).
ok: requirements-before-agreement.ttl does not conform and fails S0-Layers

6Verdict¶

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: 6
  model/caie.sysml validates under sysml -validate -strict with exit 0
  model/caie.model.ttl regenerates byte for byte, with its manifest
  the graph is within the triple budget and the manifest records both
  the model graph conforms to M4-Steps, M4-Nesting, M4-ProcessDag and M4-EveryItemProduced
  the measles evaluation conforms to S0-Layers
  requirements-before-agreement.ttl does not conform and fails S0-Layers
NOTEBOOK: PASS