Lorin Hochstein

Ramblings about software, research and other things

Crossing the river with TLA+

with one comment

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:

 

error-trace

(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.

Advertisements

Written by Lorin

June 4, 2014 at 10:27 pm

Posted in software

One Response

Subscribe to comments with RSS.

  1. how you open tla error?

    clement

    December 9, 2016 at 5:48 am


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: