Designing Concurrent & Distributed Systems with TLA+

“Why should you listen to this clown?” The clown in picture is the Turing-award winner Leslie Lamport and that’s the question he asks the viewers of his Introduction to TLA+ video part of the TLA+ Video Course, which I recommend you to watch. Lamport is also famous for LaTeX, Paxos algorithm, Lamport’s bakery algorithm, among others. In this post, we will focus on his work on temporal logic of actions (TLA) using the TLA+ language to specify and reason about concurrent and reactive systems.

A clasical problem to demonstrate the basic capabilities and syntac of TLA+ is the Die Hard jug problem. This classic puzzle involves measuring out exactly 4 gallons of water using a 3-gallon jug and a 5-gallon jug.

So, first let’s formalize the problem statement:

------------------------------ MODULE DieHard ------------------------------- 

EXTENDS Naturals

VARIABLES big,   \* The number of gallons of water in the 5 gallon jug.
          small  \* The number of gallons of water in the 3 gallon jug.

TypeOK == /\ small \in 0..3 
          /\ big   \in 0..5

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

The MODULE defines the name of our program since TLA+ are single file programs. The VARIABLES keyword defines the names of the jugs. And the TypeOK is the invariant which asserts that the value of each variable is an element of the appropriate set, for this problem this is the valid number of galons for each jug - you can read it as in the mathematical form:

$$small\in[0,3] \land big\in[0,5]$$

The Init defines that both jugs are empty at the start. With the initial baseline out of the way, we can now define the actions that can be performed per each jug:

  1. Empty the jug
  2. Fill the jug
  3. Pour from one jug to the other

These can be formalized as follows:

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)

All that is left to do is to summarize those actions as part of the Next relationship. So, we can list all 6 of the previously defined actions as being alternatives at any point in time with the mathematical symbol $\lor$. After, we define the Spec which starts in the Init state and defines the Next action that can be taken - in the background this is creating a state machine.

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

Spec == Init /\ [][Next]_<< big, small >>

Finally, we just need to define what is the state when the puzzle is not solved, which is when the big jug does not have 4 gallons (# signifies “different”), since the small one can’t accomadate that:

NotSolved == big # 4

After defining the problem, we just need to run it to get to the puzzle solution:

  1. FillBigJug (small = 0, big = 5)
  2. BigToSmall (small = 3, big = 2)
  3. EmptySmallJug (small = 0, big = 2)
  4. BigToSmall (small = 2, big = 0)
  5. FillBigJug (small = 2, big = 5)
  6. BigToSmall (small = 3, big = 4)

And that’s it! Quite simple taking into account that we just formalized the problem.

For the full code refer to DieHard.tla. This blog post was inspired by a recent workshop I attended by Markus Kuppe where we went a bit deeper on the TLA+ topic. If you are interested in a more advanced problem, you to check EWD998.