Profile

 1 ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X or 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 or 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 ``` ```--@ ensures OK; ``` ```node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool ); ``` ``` 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 ```