diff --git a/test/lustre/round.lus b/test/lustre/round.lus index ad7175ebe159a3afe1dd74a5ebb85a4e7ad45e39..770a813ebfcae975f47f238d7bfa615807e860d8 100644 --- a/test/lustre/round.lus +++ b/test/lustre/round.lus @@ -1,4 +1,4 @@ --- -- Time-stamp: <modified the 18/09/2019 (at 14:29) by Erwan Jahier> +-- -- Time-stamp: <modified the 08/10/2019 (at 21:36) by Erwan Jahier> -- -- Computing rounds in Lustre -- The inputs are 2 arrays Enab and Acti, where: @@ -9,6 +9,8 @@ -- 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. mask: bool^pn; pres: bool; psilent: bool; @@ -35,13 +37,19 @@ let res = not(a=>b); tel +function mask_update_one(Ei, Ai, pmaski: bool) returns(maski:bool); +let + maski = pmaski and Ei and not Ai; +tel function mask_update<<const an: int; const pn: int>> (E,A: bool^an^pn; pmask:bool^pn) returns (res : bool^pn); var - acti:bool^pn; -- at least one action is active + enab, acti : bool^pn; -- at least one action is active let acti = map<< red<<or, an>>, pn >>(false^pn, A); - res = map<<and, pn>>(pmask,acti); + enab = map<< red<<or, an>>, pn >>(false^pn, E); +-- res = map<<and, pn>>(pmask,acti); + res = map<<mask_update_one, pn>> (enab, acti, pmask); tel node test53=round<< 5,3 >>