var Lic_G : int (* licornes sur la rive gauche *)
var Lic_D : int (* ... rive droite *)
var Drag_G : int (* dragons sur la rive gauche *)
var Drag_D : int (* ... rive droite *)

var V : bool (* True = La contrainte sur le nombre de licornes est vérifiée *)

var Dir : bool (* True : le bateau va vers la droite *)

(* Initialement : 
   ------------

  - seulement 3 licornes et 3 dragons sur la rive droite 
  - la règle sur les licornes est vérifiée
  - le bateau va vers la droite
*)

init () { Lic_G = 3 && Drag_G = 3 &&
          Lic_D = 0 && Drag_D = 0 &&
	  Dir = True && V = True }


(* Cubicle cherche à savoir si un état est atteignable.

   Ici, l'état qu'il faut atteindre est constitué de 3 licornes et 3
   dragons sur la rive droite (et rien sur la rive gauche). La règle
   sur les licornes devant être aussi vérifiée (V = True)
*)

unsafe () { Lic_G = 0 && Drag_G = 0 && Lic_D = 3 && Drag_D = 3 && V = True }

(* Les mouvements possibles du bateau *)

(* Pour transporter une licorne vers la droite, il faut qu'il y ait
des licornes sur la rive gauche (Lic_G > 0), que le bateau se dirige à
droite (Dir = True) et que la règle des licornes soit vérifiée (V =
True).

Si toutes ces conditions sont vérifiées, le bateau peut transporter
une licorne de la rive gauche vers la rive droite. On met à jour les
compteurs et on passe le booléen V à False afin que la dernière
transition (voir fin du fichier) vérifie bien que la règle des
licornes est respectée.

*)

transition vers_la_droiteL ()
requires { Lic_G > 0 && Dir = True && V = True }
{
 Lic_G := Lic_G - 1;
 Lic_D := Lic_D + 1;
 Dir := False;
 V := False;
}

(* les autres règles se déduisent facilement... *)

transition vers_la_gaucheL ()
requires { Lic_D > 0 && Dir = False && V = True }
{
 Lic_D := Lic_D - 1;
 Lic_G := Lic_G + 1;
 Dir := True;
  V := False;
}

transition vers_la_droiteD ()
requires { Drag_G > 0 && Dir = True && V = True }
{
 Drag_G := Drag_G - 1;
 Drag_D := Drag_D + 1;
 Dir := False;
 V := False;
}

transition vers_la_gaucheD ()
requires { Drag_D > 0 && Dir = False && V = True }
{
 Drag_D := Drag_D - 1;
 Drag_G := Drag_G + 1;
 Dir := True;
 V := False; 
}

transition vers_la_droiteLL ()
requires { Lic_G > 1 && Dir = True && V = True }
{
 Lic_G := Lic_G - 2;
 Lic_D := Lic_D + 2;
 Dir := False;
 V := False;
}

transition vers_la_gaucheLL ()
requires { Lic_D > 1 && Dir = False && V = True }
{
 Lic_G := Lic_G + 2;
 Lic_D := Lic_D - 2;
 Dir := True;
 V := False; 
}

transition vers_la_droiteDD ()
requires { Drag_G > 1 && Dir = True && V = True }
{
 Drag_G := Drag_G - 2;
 Drag_D := Drag_D + 2;
 Dir := False;
 V := False; 
}

transition vers_la_gaucheDD ()
requires { Drag_D > 1 && Dir = False && V = True }
{
 Drag_G := Drag_G + 2;
 Drag_D := Drag_D - 2;
 Dir := True;
 V := False; 
}


transition vers_la_droiteLD ()
requires { Lic_G > 0 && Drag_G > 0 && Dir = True && V = True }
{
 Lic_G := Lic_G - 1;
 Lic_D := Lic_D + 1;
 Drag_G := Drag_G - 1;
 Drag_D := Drag_D + 1; 
 Dir := False;
 V := False; 
}

transition vers_la_gaucheLD ()
requires { Lic_D > 0 && Drag_D > 0 && Dir = False && V = True }
{
 Lic_G := Lic_G + 1;
 Lic_D := Lic_D - 1;
 Drag_G := Drag_G + 1;
 Drag_D := Drag_D - 1; 
 Dir := True;
 V := False; 
}

(* La règle des licornes. 

 Pour repasser le booléen V à vrai, on vérifie la règle des licornes.

 Notez que tant que le booléen V est à False, aucune autre transition
 ne peut être exécutée.

*)

transition regle_des_licornes()
requires { V = False && (Lic_G > 0 => Lic_G >= Drag_G)
                     && (Lic_D > 0 => Lic_D >= Drag_D) }
{ V := True }