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 bankThis 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%

- "no meal": (( goat = cabbage) | ( goat = wolf)) -> (goat = ferryman)

Copyright 2000 Michael Huth (huth@cis.ksu.edu)