MODULE main
        VAR
                ferryman : boolean;
		goat     : boolean;
		cabbage  : boolean;
		wolf     : boolean;
		carry    : {g, c, w, 0};
        ASSIGN
                init(ferryman) := 0;
                init(goat)     := 0;
                init(cabbage)  := 0;
                init(wolf)     := 0;
                init(carry)    := 0;

		next(ferryman) := !ferryman;

		next(carry) :=

		  case
		         (ferryman = cabbage): c;
			 1                   : 0;
		  esac union

		  case
		         (ferryman = goat) : g;
			 1                 : 0;
		  esac union


		  case
		         (ferryman = wolf)   : w;
			 1                   : 0;
		  esac union 0;

		next(goat) :=
		  case
		         (ferryman = goat) & (next(carry) = g) 
                                             : next(ferryman);
			 1                   : goat;
		  esac;

		next(cabbage) :=
		  case
		         (ferryman = cabbage) & (next(carry) = c)
                                             : next(ferryman);
			 1                   : cabbage;
		  esac;

		next(wolf) :=
		  case
		         (ferryman = wolf) & (next(carry) = w)
					     : next(ferryman);
			 1                   : wolf;
		  esac;


	
 LTLSPEC
     !((((goat=cabbage | goat = wolf) -> goat = ferryman)
       U (cabbage & goat & wolf & ferryman)))


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