mirror of
https://github.com/github/codeql.git
synced 2026-04-30 11:15:13 +02:00
Outdent river answer files
This commit is contained in:
Chris Smowton
@@ -5,108 +5,108 @@
|
||||
|
||||
/** A possible cargo item. */
|
||||
class Cargo extends string {
|
||||
Cargo() {
|
||||
this = ["Nothing", "Goat", "Cabbage", "Wolf"]
|
||||
}
|
||||
Cargo() {
|
||||
this = ["Nothing", "Goat", "Cabbage", "Wolf"]
|
||||
}
|
||||
|
||||
/** A shore, named either `Left` or `Right`. */
|
||||
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"
|
||||
}
|
||||
}
|
||||
|
||||
/** A shore, named either `Left` or `Right`. */
|
||||
class Shore extends string {
|
||||
Shore() {
|
||||
this = "Left" or
|
||||
this = "Right"
|
||||
}
|
||||
|
||||
/** Renders the state as a string. */
|
||||
string renderState(Shore manShore, Shore goatShore, Shore cabbageShore, Shore wolfShore) {
|
||||
result = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore
|
||||
|
||||
/** Returns the other shore. */
|
||||
Shore other() {
|
||||
this = "Left" and result = "Right"
|
||||
or
|
||||
this = "Right" and result = "Left"
|
||||
}
|
||||
|
||||
/** 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(visitedStatesSoFar.indexOf(result)) and // resulting state is not visited yet
|
||||
visitedStates = visitedStatesSoFar + "_" + result and
|
||||
path = pathSoFar + ",\nthen " + cargo + " is ferried " + result.towards()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** 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())
|
||||
}
|
||||
|
||||
/** The initial state, where everything is on the left shore. */
|
||||
class InitialState extends State {
|
||||
InitialState() { this = renderState("Left", "Left", "Left", "Left") }
|
||||
|
||||
/**
|
||||
* 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)
|
||||
}
|
||||
|
||||
/** The goal state, where everything is on the right shore. */
|
||||
class GoalState extends State {
|
||||
GoalState() { this = renderState("Right", "Right", "Right", "Right") }
|
||||
|
||||
/** 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"
|
||||
}
|
||||
|
||||
from string path
|
||||
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
|
||||
select path + "."
|
||||
|
||||
/**
|
||||
* 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(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 + "."
|
||||
|
||||
@@ -6,200 +6,199 @@
|
||||
|
||||
/** One of two shores. */
|
||||
class Shore extends string {
|
||||
Shore() { this = "left" or this = "right" }
|
||||
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)
|
||||
}
|
||||
|
||||
/** 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(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 = this.transition()
|
||||
}
|
||||
|
||||
/** 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
|
||||
result = super.reachesVia(path)
|
||||
}
|
||||
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)
|
||||
}
|
||||
|
||||
/** 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() }
|
||||
|
||||
/**
|
||||
* 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(pathSoFar.indexOf(result.toString())) and
|
||||
path = pathSoFar + "\n↓\n" + result
|
||||
)
|
||||
}
|
||||
|
||||
/** 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() }
|
||||
}
|
||||
|
||||
/** 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)
|
||||
)
|
||||
}
|
||||
|
||||
from string path
|
||||
where any(InitialState i).reachesVia(path) = any(GoalState g)
|
||||
select path
|
||||
|
||||
|
||||
override State reachesVia(string path) {
|
||||
path = this + "\n↓\n" + result and result = this.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
|
||||
|
||||
Reference in New Issue
Block a user