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:
- Empty the jug
- Fill the jug
- 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:
- FillBigJug (small = 0, big = 5)
- BigToSmall (small = 3, big = 2)
- EmptySmallJug (small = 0, big = 2)
- BigToSmall (small = 2, big = 0)
- FillBigJug (small = 2, big = 5)
- 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.