Meet TLA+

The question is the same: what must always be true? Units 1–5 asked it about one function. Dafny checked the code against a promise.

A design is different. Nothing runs once and returns. There are states (what the system looks like right now) and steps (the moves from one state to the next). Many parts can step in different orders.

That is where bugs hide: two leaders at once, a lock that is never released, a message delivered twice. Tests try some orders. A model checker tries every order in a small model of the system.

TLA+ is a language for describing a system as a state machine: where it starts, and how it may move. TLC is the checker that runs your description. It is called a model checker.

You write three things: the starting state, the steps the system may take, and a claim that must hold in every state. A claim like that is called an invariant. TLC starts at the first state, tries every step, and repeats from each new state. It stops when it has seen every state the model can reach, or when it finds one that breaks the claim.

The model has to be small enough to finish. That is why this checks a finite model, not the real system.

When a claim breaks, TLC gives you a trace: the states in order, from the start to the bad one. It is the same idea as a Dafny counterexample, spread across time.

The clock on the right counts hours from 1 to 12 and wraps around. Here it is one line at a time.

---- MODULE HourClock ---- and ==== open and close the file. The name has to match the file name.

EXTENDS Naturals borrows ordinary number operators such as +.

VARIABLE hr is the one thing that changes. A state is just the current value of hr.

Init == hr = 1 is the starting state. In TLA+, == means “is defined as”, and a single = means “is equal to”. So this reads: Init is defined as hr equals 1.

Next == hr' = IF hr /= 12 THEN hr + 1 ELSE 1 is one step. hr' (with the tick) is the value of hr after the step. /= means “not equal”. If the hour is not 12, the next hour is one more. Otherwise it wraps to 1.

Spec == Init /\ [][Next]_hr is the whole behavior: start in Init, then every step is a Next step, or hr stays the same. /\ means “and”. A step that changes nothing is called a stutter.

TypeOK == hr \in 1..12 is the claim: hr is always a whole number from 1 to 12. \in means “is in”. TLC checks it in every state it reaches.

Hit Verify. TLC visits all twelve hours, finds TypeOK true in each, and finds no state where the clock gets stuck with no possible step. You get a green result.

Suppose the wrap-around were removed, so Next always said hr' = hr + 1. TLC would walk through 1, 2, and so on up to 13, and stop there. At 13, TypeOK is false, so TLC shows you that list of states as the trace. You read it from the top to see how the system got there.

A green result covers only the claims you wrote, and only the model you wrote.

Specs are plain text. The symbols you will meet most: /\ is “and”, \/ is “or”, \E is “there exists”, and \in is “is in”.

Init is the starting state. Next is how the variables may change. Spec ties them together. A name such as TypeOK is a claim TLC checks in every reachable state.

In the first mission you write one of these claims yourself, for a bank balance. You do not need Lean yet.

The clock on the right already checks. Hit Verify (or ⌘↩ / Ctrl+Enter). The green check is the whole exercise. A real TLC run is the grader, so the first time you meet it, you are not solving a syntax puzzle.

Then start the bank mission. There, you will write an invariant yourself.