Skip to content
Snippets Groups Projects
Commit 68416ad3 authored by erwan's avatar erwan
Browse files

Fix: the computation of the round in lustre was wrong

parent 60123cdd
No related branches found
No related tags found
No related merge requests found
-- -- 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 >>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment