Appendix B — Models-bridge patterns

Appendix B - 6. Coverage → model-node mapping (which invariants are actually tested)

The Structure of Coverage → model-node mapping (which invariants are actually tested) — its shape at a glance:

The mapping joins coverage data to the model's nodes through the node→code map. Each node comes out covered or uncovered; the uncovered critical ones drive a backlog, and a promoted gate can require a test for each critical node.

flowchart LR
  Cov[(Coverage data)] --> Join{Node join}
  Nodes[(Model nodes)] --> Join
  Join --> Backlog[Uncovered = backlog]
  Join --> Gate{{Critical-node gate}}

Accessible description: coverage data and the model's nodes both feed a join keyed on the node-to-code map. The join labels each node covered or uncovered; uncovered nodes become a test backlog, and a gate can fail the build on an uncovered critical node.

Projected from the catalogue entry system-models / Coverage → model-node mapping (which invariants are actually tested).

On this page: Intent · Motivation · Applicability · Structure · Sample Code · Consequences · Example use within DocAble · Related Patterns

Intent

Intent — Project test coverage onto the model's nodes (its states, seams, and invariants), so "is this invariant tested?" is a queried fact, not a guess from a line-coverage percentage. The map turns the model into a test work-list: an invariant node with no covering test is a visible gap that drives the next test (our instance: a coverage-reference mapping test coverage onto the cross-service state-machine model's nodes at function granularity).

Motivation

Line and branch coverage tell you what fraction of the code ran under test, not which of the system's invariants are actually exercised. A model can show 90% line coverage while a critical race invariant has zero tests touching its states, because coverage counts lines, not meanings. So the invariants you most need verified hide inside a high aggregate number, and "are we testing the thing that matters?" is unanswerable from the coverage report. The failure is a false sense of test adequacy: a green coverage number sitting over an untested critical invariant.

Applicability

Structure

The Structure diagram appears at the top of this page.

Sample Code

The map joins per-node coverage to the model. A node is covered when any covering test hits a function that realizes it; an uncovered critical node is a finding — the model becomes a test work-list instead of a percentage to chase.

import sys

# node -> the set of functions that realize it (the node->code join key).
NODE_FUNCS = {"lease_invariant": {"acquire", "renew"}, "requeue": {"on_preempt"}}
CRITICAL   = {"lease_invariant"}

def uncovered(covered_funcs: set[str]) -> list[str]:
    """A node is covered iff some covering test hit a function realizing it."""
    findings = []
    for node, funcs in NODE_FUNCS.items():
        if not (funcs & covered_funcs):
            tag = "CRITICAL" if node in CRITICAL else "node"
            findings.append(f"{tag} '{node}' has no covering test")
    return findings

if __name__ == "__main__":
    # `covered_functions` reads the coverage report and returns the functions any test exercised.
    findings = uncovered(covered_functions())
    for f in findings:
        print(f"UNTESTED: {f}")
    # Gate mode: fail only on uncovered CRITICAL nodes; the rest is a backlog.
    sys.exit(1 if any("CRITICAL" in f for f in findings) else 0)

Consequences

Example use within DocAble

Contents
⇐ Beginning of this partNext part ⇒Next chapter ›⇤ BeginningEnd ⇥Index
© James C. Davis, 2026–present