过河¶
使用常见的 QL 功能编写一个查询，找到“过河”逻辑谜题的解决方案。
简介¶
过河谜题
一个人试图用一条船把一只山羊、一颗卷心菜和一只狼运过河。他的船只能载他本人和最多一件货物。他的问题是，如果山羊独自留下，卷心菜会被吃掉。如果狼独自留下，山羊会被吃掉。他怎样才能把所有东西都运过河？
解决方案应是一组关于如何运送物品的说明，例如“首先，把山羊运过河，什么也不带回来。然后，把卷心菜运过去，回来……”
有很多方法可以解决这个问题并在 QL 中实现它。在开始之前，请确保您熟悉如何在 QL 中定义类和谓词。以下演练只是众多可能实现方式之一，因此也尝试编写自己的查询！要查找更多示例查询，请参见下方列表。
演练¶
对谜题的元素进行建模¶
谜题的基本组成部分是货物物品和河两岸。首先，将它们建模为类。
首先，定义一个包含不同货物物品的类Cargo。请注意，这个人也可以独自旅行，因此明确包含"Nothing"作为一件货物很有帮助。
显示/隐藏代码
/** A possible cargo item. */
class Cargo extends string {
Cargo() {
this = "Nothing" or
this = "Goat" or
this = "Cabbage" or
this = "Wolf"
}
}
其次，任何物品都可以在两岸之一。让我们称它们为“左岸”和“右岸”。定义一个包含"Left"和"Right"的类Shore。
表达“另一岸”将有助于对从河的一侧移动到另一侧进行建模。您可以通过在类Shore中定义一个成员谓词other来实现，这样"Left".other()将返回"Right"，反之亦然。
显示/隐藏代码
/** One of two shores. */
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"
}
}
我们还需要一种方法来跟踪人、山羊、卷心菜和狼在任何时候的位置。我们可以将此组合信息称为“状态”。定义一个类State，它对每件货物的所在位置进行编码。例如，如果人位于左岸，山羊位于右岸，卷心菜和狼位于左岸，则状态应为Left, Right, Left, Left。
您可能会发现引入一些变量来引用人及货物物品所在的岸边很有帮助。类主体中的这些临时变量称为字段。
显示/隐藏代码
/** A record of where everything is. */
class State extends string {
Shore manShore;
Shore goatShore;
Shore cabbageShore;
Shore wolfShore;
State() { this = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore }
}
我们对两种特定状态感兴趣，即初始状态和目标状态，我们必须实现这些状态才能解决谜题。假设所有物品都从左岸开始并最终到达右岸，则将InitialState和GoalState定义为State的子类。
显示/隐藏代码
/** The initial state, where everything is on the left shore. */
class InitialState extends State {
InitialState() { this = "Left" + "," + "Left" + "," + "Left" + "," + "Left" }
}
/** The goal state, where everything is on the right shore. */
class GoalState extends State {
GoalState() { this = "Right" + "," + "Right" + "," + "Right" + "," + "Right" }
}
注意
为了避免输入冗长的字符串串联，您可以引入一个辅助谓词
renderState，它以所需格式呈现状态。
使用上述注释，到目前为止的 QL 代码如下
显示/隐藏代码
/** A possible cargo item. */
class Cargo extends string {
Cargo() {
this = "Nothing" or
this = "Goat" or
this = "Cabbage" or
this = "Wolf"
}
}
/** One of two shores. */
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"
}
}
/** 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) }
}
/** 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") }
}
对“摆渡”操作进行建模¶
基本的摆渡行为将人及一件货物运到另一岸，从而产生一个新的状态。
编写一个名为ferry的成员谓词（State），它指定摆渡特定货物后状态会发生什么。（提示：使用谓词other。）
显示/隐藏代码
/** 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())
}
当然，并非所有摆渡行为都是可能的。添加一些额外的条件来描述何时摆渡行为是“安全的”。也就是说，它不会导致山羊或卷心菜被吃掉。例如，执行以下步骤
- 定义一个谓词
isSafe，它在状态本身安全时成立。使用它来对不会被吃掉的情况进行编码。- 定义一个谓词
safeFerry，它将ferry限制为仅包含安全的摆渡行为。
显示/隐藏代码
/**
* 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() }
找到从一个状态到另一个状态的路径¶
此查询的主要目的是找到一条路径，即一系列连续的摆渡行为，以从初始状态到达目标状态。您可以通过换行符（"\n"）来分隔每个项目来编写此“列表”。
在找到解决方案时，您应该注意避免“无限”路径。例如，这个人可以来回运送山羊任何次数，而不会到达不安全状态。这样的路径将有无限次过河，而永远不会解决谜题。
限制路径到有限次过河的一种方法是定义一个成员谓词State reachesVia(string path, int steps)。此谓词的结果是任何可以通过给定路径在指定有限步数内从当前状态（this）到达的状态。
您可以将其编写为一个递归谓词，并使用以下基本情况和递归步骤
- 如果
this是结果状态，那么它（微不足道地）通过零步的空路径到达结果状态。- 任何其他状态都是可达的，如果
this可以通过某些路径（对于path和steps的某些值）到达中间状态，并且从该中间状态到结果状态有一个safeFerry操作。
为了确保谓词是有限的，您应该将steps限制为某个特定值，例如steps <= 7。
显示/隐藏代码
/**
* Returns all states that are reachable via safe ferrying.
* `path` keeps track of how it is achieved and `steps` keeps track of the number of steps it takes.
*/
State reachesVia(string path, int steps) {
// Trivial case: a state is always reachable from itself
steps = 0 and this = result and path = ""
or
// A state is reachable using pathSoFar and then safely ferrying cargo.
exists(int stepsSoFar, string pathSoFar, Cargo cargo |
result = this.reachesVia(pathSoFar, stepsSoFar).safeFerry(cargo) and
steps = stepsSoFar + 1 and
// We expect a solution in 7 steps, but you can choose any value here.
steps <= 7 and
path = pathSoFar + "\n Ferry " + cargo
)
}
但是，虽然这可以确保解决方案是有限的，但如果steps的上限很大，它仍然可能包含循环。换句话说，您可以通过多次访问同一状态来获得效率低下的解决方案。
与其为步数选择任意上限，不如完全避免计算步数。如果您跟踪已经访问过的状态，并确保每个摆渡操作都导致一个新的状态，那么该解决方案肯定不会包含任何循环。
为此，将成员谓词更改为State reachesVia(string path, string visitedStates)。此谓词的结果是任何可以通过给定路径从当前状态（this）到达的状态，而不会重新访问任何先前访问过的状态。
- 与以前一样，如果
this是结果状态，那么它（微不足道地）通过空路径和空访问状态字符串到达结果状态。- 任何其他状态都是可达的，如果
this可以通过某些路径到达中间状态，而不会重新访问任何先前状态，并且从中间状态到结果状态有一个safeFerry操作。（提示：要检查状态是否先前已访问，您可以检查状态的索引visitedStates。）
显示/隐藏代码
/**
* 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) {
// Trivial case: a state is always reachable from itself.
this = result and
visitedStates = this and
path = ""
or
// A state is reachable using pathSoFar and then safely ferrying cargo.
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(visitedStatesSoFar.indexOf(result)) and
visitedStates = visitedStatesSoFar + "/" + result and
path = pathSoFar + "\n Ferry " + cargo
)
}
显示结果¶
定义完所有必要的类和谓词后，编写一个select 子句来返回结果路径。
显示/隐藏代码
from string path
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
select path
不关心表达式（_），作为reachesVia谓词的第二个参数，表示visitedStates的任何值。
现在，在reachesVia中定义的路径仅列出了货物摆渡的顺序。您可以调整谓词和 select 子句，使解决方案更清晰。以下是一些建议
- 显示更多信息，例如货物摆渡的方向，例如
"Goat to the left shore"。- 完整地描述每一步的状态，例如
"Goat: Left, Man: Left, Cabbage: Right, Wolf: Right"。- 以更“视觉化”的方式显示路径，例如使用箭头显示状态之间的转换。
替代解决方案¶
以下是一些解决过河谜题的更多示例查询
显示/隐藏示例查询 - 修改后的路径
/**
* A solution to the river crossing puzzle using a modified `path` variable
* to describe the resulting path in detail.
*/
/** A possible cargo item. */
class Cargo extends string {
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"
}
}
/** 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())
}
/**
* 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()
)
}
}
/** 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 + "."
显示/隐藏示例查询 - 抽象类
/**
* A solution to the river crossing puzzle using abstract
* classes/predicates to model the situation and unicode
* symbols to display the answer.
*/
/** One of two shores. */
class Shore extends string {
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)
}
}
/** 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()
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
显示/隐藏示例查询 - 数据类型
/**
* "Typesafe" solution to the river crossing puzzle.
*/
/** Either the left shore or the right shore. */
newtype TShore =
Left() or
Right()
class Shore extends TShore {
Shore other() { result != this }
string toString() {
this = Left() and result = "left"
or
this = Right() and result = "right"
}
}
newtype TMan = TManOn(Shore s)
/** Models the behavior of the man. */
class Man extends TMan {
Shore s;
Man() { this = TManOn(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.isOn(s.other()) }
/** Returns a cargo and its position after being ferried. */
Cargo ferry(Cargo c) {
result = c.cross() and
c.isOn(s)
}
string toString() { result = "man " + s }
}
newtype TCargo =
TGoat(Shore s) or
TCabbage(Shore s) or
TWolf(Shore s)
/** One of three possible cargo items, with their position. */
abstract class Cargo extends TCargo {
Shore s;
/** 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();
abstract string toString();
}
/** Models the position of the goat. */
class Goat extends Cargo, TGoat {
Goat() { this = TGoat(s) }
override Cargo cross() { result = TGoat(s.other()) }
override string toString() { result = "goat " + s }
}
/** Models the position of the wolf. */
class Wolf extends Cargo, TWolf {
Wolf() { this = TWolf(s) }
override Cargo cross() { result = TWolf(s.other()) }
override string toString() { result = "wolf " + s }
}
/** Models the position of the cabbage. */
class Cabbage extends Cargo, TCabbage {
Cabbage() { this = TCabbage(s) }
override Cargo cross() { result = TCabbage(s.other()) }
override string toString() { result = "cabbage " + s }
}
newtype TState = Currently(Man man, Goat goat, Cabbage cabbage, Wolf wolf)
/** A record of where everything is. */
class State extends TState {
Man man;
Goat goat;
Cabbage cabbage;
Wolf wolf;
State() { this = Currently(man, goat, cabbage, wolf) }
/**
* Returns the possible states that you can transition to
* by ferrying one or zero cargo items.
*/
State transition() {
result = Currently(man.cross(), man.ferry(goat), cabbage, wolf) or
result = Currently(man.cross(), goat, man.ferry(cabbage), wolf) or
result = Currently(man.cross(), goat, cabbage, man.ferry(wolf)) or
result = Currently(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" + result
)
}
string toString() { result = man + "/" + goat + "/" + cabbage + "/" + wolf }
}
/** The initial state, where everything is on the left shore. */
class InitialState extends State {
InitialState() {
man.isOn(Left()) and goat.isOn(Left()) and cabbage.isOn(Left()) and wolf.isOn(Left())
}
override State reachesVia(string path) {
path = this + "\n" + result and result = this.transition()
or
result = super.reachesVia(path)
}
override string toString() { result = "Initial: " + super.toString() }
}
/** The goal state, where everything is on the right shore. */
class GoalState extends State {
GoalState() {
man.isOn(Right()) and goat.isOn(Right()) and cabbage.isOn(Right()) and wolf.isOn(Right())
}
override State transition() { none() }
override string toString() { result = "Goal: " + super.toString() }
}
/** 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() }
override string toString() { result = "ILLEGAL: " + super.toString() }
}
from string path
where any(InitialState i).reachesVia(path) = any(GoalState g)
select path