--include "bug_lib2.lus"

const ze_const_int = 5 ;

type bool4 = bool^ze_const_int ;
     tab2 = int^3^4;
     tab1 = int^2;
     tab3 = int^5^6^7;
     really = real;



-- " X vaut vrai ssi C a valu vrai au moins une fois 
--   entre A et B "
node once_from_to (C,A,B: bool) returns (X: bool);
let
-- WITH BUG :
	-- X = implies(B, once_since(C,A));
-- WITHOUT BUG :
	X = implies(B, false -> pre(once_since(C,A)));
tel

-- " X vaut vrai ssi C a valu vrai depuis A "
node once_since (C,A: bool) returns (X: bool);
let
-- WITH BUG :
	-- X = if A then false else 
-- WITHOUT BUG :
        X = if A then C else
            if after(A) then C or (false -> pre(X))
	    else false;
tel

-- " XimpliesY est vrai ssi X=>Y "
node implies (X,Y : bool) returns (XimpliesY : bool);
let
	XimpliesY = (not X) or Y;
tel

-- " afterX vaut vrai ssi X a valu vrai dans le passe "
node after (X: bool) returns (afterX: bool);
var
     bidon1, bidon2 : bool;
let
	afterX = false -> pre(X or afterX) or bidon2 and bidon1;
        (bidon1, bidon2) = bidon(X);
tel

-- "edge detecte un changement de front sur le signal d'entree. "
node edge_detect (in : bool) returns (edge : bool);
var
     bidon1, bidon2 : bool;
let
        edge = false -> in and not(pre(in)) or bidon2 and bidon1;
        (bidon1, bidon2) = bidon(in);
tel

node bidon(in: bool) returns (out1, out2 : bool);
var
    toto : tab1;
let
        toto[0] = 10;
	toto[1] = 5;

        out1 = true or in and (toto[0]<20);
--	out1 = true or in;
--	out2 = false and in and (toto[1]<10);
      out2 = false and in;
tel

-- Exemple de programme qui bug :

-- " le noeud toolate declenche une alarme si
--   pendant la periode ou active=vrai, action
--   n'a pas eu lieu "

node toolate (active,action : bool) returns (alarm : bool);
var
	begin,en : bool;
let
-- WITH BUG :
--	begin = active and (true -> not pre(active));
-- WITHOUT BUG :
	begin = active and (false -> not pre(active));
	en = (not active) and (false -> pre active);
 	alarm = not once_from_to(action,begin,en);
tel