Skip to content

Commit a019c45

Browse files
semmle-qlcisemmle-qlci
authored
Merge pull request github#1985 from shati-patel/ql-etudes
Approved by jf205
2 parents a8a7de9 + 3dd2a6c commit a019c45

File tree

5 files changed

+484
-0
lines changed

5 files changed

+484
-0
lines changed

‎docs/language/learn-ql/beginner/heir.rst

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -160,4 +160,5 @@ What next?
160160
----------
161161

162162
- Learn more about recursion in the `QL language handbook <https://help.semmle.com/QL/ql-handbook/index.html>`__.
163+
- Put your QL skills to the test and solve the :doc:`River crossing puzzle <../ql-etudes/river-crossing>`.
163164
- Start using QL to analyze projects. See :doc:`Learning QL <../../index>` for a summary of the available languages and resources.

‎docs/language/learn-ql/index.rst

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ If you are new to QL, start by looking at the following topics:
2323
introduction-to-ql
2424
about-ql
2525
beginner/ql-tutorials
26+
ql-etudes/river-crossing
2627

2728
QL training and variant analysis examples
2829
******************************************

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

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
/**
2+
* @name River crossing puzzle (version 1)
3+
* @description An "elementary" version of the solution to
4+
* the river crossing problem. It introduces more explicit and intuitive
5+
* definitions, before tidying them up in the "full" version.
6+
*
7+
* Note: Parts of this QL file are included in the corresponding .rst file.
8+
* Make sure to update the line numbers if you change anything here!
9+
*/
10+
11+
/** A possible cargo item. */
12+
class Cargo extends string {
13+
Cargo() {
14+
this = "Nothing" or
15+
this = "Goat" or
16+
this = "Cabbage" or
17+
this = "Wolf"
18+
}
19+
}
20+
21+
/** One of two shores. */
22+
class Shore extends string {
23+
Shore() { this = "Left" or this = "Right" }
24+
25+
/** Returns the other shore. */
26+
Shore other() {
27+
this = "Left" and result = "Right"
28+
or
29+
this = "Right" and result = "Left"
30+
}
31+
}
32+
33+
/** A record of where everything is. */
34+
class State extends string {
35+
Shore manShore;
36+
Shore goatShore;
37+
Shore cabbageShore;
38+
Shore wolfShore;
39+
40+
State() { this = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore }
41+
42+
State ferry(Cargo cargo) {
43+
cargo = "Nothing" and
44+
result = manShore.other() + "," + goatShore + "," + cabbageShore + "," + wolfShore
45+
or
46+
cargo = "Goat" and
47+
result = manShore.other() + "," + goatShore.other() + "," + cabbageShore + "," + wolfShore
48+
or
49+
cargo = "Cabbage" and
50+
result = manShore.other() + "," + goatShore + "," + cabbageShore.other() + "," + wolfShore
51+
or
52+
cargo = "Wolf" and
53+
result = manShore.other() + "," + goatShore + "," + cabbageShore + "," + wolfShore.other()
54+
}
55+
56+
/**
57+
* Holds if the state is safe. This occurs when neither the goat nor the cabbage
58+
* can get eaten.
59+
*/
60+
predicate isSafe() {
61+
// The goat can't eat the cabbage.
62+
(goatShore != cabbageShore or goatShore = manShore) and
63+
// The wolf can't eat the goat.
64+
(wolfShore != goatShore or wolfShore = manShore)
65+
}
66+
67+
/** Returns the state that is reached after safely ferrying a cargo item. */
68+
State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }
69+
70+
/**
71+
* Returns all states that are reachable via safe ferrying.
72+
* `path` keeps track of how it is achieved and `steps` keeps track of the number of steps it takes.
73+
*/
74+
State reachesVia(string path, int steps) {
75+
// Trivial case: a state is always reachable from itself
76+
steps = 0 and this = result and path = ""
77+
or
78+
// A state is reachable using pathSoFar and then safely ferrying cargo.
79+
exists(int stepsSoFar, string pathSoFar, Cargo cargo |
80+
result = this.reachesVia(pathSoFar, stepsSoFar).safeFerry(cargo) and
81+
steps = stepsSoFar + 1 and
82+
// We expect a solution in 7 steps, but you can choose any value here.
83+
steps <= 7 and
84+
path = pathSoFar + "\n Ferry " + cargo
85+
)
86+
}
87+
}
88+
89+
/** The initial state, where everything is on the left shore. */
90+
class InitialState extends State {
91+
InitialState() { this = "Left" + "," + "Left" + "," + "Left" + "," + "Left" }
92+
}
93+
94+
/** The goal state, where everything is on the right shore. */
95+
class GoalState extends State {
96+
GoalState() { this = "Right" + "," + "Right" + "," + "Right" + "," + "Right" }
97+
}
98+
99+
from string path
100+
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
101+
select path
102+

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

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
/**
2+
* @name River crossing puzzle
3+
* @description This implements the classical puzzle where a man is trying to
4+
* ferry a goat, a cabbage, and a wolf across a river.
5+
* His boat can only take himself and at most one item as cargo.
6+
* His problem is that if the goat is left alone with the cabbage,
7+
* it will eat it.
8+
* And if the wolf is left alone with the goat, it will eat it.
9+
* How does he get everything across the river?
10+
*
11+
* Note: Parts of this QL file are included in the corresponding .rst file.
12+
* Make sure to update the line numbers if you change anything here!
13+
*/
14+
15+
/** A possible cargo item. */
16+
class Cargo extends string {
17+
Cargo() {
18+
this = "Nothing" or
19+
this = "Goat" or
20+
this = "Cabbage" or
21+
this = "Wolf"
22+
}
23+
}
24+
25+
/** One of two shores. */
26+
class Shore extends string {
27+
Shore() {
28+
this = "Left" or
29+
this = "Right"
30+
}
31+
32+
/** Returns the other shore. */
33+
Shore other() {
34+
this = "Left" and result = "Right"
35+
or
36+
this = "Right" and result = "Left"
37+
}
38+
}
39+
40+
/** Renders the state as a string. */
41+
string renderState(Shore manShore, Shore goatShore, Shore cabbageShore, Shore wolfShore) {
42+
result = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore
43+
}
44+
45+
/** A record of where everything is. */
46+
class State extends string {
47+
Shore manShore;
48+
Shore goatShore;
49+
Shore cabbageShore;
50+
Shore wolfShore;
51+
52+
State() { this = renderState(manShore, goatShore, cabbageShore, wolfShore) }
53+
54+
/** Returns the state that is reached after ferrying a particular cargo item. */
55+
State ferry(Cargo cargo) {
56+
cargo = "Nothing" and
57+
result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore)
58+
or
59+
cargo = "Goat" and
60+
result = renderState(manShore.other(), goatShore.other(), cabbageShore, wolfShore)
61+
or
62+
cargo = "Cabbage" and
63+
result = renderState(manShore.other(), goatShore, cabbageShore.other(), wolfShore)
64+
or
65+
cargo = "Wolf" and
66+
result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore.other())
67+
}
68+
69+
/**
70+
* Holds if the state is safe. This occurs when neither the goat nor the cabbage
71+
* can get eaten.
72+
*/
73+
predicate isSafe() {
74+
// The goat can't eat the cabbage.
75+
(goatShore != cabbageShore or goatShore = manShore) and
76+
// The wolf can't eat the goat.
77+
(wolfShore != goatShore or wolfShore = manShore)
78+
}
79+
80+
/** Returns the state that is reached after safely ferrying a cargo item. */
81+
State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }
82+
83+
/**
84+
* Returns all states that are reachable via safe ferrying.
85+
* `path` keeps track of how it is achieved.
86+
* `visitedStates` keeps track of previously visited states and is used to avoid loops.
87+
*/
88+
State reachesVia(string path, string visitedStates) {
89+
// Trivial case: a state is always reachable from itself.
90+
this = result and
91+
visitedStates = this and
92+
path = ""
93+
or
94+
// A state is reachable using pathSoFar and then safely ferrying cargo.
95+
exists(string pathSoFar, string visitedStatesSoFar, Cargo cargo |
96+
result = this.reachesVia(pathSoFar, visitedStatesSoFar).safeFerry(cargo) and
97+
// The resulting state has not yet been visited.
98+
not exists(int i | i = visitedStatesSoFar.indexOf(result)) and
99+
visitedStates = visitedStatesSoFar + "/" + result and
100+
path = pathSoFar + "\n Ferry " + cargo
101+
)
102+
}
103+
}
104+
105+
/** The initial state, where everything is on the left shore. */
106+
class InitialState extends State {
107+
InitialState() { this = renderState("Left", "Left", "Left", "Left") }
108+
}
109+
110+
/** The goal state, where everything is on the right shore. */
111+
class GoalState extends State {
112+
GoalState() { this = renderState("Right", "Right", "Right", "Right") }
113+
}
114+
115+
from string path
116+
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
117+
select path
118+

0 commit comments

Comments
 (0)