In this tutorial, we will be modelling and finding a solution to the Farmer River Crossing Puzzle:

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 presense 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?

In this chapter, we are not trying to verify a global property of a system, nor are we verifying that particular operations fulfill their specifications, as in the file system example. Rather, we are trying to find a single solution, or trace, of a given state machine. The solution to this puzzle will be a sequence of states that represent the farmer's trips across the river. We will look for a trace satisfing the puzzle in exactly the same manner we would search for a (counter)example satisfying some definition of an unsafe or undesirable circumstance.

The model begins with an ** open** statement which
imposes an ordering on the set of State atoms in the model.
For now, ignore the

Next we define a signature
** Object**, which represents the set of the Farmer and
his possessions. We partition the

abstract sig Object { eats: set Object } one sig Farmer, Fox, Chicken, Grain extends Object {}

The fox will eat the chicken if the farmer is not with them, and the chicken will
eat the grain if the farmer is not with them. We represent this relationship with
the ** eats** relation from Object to Object, and we constrain the exact
value of the

fact { eats = Fox->Chicken + Chicken->Grain}

We then create a signature called ** State**, which
represents the set of states in our model. In each state, there
are a certain set of objects on the near side of the river, and a
certain set on the far side of the river.

sig State { near, far: set Object }

We would now like to say that all the ** Object**s are
on the near side of the river in the first state. We would also
like to ask Alloy to find a solution in which all the objects are
on the far side of the river in the last state. The problem is we
do not yet have a way of talking about the first state, the last
state, or the fact that one may come before or after another. In
sum, we need a way to construct a linear ordering of states and
refer to properties of that ordering. Luckily, Alloy comes with a
polymorphic linear ordering module that can do that work for
us. We import this module by adding the following
line to the beginning of our model. We parametarize on

open util/ordering[State]

The util/ordering module imposes a total ordering on the atoms of State, and
provides a few useful functions you can use, including ** first**,

returns the first State atom in the linear ordering.first

returns the last State atom in the linear ordering.last

maps each State atom (except the last atom) to the next State atom.next

Now that we've loaded util/ordering,
this is how we can use the ** util/ordering** module to say all
the

fact { first.near = Object && no first.far }

If you're thinking about this problem in terms of a state machine, this fact constrained the starting state of the state machine. Now let's describe a transition function between states.

At any state, we will call the side of the river the farmer is
currently on the '** from**' side and the other side
the '

pred crossRiver [from, from', to, to': set Object] { . . . }

Here is one way we might write this predicate:

pred crossRiver [from, from', to, to': set Object] { one x: from | { from' = from - x - Farmer - from'.eats to' = to + x + Farmer } }

We know the farmer can take at most one object with him
across the river. We use "one x: from" to pick exactly one item from the ** from** set.
There are two possibilities here:

If x is not Farmer, then the predicate says that both the Farmer and x travel from ** from**
to

If x is Farmer, then the predicate says the Farmer travels alone from ** from**
to

Next we must constrain each consecutive pair of States to abide by the transition function. If the farmer is on the near side of the river, then the near side of the river is the 'from' side and the far side of the river is the 'to' side. And if the farmer is on the far side, then the far side is 'from' and the near side 'to'. We express this constraint in the following Alloy fact.

fact { all s: State, s': s.next { Farmer in s.near => crossRiver [s.near, s'.near, s.far, s'.far] else crossRiver [s.far, s'.far, s.near, s'.near] } }

The function ** next** in the above fact is provided
by the

Here we see ** =>** followed by two expressions
(separated by the

Now that our state machine is defined, we must ask Alloy to produce a trace of the state machine in which all the objects are on the far side of the river in the final state. To do so, we ask Alloy to find a solution where at the last State, we see every Object is at the far side:

run { last.far = Object }

Recall that ** Object** is just a set and can be read
as "the set of all Objects". That is, we are saying that, in the
last State, the set of things on the far shore equals the set of
all things. This is a place where the rough OO level
understanding of Alloy will mislead you (that is, thinking of

Without specifying a scope, Alloy will assume there are 3 atoms of everything unless specified otherwise. In this case, Alloy will assume there are 3 State atoms. But Alloy Analyzer knows that there are exactly 4 Objects since it is already defined to be the union of 4 singleton disjoint atoms Farmer, Chicken, Fox, and Grain.

Not surprisingly, Alloy finds no solutions, because the problem can't be solved in only three states. If we steadily increase the scope on the set of States, we eventually reach a point at which Alloy can find a solution at a scope of 8. Thus, the command that finds the smallest solution to this puzzle is

run { last.far = Object } for exactly 8 State

Start Over . back