River crossing puzzle

The aim of this tutorial is to write a query that finds a solution to the following classical logic puzzle:

River crossing puzzle

A man is trying to ferry a goat, a cabbage, and a wolf across a river. His boat can only take himself and at most one item as cargo. His problem is that if the goat is left alone with the cabbage, it will eat it. And if the wolf is left alone with the goat, it will eat it. How does he get everything across the river?

A solution should be a set of instructions for how to ferry the items, such as “First ferry the goat across the river, and come back with nothing. Then ferry the cabbage across, and come back with …”

There are lots of ways to approach this problem and implement it in QL. Before you start, make sure that you are familiar with how to define classes and predicates in QL. The following walkthrough is just one of many possible implementations, so have a go at writing your own query too! To find more example queries, see the list below.

Walkthrough

Model the elements of the puzzle

The basic components of the puzzle are the cargo items and the shores on either side of the river. Start by modeling these as classes.

First, define a class Cargo containing the different cargo items. Note that the man can also travel on his own, so it helps to explicitly include "Nothing" as a piece of cargo.

Show/hide code
/** A possible cargo item. */
class Cargo extends string {
  Cargo() {
    this = "Nothing" or
    this = "Goat" or
    this = "Cabbage" or
    this = "Wolf"
  }
}

Second, any item can be on one of two shores. Let’s call these the “left shore” and the “right shore”. Define a class Shore containing "Left" and "Right".

It would be helpful to express “the other shore” to model moving from one side of the river to the other. You can do this by defining a member predicate other in the class Shore such that "Left".other() returns "Right" and vice versa.

Show/hide code
/** One of two shores. */
class Shore extends string {
  Shore() {
    this = "Left" or
    this = "Right"
  }

  /** Returns the other shore. */
  Shore other() {
    this = "Left" and result = "Right"
    or
    this = "Right" and result = "Left"
  }
}

We also want a way to keep track of where the man, the goat, the cabbage, and the wolf are at any point. We can call this combined information the “state”. Define a class State that encodes the location of each piece of cargo. For example, if the man is on the left shore, the goat on the right shore, and the cabbage and wolf on the left shore, the state should be Left, Right, Left, Left.

You may find it helpful to introduce some variables that refer to the shore on which the man and the cargo items are. These temporary variables in the body of a class are called fields.

Show/hide code
/** A record of where everything is. */
class State extends string {
  Shore manShore;
  Shore goatShore;
  Shore cabbageShore;
  Shore wolfShore;

  State() { this = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore }
}

We are interested in two particular states, namely the initial state and the goal state, which we have to achieve to solve the puzzle. Assuming that all items start on the left shore and end up on the right shore, define InitialState and GoalState as subclasses of State.

Show/hide code
/** The initial state, where everything is on the left shore. */
class InitialState extends State {
  InitialState() { this = "Left" + "," + "Left" + "," + "Left" + "," + "Left" }
}

/** The goal state, where everything is on the right shore. */
class GoalState extends State {
  GoalState() { this = "Right" + "," + "Right" + "," + "Right" + "," + "Right" }
}

Note

To avoid typing out the lengthy string concatenations, you could introduce a helper predicate renderState that renders the state in the required form.

Using the above note, the QL code so far looks like this:

Show/hide code
/** A possible cargo item. */
class Cargo extends string {
  Cargo() {
    this = "Nothing" or
    this = "Goat" or
    this = "Cabbage" or
    this = "Wolf"
  }
}

/** One of two shores. */
class Shore extends string {
  Shore() {
    this = "Left" or
    this = "Right"
  }

  /** Returns the other shore. */
  Shore other() {
    this = "Left" and result = "Right"
    or
    this = "Right" and result = "Left"
  }
}

/** Renders the state as a string. */
string renderState(Shore manShore, Shore goatShore, Shore cabbageShore, Shore wolfShore) {
  result = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore
}

/** A record of where everything is. */
class State extends string {
  Shore manShore;
  Shore goatShore;
  Shore cabbageShore;
  Shore wolfShore;

  State() { this = renderState(manShore, goatShore, cabbageShore, wolfShore) }
}

/** The initial state, where everything is on the left shore. */
class InitialState extends State {
  InitialState() { this = renderState("Left", "Left", "Left", "Left") }
}

/** The goal state, where everything is on the right shore. */
class GoalState extends State {
  GoalState() { this = renderState("Right", "Right", "Right", "Right") }
}

Model the action of “ferrying”

The basic act of ferrying moves the man and one cargo item to the other shore, resulting in a new state.

Write a member predicate (of State) called ferry, that specifies what happens to the state after ferrying a particular cargo. (Hint: Use the predicate other.)

Show/hide code
  /** Returns the state that is reached after ferrying a particular cargo item. */
  State ferry(Cargo cargo) {
    cargo = "Nothing" and
    result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore)
    or
    cargo = "Goat" and
    result = renderState(manShore.other(), goatShore.other(), cabbageShore, wolfShore)
    or
    cargo = "Cabbage" and
    result = renderState(manShore.other(), goatShore, cabbageShore.other(), wolfShore)
    or
    cargo = "Wolf" and
    result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore.other())
  }

Of course, not all ferrying actions are possible. Add some extra conditions to describe when a ferrying action is “safe”. That is, it doesn’t lead to a state where the goat or the cabbage get eaten. For example, follow these steps:

  1. Define a predicate isSafe that holds when the state itself is safe. Use this to encode the conditions for when nothing gets eaten.
  2. Define a predicate safeFerry that restricts ferry to only include safe ferrying actions.
Show/hide code
  /**
   * Holds if the state is safe. This occurs when neither the goat nor the cabbage
   * can get eaten.
   */
  predicate isSafe() {
    // The goat can't eat the cabbage.
    (goatShore != cabbageShore or goatShore = manShore) and
    // The wolf can't eat the goat.
    (wolfShore != goatShore or wolfShore = manShore)
  }

  /** Returns the state that is reached after safely ferrying a cargo item. */
  State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }

Find paths from one state to another

The main aim of this query is to find a path, that is, a list of successive ferrying actions, to get from the initial state to the goal state. You could write this “list” by separating each item by a newline ("\n").

When finding the solution, you should be careful to avoid “infinite” paths. For example, the man could ferry the goat back and forth any number of times without ever reaching an unsafe state. Such a path would have an infinite number of river crossings without ever solving the puzzle.

One way to restrict our paths to a finite number of river crossings is to define a member predicate State reachesVia(string path, int steps). The result of this predicate is any state that is reachable from the current state (this) via the given path in a specified finite number of steps.

You can write this as a recursive predicate, with the following base case and recursion step:

  • If this is the result state, then it (trivially) reaches the result state via an empty path in zero steps.
  • Any other state is reachable if this can reach an intermediate state (for some value of path and steps), and there is a safeFerry action from that intermediate state to the result state.

To ensure that the predicate is finite, you should restrict steps to a particular value, for example steps <= 7.

Show/hide code
  /**
   * Returns all states that are reachable via safe ferrying.
   * `path` keeps track of how it is achieved and `steps` keeps track of the number of steps it takes.
   */
  State reachesVia(string path, int steps) {
    // Trivial case: a state is always reachable from itself
    steps = 0 and this = result and path = ""
    or
    // A state is reachable using pathSoFar and then safely ferrying cargo.
    exists(int stepsSoFar, string pathSoFar, Cargo cargo |
      result = this.reachesVia(pathSoFar, stepsSoFar).safeFerry(cargo) and
      steps = stepsSoFar + 1 and
      // We expect a solution in 7 steps, but you can choose any value here.
      steps <= 7 and
      path = pathSoFar + "\n Ferry " + cargo
    )
  }

However, although this ensures that the solution is finite, it can still contain loops if the upper bound for steps is large. In other words, you could get an inefficient solution by revisiting the same state multiple times.

Instead of picking an arbitrary upper bound for the number of steps, you can avoid counting steps altogether. If you keep track of states that have already been visited and ensure that each ferrying action leads to a new state, the solution certainly won’t contain any loops.

To do this, change the member predicate to State reachesVia(string path, string visitedStates). The result of this predicate is any state that is reachable from the current state (this) via the given path without revisiting any previously visited states.

  • As before, if this is the result state, then it (trivially) reaches the result state via an empty path and an empty string of visited states.
  • Any other state is reachable if this can reach an intermediate state via some path, without revisiting any previous states, and there is a safeFerry action from the intermediate state to the result state. (Hint: To check whether a state has previously been visited, you could check if there is an index of visitedStates at which the state occurs.)
Show/hide code
  /**
   * Returns all states that are reachable via safe ferrying.
   * `path` keeps track of how it is achieved.
   * `visitedStates` keeps track of previously visited states and is used to avoid loops.
   */
  State reachesVia(string path, string visitedStates) {
    // Trivial case: a state is always reachable from itself.
    this = result and
    visitedStates = this and
    path = ""
    or
    // A state is reachable using pathSoFar and then safely ferrying cargo.
    exists(string pathSoFar, string visitedStatesSoFar, Cargo cargo |
      result = this.reachesVia(pathSoFar, visitedStatesSoFar).safeFerry(cargo) and
      // The resulting state has not yet been visited.
      not exists(int i | i = visitedStatesSoFar.indexOf(result)) and
      visitedStates = visitedStatesSoFar + "/" + result and
      path = pathSoFar + "\n Ferry " + cargo
    )
  }

Display the results

Once you’ve defined all the necessary classes and predicates, write a select clause that returns the resulting path.

Show/hide code
from string path
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
select path

The don’t-care expression (_), as the second argument to the reachesVia predicate, represents any value of visitedStates.

For now, the path defined in reachesVia just lists the order of cargo items to ferry. You could tweak the predicate and the select clause to make the solution clearer. Here are some suggestions:

  • Display more information, such as the direction in which the cargo is ferried, for example "Goat to the left shore".
  • Fully describe the state at every step, for example "Goat: Left, Man: Left, Cabbage: Right, Wolf: Right".
  • Display the path in a more “visual” way, for example by using arrows to display the transitions between states.

Alternative solutions

Here are some more example queries that solve the river crossing puzzle:

  1. This query uses a modified path variable to describe the resulting path in more detail.

    See solution in the query console

  2. This query models the man and the cargo items in a different way, using an abstract class and predicate. It also displays the resulting path in a more visual way.

    See solution in the query console

  3. This query introduces algebraic datatypes to model the situation, instead of defining everything as a subclass of string.

    See solution in the query console