{

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

This page was created by F1toHTML