track file for coloring

test/coloring/coloring_oracle.lus

+
+-- Here, we use the  Lustre version of the algorithm as an oracle for the ocaml version
+ 
+include "../../lib/utils.lus"
+
+node coloring_oracle(
+  legitimate : bool;
+  ocaml_cost : real;
+  ocaml_enabled : bool^actions_number^card;
+  active : bool^actions_number^card; 
+  ocaml_config : state^card;
+  round:bool;
+  round_nb:int;                   
+)  
+returns (ok : bool);
+var
+  lustre_config : state^card;
+  lustre_enabled : bool^actions_number^card;
+  lustre_round : bool;
+  lustre_round_nb : int;
+--  lustre_cost:int;
+let
+  lustre_config, lustre_enabled, lustre_round, lustre_round_nb = 
+    topology(active -> pre active, -- ignored at the first step
+             ocaml_config -- used at the first step only
+             );
+--  lustre_cost = cost(lustre_enabled, lustre_config);
+  ok =     lustre_enabled = ocaml_enabled 
+           -- compare the sasa dot interpretation and the salut dot to lustre compilation
+       and lustre_config = ocaml_config
+          -- compare the lustre and the ocaml version of the processes
+--       and Lustre::real2int(ocaml_cost) = lustre_cost
+--       and lustre_round = round
+--       and lustre_round_nb = round_nb
+;
+         -- compare the cost functions 
+tel

test/coloring/config.ml

+../../../test/coloring/config.ml
\ No newline at end of file

test/coloring/simu.lus

-include "../../lib/sas.lus"
-include "ER.lus"
-
-node incr(ain : int) returns (aout, z : int);
-let
-    z = ain; aout = ain + 1;
-tel;
-
-node simu(x:bool) returns (s : bool);
-var
-  initials : state^card;
-  Enab_p : bool^actions_number^card;
-  p : bool^actions_number^card;
-  _d:int;
-
-  p_c : state^card;
-
-let
-  _d, initials= fill<<incr; card>>(0);
-
-  p = false^actions_number^card -> pre Enab_p;
-  p_c, Enab_p = ER(p, initials -> 0^card);
-
-  s = silent<<actions_number,card>>(Enab_p);
-tel

test/coloring/state.lus

+-- automatically generated by salut 
+
+type state = int;
+
+type action = enum { recolor };
+const actions_number = 1;
+
+function action_of_int(i : int) returns (a : action);
+let
+	a = recolor;
+tel;
+
+function legitimate<<const actions_number:int; const card:int>>(enables : bool^actions_number^card; config: state^card)
+returns (res : bool);
+let
+  res=silent<<actions_number,card>>(enables);
+tel;
\ No newline at end of file

test/coloring/verify.lus

@@ -15,7 +15,7 @@ let
 
 	config, enables,r,rn = topology(activations, inits);
 
-	legitimate = legitimate<<actions_number,card>>(enables,config);;
+	legitimate = legitimate<<actions_number,card>>(enables,config);
 	closure = true -> (pre(legitimate) => legitimate);
 	moves = move_count<<actions_number,card>>(activations);