First draft update tutorials

docs/codeql/writing-codeql-queries/catch-the-fire-starter.rst

@@ -105,7 +105,7 @@ Now try applying ``isAllowedIn(string region)`` to a person ``p``. If ``p`` is n
 
 You know that the fire starters live in the south *and* that they must have been able to travel to the north. Write a query to find the possible suspects. You could also extend the ``select`` clause to list the age of the suspects. That way you can clearly see that all the children have been excluded from the list.
 
-➤ `See the answer in the query console on LGTM.com <https://lgtm.com/query/2551838470440192723/>`__
+➤ `Check your answer <#exercise-1>`__
 
 You can now continue to gather more clues and find out which of your suspects started the fire...
 
@@ -142,7 +142,7 @@ The predicate ``isBald`` is defined to take a ``Person``, so it can also take a
 
 You can now write a query to select the bald southerners who are allowed into the north.
 
-➤ `See the answer in the query console on LGTM.com <https://lgtm.com/query/2572701606358725253/>`__
+➤ `Check your answer <#exercise-2>`__
 
 You have found the two fire starters! They are arrested and the villagers are once again impressed with your work.
 
@@ -150,3 +150,65 @@ Further reading
 ---------------
 
 .. include:: ../reusables/codeql-ref-tools-further-reading.rst
+
+--------------
+
+Answers
+-------
+
+In these answers, we use ``/*`` and ``*/`` to label the different parts of the query. Any text surrounded by ``/*`` and ``*/`` is not evaluated as part of the QL code, but is treated as a *comment*.
+
+Exercise 1
+~~~~~~~~~~
+
+.. code-block:: ql
+
+   import tutorial
+
+   predicate isSouthern(Person p) { p.getLocation() = "south" }
+
+   class Southerner extends Person {
+   /* the characteristic predicate */
+   Southerner() { isSouthern(this) }
+   }
+
+   class Child extends Person {
+   /* the characteristic predicate */
+   Child() { this.getAge() < 10 }
+
+   /* a member predicate */
+   override predicate isAllowedIn(string region) { region = this.getLocation() }
+   }
+
+   from Southerner s
+   where s.isAllowedIn("north")
+   select s, s.getAge()
+
+Exercise 2
+~~~~~~~~~~
+
+.. code-block:: ql
+
+   import tutorial
+
+   predicate isSouthern(Person p) { p.getLocation() = "south" }
+
+   class Southerner extends Person {
+   /* the characteristic predicate */
+   Southerner() { isSouthern(this) }
+   }
+
+   class Child extends Person {
+   /* the characteristic predicate */
+   Child() { this.getAge() < 10 }
+
+   /* a member predicate */
+   override predicate isAllowedIn(string region) { region = this.getLocation() }
+   }
+
+   predicate isBald(Person p) { not exists(string c | p.getHairColor() = c) }
+
+   from Southerner s
+   where s.isAllowedIn("north") and isBald(s)
+   select s
+

docs/codeql/writing-codeql-queries/cross-the-river.rst

@@ -260,21 +260,34 @@ Alternative solutions
 
 Here are some more example queries that solve the river crossing puzzle:
 
-  #. This query uses a modified ``path`` variable to describe the resulting path in
-     more detail.
+.. container:: toggle
 
-     ➤ `See solution in the query console on LGTM.com <https://lgtm.com/query/659603593702729237/>`__
+   .. container:: name
 
-  #. This query models the man and the cargo items in a different way, using an 
-     :ref:`abstract <abstract>`
-     class and predicate. It also displays the resulting path in a more visual way.
+      *Show/hide eaxmple query - modified path*
 
-     ➤ `See solution in the query console on LGTM.com <https://lgtm.com/query/1025323464423811143/>`__
+   .. literalinclude:: river-answer-1-path.ql
+      :language: ql
 
-  #. This query introduces :ref:`algebraic datatypes <algebraic-datatypes>`
-     to model the situation, instead of defining everything as a subclass of ``string``.
 
-     ➤ `See solution in the query console on LGTM.com <https://lgtm.com/query/7260748307619718263/>`__
+.. container:: toggle
+
+   .. container:: name
+
+      *Show/hide eaxmple query - abstract class*
+
+   .. literalinclude:: river-answer-2-abstract-class.ql
+      :language: ql
+
+
+.. container:: toggle
+
+   .. container:: name
+
+      *Show/hide eaxmple query - datatypes*
+
+   .. literalinclude:: river-answer-3-datatypes.ql
+      :language: ql
 
 Further reading
 ---------------

docs/codeql/writing-codeql-queries/crown-the-rightful-heir.rst

@@ -129,7 +129,7 @@ Here is one way to define ``relativeOf()``:
 
 Don't forget to use the predicate ``isDeceased()`` to find relatives that are still alive.
 
-➤ `See the answer in the query console on LGTM.com <https://lgtm.com/query/6710025057257064639/>`__
+➤ `Check your answer <#exercise-1>`__
 
 Select the true heir
 --------------------
@@ -142,7 +142,7 @@ To decide who should inherit the king's fortune, the villagers carefully read th
 
 As your final challenge, define a predicate ``hasCriminalRecord`` so that ``hasCriminalRecord(p)`` holds if ``p`` is any of the criminals you unmasked earlier (in the ":doc:`Find the thief <find-the-thief>`" and ":doc:`Catch the fire starter <catch-the-fire-starter>`" tutorials).
 
-➤ `See the answer in the query console on LGTM.com <https://lgtm.com/query/1820692755164273290/>`__
+➤ `Check your answer <#exercise-2>`__
 
 Experimental explorations
 -------------------------
@@ -164,3 +164,47 @@ Further reading
 ---------------
 
 .. include:: ../reusables/codeql-ref-tools-further-reading.rst
+
+--------------
+
+Answers
+-------
+
+In these answers, we use ``/*`` and ``*/`` to label the different parts of the query. Any text surrounded by ``/*`` and ``*/`` is not evaluated as part of the QL code, but is treated as a *comment*.
+
+Exercise 1
+~~~~~~~~~~
+
+.. code-block:: ql
+
+   import tutorial
+
+   Person relativeOf(Person p) { parentOf*(result) = parentOf*(p) }
+
+   from Person p
+   where
+   not p.isDeceased() and
+   p = relativeOf("King Basil")
+   select p
+
+Exercise 2
+~~~~~~~~~~
+
+.. code-block:: ql
+
+   import tutorial
+
+   Person relativeOf(Person p) { parentOf*(result) = parentOf*(p) }
+
+   predicate hasCriminalRecord(Person p) {
+   p = "Hester" or
+   p = "Hugh" or
+   p = "Charlie"
+   }
+
+   from Person p
+   where
+   not p.isDeceased() and
+   p = relativeOf("King Basil") and
+   not hasCriminalRecord(p)
+   select p

docs/codeql/writing-codeql-queries/find-the-thief.rst

@@ -50,9 +50,7 @@ You start asking some creative questions and making notes of the answers so you
 
 There is too much information to search through by hand, so you decide to use your newly acquired QL skills to help you with your investigation...
 
-#. Open the `query console on LGTM.com <https://lgtm.com/query>`__ to get started.
-#. Select a language and a demo project. For this tutorial, any language and project will do.
-#. Delete the default code ``import <language> select "hello world"``.
+.. include:: ../reusables/setup-to-run-tutorials.rst
 
 QL libraries
 ------------
@@ -209,13 +207,7 @@ Hints
 
 Once you have finished, you will have a list of possible suspects. One of those people must be the thief!
 
-➤ `See the answer in the query console on LGTM.com <https://lgtm.com/query/1505743955992/>`__
-
-.. pull-quote::
-
-   Note
-
-   In the answer, we used ``/*`` and ``*/`` to label the different parts of the query. Any text surrounded by ``/*`` and ``*/`` is not evaluated as part of the QL code, but is just a *comment*.
+➤ `Check your answer <#exercise-1>`__
 
 You are getting closer to solving the mystery! Unfortunately, you still have quite a long list of suspects... To find out which of your suspects is the thief, you must gather more information and refine your query in the next step.
 
@@ -291,9 +283,59 @@ You can now translate the remaining questions into QL:
 
 Have you found the thief?
 
-➤ `See the answer in the query console on LGTM.com <https://lgtm.com/query/1505744186085/>`__
+➤ `Check your answer <#exercise-2>`__
 
 Further reading
 ---------------
 
 .. include:: ../reusables/codeql-ref-tools-further-reading.rst
+
+
+--------------
+
+Answers
+-------
+
+In these answers, we use ``/*`` and ``*/`` to label the different parts of the query. Any text surrounded by ``/*`` and ``*/`` is not evaluated as part of the QL code, but is treated as a *comment*.
+
+Exercise 1
+^^^^^^^^^^
+
+.. code-block:: ql
+
+   import tutorial
+
+   from Person t
+   where
+   /* 1 */ t.getHeight() > 150 and
+   /* 2 */ not t.getHairColor() = "blond" and
+   /* 3 */ exists (string c | t.getHairColor() = c) and
+   /* 4 */ not t.getAge() < 30 and
+   /* 5 */ t.getLocation() = "east" and
+   /* 6 */ (t.getHairColor() = "black" or t.getHairColor() = "brown") and
+   /* 7 */ not (t.getHeight() > 180 and t.getHeight() < 190) and
+   /* 8 */ exists(Person p | p.getAge() > t.getAge())
+   select t
+
+Exercise 2
+^^^^^^^^^^
+
+.. code-block:: ql
+
+   import tutorial
+
+   from Person t
+   where
+   /* 1 */ t.getHeight() > 150 and
+   /* 2 */ not t.getHairColor() = "blond" and
+   /* 3 */ exists (string c | t.getHairColor() = c) and
+   /* 4 */ not t.getAge() < 30 and
+   /* 5 */ t.getLocation() = "east" and
+   /* 6 */ (t.getHairColor() = "black" or t.getHairColor() = "brown") and
+   /* 7 */ not (t.getHeight() > 180 and t.getHeight() < 190) and
+   /* 8 */ exists(Person p | p.getAge() > t.getAge()) and
+   /* 9 */ not t = max(Person p | | p order by p.getHeight()) and
+   /* 10 */ t.getHeight() < avg(float i | exists(Person p | p.getHeight() = i) | i) and
+   /* 11 */ t = max(Person p | p.getLocation() = "east" | p order by p.getAge())
+   select "The thief is " + t + "!"
+   

docs/codeql/writing-codeql-queries/river-answer-1-path.ql

@@ -0,0 +1,115 @@
+/**
+ * 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" 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) }
+  
+    /** 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(int i | i = 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 + "."

docs/codeql/writing-codeql-queries/river-answer-2-abstract-class.ql

@@ -0,0 +1,205 @@
+/**
+ * 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(int i | i = 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 = 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
+  

docs/codeql/writing-codeql-queries/river-answer-3-datatypes.ql

@@ -0,0 +1,172 @@
+/**
+ * "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(int i | i = 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 = 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