# `ExTLA.Coverage` [🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/coverage.ex#L1) What a model-checking run exercised. A green check mark is only as good as what was behind it. Three ways a run can report success while having verified almost nothing: - **An action that was never enabled.** A typo in a guard (`status == :Idle`) turns an action off entirely. The spec still model-checks — it is simply a *weaker* spec now, and a weaker spec passes more easily. - **A property satisfied vacuously.** `P ~> Q` where `P` never holds in any reachable state is trivially true and says nothing about `Q`. - **An invariant that was never at risk.** An invariant no reachable state ever came close to falsifying is indistinguishable from `true`. None of these are exotic; they are the routine failure mode of specification work. Reporting them is not a nice-to-have — it is the difference between a verdict and a claim. ## Collected during the run, not computed after it Coverage costs no additional exploration, but it is not computed from the finished state graph: the graph deliberately retains neither states nor per-action counts (`ExTLA.StateGraph`), so there is nothing in it to compute these from. They are accumulated while the search runs, which is the only way to have them at all. See "Reading the coverage report" in `guides/reference.md` for what each line of the report means. # `action_coverage` ```elixir @type action_coverage() :: %{ enabled_in: non_neg_integer(), states_generated: non_neg_integer(), distinct_generated: non_neg_integer() } ``` # `invariant_coverage` ```elixir @type invariant_coverage() :: %{ evaluated_in: non_neg_integer(), near_misses: non_neg_integer() | nil } ``` # `t` ```elixir @type t() :: %ExTLA.Coverage{ actions: %{required(atom()) => action_coverage()}, bounded_by: :none | :state_constraint | :max_states | :violation, held_back: non_neg_integer(), invariants: %{required(atom()) => invariant_coverage()}, live_terminals: term(), never_enabled: [atom()], param_universe: term(), probes: term(), seen_bindings: term(), terminal_but_live: [atom()], terminals: %{required(atom()) => %{admitted: non_neg_integer()}}, unreached_params: %{required(atom()) => [map()]}, vacuous: [vacuity()] } ``` # `vacuity` ```elixir @type vacuity() :: %{ property: atom(), binding: [term()], reason: :antecedent_never_held | :consequent_always_held } ``` # `clean?` Whether this run found anything worth a warning. Everything a run can say about itself, including the two that are **not** failures — a `terminal` that admitted a live state and an invariant never at risk. This is what decides whether the report is printed, and a report that stayed silent about them would hide the thing it exists to surface. `--strict-coverage` asks a different question, and `strict_failures/1` is where it is asked: a report can be worth printing without being worth failing a build over. # `finalize` Finish the accumulator into the report. # `format` Render for terminal output. # `init` A fresh accumulator for a run. # `merge` Combine one worker's accumulator into the coordinator's. `ExTLA.ModelChecker.Parallel` gives each worker a **fresh** accumulator from `init/3` and merges what comes back, so `from` describes only that worker's share of the level. The three initial probe values — `ever: false`, `always: true`, `evaluated: false` — are the identities of the operations below, which is what makes a worker that observed nothing contribute nothing. Three different rules, and using the wrong one produces a report that looks right: * **Counts add.** Each state is observed by exactly one worker — the one that won its fingerprint — and each `{state, action}` pair is expanded by exactly one worker, so nothing is observed twice and summing is exact rather than approximate. One of them is exact only in total: `distinct_generated` attributes a state to the action that reached it *first*, and which action that is depends on the order the search took. Its sum over all actions is invariant — every distinct state is credited exactly once — and its split across them is not. That is a property of the quantity, not of this merge; a single-threaded run redistributes it too if the actions are declared in a different order. And none of them is exact when the run **halted**. A search that stops at a counterexample stops mid-expansion, so every count is a lower bound rather than a census — which is what `bounded_by: :violation` records. Under workers the bound is looser and varies between runs: the coordinator starts a whole level at once and halts on the first violation it receives, so how much of that level was already merged depends on which worker finished when. Two runs of the same violating spec at different worker counts agree on the verdict and on the counterexample's length, and need not agree on the counts. * **Sets union, and predicates fold.** `ever` is a disjunction over reachable states, `always` a conjunction; splitting the states across workers and combining with `or` and `and` is the same computation in a different order. * **`param_universe` does neither.** It is a property of the CONSTANTS, not of any state: `observe_universe/4` enumerates it once, on the first initial state, before any worker exists. Every worker's copy is therefore either the coordinator's own or `:unknown`, and merging it could only replace a computed universe with an unknown one. The coordinator's is kept, deliberately. # `observe_enabled` Record that this action was enabled in a state, and with which bindings. Called *before* the successors are generated, and that is the whole point. Enablement is established the moment the guard admits a binding: it is true before any successor exists, and it stays true whether or not the expansion finishes. Recorded at the end instead, a violation that halted the expansion would lose the enablement of the action that caused it — and an action enabled in exactly one state would then be reported `never_enabled` while being named in the counterexample, warning the user that the offending action had a broken guard. `seen_bindings` belongs here too: it is a fact about the bindings the guard admitted, not about what expanding them produced. # `observe_generated` Record what expanding one state through one action produced. The other half of `observe_enabled/3`, and deliberately not the same call: *was this action enabled here* and *how many states did it generate* are different facts, known at different moments. This one stays where the numbers are known — after the expansion — because a halt there legitimately means the count is not known, which is what `bounded_by` already says. # `observe_held_back` One more state the `state_constraint:` held back. Counted where the constraint is applied rather than inferred from the config, because "a constraint was configured" and "a constraint bound this run" are different facts and only the second is a reason to call the result partial. # `observe_live_terminal` Record a state that a `terminal` predicate admits but that still has an enabled action. Not an error — nothing is cut — but almost always a predicate broader than the end state it was written for. # `observe_state` Record a newly discovered state: which invariants were evaluated on it, which were pressed against, and which temporal probes it satisfied. # `observe_stuck` Record a successor-less state and which `terminal` predicates admitted it. `admitting` is the list of terminal names whose predicate held there — the same evaluation `ExTLA.ModelChecker.Safety.classify_stuck/3` made to call the state terminal rather than deadlocked, handed over so it is counted once and not evaluated twice. An empty list is a deadlock, and counts against nothing. # `observe_universe` Note the universe of parameter combinations for an action, so the unexercised ones can be named. Only actions whose every param draws from a constant or a literal have one: the set a state function returns changes from state to state, so there is no fixed universe to subtract from. # `strict_failures` What `--strict-coverage` may fail a build on: **a never-enabled action or a vacuous property**, and only where this run is in a position to accuse. The other two warnings are not failures. A `terminal` that admitted a live state is not an error — nothing is cut — and an invariant never at risk says the run did not press on it, not that the spec is wrong. Both are still printed (`clean?/1`); neither fails the build. Returns a list of `{kind, name}`, so a caller can say which. # `warn_unless_clean` Print the warnings unless the run was clean, or fail under `strict_coverage`. Warnings by default, errors on request: a never-enabled action is a bug often enough to be worth a build failure, but not always, and a tool that refuses to proceed on a judgement call gets its check turned off entirely. # `warnings` The warnings, one line each. --- *Consult [api-reference.md](api-reference.md) for complete listing*