var Loup_droite : bool
var Chevre_droite : bool
var Pomme_droite : bool
var Bateau_droite : bool
var V : bool (* feu vert pour le bateau *)

init() { Loup_droite=False && Chevre_droite=False && Pomme_droite=False && Bateau_droite=False }

unsafe() { Loup_droite=True && Chevre_droite=True && Pomme_droite=True && Bateau_droite=True }



transition le_loup_traverse ()
requires { Loup_droite=Bateau_droite && V=True }
{
Loup_droite := case
		| Loup_droite=True : False
		| _ : True;
(* le bateau traverse avec le loup *)
Bateau_droite := case
		| Bateau_droite=True : False
		| _ : True;
V := False;
}

transition la_chevre_traverse ()
requires { Chevre_droite=Bateau_droite && V=True }
{
Chevre_droite := case
		| Chevre_droite=True : False
		| _ : True;
(* le bateau traverse avec la chevre *)
Bateau_droite := case
		| Bateau_droite=True : False
		| _ : True;
V := False;
}

transition la_pomme_traverse ()
requires { Pomme_droite=Bateau_droite && V=True }
{
Pomme_droite := case
		| Pomme_droite=True : False
		| _ : True;
(* le bateau traverse avec la pomme *)
Bateau_droite := case
		| Bateau_droite=True : False
		| _ : True;
V := False;
}

transition le_bateau_traverse ()
requires { V = True }
{
Bateau_droite := case
		| Bateau_droite=True : False
		| _ : True;
V := False;
}


transition no_problemo ()
requires { V=False  
        && (Loup_droite=Chevre_droite => Bateau_droite=Chevre_droite)
	&& (Pomme_droite=Chevre_droite => Bateau_droite=Chevre_droite) }
{ V := True }