River Crossing

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 open statement.

Next we define a signature Object, which represents the set of the Farmer and his possessions. We partition the Object set into four singleton subsets: Farmer, Fox, Chicken, and Grain.

  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 eats relation using the following fact:

  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 Objects 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 State, so now we can call order comparison operations on elements of the State signature.

   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, next, and last.

first returns the first State atom in the linear ordering.
last returns the last State atom in the linear ordering.
next maps each State atom (except the last atom) to the next State atom.

Now that we've loaded util/ordering, this is how we can use the util/ordering module to say all the Objects are on the near side of the river and none are on the far side in the initial state:

   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 'to' side. So our function will stipulate how the set of objects on the 'from' and 'to' sides change from state to state. Thus, we have the following signature for our transition function:

   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 to, and if there were objects that would eat each other when left alone then the eating happens.

If x is Farmer, then the predicate says the Farmer travels alone from from to to, and if there were objects that would eat each other when left alone then the eating happens.

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 util/ordering module. It returns the state that follows its argument in the linear ordering. That is, s.next returns the state immediately following s; unless s is the last state in the linear order, in which case it returns the empty set. So the quantifying expression "all s: State, s': s.next" effectively says "for all consecutive pairs of states". It is equivalent to writing "all s, s': State | s' = s.next => ...".

Here we see => followed by two expressions (separated by the else keyword) used to denote a conditional (if-then-else) logical operation.

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 Object as a class), and a set theoric level of understanding is required to make sense of the model. (Recall our earlier discussion of three levels of abstractness for interpreting an Alloy model.)

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