Update: enhance the oracle generation (-glos)

The generation scheme is now makes it easier to write oracles that do
not depend on the topology.  The idea is to generate an oracle
(specific to the graph) that includes a file that the user should
provide, and which ougth to define a generic oracle, i.e., depending
on m and n (process and actions numbers).

lib/sasacore/genOracle.ml

-(* Time-stamp: <modified the 26/06/2019 (at 12:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 05/07/2019 (at 11:30) by Erwan Jahier> *)
 
 open Process
 
 
 let (f: 'v Process.t list -> string) =
   fun pl ->
-    let degree = 0 in
-    let diameter = 0 in
+    let degree = Register.max_degree () in
+    let diameter = Register.diameter () in
     let actions_nb = List.map (fun p -> List.length p.actions) pl in
     let m = List.fold_left max (List.hd actions_nb) (List.tl actions_nb) in
     let n = List.length pl in
-    
-    let al = List.flatten (List.map (fun p -> List.map (fun a -> p.pid^"_"^a) p.actions) pl) in
+
+    let al = List.map (fun p -> List.map (fun a -> p.pid^"_"^a) p.actions) pl in
+    let al = List.flatten al in
     let enabl = List.map (fun a -> "Enab_"^a) al in
     let input_decl = (String.concat ","(al@enabl)) ^ ":bool" in
     let array_decl = Printf.sprintf "\tActi:bool^%d^%d;\n\tEnab:bool^%d^%d;\n" m n m n in
@@ -20,33 +21,39 @@ let (f: 'v Process.t list -> string) =
     let array_def_acti =
       Printf.sprintf "\tActi = [%s];\n"
         (String.concat ","
-           (List.map (fun p -> "["^(String.concat "," (List.map (acti_name p) p.actions))^"]") pl))
+           (List.map (fun p ->
+                "["^(String.concat "," (List.map (acti_name p) p.actions))^"]") pl))
     in
     let array_def_enab =
       Printf.sprintf "\tEnab = [%s];\n"
         (String.concat ","
-           (List.map (fun p -> "["^(String.concat "," (List.map (enab_name p) p.actions))^"]") pl))
+           (List.map (fun p ->
+                "["^(String.concat "," (List.map (enab_name p) p.actions))^"]") pl))
+    in
+    let algo = Filename.basename (Sys.getcwd()) in
+    let algo = (* Make sure that we generate valid Lustre idents *)
+      Str.global_replace (Str.regexp "[-,\\.]") "_" algo
     in
-    Printf.sprintf "%sconst n=%d;
+    Printf.sprintf "%sinclude \"%s_oracle.lus\"
+const n=%d;
 const m=%d;
 const degree=%d;
 const diameter=%d;
 
-
 node oracle(%s) returns (ok:bool);
 var
   %slet
-  %s
-  %s
-  ok = false; -- XXX set me !             
+  %s  %s
+  ok = %s_oracle<<m,n>>(Enab,Acti);
 tel
 "
-        (Mypervasives.entete "--"  SasaVersion.str SasaVersion.sha)
-        n m degree diameter
-        input_decl
-        array_decl
-        array_def_acti
-        array_def_enab
-        
-    
+      (Mypervasives.entete "--"  SasaVersion.str SasaVersion.sha)
+      algo
+      n m degree diameter
+      input_decl
+      array_decl
+      array_def_acti
+      array_def_enab
+      algo
+
 

test/bfs-spanning-tree/Makefile

-# Time-stamp: <modified the 26/06/2019 (at 14:50) by Erwan Jahier>
+# Time-stamp: <modified the 05/07/2019 (at 11:09) by Erwan Jahier>
 
 
 test: test0 test2 lurette0 lurette1
@@ -31,11 +31,11 @@ lurette0:cmxs fig5.1-noinit.lut
       -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
       -sut "lutin fig5.1-noinit.lut -n distributed"
 
-lurette1:cmxs fig5.1-noinit.lut
+lurette1:cmxs fig5.1.lut
 	rdbg -lurette -o lurette.rif  \
-      -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
-      -sut "lutin fig5.1-noinit.lut -n distributed" \
-		-oracle "lv6 fig5.1-noinit_oracle.lus -n oracle"
+      -env "$(sasa) fig5.1.dot -custd -rif" \
+      -sut "lutin fig5.1.lut -n distributed" \
+		-oracle "lv6 fig5.1_oracle.lus -n oracle"
 
 lurette: lurette0
 	sim2chrogtk -ecran -in lurette.rif > /dev/null
@@ -46,6 +46,11 @@ rdbg: cmxs fig5.1-noinit.lut
       -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
       -sut-nd "lutin fig5.1-noinit.lut -n distributed"
 
+rdbg2: cmxs fig5.1.lut
+	rdbg -o lurette.rif  \
+      -env "$(sasa) fig5.1.dot -custd -rif" \
+      -sut-nd "lutin fig5.1.lut -n distributed"
+
 
 manual:cmxs fig5.1-noinit.lut
 	lurette -o lurette.rif --sim2chro \

test/lustre/round.lus

--- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
+-- -- Time-stamp: <modified the 05/07/2019 (at 11:34) by Erwan Jahier>
 --  
 -- Computing rounds in Lustre
 -- The inputs are 2 arrays Enab and Acti, where:
@@ -14,12 +14,11 @@ var
 let
   pres = true -> pre res;
   mask = merge pres (true  -> mask_init<<m, n>>  (Enab, Acti) when pres)
-                    (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);       
-
+                    (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);
   res = boolred<<0,0,n>>(mask); -- when all are false, 
 tel
 
-node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
+function mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
 var
   enab:bool^n; -- at least one action is enabled
   acti:bool^n; -- at least one action is active  
@@ -34,7 +33,8 @@ let
   res = not(a=>b);
 tel
 
-node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
+function mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n)
+returns (res : bool^n);
 var
   acti:bool^n; -- at least one action is active
 let
@@ -53,7 +53,7 @@ let
 tel
 -----------------------------------------------------------------------------
 
-node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
+function silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
 var
   enab:bool^n; -- at least one action is enabled
 let