# River Crossing Puzzle with Alloy

### david karapetyan ・5 min read

Last time we solved the 8 queens puzzle by writing the attack constraints for queens on the board and then let Alloy figure out if the constraints were consistent or not. Our constraints did not involve any state transitions in the sense that we didn't specify how to place queens on the board one after the other. We just wrote the constraint that every valid solution had to satisfy and let Alloy do the rest.

In this tutorial we learn about `util/ordering`

and how it allows us to succinctly express transition relations between states.

I'm going to use the river crossing puzzle to demonstrate. There are many variations of this puzzle but I'm going to use the one with a farmer, a cabbage, a goat, and a wolf. The solution of the puzzle is a sequence of steps/states that describes how the farmer gets the wolf, the goat, and the cabbage from one side of the river to the other without the goat eating the cabbage and the wolf eating the goat.

First we open the ordering module so that we get access to the ordering relations on our state representation

```
// The states are ordered so that we can talk about transitions
open util/ordering[State]
```

I haven't defined yet what `State`

means but I will shortly after defining the entities of the puzzle

```
// The farmer, cabbage, goat, and wolf
abstract sig Entity { }
one sig Farmer, Cabbage, Goat, Wolf extends Entity { }
```

The puzzle specifies a certain relation between the entities and the relation is that when the farmer is not around the goat will eat the cabbage and the wolf will eat the goat

```
// If the farmer is not around then X - eats -> Y
let eats = (Goat -> Cabbage) + (Wolf -> Goat)
```

The above is enough to define our `State`

```
// State consists of a left and right entity sets modeling
// the banks of the river. The banks are disjoint and together
// they include all the entities
sig State {
left, right: set Entity
} {
// The combination of left and right must include all entities
Entity = left + right
// The left and right banks must be disjoint
no left & right
// NOTE: Try removing one of the conditions and running the model to see what
// happens. It's actually interesting
}
```

This is some new syntax and consists of defining fields and the invariants that each instance of the state must conform to. In the above we have two constraints: `Entity = left + right`

, `no left & right`

. In plain english it says that the left and right bank of the river contain all the entities and the left and right banks are disjoint so that we don't have a cabbage on both sides of the river.

We still need to define some predicates to further constrain allowed states. The simplest constraint is that a set of entities is valid if it has a farmer or there are no pairs of entities such that one will eat the other

```
// The entities on the bank are valid if the Farmer is there or
// there are no eating combinations
pred validSubState(s: set Entity) {
Farmer in s || no (s & s.eats)
}
```

With a definition for a valid set of entities we can define a valid state as one for which each side of the river consists of a valid set of entities, i.e. one side or the other has a farmer and neither side has anything that will eat anything else if the farmer is not around

```
// Valid state means both banks are valid
pred validState(s: State) {
validSubState[s.left] && validSubState[s.right]
}
```

With all of that out of the way we can define the transition relation between states, i.e. how does the farmer carry something from one side of the river to the other

```
// Now we specify a valid transition from s to s' = s.next
pred transition(s: State, s': State) {
// This is redundant but doesn't hurt to have it
s' = s.next
// The transition can move at most one item along with the Farmer. Since
// we don't exclude e from being the Farmer it could be that the Farmer
// is the only thing that moves from one bank to the next when e = Farmer
one e: Entity {
Farmer in s.left => {
e in s.left && s'.right = s.right + Farmer + e
} else {
e in s.right && s'.left = s.left + Farmer + e
}
}
// The pre and post states must be valid. Although technically if we start
// with a valid state then we can never end up in an invalid state so checking
// that the initial state is valid is redundant
validState[s] && validState[s']
}
```

In plain english the above says that we have two states `s`

and `s'`

where `s'`

is the state right after `s`

and related to it by a single step in the transition relation. The transition relation in turn is specified as a set of constraints about the the left and right banks of the pre (`s`

) and post state (`s'`

). In plain english it says that to transition from `s`

to `s'`

the farmer must move from one side to the other either by himself or by carrying some entity with him.

Now we have a valid transition relation but it doesn't mean much yet because we haven't defined conditions for the starting and ending states so we do that now

```
// We are done when everything is on the right bank
pred done(s: State) { Entity = s.right }
// We start with everything on the left bank
pred init(s: State) { Entity = s.left }
```

We are done when all the entities are on the right bank and we start with all the entities in the left bank.

Now we can run the model to get a solution

```
// Make sure the first and last state are what we want and that we can transition
// from the first state to the last state
run {
init[first]
all s: State, s': s.next | transition[s, s']
done[last]
} for 8 State
```

Because we opened `util/ordering`

we have access to `first`

, `last`

, and `next`

relations on our `State`

. The above says the first state (`first`

) must satisfy `init`

and the last state (`last`

) must satisfy `done`

. Every state in between those two must be related by the transition relation that we defined.

You're encouraged to run the model and see how Alloy presents the states. In the UI you want to use the the projection function and project over `State`

:

That will let you interactively go from one state to the next by pressing ">>":