round.lus

-- -- Time-stamp: <modified the 26/06/2019 (at 15:13) 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 m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
var 
  mask: bool^n;
  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);       

  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);
var
  enab:bool^n; -- at least one action is enabled
  acti:bool^n; -- 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);
tel

function not_implies(a,b:bool) returns (res:bool);
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);
var
  acti:bool^n; -- at least one action is active
let
  acti = map<< red<<or, m>>, n >>(false^n, A);
  res = map<<not_implies, n>>(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

-----------------------------------------------------------------------------
-----------------------------------------------------------------------------
node bool_to_int(X:int; Y:bool) returns (Z:int);
let
  Z = if(Y) then X+1 else X;
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 count_true_acc(X:int; Y:bool^m) returns (Z:int);
let
  Z = red<<bool_to_int,m>>(X,Y);
tel

-----------------------------------------------------------------------------
node one_true (tab:bool^m^n) returns (res:bool);
let
  res = (((red<<count_true_acc,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 compt_move (tab_acti:bool^m^n) returns (nb_act:int);
let
  nb_act = 0 -> pre(nb_act) + (red<<count_true_acc,n>>(0,tab_acti));    
tel

-----------------------------------------------------------------------------
node is_distributed(acti,enab:bool^m^n) returns (res:bool);
let
  res = true ->  (((red<<count_true_acc,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
tel

-----------------------------------------------------------------------------
node is_central(acti:bool^m^n) returns (res:bool);
let
  res = true ->  (one_true(acti)) and pre(res);
tel

-----------------------------------------------------------------------------
node is_synchronous(enab,acti:bool^m^n) returns (res:bool);
let
  res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
tel