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))
SPEC
       EF (ferryman & goat & wolf & cabbage)
SPEC
       EF (!ferryman & goat & wolf & cabbage)
SPEC
       EF (ferryman & !goat & wolf & cabbage)
SPEC
       EF (ferryman & goat & !wolf & cabbage)
SPEC
       EF (ferryman & goat & wolf & !cabbage)
SPEC
       EF (!ferryman & !goat & wolf & cabbage)
SPEC
       EF (!ferryman & goat & !wolf & cabbage)
SPEC
       EF (!ferryman & goat & wolf & !cabbage)
SPEC
       EF (ferryman & !goat & !wolf & cabbage)
SPEC
       EF (ferryman & !goat & wolf & !cabbage)
SPEC
       EF (ferryman & goat & !wolf & !cabbage)
SPEC
       EF (!ferryman & !goat & !wolf & cabbage)
SPEC
       EF (!ferryman & goat & !wolf & !cabbage)
SPEC
       EF (!ferryman & goat & !wolf & !cabbage)
SPEC
       EF (ferryman & !goat & !wolf & !cabbage)
SPEC
       EF (!ferryman & !goat & !wolf & !cabbage)