The names of every terminal whose predicate admits state. Empty means a deadlock.

classify_stuck/3 is this with the names thrown away; the checker asks for the names so coverage can count which terminal ended which behaviour from one evaluation.

Check all action properties against a transition.

Check the selected invariants against a single state.

only restricts the check to named invariants, the way a TLC .cfg selects which of a module's invariants a run checks; :all is every declared one.

Classify a state that produced no successors: :terminal if a terminal predicate admits it (02-dsl-semantics.md §5.3), :deadlocked otherwise.

A terminal says which states are meant to be final, which is why it is preferred over check_deadlock: false — that turns the check off for every other state in the spec at the same time.

Refuse a selection naming something the spec does not declare.

Without this, a typo checks nothing and the run reports :ok:

invariants: [:cap]         status=:violation
invariants: [:capp] (typo) status=:ok  warnings=[]

The filter matched no declaration, the coverage table came out empty, and the search had nothing to evaluate — so the run would be green because it verified nothing. A checker must never report success for a check it did not perform.

It matters beyond a hand-typed config: a test that selects invariants by names read from a file would, on a misspelled name, make assert result.status == :ok pass having checked nothing at all.

The declarations a run with only will actually check.

Selection exists because a run halts at the first violation, as TLC's does: getting a verdict for each invariant separately means one run per invariant, and a run that only measures the state count has to check nothing at all.