CodeQL documentation
CodeQL resources

Cross the river

Use common QL features to write a query that finds a solution to the “River crossing” logic puzzle.

Introduction

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(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:

Show/hide example query - modified path
/**
 * A solution to the river crossing puzzle using a modified `path` variable
 * to describe the resulting path in detail.
 */

/** A possible cargo item. */
class Cargo extends string {
  Cargo() { this = ["Nothing", "Goat", "Cabbage", "Wolf"] }
}

/** A shore, named either `Left` or `Right`. */
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) }

  /** 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())
  }

  /**
   * 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() }

  string towards() {
    manShore = "Left" and result = "to the left"
    or
    manShore = "Right" and result = "to the right"
  }

  /**
   * 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) {
    // Reachable in 1 step by ferrying a specific cargo
    exists(Cargo cargo |
      result = this.safeFerry(cargo) and
      visitedStates = result and
      path = "First " + cargo + " is ferried " + result.towards()
    )
    or
    // Reachable by first following pathSoFar and then ferrying cargo
    exists(string pathSoFar, string visitedStatesSoFar, Cargo cargo |
      result = this.reachesVia(pathSoFar, visitedStatesSoFar).safeFerry(cargo) and
      not exists(visitedStatesSoFar.indexOf(result)) and // resulting state is not visited yet
      visitedStates = visitedStatesSoFar + "_" + result and
      path = pathSoFar + ",\nthen " + cargo + " is ferried " + result.towards()
    )
  }
}

/** 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") }
}

from string path
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
select path + "."
Show/hide example query - abstract class
/**
 * A solution to the river crossing puzzle using abstract
 * classes/predicates to model the situation and unicode
 * symbols to display the answer.
 */

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

/** Models the behavior of the man. */
class Man extends string {
  Shore s;

  Man() { this = "man " + s }

  /** Holds if the man is on a particular shore. */
  predicate isOn(Shore shore) { s = shore }

  /** Returns the other shore, after the man crosses the river. */
  Man cross() { result != this }

  /** Returns a cargo and its position after being ferried. */
  Cargo ferry(Cargo c) {
    result = c.cross() and
    c.isOn(s)
  }
}

/** One of three possible cargo items, with their position. */
abstract class Cargo extends string {
  Shore s;

  bindingset[this]
  Cargo() { any() }

  /** Holds if the cargo is on a particular shore. */
  predicate isOn(Shore shore) { s = shore }

  /** Returns the other shore, after the cargo crosses the river. */
  abstract Cargo cross();
}

/** Models the position of the goat. */
class Goat extends Cargo {
  Goat() { this = "goat " + s }

  override Goat cross() { result != this }
}

/** Models the position of the wolf. */
class Wolf extends Cargo {
  Wolf() { this = "wolf " + s }

  override Wolf cross() { result != this }
}

/** Models the position of the cabbage. */
class Cabbage extends Cargo {
  Cabbage() { this = "cabbage " + s }

  override Cabbage cross() { result != this }
}

/** Returns a unicode representation of everything on the left shore. */
string onLeft(Man man, Goat goat, Cabbage cabbage, Wolf wolf) {
  exists(string manOnLeft, string goatOnLeft, string cabbageOnLeft, string wolfOnLeft |
    (
      man.isOn("left") and manOnLeft = "🕴"
      or
      man.isOn("right") and manOnLeft = "____"
    ) and
    (
      goat.isOn("left") and goatOnLeft = "🐐"
      or
      goat.isOn("right") and goatOnLeft = "___"
    ) and
    (
      cabbage.isOn("left") and cabbageOnLeft = "🥬"
      or
      cabbage.isOn("right") and cabbageOnLeft = "___"
    ) and
    (
      wolf.isOn("left") and wolfOnLeft = "🐺"
      or
      wolf.isOn("right") and wolfOnLeft = "___"
    ) and
    result = manOnLeft + "__" + goatOnLeft + "__" + cabbageOnLeft + "__" + wolfOnLeft
  )
}

/** Returns a unicode representation of everything on the right shore. */
string onRight(Man man, Goat goat, Cabbage cabbage, Wolf wolf) {
  exists(string manOnLeft, string goatOnLeft, string cabbageOnLeft, string wolfOnLeft |
    (
      man.isOn("right") and manOnLeft = "🕴"
      or
      man.isOn("left") and manOnLeft = "_"
    ) and
    (
      goat.isOn("right") and goatOnLeft = "🐐"
      or
      goat.isOn("left") and goatOnLeft = "__"
    ) and
    (
      cabbage.isOn("right") and cabbageOnLeft = "🥬"
      or
      cabbage.isOn("left") and cabbageOnLeft = "__"
    ) and
    (
      wolf.isOn("right") and wolfOnLeft = "🐺"
      or
      wolf.isOn("left") and wolfOnLeft = "__"
    ) and
    result = manOnLeft + "__" + goatOnLeft + "__" + cabbageOnLeft + "__" + wolfOnLeft
  )
}

/** Renders the state as a string, using unicode symbols. */
string render(Man man, Goat goat, Cabbage cabbage, Wolf wolf) {
  result =
    onLeft(man, goat, cabbage, wolf) + "___🌊🌊🌊🌊🌊🌊🌊🌊🌊🌊___" +
      onRight(man, goat, cabbage, wolf)
}

/** A record of where everything is. */
class State extends string {
  Man man;
  Goat goat;
  Cabbage cabbage;
  Wolf wolf;

  State() { this = render(man, goat, cabbage, wolf) }

  /**
   * Returns the possible states that you can transition to
   * by ferrying one or zero cargo items.
   */
  State transition() {
    result = render(man.cross(), man.ferry(goat), cabbage, wolf) or
    result = render(man.cross(), goat, man.ferry(cabbage), wolf) or
    result = render(man.cross(), goat, cabbage, man.ferry(wolf)) or
    result = render(man.cross(), goat, cabbage, wolf)
  }

  /**
   * Returns all states that are reachable via a transition
   * and have not yet been visited.
   * `path` keeps track of how it is achieved.
   */
  State reachesVia(string path) {
    exists(string pathSoFar |
      result = this.reachesVia(pathSoFar).transition() and
      not exists(pathSoFar.indexOf(result.toString())) and
      path = pathSoFar + "\n↓\n" + result
    )
  }
}

/** The initial state, where everything is on the left shore. */
class InitialState extends State {
  InitialState() {
    exists(Shore left | left = "left" |
      man.isOn(left) and goat.isOn(left) and cabbage.isOn(left) and wolf.isOn(left)
    )
  }

  override State reachesVia(string path) {
    path = this + "\n↓\n" + result and result = this.transition()
    or
    result = super.reachesVia(path)
  }
}

/** The goal state, where everything is on the right shore. */
class GoalState extends State {
  GoalState() {
    exists(Shore right | right = "right" |
      man.isOn(right) and goat.isOn(right) and cabbage.isOn(right) and wolf.isOn(right)
    )
  }

  override State transition() { none() }
}

/** An unsafe state, where something gets eaten. */
class IllegalState extends State {
  IllegalState() {
    exists(Shore s |
      goat.isOn(s) and cabbage.isOn(s) and not man.isOn(s)
      or
      wolf.isOn(s) and goat.isOn(s) and not man.isOn(s)
    )
  }

  override State transition() { none() }
}

from string path
where any(InitialState i).reachesVia(path) = any(GoalState g)
select path
Show/hide example query - datatypes
/**
 * "Typesafe" solution to the river crossing puzzle.
 */

/** Either the left shore or the right shore. */
newtype TShore =
  Left() or
  Right()

class Shore extends TShore {
  Shore other() { result != this }

  string toString() {
    this = Left() and result = "left"
    or
    this = Right() and result = "right"
  }
}

newtype TMan = TManOn(Shore s)

/** Models the behavior of the man. */
class Man extends TMan {
  Shore s;

  Man() { this = TManOn(s) }

  /** Holds if the man is on a particular shore. */
  predicate isOn(Shore shore) { s = shore }

  /** Returns the other shore, after the man crosses the river. */
  Man cross() { result.isOn(s.other()) }

  /** Returns a cargo and its position after being ferried. */
  Cargo ferry(Cargo c) {
    result = c.cross() and
    c.isOn(s)
  }

  string toString() { result = "man " + s }
}

newtype TCargo =
  TGoat(Shore s) or
  TCabbage(Shore s) or
  TWolf(Shore s)

/** One of three possible cargo items, with their position. */
abstract class Cargo extends TCargo {
  Shore s;

  /** Holds if the cargo is on a particular shore. */
  predicate isOn(Shore shore) { s = shore }

  /** Returns the other shore, after the cargo crosses the river. */
  abstract Cargo cross();

  abstract string toString();
}

/** Models the position of the goat. */
class Goat extends Cargo, TGoat {
  Goat() { this = TGoat(s) }

  override Cargo cross() { result = TGoat(s.other()) }

  override string toString() { result = "goat " + s }
}

/** Models the position of the wolf. */
class Wolf extends Cargo, TWolf {
  Wolf() { this = TWolf(s) }

  override Cargo cross() { result = TWolf(s.other()) }

  override string toString() { result = "wolf " + s }
}

/** Models the position of the cabbage. */
class Cabbage extends Cargo, TCabbage {
  Cabbage() { this = TCabbage(s) }

  override Cargo cross() { result = TCabbage(s.other()) }

  override string toString() { result = "cabbage " + s }
}

newtype TState = Currently(Man man, Goat goat, Cabbage cabbage, Wolf wolf)

/** A record of where everything is. */
class State extends TState {
  Man man;
  Goat goat;
  Cabbage cabbage;
  Wolf wolf;

  State() { this = Currently(man, goat, cabbage, wolf) }

  /**
   * Returns the possible states that you can transition to
   * by ferrying one or zero cargo items.
   */
  State transition() {
    result = Currently(man.cross(), man.ferry(goat), cabbage, wolf) or
    result = Currently(man.cross(), goat, man.ferry(cabbage), wolf) or
    result = Currently(man.cross(), goat, cabbage, man.ferry(wolf)) or
    result = Currently(man.cross(), goat, cabbage, wolf)
  }

  /**
   * Returns all states that are reachable via a transition
   * and have not yet been visited.
   * `path` keeps track of how it is achieved.
   */
  State reachesVia(string path) {
    exists(string pathSoFar |
      result = this.reachesVia(pathSoFar).transition() and
      not exists(pathSoFar.indexOf(result.toString())) and
      path = pathSoFar + "\n" + result
    )
  }

  string toString() { result = man + "/" + goat + "/" + cabbage + "/" + wolf }
}

/** The initial state, where everything is on the left shore. */
class InitialState extends State {
  InitialState() {
    man.isOn(Left()) and goat.isOn(Left()) and cabbage.isOn(Left()) and wolf.isOn(Left())
  }

  override State reachesVia(string path) {
    path = this + "\n" + result and result = this.transition()
    or
    result = super.reachesVia(path)
  }

  override string toString() { result = "Initial: " + super.toString() }
}

/** The goal state, where everything is on the right shore. */
class GoalState extends State {
  GoalState() {
    man.isOn(Right()) and goat.isOn(Right()) and cabbage.isOn(Right()) and wolf.isOn(Right())
  }

  override State transition() { none() }

  override string toString() { result = "Goal: " + super.toString() }
}

/** An unsafe state, where something gets eaten. */
class IllegalState extends State {
  IllegalState() {
    exists(Shore s |
      goat.isOn(s) and cabbage.isOn(s) and not man.isOn(s)
      or
      wolf.isOn(s) and goat.isOn(s) and not man.isOn(s)
    )
  }

  override State transition() { none() }

  override string toString() { result = "ILLEGAL: " + super.toString() }
}

from string path
where any(InitialState i).reachesVia(path) = any(GoalState g)
select path

Further reading

  • © GitHub, Inc.
  • Terms
  • Privacy