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;
}