Crossing the river with TLA+

Lately, I’ve been interested in approaches to software specifications that are amenable to model checking. A few weeks ago in this blog, I wrote about solving a logic puzzle with Alloy. Today’s post is about solving a different logic puzzle. I found this one from the Alloy online tutorial:

A farmer is on one shore of a river and has with him a fox, a chicken,
and a sack of grain. He has a boat that fits one object besides himself.

In the presence of the farmer nothing gets eaten, but if left without the
farmer, the fox will eat the chicken, and the chicken will eat the grain.
How can the farmer get all three possessions across the river safely?

To solve this, I used TLA+, a specification language developed by Leslie Lamport. It also uses PlusCal, which is an algorithm language that can be automated translated into TLA+ using the TLA toolbox.

Here’s my solution, which includes PlusCal but doesn’t show the automatically translated parts of the model.

-------------------------------- MODULE boat --------------------------------
EXTENDS Integers, FiniteSets
CONSTANTS Farmer, Fox, Chicken, Grain
CREATURES == {Farmer, Fox, Chicken, Grain}

alone(animals, side) == (animals \in SUBSET side) /\ ~ Farmer \in side

somebodyGetsEaten(l, r) == \/ alone({Fox, Chicken}, l)
                           \/ alone({Fox, Chicken}, r)
                           \/ alone({Chicken, Grain}, l)
                           \/ alone({Chicken, Grain}, r)

safe(l, r) == ~somebodyGetsEaten(l, r)

safeBoats(from, to) ==
    { boat \in SUBSET from : /\ Farmer \in boat
                             /\ Cardinality(boat) <= 2
                             /\ safe(from \ boat, to \cup boat) }   
(***************************************************************************
    --algorithm RiverCrossing {
    variables left = CREATURES; right = {};
    process ( LeftToRight = 0 )
        { l: while (left /= {})
             { await (Farmer \in left);
               with(boat \in safeBoats(left, right))
                 {
                   left := left \ boat;
                   right := right \cup boat
                 }
             }
        }
    process ( RightToLeft = 1 )
        { r: while (left /= {})
             { await (Farmer \in right);
               with(boat \in safeBoats(right, left))
                 {
                   left := left \cup boat;
                   right := right \ boat
                 }
             }
        }
    }
***************************************************************************)

============================================================

To solve the problem with the TLA toolbox, you’ll need to specify an invariant that will be violated when the puzzle is solved. I used right /= CREATURES.

Run the model, and it will produce a trace that violates the invariant:

(You’ll first need to translate the PlusCal into TLA+, and you’ll need to specify the value of the constants. I just chose “Model value” for each of them).

You can see the full model with the automatic PlusCal translation in one of my Github repos.