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.

Finish the accumulator into the report.

Render for terminal output.

A fresh accumulator for a run.

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.

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.

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.

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.

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.

Record a newly discovered state: which invariants were evaluated on it, which were pressed against, and which temporal probes it satisfied.

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.

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.

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.

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.

The warnings, one line each.