feat: give to the oracles the configuration, and the potential when available

lib/sasacore/genOracle.ml

-(* Time-stamp: <modified the 28/07/2021 (at 11:23) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/05/2022 (at 11:18) by Erwan Jahier> *)
 
 open Process
 
@@ -54,16 +54,20 @@ let (f: Topology.t -> 'v Process.t list -> string) =
     List.fold_left
       (fun acc p ->
          let l = SasaState.to_rif_decl p.pid p.init in
-         List.fold_left (fun acc (n,t) -> (n^":"^Data.type_to_string t)::acc) acc l
+         List.fold_left (fun acc (n,t) -> (n, Data.type_to_string t)::acc) acc l
       )
       []
       (List.rev pl)
   in
-  let input_state = "\n  "^(String.concat ";" vars)  in
+  let vars_decl = List.map (fun (v,t)-> v^":"^t) vars in
+  let input_state = "\n  "^(String.concat ";" vars_decl)  in
   let input_trig = ";\n  "^(String.concat "," al) ^ ":bool" in
   let input_enab = ";\n  "^(String.concat "," enabl) ^ ":bool" in
   let input_decl = input_state^input_enab^input_trig in
-  let array_decl = Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n" in
+  let array_decl =
+    Printf.sprintf "\tActi:bool^an^pn;\n\tEnab:bool^an^pn;\n\tConfig:%s^pn;\n"
+      (fst (List.hd vars))
+  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
   let array_def_acti =
@@ -78,6 +82,9 @@ let (f: Topology.t -> 'v Process.t list -> string) =
          (List.map (fun p ->
               "["^(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))
+  in
   let algo = Filename.basename (Sys.getcwd()) in
   let algo = StringOf.action algo in
   Printf.sprintf "%sinclude \"%s_oracle.lus\"
@@ -96,11 +103,11 @@ const f=false;
 const t=true;
 const adjacency=%s;
 %s
-node oracle(legitimate:bool; %s) \nreturns (ok:bool);
+node oracle(legitimate:bool;%s%s) \nreturns (ok:bool);
 var
   %slet
-  %s  %s
-  ok = %s_oracle(legitimate, Enab, Acti);
+  %s  %s  %s
+  ok = %s_oracle(legitimate,%s Enab, Acti, Config);
 tel
 "
     (Mypervasives.entete "--"  SasaVersion.str SasaVersion.sha)
@@ -117,10 +124,13 @@ tel
     (Register.is_tree ())
     (matrix_to_string (Topology.to_adjacency g))
     (graph_attributes_to_string ())
+    (if Register.get_potential () = None then "" else  "potential:real; ")
     input_decl
     array_decl
     array_def_acti
     array_def_enab
+    array_def_config
     algo
+    (if Register.get_potential () = None then "" else  "potential,")
 
 

test/async-unison/async_unison_oracle.lus

@@ -9,7 +9,7 @@ let
 tel
 
 -- all neigbhbors are close 
-function is_stable<<const l:int>>(State : int^pn) returns (res:bool)
+function is_legitimate<<const l:int>>(State : int^pn) returns (res:bool)
 var
   i,j:int;
 let
@@ -17,16 +17,16 @@ let
   j = l mod pn;
   res = 
      with l = 0 then true
-     else is_stable<<l-1>>(State) and
+     else is_legitimate<<l-1>>(State) and
        (i<=j or (adjacency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn])));
 tel
 
 node async_unison_oracle (State : int^pn; Enab, Acti: bool^an^pn) 
-returns (res, Stable:bool; rn:int);
+returns (res, Legitimate:bool; rn:int);
 let
   rn = count(round <<an,pn>>(Enab,Acti));
-  Stable = is_stable <<pn*pn-1>>(State);
-  res = redge(Stable) => (rn <= diameter*card);
+  Legitimate = is_legitimate <<pn*pn-1>>(State);
+  res = redge(Legitimate) => (rn <= diameter*card);
 tel
 
 node redge(x:bool) returns (res:bool);

test/st-KK06-algo1/st_KK06_algo1_oracle.lus

@@ -2,7 +2,7 @@
 include "../lustre/utils.lus"
 
 node st_KK06_algo1_oracle<<const an:int; const pn:int>>
-(legitimate:bool; Enab,Acti:bool^an^pn) returns (ok:bool);
+(legitimate:bool; Enab,Acti:bool^an^pn; Config: int^pn) returns (ok:bool);
 var
   moves : int;
 let

test/st-KK06-algo2/st_KK06_algo2_oracle.lus

@@ -3,7 +3,7 @@ include "../lustre/utils.lus"
 
 const bigN = 2*card;
 
-node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn) 
+node st_KK06_algo2_oracle<<const an:int; const pn:int>>(leg:bool; Enab,Acti:bool^an^pn; Config: int^pn)
 returns (ok:bool);
 var
   moves : int;

test/unison/unison_oracle.lus

@@ -26,7 +26,7 @@ let
 tel
 
 -----------------------------------------------------------------------------
-node unison_oracle<<const an:int; const pn:int>> (legit:bool; Enab, Acti: bool^an^pn) 
+node unison_oracle<<const an:int; const pn:int>> (legit:bool; Enab, Acti: bool^an^pn; Config:int^pn)
 returns (ok:bool);
 let