Test: split round.lus, plus other minor oracles refactoring

test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus

-include "../lustre/round.lus"
+include "../lustre/oracle_utils.lus"
 
-
-
------------------------------------------------------------------------------
-
-function first_element (X:bool^m) returns (res:bool);
+function first_element<<const an : int>> (X:bool^an) returns (res:bool);
 let
    res = X[0];
 tel 
-function first_column (X:bool^m^n) returns (Z:bool^n);
+function first_column<<const an : int; const pn: int>>(X:bool^an^pn) returns (Z:bool^pn);
 let
-   Z = map<<first_element,n>>(X); 
+   Z = map<<first_element<<an>>,pn>>(X); 
 tel
-function all_CD_are_false (tab_enab:bool^m^n) returns (res:bool);
+function all_CD_are_false (tab_enab:bool^an^pn) returns (res:bool);
 let
-  res = not (red<<or,n>>(false,first_column(tab_enab))) ;
+  res = not (red<<or,pn>>(false,first_column(tab_enab))) ;
 tel
 
-
-
-
-node lemma_5_16<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+node lemma_5_16<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) 
+returns (res:bool);
 var
   Round:bool;
   RoundNb:int;
   CD_disable:bool;
 let 
-  Round = round <<m,n>>(Enab,Acti);
+  Round = round <<an,pn>>(Enab,Acti);
   RoundNb = count(Round); 
   CD_disable = all_CD_are_false(Enab); 
   res = (RoundNb>=diameter+1) => CD_disable ; -- Lemma 5.16 ! 
 tel
 
 -----------------------------------------------------------------------------
-
-node theorem_5_18<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+node theorem_5_18<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) 
+returns (res:bool);
 var
   Round:bool;
   RoundNb:int;
   Silent:bool;
 let
-  Round = round <<m,n>>(Enab,Acti);
+  Round = round <<an,pn>>(Enab,Acti);
   RoundNb = count(Round); 
-  Silent = silent<<m,n>>(Enab);
+  Silent = silent<<an,pn>>(Enab);
   res = (RoundNb>=diameter+2) => Silent ; -- from theorem 5.18 page 57
 tel

test/lustre/demon.lus

+
+node is_distributed<<const an : int; const pn: int>> (acti,enab:bool^an^pn) 
+returns (res:bool);
+let
+  res = true ->
+    pre(res) and (((red<<count_true_acc<<an>>,n>>(0,acti))>=1) or silent<<an,n>>(enab));
+tel
+
+-----------------------------------------------------------------------------
+node is_central <<const an : int; const pn: int>> (acti:bool^an^pn) returns (res:bool);
+let
+  res = true -> pre(res) and one_true(acti)  ;
+tel
+
+-----------------------------------------------------------------------------
+node is_synchronous <<const an : int; const pn: int>> (enab,acti:bool^an^pn) 
+returns (res:bool);
+let
+  res = true -> pre(res) and all_true(map<<implies_list,n>>(enab,acti));
+tel

test/lustre/oracle_utils.lus

+include "round.lus"
+include "demon.lus"
+include "utils.lus"
+
+
+-----------------------------------------------------------------------------
+-- An algo is silent when no action is enable
+node silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool);
+var
+  enab:bool^pn; -- at least one action is enabled
+let
+  enab = map<< red<<or, an>>, pn >>(false^pn, Enab);
+  ok = not(red<<or, pn>>(false, enab)); 
+tel
+
+-----------------------------------------------------------------------------
+node move_count (tab_acti:bool^an^pn) returns (nb_act:int);
+let
+  nb_act = 0 -> pre(nb_act) + (red<<count_true_acc<<an>>,pn>>(0,tab_acti));    
+tel
+
+
+

test/lustre/round.lus

--- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
+-- -- Time-stamp: <modified the 08/07/2019 (at 15:20) by Erwan Jahier>
 --  
 -- Computing rounds in Lustre
 -- The inputs are 2 arrays Enab and Acti, where:
@@ -7,26 +7,26 @@
  
 -- n holds the number of processes
 -- m holds the number of actions per process
-node round<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
+node round<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) returns (res:bool);
 var 
-  mask: bool^n;
+  mask: bool^pn;
   pres: bool;
 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);       
+  mask = merge pres (true  -> mask_init<<an, pn>>  (Enab, Acti) when pres)
+                    (false -> mask_update<<an, pn>>(Enab, Acti, pre mask) when not pres);
 
-  res = boolred<<0,0,n>>(mask); -- when all are false, 
+  res = boolred<<0,0,pn>>(mask); -- when all are false, 
 tel
 
-node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
+node mask_init <<const an:int; const pn:int>> (E,A: bool^an^pn) returns (res : bool^pn);
 var
-  enab:bool^n; -- at least one action is enabled
-  acti:bool^n; -- at least one action is active  
+  enab:bool^pn; -- at least one action is enabled
+  acti:bool^pn; -- at least one action is active  
 let
-  enab = map<< red<<or, m>>, n >>(false^n, E);
-  acti = map<< red<<or, m>>, n >>(false^n, A);
-  res  = map<<not_implies, n>>(enab,acti);
+  enab = map<< red<<or, an>>, pn >>(false^pn, E);
+  acti = map<< red<<or, an>>, pn >>(false^pn, A);
+  res  = map<<not_implies, pn>>(enab,acti);
 tel
 
 function not_implies(a,b:bool) returns (res:bool);
@@ -34,102 +34,15 @@ 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);
+node mask_update<<const an: int; const pn: int>> (E,A: bool^an^pn; pmask:bool^pn) 
+returns (res : bool^pn);
 var
-  acti:bool^n; -- at least one action is active
+  acti:bool^pn; -- at least one action is active
 let
-  acti = map<< red<<or, m>>, n >>(false^n, A);
-  res = map<<not_implies, n>>(pmask,acti);
+  acti = map<< red<<or, an>>, pn >>(false^pn, A);
+  res = map<<not_implies, pn>>(pmask,acti);
 tel
 
-
 node test53=round<< 5,3 >>
 node test52=round<< 5,2 >>
 
------------------------------------------------------------------------------
-node count(x:bool) returns(cpt:int);
-let
-  cpt = 0 -> if x then pre cpt + 1 else pre cpt;
-tel
------------------------------------------------------------------------------
-
-node 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
-  enab = map<< red<<or, m>>, n >>(false^n, Enab);
-  ok = not(red<<or, n>>(false, enab)); 
-tel
-
------------------------------------------------------------------------------
-node after_n(n:int; x:bool) returns (res:bool);
-var cpt:int;
-let
-  cpt = 0 -> pre cpt + 1;
-  res = cpt <= n or x;
-tel
-
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-function add_one_if_true(i:int;Y:bool) returns (res:int);
-let
-  res= if Y then i+1 else i;
-tel
-
------------------------------------------------------------------------------
-function count_true<<const m:int>>(Acc:int;Y:bool^m) returns (Z:int);
-let
-  Z=red<<add_one_if_true,m>>(Acc,Y);
-tel
-
------------------------------------------------------------------------------
-node map_and (X,Y:bool^m) returns (Z:bool^m);
-let
-  Z = map<<and,m>>(X,Y) ;
-tel 
-
------------------------------------------------------------------------------
-node implies_list(A,B:bool^m) returns (res:bool^m);
-let
-  res = map<<=>,m>>(A,B) ;
-tel
-
------------------------------------------------------------------------------
-node one_true (tab:bool^m^n) returns (res:bool);
-let
-  res = (((red<<count_true<<m>>,n>>(0,tab)))=1);
-tel
-
------------------------------------------------------------------------------
-node all_true (tab_acti:bool^m^n) returns (res:bool);
-let
-  res = boolred<<m,m,m>>((red<<map_and,n>>(true^m,tab_acti))) ;
-tel
-
------------------------------------------------------------------------------
-node move_count (tab_acti:bool^m^n) returns (nb_act:int);
-let
-  nb_act = 0 -> pre(nb_act) + (red<<count_true<<m>>,n>>(0,tab_acti));    
-tel
-
------------------------------------------------------------------------------
-node is_distributed<<const m : int; const n: int>> (acti,enab:bool^m^n) returns (res:bool);
-let
-  res = true ->  (((red<<count_true<<m>>,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_central <<const m : int; const n: int>> (acti:bool^m^n) returns (res:bool);
-let
-  res = true ->  (one_true(acti)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_synchronous <<const m : int; const n: int>> (enab,acti:bool^m^n) returns (res:bool);
-let
-  res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
-tel
-
-
------------------------------------------------------------------------------
-

test/lustre/utils.lus

+-- Various nodes that are not specific to sasa 
+
+-----------------------------------------------------------------------------
+node count(x:bool) returns(cpt:int);
+let
+  cpt = 0 -> if x then pre cpt + 1 else pre cpt;
+tel
+
+-----------------------------------------------------------------------------
+node after_n(n:int; x:bool) returns (res:bool);
+var cpt:int;
+let
+  cpt = 0 -> pre cpt + 1;
+  res = cpt <= n or x;
+tel
+
+-----------------------------------------------------------------------------
+function add_one_if_true(i:int;Y:bool) returns (res:int);
+let
+  res= if Y then i+1 else i;
+tel
+
+function count_true_acc<<const n:int>>(Acc:int;Y:bool^n) returns (Z:int);
+let
+  Z=red<<add_one_if_true, n>>(Acc,Y);
+tel
+
+-----------------------------------------------------------------------------
+node map_and<<const n:int>> (X,Y:bool^n) returns (Z:bool^n);
+let
+  Z = map<<and,n>>(X,Y) ;
+tel 
+
+-----------------------------------------------------------------------------
+node implies_list(A,B:bool^m) returns (res:bool^m);
+let
+  res = map<<=>,an>>(A,B) ;
+tel
+
+-----------------------------------------------------------------------------
+node one_true (tab:bool^an^pn) returns (res:bool);
+let
+  res = (((red<<count_true_acc<<an>>,pn>>(0,tab)))=1);
+tel
+
+-----------------------------------------------------------------------------
+node all_true (tab_acti:bool^m^n) returns (res:bool);
+let
+  res = boolred<<m,m,m>>((red<<map_and<<m>>,n>>(true^m,tab_acti))) ;
+tel