```{

Three cannibals and three missionaries want to cross a river in a canoe which
only holds two people. Someone has to bring the boat back. The trouble is, if
there are ever more cannibals than missionaries the cannibals will eat the
missionaries. How can the six get safely across?

The following code solves the problem by calling the query
"all Cannibals()"

There are infinitely many solutions, as it is possible to have one guy paddling
across and back as many times as we want, but we are only interested in solutions
that do not contain repeating sequences. For this purpose we keep two history lists,
one for each river bank. If a trip would result in the same distribution of
missionaries and cannibals as we already encountered previously (i.e. is in the history list),
trip is discarted. Otherwise the trip is added to the list of trips and also the
history list is updated to reflect the new trip. And, of coures, we make sure
cannibals never outnumber missionaries.

}

People = cannibals:I[0..3], missionaries:I[0..3]
Direction = A | B
Trips = direction:Direction,cannibals:I[0..3], missionaries:I[0..3]

History = list People
Trip = list Trips

pred Cannibals() iff
// Specify the initial conditions:
left  :. People & left  := (3,3) & // all 6 people on the left bank
right :. People & right := (0,0) & // nobody on the right bank
hl :.History & hl := left,Nil &    // initial history of the left bank state
hr :.History & hr := right,Nil &   // initial history of the right bank state
trip :. Trip & trip := Nil &
NextTrip(left,hl,right,hr,trip) & PrintOneSolution(trip)

local pred NextTrip(left:.People,hl:.History,right:.People,hr :.History,trip :.Trip) iff
Accross(left,right,hl,trip) &
if right <> (3,3) then
Back(left,right,hr,trip) & NextTrip(left,hl,right,hr,trip)
end

// Going accross: moving people from the left river bnk to right river bank.

local pred Accross(left:.People, right:.People, history:.History,trip :.Trip) iff
OneTrip(cannibals, missionaries) &
left.cannibals     := left.cannibals - cannibals &
right.cannibals    := right.cannibals + cannibals &
left.missionaries  := left.missionaries - missionaries &
right.missionaries := right.missionaries + missionaries &
SafeMissionaries(left,right) &
~left in history & history := left,history &
trip := (A,cannibals,missionaries),trip

// Going back: moving people from the right to the left river bank

local pred Back(left:.People, right:.People, history :. History,trip :.Trip) iff
OneTrip(cannibals, missionaries) &
left.cannibals     := left.cannibals + cannibals &
right.cannibals    := right.cannibals - cannibals &
left.missionaries  := left.missionaries + missionaries &
right.missionaries := right.missionaries - missionaries &
SafeMissionaries(left,right) &
~right in history & history := right,history &
trip := (B,cannibals,missionaries),trip

// We don't differentiate between trips, after all, the canoe can transport up to
// two people regardless of the direction...
// So we just generate all possible occupancies.

local pred OneTrip(cannibals :>I, missionaries :> I) iff
(
(cannibals = 1 & missionaries = 0)  |
(cannibals = 0 & missionaries = 1)  |
(cannibals = 2 & missionaries = 0)  |
(cannibals = 1 & missionaries = 1)  |
(cannibals = 0 & missionaries = 2)
)

// Helper routine to make sure cannibals don't outnumber any missionaries present

local proc SafeMissionaries(left:<People,right:<People)  iff
if left.missionaries > 0 then
left.cannibals <= left.missionaries
end &
if right.missionaries > 0 then
right.cannibals <= right.missionaries
end

// ----------------------------------------------------------------------------
// The following is just code to display the resulting list of the trips
// in a format that is more user friendly
// ----------------------------------------------------------------------------

local proc PrintOneSolution(trip :< Trip) iff
Print('\n\n        Left  Right  Trip          Left  Right') &
left :.  People & left  := (3,3) &
right :. People & right := (0,0) &
// Our list of trips is in order tripLast...,trip7,trip6,...trip1,Nil
// We want to print the solution in order trip1,trip2,....,tripLast
revtrip :. Trip & revtrip := Nil  & ListReverse(trip,revtrip) &
// Traverse the reversed list and print states before and after each trip
PrintOneSolution1(revtrip,left,right)

local proc PrintOneSolution1(trip :< Trip,left:.People,right:.People) iff
if trip = h,t then
Print ('\nStart: ') & PrintPeople(left) & PrintPeople(right) &
crew:.People & crew:= (h.cannibals,h.missionaries) &
if h.direction = A then
PrintPeople(crew) & Print(' -> ') &
left.missionaries  := left.missionaries - h.missionaries &
left.cannibals     := left.cannibals - h.cannibals &
right.missionaries := right.missionaries + h.missionaries &
right.cannibals    := right.cannibals + h.cannibals
else Print(' <- ') & PrintPeople(crew) &
left.missionaries  := left.missionaries + h.missionaries &
left.cannibals     := left.cannibals + h.cannibals &
right.missionaries := right.missionaries - h.missionaries &
right.cannibals    := right.cannibals - h.cannibals
end & Print(' End:') & PrintPeople(left) & PrintPeople(right) & PrintOneSolution1(t,left,right)
else
Print('\n\n')
end

// Formatted printout of People. Don't print zeros

local proc PrintPeople(p:<People) iff
Print(' ') &
if p.cannibals = 0 then Print('  ')
else Print(p.cannibals,'c')
end &
if p.missionaries = 0 then Print('   ')
else Print(p.missionaries,'m ')
end

// Code to create a reversed list
local proc ListReverse(inlist:< Trip, outlist:.Trip) iff
if inlist = h,t then outlist := h,outlist & ListReverse(t,outlist) end

```