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:

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:

                ferryman : boolean;
		goat     : boolean;
		cabbage  : boolean;
		wolf     : boolean;
                init(ferryman) := 1;
                init(goat)     := 1;
                init(cabbage)  := 1;
                init(wolf)     := 1;

		next(ferryman) := !ferryman;

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

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

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


Copyright 2000 Michael Huth (