### Profile

Download (2.99 KB) Statistics
| Branch: | Tag: | Revision:
1 2 3 0cbf0839 ploc ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); ``` ```let ``` ``` excludes = not ( X1 and X2 and X1 and X3 and X1 and X4 or ``` ``` X2 and X3 or X2 and X4 or ``` ``` X3 and X4 ); ``` ```tel ``` ```node moesi(init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool)returns( ``` ```modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; erreur_mo : bool ``` ```); ``` ```var ``` ``` garde_mo1, garde_mo2, garde_mo3, garde_mo4 : bool; ``` ```let ``` ``` garde_mo1 = pre invalid_mo >= 1; ``` ``` garde_mo2 = pre exclusive_mo>=1; ``` ``` garde_mo3 = pre shared_mo + pre owned_mo>=1; ``` ``` garde_mo4 = pre invalid_mo>=1; ``` ``` erreur_mo = false -> exclusive_mo >= 2; ``` ``` modified_mo = 0 -> ``` ``` if(etat_mo1) then if(garde_mo1) then 0 else pre modified_mo else ``` ``` if(etat_mo2) then if(garde_mo2) then pre modified_mo+1 else pre modified_mo else ``` ``` if(etat_mo3) then if(garde_mo3) then 0 else pre modified_mo else ``` ``` if(etat_mo4) then if(garde_mo4) then 0 else pre modified_mo else ``` ``` pre modified_mo; ``` ``` exclusive_mo = 0 -> ``` ``` if(etat_mo1) then if(garde_mo1) then 0 else pre exclusive_mo else ``` ``` if(etat_mo2) then if(garde_mo2) then pre exclusive_mo-1 else pre exclusive_mo else ``` ``` if(etat_mo3) then if(garde_mo3) then 1 else pre exclusive_mo else ``` ``` if(etat_mo4) then if(garde_mo4) then 1 else pre exclusive_mo else ``` ``` pre exclusive_mo; ``` ``` shared_mo = 0 -> ``` ``` if(etat_mo1) then if(garde_mo1) then pre shared_mo + pre exclusive_mo + 1 else pre shared_mo else ``` ``` if(etat_mo3) then if(garde_mo3) then 0 else pre shared_mo else ``` ``` if(etat_mo4) then if(garde_mo4) then 0 else pre shared_mo else ``` ``` pre shared_mo; ``` ``` invalid_mo = init_invalid_mo -> ``` ``` if(etat_mo1) then if(garde_mo1) then pre invalid_mo-1 else pre invalid_mo else ``` ``` if(etat_mo3) then if(garde_mo3) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else ``` ``` if(etat_mo4) then if(garde_mo4) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else ``` ``` pre invalid_mo; ``` ``` owned_mo = 0 -> ``` ``` if(etat_mo1) then if(garde_mo1) then pre owned_mo + pre modified_mo else pre owned_mo else ``` ``` if(etat_mo3) then if(garde_mo3) then 0 else pre owned_mo else ``` ``` if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else ``` ``` pre owned_mo; ``` ```tel ``` 3e36d4e0 ploc ```--@ ensures OK; ``` 0cbf0839 ploc ```node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool ) ``` ```returns ( OK : bool ); ``` ``` var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; ``` ``` erreur_mo : bool; ``` ``` env : bool; ``` ```let ``` ``` ( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) = ``` ``` moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 ); ``` ``` env = Sofar( excludes4( etat_mo1, etat_mo2, etat_mo3, etat_mo4 ) ); ``` ``` OK = env => (true -> ``` ``` (modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo) = ``` ``` pre(modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo)); ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```