Solving the “Wolf, Sheep and Cabbage” problem using TLA+ and the TLC model checker

Last week I bumped into a Microsoft Research talk by Leslie Lamport, named “Thinking above the code”.

As a software engineer with over 20 years of experiencing, I’ve always assumed that describing systems formally with mathematics was all well and good for academic environments, not for real world companies and businesses.

Leslie’s talk and some of the real-world examples he presented made me think twice. Namely the existence of a model checker made me think twice.

If TLA+ delivers as “advertised”, you could write your formal specification and verify it using Leslie’s TLC model checker. As stated in the talk, some big real-world companies found subtle bugs in their algorithms while they were still in the design phase, before a single line of code was written. And when I say big companies I mean companies like Amazon, Microsoft and even IBM.

Formal specification seemed to be working for these big guys so I decided to learn TLA+, Leslie’s specification language containing “as little as possible beyond what is needed to write simple mathematics precisely”.

Learning TLA+

Leslie has a small video course online, so I started there. It was way funnier than I imagined!

Leslie is a great teacher, with an awesome sense of humor and a wide selection of hats and sun glasses — see the course videos and you’ll understand why :)

If you know your way around simple boolean logic, state-machines and the concepts in mathematical sets and their operators, you’ll find out that as soon as you conquer some of the cumbersome ASCII notations, you’ll be able to read most of the specs available and even write your own.

The documentation seems hard to understand, with many formal proofs, but if you don’t give up at a first read, you’ll find out that with time you learn how to skip some of the hard proofing parts and learn the essentials semantics to write your own specs.

As times goes by and you need to gain more “vocabulary” to express your algorithms, you can go back to the documentation and suddenly some of the hard proofs become more understandable. Your brain automatically enters the “math” zone when you start writing TLA+ specs.

Solving a problem with TLC

I learn better through examples, so following Leslie’s lead with the “Die Hard” problem solution, I have decided to write a specification in TLA+ that could solve the “Wolf, Sheep and Cabbage” problem.

The problem is defined as follows:

1. A boatman has a wolf, a sheep and a cabbage on one side of the river and he must cross them to the other side.
2. He can only take one item in each trip between the river banks
3. He cannot leave the wolf and the sheep alone, as well as the sheep and the cabbage alone. Otherwise the wolf will eat the sheep and the sheep will eat the cabbage.

The problem solution is the right sequence of crossings the boatman needs to perform to cross all the items safely.

This means we can use TLC model checker to check the state tree for a viable branch where the desired state is reached (all items crossed safely). This is easily obtained by configuring a model with an invariant function. If the invariant function evaluates to FALSE at a given state, TLC will show you the state trace (the steps) required to reach that state (the solution).

Since TLC uses a breadth-first search, the sequence of steps will be the shortest path to the solution.

The state machine

In TLC you define a state machine by defining the initial state and all the possible steps to change the current state.

In the “wolf, sheep and cabbage” problem the initial state is “the wolf, the sheep, the cabbage and the boatman, are all in one bank of the river (let’s assume it’s the left bank).

To change from the current state (in fact, any state) to the next state we have the two following steps:

1. The boatman crosses with an item
2. The boatman crosses alone

In order for the boatman to be able to cross with an item (aka payload), he must select one, keeping in mind that the wolf cannot be left alone with the sheep and the sheep cannot be left alone with the cabbage.

With this in mind we can add a new action to our list, “Select an item to cross”.

These are the final possible steps:

1. The boatman selects an item to cross
2. The boatman crosses with a selected item
3. The boatman crosses alone

From now on I’ll assume you already know the basics of TLA+ notation.

Let’s start with our state variables. These are the variables required to describe a given state of our problem state machine:

The trivial definition of the initial state is the following:

This means that in the initial state all items are on the left bank of the river, no item was yet selected to transport (the payload), and obviously no item was transported on the previous step (since there was none).

Now let’s define our first action, “The boatman selects an item to cross”.

We know the boatman can only select an item from the current bank (the bank where he currently is), but not just any random item. It must be an item such that the remaining items are allowed to be left alone in the river bank when the boatman leaves to cross the river.

The predicate Allowed asserts if a certain set of entities are allowed to be left alone, and it can be trivially defined as follows:

Notice that leaving all items alone is not allowed by our problem rules, since the wolf would start eating the sheep that would be eating the cabbage!

Now that we have a predicate asserting if a given set of items are allowed to be left alone, we can specify our SelectPayload action rules as follows:

Using the existential quantifier we can express that the payload selected for transport (payload’), can only be considered if the set resulting from removing it is an allowed set, otherwise the payload is not valid and the step is not possible according to our rules. The TLC model checker will search for another item according to the existential quantifier that enables the state transition.

It’s also important that the item transported in the previous step (state variable last) is not transported back in the immediate step, since this would be simply “undoing” the current state. This condition will significantly reduce the number of possible states.

If no item is found and we are not yet in the solution state, the boatman has no other option than crossing the river alone to pick another item from the other river bank.

Now that we have selected (or not) an item to transport we can trivially define the CrossAlone and CrossItem steps as follows:

Since crossing means toggling the boatman current margin, we defined a simple function OtherBank that will return the opposite bank name:

Our next-state action is a simple disjunction of all the possible steps:

Defining the consistency invariant

Now that we have our state machine rules defined, let’s define a function that guarantees our model consistency. This function must be an invariant throughout the model checking. If at any time we get into a state where the function is not true, then we have an error in our algorithm.

The ConsistencyOK function can be defined as follows:

These three things must be true for every single state:

1. The boatman can only be in one of the river banks, left or right
2. The total number of items in the two banks must always be 3
3. The items left alone in the other bank (where the boatman is not present) must be an allowed set of items

Defining the solution found assertion

To solve this problem we will use the TLC model checker ability to verify if a given function is an invariant through the states checked. This means that if we define a function that is false when our solution is found, TLC will report it as an error and we will be able to inspect the error trace. This error trace will be the steps sequence required to reach the solution.

This invariant function, SolutionNotFound, can easily be defined as follows:

Assuming our model is consistent (assured by the ConsistencyOK invariant), if the left bank is empty then it implies all items are in the right bank as we intended and we have found our solution.

The specification pretty-print

The TLA+ Toolbox has a nice pretty-print feature that makes the spec a little bit easier to read. Here is our specification pretty-print as generated by the Toolbox:

Finding the solution

In order to use the TLC model checker to find the solution to the boatman problem we just need to create a specification and a model in the Toolbox.

The full ASCII version of the specification is the following:

In the Toolbox model overview we need to enter our initial predicate and next-state relation as follows:

Don’t forget to define the invariants also:

We are now ready to check our model and find our solution. Select the Run Model option from the Toolbox TLC Model Checker menu.

After a few seconds we get an error saying that “Invariant SolutionNotFound is violated”.

Great! This means we have a solution in the “error” trace.

In the “Error-Trace” output window scroll-down to the last state listed, the state where the invariant failed. Inspecting the log state variable will give us the sequence of steps to reach the solution, and it will be something like this:

From this inspection we learn that the solution steps sequence is the following:

1. Cross the sheep
2. Cross alone
3. Cross the wolf
4. Cross the sheep
5. Cross the cabbage
6. Cross alone
7. Cross the sheep

By inspecting the right bank state variable we verify that indeed all items were successfully crossed from left to right, without breaking the rules we have defined.

Who said math can’t be fun? :)