CIS 301. Logical Foundations of Programming, Spring 2000

A puzzle: crossing the Mississippi. A ferry-man has to bring a goat, a cabbage, and a wolf safely from the west bank to the east bank of the Mississippi in New Orleans. The ferry-man can cross the river alone or with exactly one of these three passengers. At any time, either the ferry-man should be on the same bank as the goat, or the goat should be alone on a bank. Otherwise, the goat could go ahead and eat the cabbage or the wolf may eat the goat.

We model this system as an SMV program and then explore the puzzle with specifications written in CTL. It is convenient to model all four agents as boolean variables ("1" means "true" and "0" means "false") since we only care about the agents' being on the east or west bank:

agent = 1    means that the agent is on the west bank
agent = 0    means that the agent is on the east bank

This is an abstraction of the actual system:

We don't care about what else the agents do as they cross the river or stay on a bank.
We don't model the ferry and also ignore the fact that this ferry may sink in the treacherous waters.
We ignore real-time or probabilistic aspects.
We won't model the two potential "meals".

The advantage of this abstraction is that the boolean vector (ferry-man, goat, cabbage, wolf) determines the state of the entire system. Thus, there are 16 possible states. Question: how many of these states are reachable from the initial state?.

Several design decisions need to be made. For example, we could specify all state-transitions in such a way that they never reach a "meal" state. This requires a rather complicated description of the state-transition relation. Alternatively, we could specify all the possible behavior and then enforce in the temporal logic specification that no meals happen.

Here is the SMV code that describes this system:

MODULE main
        VAR
                ferryman : boolean;
		goat     : boolean;
		cabbage  : boolean;
		wolf     : boolean;
        ASSIGN
                init(ferryman) := 1;
                init(goat)     := 1;
                init(cabbage)  := 1;
                init(wolf)     := 1;

		next(ferryman) := !ferryman;

		next(goat) :=
		  case
		         (ferryman = goat) & (next(cabbage) = cabbage) &
			 (next(wolf) = wolf) : { 0, 1};
			 1                   : goat;
		  esac;

		next(cabbage) :=
		  case
		         (ferryman = cabbage) & (next(goat) = goat) &
			 (next(wolf) = wolf) : { 0, 1};
			 1                   : cabbage;
		  esac;

		next(wolf) :=
		  case
		         (ferryman = wolf) & (next(cabbage) = cabbage) &
			 (next(goat) = goat) : { 0, 1};
			 1                   : wolf;
		  esac;
SPEC
       AG ( (ferryman = !goat) -> ((goat = !cabbage) & (goat = !wolf))) ->
       EF ((((!cabbage & !goat) & !wolf) & !ferryman))

Observations:

The system assumes that the ferry-man crosses the river at each move of the system (otherwise, the entire system is idle).
The code for "next(agent)" is symmetric in the agents "goat", "cabbage", and "wolf".

The formula

       AG ( (ferryman = !goat) -> ((goat = !cabbage) & (goat = !wolf))) ->
       EF ((((!cabbage & !goat) & !wolf) & !ferryman))

checks: If the system cannot reach a "meal"-state from the initial state, then the ferry-man can bring all parties safely to the east bank.
This turns out to be true, simply because we can make the premise false: the ferry-man could cross the river alone! Thus we need to improve our specification. Ideally, we want to say:

E ( (G "no meal") and (F "all parties on east bank"))

with codings for

"no meal": (( goat = cabbage) | ( goat = wolf)) -> (goat = ferryman)
"all parties on east bank": !goat & !cabbage & !wolf

Unfortunately, formulas of the type E ((G p) and (F q)) are NOT CTL formulas. So we have to do better than that. But the (G "no meal") part only has to be valid UNTIL all parties are safely on the east bank. Thus we can simple model check our system with the SPEC

       !E[ ((goat = cabbage) | (goat = wolf) -> (goat = ferryman)) U
           ( !cabbage & !goat & !wolf & !ferryman)]

Notice the use of negation: otherwise, the SMV program simply returns "true" and we then know that the puzzle has a solution. However, the use of negation causes SMV to produce a counter example to the SPEC, i.e. an actual solution to the puzzle.

-- specification !E((goat = cabbage | goat = wolf -> goat... is false
-- as demonstrated by the following execution sequence
state 1.1:   // initial state
ferryman = 1
goat = 1
cabbage = 1
wolf = 1

state 1.2:   // ferryman transports goat to east bank
ferryman = 0
goat = 0

state 1.3:   // ferryman returns (alone) to west bank
ferryman = 1

state 1.4:   // ferryman transports cabbage to east bank
ferryman = 0
cabbage = 0

state 1.5:   // ferryman brings goat back to west bank
ferryman = 1
goat = 1

state 1.6:   // ferryman transports wolf to east bank
ferryman = 0
wolf = 0

state 1.7:   // ferryman returns (alone) to west bank
ferryman = 1

state 1.8:   // ferryman transports goat (again) to east bank
ferryman = 0
goat = 0
             // puzzle solved!

resources used:
user time: 0 s, system time: 0.07 s
BDD nodes allocated: 926
Bytes allocated: 1245184
BDD nodes representing transition relation: 25 + 1
nunk%