Invariants & Running TLC

What an invariant is

An invariant is a predicate on the state that we claim is true in every reachable state of a spec — the initial state, and every state reachable from it by taking Next steps. In set-theoretic terms, if Reachable is the set of all states a spec can ever be in, and we use Inv as a stand-in name for whatever invariant we're checking (not a specific operator — TypeOK below is a concrete example of one), then Inv is an invariant exactly when:

Reachable ⊆ { s ∈ States : Inv(s) }

Reading this symbol by symbol: ⊆ means "is a subset of" — everything on the left is also in the set on the right. { s ∈ States : Inv(s) } is set-builder notation — "the set of every s drawn from States, such that Inv(s) is true" (s ∈ States names s as ranging over States; : reads as "such that"; Inv(s) is a true/false question asked of that particular s). So the whole line says: every reachable state is one where Inv holds — which is exactly what "invariant" means.

The most basic invariant you'll write for almost every spec is a type invariant, conventionally named TypeOK: a statement of what set each variable's value must always belong to. It doesn't say anything about how the variables relate to each other over time — just that they never leave their expected domain. For the hour clock from the previous chapters:

TypeOK == hr \in (1..12)

This reads exactly like the set membership you already know: hr is an element of the set 1..12. If Next ever computed something like hr' = 13, TypeOK would be false in the resulting state, and we'd want to know about it.

TLC: a model checker, not a proof assistant

TLC is the tool that actually checks an invariant holds. Give it:

1. a Spec (built from Init and Next, as in the last chapter), and
2. one or more invariants to check,

and TLC explores the entire reachable state space — every state reachable from Init by repeatedly applying Next — checking the invariant in each one it visits. If it ever finds a state where the invariant is false, it stops and prints the shortest trace of states from Init that gets you there: a concrete counterexample you can read step by step.

This only works because TLC restricts itself to finite state spaces (bounded CONSTANTS, bounded ranges like 1..12) — it is doing exhaustive search, not symbolic proof. That's the trade-off: TLC can't tell you an invariant holds for all possible sizes of a system, only that it holds for the specific finite instance you modeled. But it will catch real bugs — off-by-one errors, missed edge cases in Next — that are easy to miss by eye.

The .cfg file

TLA+ modules don't say which invariants to check or what values CONSTANTS should take — that's the model checker's job, configured in a separate .cfg file:

SPECIFICATION Spec
INVARIANT TypeOK

This tells TLC: use Spec as the specification to check, and verify TypeOK in every reachable state.

What you'll do in this exercise

You'll write (or fix) HourClock.tla — Lamport's classic first example from Specifying Systems: a clock that cycles through the hours 1 to 12 — and run it through TLC against TypeOK. If your Next action has a bug (say, it lets hr go from 12 to 13 instead of wrapping to 1), TLC will show you the exact trace: hr = 12 in one state, hr = 13 in the next, invariant violated.