Skip to content

Commit f4f4de3

Browse files
smowtonsmowton
committed
Outdent river answer files
1 parent f373b7f commit f4f4de3

File tree

2 files changed

+285
-286
lines changed

2 files changed

+285
-286
lines changed

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

Lines changed: 99 additions & 99 deletions
Original file line numberDiff line numberDiff line change
@@ -5,108 +5,108 @@
55

66
/** A possible cargo item. */
77
class Cargo extends string {
8-
Cargo() {
9-
this = ["Nothing", "Goat", "Cabbage", "Wolf"]
10-
}
8+
Cargo() {
9+
this = ["Nothing", "Goat", "Cabbage", "Wolf"]
1110
}
12-
13-
/** A shore, named either `Left` or `Right`. */
14-
class Shore extends string {
15-
Shore() {
16-
this = "Left" or
17-
this = "Right"
18-
}
19-
20-
/** Returns the other shore. */
21-
Shore other() {
22-
this = "Left" and result = "Right"
23-
or
24-
this = "Right" and result = "Left"
25-
}
11+
}
12+
13+
/** A shore, named either `Left` or `Right`. */
14+
class Shore extends string {
15+
Shore() {
16+
this = "Left" or
17+
this = "Right"
18+
}
19+
20+
/** Returns the other shore. */
21+
Shore other() {
22+
this = "Left" and result = "Right"
23+
or
24+
this = "Right" and result = "Left"
2625
}
27-
28-
/** Renders the state as a string. */
29-
string renderState(Shore manShore, Shore goatShore, Shore cabbageShore, Shore wolfShore) {
30-
result = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore
26+
}
27+
28+
/** Renders the state as a string. */
29+
string renderState(Shore manShore, Shore goatShore, Shore cabbageShore, Shore wolfShore) {
30+
result = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore
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 = renderState(manShore, goatShore, cabbageShore, wolfShore) }
41+
42+
/** Returns the state that is reached after ferrying a particular cargo item. */
43+
State ferry(Cargo cargo) {
44+
cargo = "Nothing" and
45+
result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore)
46+
or
47+
cargo = "Goat" and
48+
result = renderState(manShore.other(), goatShore.other(), cabbageShore, wolfShore)
49+
or
50+
cargo = "Cabbage" and
51+
result = renderState(manShore.other(), goatShore, cabbageShore.other(), wolfShore)
52+
or
53+
cargo = "Wolf" and
54+
result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore.other())
3155
}
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 = renderState(manShore, goatShore, cabbageShore, wolfShore) }
41-
42-
/** Returns the state that is reached after ferrying a particular cargo item. */
43-
State ferry(Cargo cargo) {
44-
cargo = "Nothing" and
45-
result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore)
46-
or
47-
cargo = "Goat" and
48-
result = renderState(manShore.other(), goatShore.other(), cabbageShore, wolfShore)
49-
or
50-
cargo = "Cabbage" and
51-
result = renderState(manShore.other(), goatShore, cabbageShore.other(), wolfShore)
52-
or
53-
cargo = "Wolf" and
54-
result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore.other())
55-
}
56-
57-
/**
58-
* Holds if the state is safe. This occurs when neither the goat nor the cabbage
59-
* can get eaten.
60-
*/
61-
predicate isSafe() {
62-
// The goat can't eat the cabbage.
63-
(goatShore != cabbageShore or goatShore = manShore) and
64-
// The wolf can't eat the goat.
65-
(wolfShore != goatShore or wolfShore = manShore)
66-
}
67-
68-
/** Returns the state that is reached after safely ferrying a cargo item. */
69-
State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }
70-
71-
string towards() {
72-
manShore = "Left" and result = "to the left"
73-
or
74-
manShore = "Right" and result = "to the right"
75-
}
76-
77-
/**
78-
* Returns all states that are reachable via safe ferrying.
79-
* `path` keeps track of how it is achieved.
80-
* `visitedStates` keeps track of previously visited states and is used to avoid loops.
81-
*/
82-
State reachesVia(string path, string visitedStates) {
83-
// Reachable in 1 step by ferrying a specific cargo
84-
exists(Cargo cargo |
85-
result = this.safeFerry(cargo) and
86-
visitedStates = result and
87-
path = "First " + cargo + " is ferried " + result.towards()
88-
)
89-
or
90-
// Reachable by first following pathSoFar and then ferrying cargo
91-
exists(string pathSoFar, string visitedStatesSoFar, Cargo cargo |
92-
result = this.reachesVia(pathSoFar, visitedStatesSoFar).safeFerry(cargo) and
93-
not exists(visitedStatesSoFar.indexOf(result)) and // resulting state is not visited yet
94-
visitedStates = visitedStatesSoFar + "_" + result and
95-
path = pathSoFar + ",\nthen " + cargo + " is ferried " + result.towards()
96-
)
97-
}
56+
57+
/**
58+
* Holds if the state is safe. This occurs when neither the goat nor the cabbage
59+
* can get eaten.
60+
*/
61+
predicate isSafe() {
62+
// The goat can't eat the cabbage.
63+
(goatShore != cabbageShore or goatShore = manShore) and
64+
// The wolf can't eat the goat.
65+
(wolfShore != goatShore or wolfShore = manShore)
9866
}
99-
100-
/** The initial state, where everything is on the left shore. */
101-
class InitialState extends State {
102-
InitialState() { this = renderState("Left", "Left", "Left", "Left") }
67+
68+
/** Returns the state that is reached after safely ferrying a cargo item. */
69+
State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }
70+
71+
string towards() {
72+
manShore = "Left" and result = "to the left"
73+
or
74+
manShore = "Right" and result = "to the right"
10375
}
104-
105-
/** The goal state, where everything is on the right shore. */
106-
class GoalState extends State {
107-
GoalState() { this = renderState("Right", "Right", "Right", "Right") }
76+
77+
/**
78+
* Returns all states that are reachable via safe ferrying.
79+
* `path` keeps track of how it is achieved.
80+
* `visitedStates` keeps track of previously visited states and is used to avoid loops.
81+
*/
82+
State reachesVia(string path, string visitedStates) {
83+
// Reachable in 1 step by ferrying a specific cargo
84+
exists(Cargo cargo |
85+
result = this.safeFerry(cargo) and
86+
visitedStates = result and
87+
path = "First " + cargo + " is ferried " + result.towards()
88+
)
89+
or
90+
// Reachable by first following pathSoFar and then ferrying cargo
91+
exists(string pathSoFar, string visitedStatesSoFar, Cargo cargo |
92+
result = this.reachesVia(pathSoFar, visitedStatesSoFar).safeFerry(cargo) and
93+
not exists(visitedStatesSoFar.indexOf(result)) and // resulting state is not visited yet
94+
visitedStates = visitedStatesSoFar + "_" + result and
95+
path = pathSoFar + ",\nthen " + cargo + " is ferried " + result.towards()
96+
)
10897
}
109-
110-
from string path
111-
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
112-
select path + "."
98+
}
99+
100+
/** The initial state, where everything is on the left shore. */
101+
class InitialState extends State {
102+
InitialState() { this = renderState("Left", "Left", "Left", "Left") }
103+
}
104+
105+
/** The goal state, where everything is on the right shore. */
106+
class GoalState extends State {
107+
GoalState() { this = renderState("Right", "Right", "Right", "Right") }
108+
}
109+
110+
from string path
111+
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
112+
select path + "."

0 commit comments

Comments
 (0)