The TLA+ / TLC Intuition

Before diving into TLA+ syntax, let's build an intuition for what TLA+ actually does. In TLA+, every algorithm is modeled as a state machine:

• A set of variables that define the state
• An initial state predicate
• A next-state relation describing all possible transitions
• Invariants — properties that must hold in every reachable state

Here's the DieHard water jugs puzzle as a TLA+ spec. You have a 5-gallon jug (big) and a 3-gallon jug (small), and need to measure exactly 4 gallons:

----------------------------- MODULE DieHard --------------------------------
EXTENDS Naturals

VARIABLES big,   \* gallons in the 5-gallon jug
          small  \* gallons in the 3-gallon jug

Init == /\ big = 0
        /\ small = 0

FillSmallJug  == /\ small' = 3
                 /\ big' = big

FillBigJug    == /\ big' = 5
                 /\ small' = small

EmptySmallJug == /\ small' = 0
                 /\ big' = big

EmptyBigJug   == /\ big' = 0
                 /\ small' = small

Min(m,n) == IF m < n THEN m ELSE n

SmallToBig == /\ big'   = Min(big + small, 5)
              /\ small' = small - (big' - big)

BigToSmall == /\ small' = Min(big + small, 3)
              /\ big'   = big - (small' - small)

Next == \/ FillSmallJug
        \/ FillBigJug
        \/ EmptySmallJug
        \/ EmptyBigJug
        \/ SmallToBig
        \/ BigToSmall

NotSolved == big # 4
=============================================================================

Notice the invariant at the bottom: NotSolved == big # 4. This says "the big jug must never contain exactly 4 gallons." We'll see how TLC uses this.