### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / memory2 / MESI_3_e1_2517_e8_2163.lus @ 2d37a1e1

 1 ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node Abs( X : int ) returns ( Abs : int ); ``` ```let ``` ``` Abs = if X < 0 then -X else X; ``` ```tel ``` ```node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); ``` ```let ``` ``` excludes = not ( X1 and X2 and X1 and X3 or X1 and X4 or ``` ``` X2 and X3 or X2 and X4 or ``` ``` X3 and X4 ); ``` ```tel ``` ```node mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool ``` ```) returns ( ``` ``` modified_me, exclusive_me, shared_me, invalid_me : int ``` ```); ``` ```var ``` ``` garde_me1, garde_me2, garde_me3, garde_me4 : bool; ``` ```let ``` ``` garde_me1 = pre invalid_me >= 1; ``` ``` garde_me2 = pre exclusive_me>=1; ``` ``` garde_me3 = pre shared_me>=1; ``` ``` garde_me4 = pre invalid_me>=1; ``` ``` modified_me = 0 -> ``` ``` if(etat_me1) then if(garde_me1) then 0 else pre modified_me else ``` ``` if(etat_me2) then if(garde_me2) then pre modified_me -1 else pre modified_me else ``` ``` if(etat_me3) then if(garde_me3) then 0 else pre modified_me else ``` ``` if(etat_me4) then if(garde_me4) then 0 else pre modified_me else ``` ``` pre modified_me; ``` ``` exclusive_me = 0 -> ``` ``` if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else ``` ``` if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else ``` ``` if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else ``` ``` if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else ``` ``` pre exclusive_me; ``` ``` shared_me = 0 -> ``` ``` if(etat_me1) then if(garde_me1) then pre shared_me +1+ pre exclusive_me + pre modified_me - 1 else pre shared_me else ``` ``` if(etat_me2) then if(garde_me2) then pre shared_me else pre shared_me else ``` ``` if(etat_me3) then if(garde_me3) then 0 else pre shared_me else ``` ``` if(etat_me4) then if(garde_me4) then 0 else pre shared_me else ``` ``` pre shared_me; ``` ``` invalid_me = 3 -> ``` ``` if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else ``` ``` if(etat_me2) then if(garde_me2) then pre invalid_me else pre invalid_me else ``` ``` if(etat_me3) then if(garde_me3) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else ``` ``` if(etat_me4) then if(garde_me4) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else ``` ``` pre invalid_me; ``` ```tel ``` ```node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool ); ``` ```--@ contract guarantees OK; ``` ``` var modified_me, exclusive_me, shared_me, invalid_me : int; ``` ``` env : bool; ``` ```let ``` ``` ( modified_me, exclusive_me, shared_me, invalid_me ) = ``` ``` mesi( etat_me1, etat_me2, etat_me3, etat_me4 ); ``` ``` env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) ); ``` ``` OK = env => (Abs(modified_me)+Abs(exclusive_me)+ ``` ``` Abs(shared_me)+Abs(invalid_me)) <= 3; ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```