MODULE main
VAR
	ferryman : boolean;
	goat : boolean;
	cabbage : boolean;
	wolf : boolean;
	carry : { g,c,w,nothing } ;
ASSIGN
	init(ferryman) := FALSE; init(goat) := FALSE;
	init(cabbage) := FALSE; init(wolf) := FALSE;
	init(carry) := nothing;
	next(ferryman) := {FALSE,TRUE};
	next(carry) :=
		case
			ferryman=goat : g;
			TRUE : nothing;
		esac
		union
		case
			ferryman=cabbage : c;
			TRUE : nothing;
		esac
		union
		case
			ferryman=wolf : w;
			TRUE : nothing;
		esac
		union
		nothing;
	next(goat) := case
		ferryman=goat & next(carry)=g : next(ferryman);
		TRUE : goat;
	esac;
	next(cabbage) := case
		ferryman=cabbage & next(carry)=c : next(ferryman);
		TRUE : cabbage;
	esac;
	next(wolf) := case
		ferryman=wolf & next(carry)=w : next(ferryman);
		TRUE : wolf;
	esac;
	LTLSPEC !(( (goat=cabbage | goat=wolf) -> goat=ferryman)
			U (cabbage & goat & wolf & ferryman))