Learning QL: Add river crossing puzzle [SD-3133] #1985

shati-patel · 2019-09-20T13:36:30Z

This is an initial attempt at turning one of the "QL etudes" into a tutorial.
The fun of the puzzle should come from writing your own solution, so I've tried to explain a model solution, but also suggest that people experiment more freely... It still needs work, but it would be helpful to get some feedback first :)

@RasmusSemmle @jf205 @felicitymay - you may have suggestions? Here is a preview.

In particular: Does this kind of format work? Is the query itself easy to follow? Should the walkthrough provide more/less guidance? Does it follow a logical structure?

WIP

RasmusSemmle

I put one comment where I think the guidance could throw people down a difficult path.
I do think the structure is logical, albeit different from how I think about it. Personally, I see it as a search through a state space, leading to two challenges: Model the state and implement the search. However, the bottom-up thinking described here probably works much better for a tutorial.

RasmusSemmle · 2019-09-20T14:10:17Z

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

+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.


It might even work, and read nicer, to call the predicate "other".

RasmusSemmle · 2019-09-20T14:14:56Z

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

+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.


This formulation does not make me think of a predicate with two arguments for predator and prey. Maybe something along the lines of "...for when a predator would be able to eat an unguarded prey" would provide a stronger hint. (Even though predator and prey also seem slightly wrong for the goat-cabbage situation.)

RasmusSemmle · 2019-09-20T14:20:12Z

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

+}
+
+from string path
+where any(InitialState is).reachesVia(path, _) = any(GoalState gs)


A nice feature of high-level code is that it often reads like prose. Perhaps change the variable is to s to avoid it reading like bad grammar.

felicitymay

I haven't tried this puzzle but have just reviewed the text. A couple of minor points, but that's all from me.

It seems like a sensible approach from my point of view.

felicitymay · 2019-09-20T14:32:46Z

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

+      *Show/hide code*
+
+   .. literalinclude:: river-crossing.ql
+      :lines: 15-22


This is cool. I don't think that I'd realized that we could include just a section of a file. 👍

I think this should be :lines: 15-23

felicitymay · 2019-09-20T14:39:19Z

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

+
+  /**
+   * Holds if predator and prey are on the same shore and the man
+   * is on the other shore.


I'd suggest changing this to "and the man is not present" - since this is also true if the man is in the ferry and not on either shore.

The way it is being modelled here, the ferrying steps are instantaneous and states are computed "before" and "after" ferrying. Therefor the man is never in the ferry when looking at the states. However, mentally, I can see that you are considering the state that the man is leaving behind, and the wolf probably has no intention of waiting for the man to reach the other side before eating the goat...

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

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

rdmarsh2 · 2019-09-23T15:24:53Z

Should the .ql files be autoformatted?

jf205

I have a few comments, but overall I think this is really good.

The structure guides the reader through in a logical fashion and, as Rasmus says, this approach is probably best for a beginner tutorial.

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

jf205 · 2019-09-24T11:32:23Z

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

+}
+
+/** A record of where everything is. */
+class State extends string {


I would prefer each variable declared here to be more obviously linked to a location. Using the cargo name by itself is a tiny bit confusing to me. Would manLocation, goatLocation etc be clearer? Perhaps that would make later parts of the query look more complicated than is necessary though.... 🤷‍♂

Good point. I've changed them all to manShore, goatShore etc, which makes things clearer in most places. The only problem was the eats(predicateShore, preyShore) predicate, which looked a bit funny. I've changed it to eating, which possibly helps?

I guess you want some synonym of eatingSituation, but I can only think of silly ones... (eatery, snackTime, etc..)

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

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

shati-patel · 2019-09-24T16:36:15Z

Thanks @jf205 - I've incorporated your suggestions locally (along with some other edits).
Annoyingly, we need to manually update the included line numbers every time the query changes, but I don't think there's a way around that...

shati-patel · 2019-09-25T12:02:31Z

I've finally tidied up the example queries in the last section and removed the TODO.

@RasmusSemmle - could you check that the linked queries look okay? I've included one using newtypes because I thought it was a helpful example (and some of the standard libraries use them anyway). But I'm happy to hide it again if we don't want to "advertise" them beyond the note in the handbook.

@AlexTereshenkov - perhaps you'd like to have a look too? (This is also an example of including code snippets in .rst files as we talked about re: cookbook yesterday.)

PREVIEW

RasmusSemmle · 2019-09-25T12:31:36Z

You might want to harmonise the denotations across the linked solution. For instance, the first link writes "ferry X to the far shore" and "ferry Y back" rather than "to the right" and "to the left".

I the third link, I would define Man cross() { result.isOn(s.flip()) } (rather than Man cross() { not result.isOn(s) }).

You might also want to rename flip to other.

I think it is fine to show the newtype, it is documented after all.

robertbrignull

@shati-patel asked me to have a quick look as another pair of eyes and also being roughly the target audience for this tutorial. I spotted a couple of tiny typos when including the code snippets, and also a couple of comments on the QL that you are free to take or ignore.

robertbrignull · 2019-09-30T10:13:07Z

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

+  State reachesVia(string path, string visitedStates) {
+    // Trivial case: a state is always reachable from itself.
+    this = result and
+    visitedStates = "" and


For the base case should it be visitedStates = this? Otherwise I think it would consider the path A => B => A to be valid and wouldn't detect the loop.

robertbrignull · 2019-09-30T10:13:45Z

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

+    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


I think this could be written as not exists(visitedStatesSoFar.indexOf(result)) and omit the variable declaration, though I'll leave it up to you to decide if that's a improvement.

robertbrignull · 2019-09-30T10:20:14Z

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

+}
+
+from string path
+where any(InitialState i).reachesVia(path, _) = any(GoalState g)


I think it would be equivalent to write this as

any(InitialState i).reachesVia(path, _) instanceof GoalState

Again up to you if you think it's an improvement or not.

robertbrignull · 2019-09-30T10:21:16Z

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

+      *Show/hide code*
+
+   .. literalinclude:: river-crossing.ql
+      :lines: 14-55,105-115


I think this should be :lines: 14-55,106-116

robertbrignull · 2019-09-30T10:21:44Z

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

+      *Show/hide code*
+
+   .. literalinclude:: river-crossing.ql
+      :lines: 15-22


I think this should be :lines: 15-23

shati-patel · 2019-10-01T10:30:57Z

Thank you for having a look! I've made some changes (including what you mentioned offline about the eating predicate being more confusing than helpful, and the explanation of using newlines to create a "list").
Due to a change in auto-formatting, I've had to update some more line numbers (hopefully correctly this time). It's a pain to have to update these manually, but I don't know of a better solution yet.

Let me know what you think. It should hopefully be in a mergeable state now 🤞

jf205 · 2019-10-02T09:54:59Z

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

+Once you've defined all the necessary classes and predicates, write a `select clause <https://help.semmle.com/QL/ql-handbook/queries.html#select-clauses>`__
+that returns the resulting path.
+
+.. container:: toggle


I think it would be good to add a sentence explaining the use of _ in the select clause (including a link to
https://help.semmle.com/QL/ql-handbook/expressions.html#don-t-care-expressions).

jf205 · 2019-10-02T10:01:33Z

Thanks for all of the updates @shati-patel! I have made one comment that would be good to address before we merge this.

Do you think that there should be a link to this topic at the end of the detective tutorials? (Perhaps in the 'What next?' section here https://help.semmle.com/QL/learn-ql/beginner/heir.html
and somewhere on this page https://help.semmle.com/QL/learn-ql/beginner/ql-tutorials.html)

shati-patel · 2019-10-02T11:32:09Z

Thanks @jf205 - I've added a link from the final detective tutorial. It doesn't really fit on https://help.semmle.com/QL/learn-ql/beginner/ql-tutorials.html, but there's already a link from the global Learning QL page, so hopefully it's sufficiently visible!
Once we have more puzzles we could perhaps add more prominent links.

jf205

Thanks @shati-patel!

QL etudes: Add river crossing puzzle

56bc8cb

WIP

shati-patel added the documentation label Sep 20, 2019

shati-patel requested a review from jf205 as a code owner September 20, 2019 13:36

RasmusSemmle reviewed Sep 20, 2019

View reviewed changes

felicitymay reviewed Sep 20, 2019

View reviewed changes

QL etudes: Address comments + fix sphinx warning

f94b01c

RasmusSemmle reviewed Sep 23, 2019

View reviewed changes

docs/language/learn-ql/ql-etudes/river-crossing.ql Outdated Show resolved Hide resolved

QL etudes: Update predicate

f88f796

Autoformat QL

c156d6a

jf205 reviewed Sep 24, 2019

View reviewed changes

Apply suggestions from code review

3441696

QL etudes: Tidy up alternative solns

0b0f69f

QL etudes: Update linked queries

886b258

robertbrignull reviewed Sep 30, 2019

View reviewed changes

QL etudes: Update with Robert's suggestions

427325b

jf205 reviewed Oct 2, 2019

View reviewed changes

QL etudes: Add further explanation + link

3dd2a6c

jf205 approved these changes Oct 2, 2019

View reviewed changes

semmle-qlci merged commit a019c45 into github:master Oct 3, 2019

shati-patel deleted the ql-etudes branch October 3, 2019 09:20

Learning QL: Add river crossing puzzle [SD-3133] #1985

Learning QL: Add river crossing puzzle [SD-3133] #1985

Uh oh!

Conversation

shati-patel commented Sep 20, 2019

Uh oh!

RasmusSemmle left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

felicitymay left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

rdmarsh2 commented Sep 23, 2019

Uh oh!

jf205 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

shati-patel commented Sep 24, 2019

Uh oh!

shati-patel commented Sep 25, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

RasmusSemmle commented Sep 25, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robertbrignull left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

shati-patel commented Oct 1, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jf205 commented Oct 2, 2019

Uh oh!

shati-patel commented Oct 2, 2019

Uh oh!

jf205 left a comment

Choose a reason for hiding this comment

shati-patel commented Sep 25, 2019 •

edited

Loading

RasmusSemmle commented Sep 25, 2019 •

edited

Loading

robertbrignull left a comment •

edited

Loading