round update

lib/round.lus

--- -- Time-stamp: <modified the 10/06/2022 (at 16:45) by Erwan Jahier>
---  
--- Computing rounds in Lustre
--- The inputs are 2 arrays Enab and Acti, where:
---     - Enab[i][j] is true iff action i of process j is enabled
---     - Acti[i][j] is true iff action i of process j is active
- 
--- n holds the number of processes
--- m holds the number of actions per process
-node round<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn)
-returns (res:bool);
-var 
-  -- mask[i] is true iff pi should be activated or stop being enabled
-  -- when forall i mask[i] is false, we have a round.
-  pmask: bool^pn;
-  init_mask, silent: bool;
-  mask0, mask: bool^pn;
-let
-  silent = silent<<an,pn>>(Enab);
-  pmask = (false^pn) fby mask;
-  init_mask = boolred<<0,0,pn>>(mask0);
-  mask0 = (false^pn) -> mask_update<<an, pn>>(Enab, pre Acti, pmask);
-  mask = merge init_mask (true  -> mask_init<<an, pn>>(Enab when init_mask))
-                         (false -> mask0 when not init_mask);
-  res = true -> not(silent) and (boolred<<0,0,pn>>(mask0));
-tel
-
--- At the first instant, the round has not begun
--- At the very end, no incr should be done (
-node round_count (r,silent:bool) returns (res:int);
-var cpt : int;
-let
-  cpt = (if r and not silent then 1 else 0) + 0 fby cpt;
-  res = 0 -> cpt;
-tel
-
-
-function not_implies(a,b:bool) returns (res:bool);
-let
-  res = not(a=>b);
-tel
-
-function mask_update_one(Ei, Ai, pmaski: bool) returns(maski:bool);
-let
-  maski = pmaski
-          and Ei -- neutralisation
-          and not Ai; -- activation
-tel
-function mask_update<<const an: int; const pn: int>> (E,A: bool^an^pn; pmask:bool^pn) 
-returns (res : bool^pn);
-var
-  enab, acti : bool^pn;
-let
---  acti = map<< red<<or, an>>, pn >>(false^pn, A);
---  enab = map<< red<<or, an>>, pn >>(false^pn, E);
-  acti = map<< boolred<<1,an,an>>, pn >>(A); -- a process is active iff at least one action is
-  enab = map<< boolred<<1,an,an>>, pn >>(E); --              enabled
---  res  = map<<and, pn>>(pmask,acti);
-   res = map<<mask_update_one, pn>> (enab, acti, pmask);
-tel
-
-function mask_init <<const an:int; const pn:int>> (E: bool^an^pn) returns (res : bool^pn);
-let
-  res = map<< red<<or, an>>, pn >>(false^pn, E);
-tel
-

lib/sas.lus

 include "utils.lus"
 include "bitset.lus"
-include "round.lus"
+include "../../test/lustre/round.lus"
 
 -- No nodes enabled, the network is silent.
 function silent<<const an:int; const pn:int>>(enab: bool^an^pn)