Add to_state function and modificat oracle.lus in test directory

lib/sasacore/genOracle.ml

@@ -66,8 +66,7 @@ let (f: Topology.t -> 'v Process.t list -> string) =
   let input_enab = ";\n  "^(String.concat "," enabl) ^ ":bool" in
   let input_decl = input_state^input_enab^input_trig^ ";round:bool; round_nb:int" in
   let array_decl =
-    Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n\tConfig:%s^%d;\n"
-      (fst (List.hd vars)) vars_nb
+    Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n\tConfig:state^card;\n"
   in
   let acti_name p a = Printf.sprintf "%s_%s" p.pid (StringOf.action a) in
   let enab_name p a = Printf.sprintf "Enab_%s_%s" p.pid (StringOf.action a) in
@@ -84,7 +83,22 @@ let (f: Topology.t -> 'v Process.t list -> string) =
               "["^(String.concat "," (List.map (enab_name p) p.actions))^"]") pl))
   in
   let array_def_config =
-    Printf.sprintf "\tConfig = [%s];\n" (String.concat "," (List.map fst vars))
+    if vars_nb <> n then
+      let struct_nb_var = vars_nb/n in
+      let rec struct_string vars_list count =
+        match vars_list with
+        | []->""
+        | e::[]->(Printf.sprintf "%s) " e)
+        | e::tail-> (if (count mod struct_nb_var) = 0 then
+                       (Printf.sprintf "to_state(%s, " e ) ^ (struct_string tail (count-1))
+                     else if (count mod struct_nb_var) = 1 then
+                       (Printf.sprintf "%s), " e) ^ (struct_string tail (count-1))
+                     else
+                       (Printf.sprintf "%s, " e) ^ (struct_string tail (count-1))
+                    ) in
+      Printf.sprintf "\tConfig = [%s];\n" (struct_string (List.map fst vars) vars_nb)
+    else
+      Printf.sprintf "\tConfig = [%s];\n" (String.concat "," (List.map fst vars))
   in
   let algo = Filename.basename (Sys.getcwd()) in
   let algo = StringOf.action algo in

test/async-unison/async_unison_oracle.lus

 include "../lustre/oracle_utils.lus"
 
+type state = int;
+
 const k = pn * pn + 1;
 
 -- The absolute value of the difference modulo k is <= 1

test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus

 include "../lustre/oracle_utils.lus"
 
+type state = { par:int; d:int };
+
+function to_state( par:int; d:int)
+returns(res : state);
+let
+  res = state {par=par; d=d};
+tel;
+
+
 node bfs_spanning_tree_oracle<<const an:int; const pn:int>>
-        (legitimate: bool; Enab, Acti: bool^an^pn; config:int^(2*pn);round:bool; round_nb:int)
+        (legitimate: bool; Enab, Acti: bool^an^pn; config:state^pn;round:bool; round_nb:int)
 returns (ok:bool);
 var
   CD_disable:bool;

test/skeleton/some_session

-silence
+n
+n
+n
+n
 wait 3
 print_event !e;;
 

test/st-KK06-algo1/st_KK06_algo1_oracle.lus

 
 include "../lustre/utils.lus"
 
+type state = int;
 node st_KK06_algo1_oracle<<const an:int; const pn:int>>
 (legitimate:bool; Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int) returns (ok:bool);
 var

test/st-KK06-algo2/st_KK06_algo2_oracle.lus

 
 include "../lustre/utils.lus"
 
+type state = int;
+
 const bigN = 2*card;
 
 node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn; Config: int^pn;round:bool; round_nb:int)

test/unison/Makefile

@@ -5,6 +5,8 @@ DECO_PATTERN="0-:unison.ml"
 -include ../Makefile.inc
 -include Makefile.untracked
 
+DAEMON=-sd
+
 ##############################################################################
 # Non-regression tests
 

test/unison/unison_oracle.lus

 include "../lustre/oracle_utils.lus"
 
+type state = int;
 -----------------------------------------------------------------------------
 node theorem_4_11<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) 
 returns (res:bool);