Profile

Download (3.93 KB) Statistics
| Branch: | Tag: | Revision:
 1 ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : 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 and not X9 or ``` ``` X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8 and not X9 or ``` ``` not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and X9; ``` ```tel ``` ```node illinois(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) ``` ```returns(invalid, dirty, exclusive, shared : int); ``` ```var ``` ``` g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool; ``` ```let ``` ``` g1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0; ``` ``` g2 = pre invalid>=1 and pre dirty>=1; ``` ``` g3 = pre invalid>=1 and pre shared+pre exclusive>=1; ``` ``` g4 = pre exclusive>=1; ``` ``` g5 = pre shared>=1; ``` ``` g6 = pre invalid>=1; ``` ``` g7 = pre dirty>=1; ``` ``` g8 = pre shared>=1; ``` ``` g9 = pre exclusive>=1; ``` ``` invalid = (if(init_invalid>0) then init_invalid else 1-init_invalid) -> ``` ``` if(e1) then if(g1) then pre invalid-1 else pre invalid else ``` ``` if(e2) then if(g2) then pre invalid-1 else pre invalid else ``` ``` if(e3) then if(g3) then pre invalid-1 else pre invalid else ``` ``` if(e5) then if(g5) then pre invalid+pre shared-1 else pre invalid else ``` ``` if(e6) then if(g6) then pre invalid+pre dirty+pre shared+pre exclusive-1 else pre invalid else ``` ``` if(e7) then if(g7) then pre invalid+1 else pre invalid else ``` ``` if(e8) then if(g8) then pre invalid+1 else pre invalid else ``` ``` if(e9) then if(g9) then pre invalid+1 else pre invalid else ``` ``` pre invalid; ``` ``` dirty = 0 -> ``` ``` if(e2) then if(g2) then pre dirty-1 else pre dirty else ``` ``` if(e4) then if(g4) then pre dirty+1 else pre dirty else ``` ``` if(e5) then if(g5) then pre dirty+1 else pre dirty else ``` ``` if(e6) then if(g6) then 1 else pre dirty else ``` ``` if(e7) then if(g7) then pre dirty-1 else pre dirty else ``` ``` pre dirty; ``` ``` exclusive = 0 -> ``` ``` if(e1) then if(g1) then pre exclusive+1 else pre exclusive else ``` ``` if(e3) then if(g3) then pre 0 else pre exclusive else ``` ``` if(e4) then if(g4) then pre exclusive-1 else pre exclusive else ``` ``` if(e6) then if(g6) then 0 else pre exclusive else ``` ``` if(e9) then if(g9) then pre exclusive-1 else pre exclusive else ``` ``` pre exclusive; ``` ``` shared = 0 -> ``` ``` if(e2) then if(g2) then pre shared+2 else pre shared else ``` ``` if(e3) then if(g3) then pre shared+pre exclusive+1 else pre shared else ``` ``` if(e5) then if(g5) then 0 else pre shared else ``` ``` if(e6) then if(g6) then 0 else pre shared else ``` ``` if(e8) then if(g8) then pre shared-1 else pre shared else ``` ``` pre shared; ``` ```tel ``` ```node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) ``` ```returns( OK : bool); ``` ```--@ contract guarantees OK; ``` ``` var invalid, dirty, exclusive, shared : int; ``` ``` env : bool; ``` ```let ``` ``` ( invalid, dirty, exclusive, shared ) = ``` ``` illinois( e1, e2, e3, e4, e5, e6, e7, e8, e9, init_invalid ); ``` ``` env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) ); ``` ``` OK = env => (true -> invalid -1+ dirty - exclusive + shared = ``` ``` pre ( invalid + dirty + exclusive + shared ) ); ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```
(43-43/911)