### Profile

Download (3.7 KB) Statistics
| Branch: | Tag: | Revision:
 1 ```node First( X : int ) returns ( First : int ); ``` ```let ``` ``` First = X -> pre First; ``` ```tel ``` ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node excludes8( X1, X2, X3, X4, X5, X6, X7, X8 : bool ) returns ( excludes : bool ); ``` ```let ``` ``` excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or ``` ``` X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or ``` ``` not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or ``` ``` not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 or ``` ``` not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 or ``` ``` not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8; ``` ```tel ``` ```node firefly(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) ``` ``` returns(invalid, dirty, exclusive, shared : int); ``` ```var ``` ``` garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8 : bool; ``` ``` mem_invalid : int; ``` ```let ``` ``` mem_invalid = i_invalid -> pre mem_invalid; ``` ``` garde1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 ; ``` ``` garde2 = pre invalid>=1 and pre dirty>=1; ``` ``` garde3 = pre invalid>=1 and pre shared+pre exclusive>=1; ``` ``` garde4 = pre exclusive>=1; ``` ``` garde5 = pre shared=1; ``` ``` garde6 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0; ``` ``` garde7 = pre invalid>=1 and pre dirty>=1; ``` ``` garde8 = pre invalid>=1 and pre shared+pre exclusive>=1; ``` ``` invalid = mem_invalid -> ``` ``` if(e1) then if(garde1) then pre invalid-1 else pre invalid else ``` ``` if(e2) then if(garde2) then pre invalid-1 else pre invalid else ``` ``` if(e3) then if(garde3) then pre invalid-1 else pre invalid else ``` ``` if(e6) then if(garde6) then pre invalid-1 else pre invalid else ``` ``` if(e7) then if(garde7) then pre invalid-1 else pre invalid else ``` ``` if(e8) then if(garde8) then pre invalid-1 else pre invalid else ``` ``` pre invalid; ``` ``` dirty = 0 -> ``` ``` if(e2) then if(garde2) then pre dirty-1 else pre dirty else ``` ``` if(e4) then if(garde4) then pre dirty+1 else pre dirty else ``` ``` if(e6) then if(garde6) then 1 else pre dirty else ``` ``` if(e7) then if(garde7) then pre dirty-1 else pre dirty else ``` ``` pre dirty; ``` ``` exclusive = 0 -> ``` ``` if(e1) then if(garde1) then pre exclusive+1 else pre exclusive else ``` ``` if(e3) then if(garde3) then 0 else pre exclusive else ``` ``` if(e4) then if(garde4) then pre exclusive-1 else pre exclusive else ``` ``` if(e5) then if(garde5) then pre exclusive+1 else pre exclusive else ``` ``` if(e8) then if(garde8) then 0 else pre exclusive else ``` ``` pre exclusive; ``` ``` shared = 0 -> ``` ``` if(e2) then if(garde2) then pre shared+2 else pre shared else ``` ``` if(e3) then if(garde3) then pre shared - pre exclusive - 1 else pre shared else ``` ``` if(e5) then if(garde5) then pre 0 else pre shared else ``` ``` if(e7) then if(garde7) then pre shared+2 else pre shared else ``` ``` if(e8) then if(garde8) then pre shared + pre exclusive + 1 else pre shared else ``` ``` pre shared; ``` ```tel ``` ```node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) ``` ``` returns( OK : bool ); ``` ```--@ contract guarantees OK; ``` ``` var invalid, dirty, exclusive, shared : int; ``` ``` env : bool; ``` ```let ``` ``` ( invalid, dirty, exclusive, shared ) = ``` ``` firefly( e1, e2, e3, e4, e5, e6, e7, e8, i_invalid ); ``` ``` env = Sofar( excludes8( e1, e2, e3, e4, e5, e6, e7, e8 ) and ``` ``` i_invalid >= 0 ); ``` ``` OK = env => invalid + dirty + exclusive + shared = First( i_invalid ); ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```
(798-798/1414)