An invariant is true in every state
An invariant is a statement that must be true in every state a system can reach. TLA+ describes a system as states and steps, and its checker TLC searches for a state that breaks the invariant.
When it finds one, TLC prints the shortest list of steps that leads there.
By the end of this lesson
Note
I can write an invariant and read the counterexample for a broken design.
Key words
| Word | What it means |
|---|---|
| State | the value of every variable at one moment |
| Step | a change from one state to the next |
| Invariant | a statement true in every reachable state |
| Reachable state | a state some run of steps can get to |
| TLC | the checker that searches every reachable state |
| Counterexample | a run of steps that ends in a bad state |
The cells students fill in are left blank in this preview.
A system is states and steps
A cash machine pays out 10 pounds. Two machines draw on one account of 10 pounds. Each machine does two steps: check that the balance is at least 10, then take 10.
TLA+ writes this as variables and rules. Init is the starting state. Each action says when a step may happen and what changes. Next allows any action.
Worked example: the model, line by line
| Line | What it says |
|---|---|
| Init == balance = 10 /\ a = 0 /\ b = 0 | start with 10 pounds and both machines waiting |
| CheckA == a = 0 /\ balance >= 10 /\ a' = 1 /\ ... | machine A may check if it waits and money is there |
| TakeA == a = 1 /\ balance' = balance - 10 /\ ... | a machine that checked takes 10 |
| Next == CheckA \/ TakeA \/ CheckB \/ TakeB \/ ... | any one of the four steps may happen |
| NotOverdrawn == balance >= 0 | the invariant: the balance is never below 0 |
The cells students fill in are left blank in this preview.
Write the model
printf '%s\n' "---- MODULE Atm ----" "EXTENDS Integers" "VARIABLES balance, a, b" "vars == <<balance, a, b>>" "Init == balance = 10 /\ a = 0 /\ b = 0" "CheckA == a = 0 /\ balance >= 10 /\ a' = 1 /\ UNCHANGED <<balance, b>>" "TakeA == a = 1 /\ balance' = balance - 10 /\ a' = 2 /\ UNCHANGED b" "CheckB == b = 0 /\ balance >= 10 /\ b' = 1 /\ UNCHANGED <<balance, a>>" "TakeB == b = 1 /\ balance' = balance - 10 /\ b' = 2 /\ UNCHANGED a" "Next == CheckA \/ TakeA \/ CheckB \/ TakeB \/ UNCHANGED vars" "Spec == Init /\ [][Next]_vars" "NotOverdrawn == balance >= 0" "====" > Atm.tlaShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
TLC prints the shortest bad run
TLC tries every one-step run, then every two-step run, and so on. The first bad state it meets is therefore reached by a shortest run.
The Run below checks NotOverdrawn. The grep keeps the verdict, each state's heading and the balance, so the five states are easy to read.
Check the invariant
tlc Atm NotOverdrawn | grep -E 'violated|^State|balance'Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Worked example: the shortest bad run
| State | Step | Balance |
|---|---|---|
| 1 | start | 10 |
| 2 | A checks: balance is 10, enough | 10 |
| 3 | B checks: balance is still 10 | 10 |
| 4 | A takes 10 | 0 |
| 5 | B takes 10 | -10 |
The cells students fill in are left blank in this preview.
Check again at the moment you take
The fault is that the check is old by the time of the take. The fix is to check again in the take step. The second machine then finds 0 and does not take.
The next two Runs write the fixed model and check the same invariant.
Write the fixed model
printf '%s\n' "---- MODULE AtmSafe ----" "EXTENDS Integers" "VARIABLES balance, a, b" "vars == <<balance, a, b>>" "Init == balance = 10 /\ a = 0 /\ b = 0" "CheckA == a = 0 /\ balance >= 10 /\ a' = 1 /\ UNCHANGED <<balance, b>>" "TakeA == a = 1 /\ balance >= 10 /\ balance' = balance - 10 /\ a' = 2 /\ UNCHANGED b" "CheckB == b = 0 /\ balance >= 10 /\ b' = 1 /\ UNCHANGED <<balance, a>>" "TakeB == b = 1 /\ balance >= 10 /\ balance' = balance - 10 /\ b' = 2 /\ UNCHANGED a" "Next == CheckA \/ TakeA \/ CheckB \/ TakeB \/ UNCHANGED vars" "Spec == Init /\ [][Next]_vars" "NotOverdrawn == balance >= 0" "====" > AtmSafe.tlaShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Check the fixed model
tlc AtmSafe NotOverdrawn | grep 'No error'Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A common mistake
Warning
Many people think a system works once its invariant holds. The fixed machines never overdraw, but one customer may be refused and never paid. An invariant says what never happens. It does not say that anything useful ever happens.