QL etudes: Address comments + fix sphinx warning

docs/language/learn-ql/index.rst

@@ -23,6 +23,7 @@ If you are new to QL, start by looking at the following topics:
    introduction-to-ql
    about-ql
    beginner/ql-tutorials
+   ql-etudes/river-crossing
 
 QL training and variant analysis examples
 ******************************************

docs/language/learn-ql/ql-etudes/river-crossing-1.ql

@@ -1,7 +1,8 @@
 /**
  * @name River crossing puzzle (version 1)
  * @description An "elementary" version of the solution to
- * the river crossing problem.
+ * the river crossing problem. It introduces more explicit and intuitive
+ * definitions, before tidying them up in the "full" version.
  *
  * Note: Parts of this QL file are included in the corresponding .rst file.
  * Make sure to update the line numbers if you change anything here!
@@ -21,8 +22,8 @@ class Cargo extends string {
 class Shore extends string {
   Shore() { this = "Left" or this = "Right" }
 
-  /** Returns "the other shore". */
-  Shore flip() {
+  /** Returns the other shore. */
+  Shore other() {
     this = "Left" and result = "Right"
     or
     this = "Right" and result = "Left"
@@ -42,20 +43,20 @@ class State extends string {
   State() { this = man + "," + goat + "," + cabbage + "," + wolf }
 
   State ferry(Cargo cargo) {
-    cargo = "Nothing" and result = man.flip() + "," + goat + "," + cabbage + "," + wolf
+    cargo = "Nothing" and result = man.other() + "," + goat + "," + cabbage + "," + wolf
     or
-    cargo = "Goat" and result = man.flip() + "," + goat.flip() + "," + cabbage + "," + wolf
+    cargo = "Goat" and result = man.other() + "," + goat.other() + "," + cabbage + "," + wolf
     or
-    cargo = "Cabbage" and result = man.flip() + "," + goat + "," + cabbage.flip() + "," + wolf
+    cargo = "Cabbage" and result = man.other() + "," + goat + "," + cabbage.other() + "," + wolf
     or
-    cargo = "Wolf" and result = man.flip() + "," + goat + "," + cabbage + "," + wolf.flip()
+    cargo = "Wolf" and result = man.other() + "," + goat + "," + cabbage + "," + wolf.other()
   }
 
   /**
    * Holds if predator and prey are on the same shore and the man
-   * is on the other shore.
+   * is not present.
    */
-  predicate eats(Shore predator, Shore prey) { predator = prey and man = predator.flip() }
+  predicate eats(Shore predator, Shore prey) { predator = prey and man = predator.other() }
 
   /** Holds if nothing gets eaten in this state. */
   predicate isSafe() { not (eats(goat, cabbage) or eats(wolf, goat)) }
@@ -93,6 +94,6 @@ class GoalState extends State {
 }
 
 from string path
-where any(InitialState is).reachesVia(path, _) = any(GoalState gs)
+where any(InitialState i).reachesVia(path, _) = any(GoalState g)
 select path
 

docs/language/learn-ql/ql-etudes/river-crossing.ql

@@ -29,8 +29,8 @@ class Shore extends string {
     this = "Right"
   }
 
-  /** Returns "the other shore". */
-  Shore flip() {
+  /** Returns the other shore. */
+  Shore other() {
     this = "Left" and result = "Right"
     or
     this = "Right" and result = "Left"
@@ -56,20 +56,20 @@ class State extends string {
 
   /** Returns the state that is reached after ferrying a particular cargo item. */
   State ferry(Cargo cargo) {
-    cargo = "Nothing" and result = renderState(man.flip(), goat, cabbage, wolf)
+    cargo = "Nothing" and result = renderState(man.other(), goat, cabbage, wolf)
     or
-    cargo = "Goat" and result = renderState(man.flip(), goat.flip(), cabbage, wolf)
+    cargo = "Goat" and result = renderState(man.other(), goat.other(), cabbage, wolf)
     or
-    cargo = "Cabbage" and result = renderState(man.flip(), goat, cabbage.flip(), wolf)
+    cargo = "Cabbage" and result = renderState(man.other(), goat, cabbage.other(), wolf)
     or
-    cargo = "Wolf" and result = renderState(man.flip(), goat, cabbage, wolf.flip())
+    cargo = "Wolf" and result = renderState(man.other(), goat, cabbage, wolf.other())
   }
 
   /**
    * Holds if predator and prey are on the same shore and the man
-   * is on the other shore.
+   * is not present.
    */
-  predicate eats(Shore predator, Shore prey) { predator = prey and man = predator.flip() }
+  predicate eats(Shore predator, Shore prey) { predator = prey and man = predator.other() }
 
   /** Holds if nothing gets eaten in this state. */
   predicate isSafe() { not (eats(goat, cabbage) or eats(wolf, goat)) }
@@ -110,5 +110,5 @@ class GoalState extends State {
 }
 
 from string path
-where any(InitialState is).reachesVia(path, _) = any(GoalState gs)
+where any(InitialState i).reachesVia(path, _) = any(GoalState g)
 select path

docs/language/learn-ql/ql-etudes/river-crossing.rst

@@ -48,7 +48,7 @@ Second, any item can be on one of two shores. Let's call these the "left shore"
 Define a class ``Shore`` containing ``"Left"`` and ``"Right"``.
 
 It would be helpful to express "the other shore". You can do this by defining a member predicate
-``flip`` in the class ``Shore`` such that ``"Left".flip()`` returns ``"Right"`` and vice versa.
+``other`` in the class ``Shore`` such that ``"Left".other()`` returns ``"Right"`` and vice versa.
 
 .. container:: toggle
 
@@ -74,7 +74,7 @@ temporary variables in the body of a class are called `fields <https://help.semm
       *Show/hide code*
 
    .. literalinclude:: river-crossing-1.ql
-      :lines: 32-42,83
+      :lines: 33-43,84
 
 We are interested in two particular states, namely the initial state and the goal state.
 Assuming that all items start on the left shore and end up on the right shore, define
@@ -87,7 +87,7 @@ Assuming that all items start on the left shore and end up on the right shore, d
       *Show/hide code*
 
    .. literalinclude:: river-crossing-1.ql
-      :lines: 85-93
+      :lines: 86-94
 
 .. pull-quote::
 
@@ -114,7 +114,7 @@ The basic act of ferrying moves the man and a 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 ``flip``.)
+after ferrying a particular cargo. (Hint: Use the predicate ``other``.)
 
 .. container:: toggle
 
@@ -129,7 +129,8 @@ Of course, not all ferrying actions are possible. Add some extra conditions to d
 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:
 
-   #. Define a predicate ``eats`` that encodes the conditions for when something gets eaten.
+   #. Define a predicate ``eats`` that encodes the conditions for when a "predator" is able to eat an
+      unguarded "prey".
    #. Define a predicate ``isSafe`` that holds when nothing gets eaten.
    #. Define a predicate ``safeFerry`` that restricts ``ferry`` to only include safe ferrying actions.
 
@@ -175,7 +176,7 @@ for example ``steps <= 7``.
       *Show/hide code*
 
    .. literalinclude:: river-crossing-1.ql
-      :lines: 66-82
+      :lines: 67-83
 
 However, although this ensures that the solution is finite, it can still contain loops if the upper bound
 for ``steps`` is large.