River crossing puzzle is quite common. The Association of Automated Reasoning (AAR) President, Larry Wos, presented a simple crossing puzzle in the latest AAR newsletter.
The puzzle is described below:
The puzzle: On one side of a deep river, three foxes and three rabbits
reside.
A forest fire breaks out on this side of the river.
The creatures instinctively would like to cross the river to safety, and
indeed a boat exists that could be used.
But a serious obstacle exists: The boat is so small that it can hold
only two creatures at a time.
Fortunately, all the foxes and all the rabbits know how to use a boat.
Unfortunately, if at any time, on either side of the river, the number
of foxes outnumbers the number of rabbits, the outnumbering foxes will
eat the rabbits.
The challenge: Can a sequence of moves be made so that all six creatures
finally end up safely on the side of the river away from the forest
fire?
CSP solution
Modelling
Escape from the left side of the river to the right bank.
FR - all creatures. LS - the set of creatures on the left side. Initially it's FR and finally empty. RS - the set of creatures on the left side. Initially it's empty and finally FR. move - every time two creatures will be moved from the left side to the right side by the boat. back - every time one of two creatures on move has to return back to the left side, but it still stays on the boat.
Specification
-- Z is dedicated for non-creature on boat
datatype DFR = F1 | F2 | F3 | R1 | R2 | R3 | Z -- F for the set of foxes
F = {F1, F2, F3} -- R for the set of rabbits
R = {R1, R2, R3} -- FR for the set of creatures
FR = union(F, R)
channel move: FR
channel back: FR
channel end -- successfully
-- check if the number of foxes in s outnumbers the number of rabbits
FoxesEatRabbits(s) = (card(inter(R,s)) != 0) and (card(inter(F,s)) > card(inter(R,s)))
CROSS = let -- z - creature on boat -- LS - left bank -- RS - right bank
S(z, LS, RS) =
if (FoxesEatRabbits(LS) or FoxesEatRabbits(RS)) then
STOP
else
if not empty(LS) then
if z == Z then
move?x:LS -> move?y:diff(LS, {x}) -> (
SS(x, diff(LS, {x,y}), union(RS, {y}))
[]
SS(y, diff(LS, {x,y}), union(RS, {x}))
)
else
move?x:LS -> (
SS(x, diff(LS, {x}), union(RS, {z}))
[]
SS(z, diff(LS, {x}), union(RS, {x}))
)
else
end -> SKIP
-- x - creature on boat -- LS - left bank -- RS - right bank
SS(x, LS, RS) =
if (FoxesEatRabbits(LS) or FoxesEatRabbits(RS)) then
STOP
else
if not empty(LS) then
back.x -> S(x, LS, RS)
else
end -> SKIP -- Initially, there's no creatures on boat, all on left bank and non on right bank
within S(Z, FR, {})
MAIN = CROSS
Model Checking
By modelling in CSP, if the situation, that the number of foxes outnumbers the number of rabbits on both sides, occurrs, it behaves like STOP (deadlock). Otherwise, finally it will terminate successfully after engaged in the end event.
Using the CTL checking capability for CSP specification in ProB to check the formula "AG(not e(end))", the statement that the end event always is not enable, to be false. At the same time, a counterexample is provided. This is one of the desired solutions.
