Month: June 2014

Estimating confidence intervals, part 3

Another episode in our continuing series of effort estimation in the small with 90% confidence intervals. I recently finished implementing another feature after doing the effort estimates for each day. Here’s the plot:

 

Effort estimation, 90% confidence intervals

Once again, I underestimated the effort even at the 90% level, although not as badly as last time. Here’s a plot of the error.

Error plot

I also find it takes real mental energy to do these daily effort estimates.

 

 

 

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:

 

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.