### Profile

Download (3.86 KB) Statistics
| Branch: | Tag: | Revision:
 1 node Sofar( X : bool ) returns ( Sofar : bool ); let Sofar = X -> X or pre Sofar; tel node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool ); let excludes = not X1 or 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 ) and init_invalid > 0 ); OK = env => exclusive >= 0; --%MAIN; --%PROPERTY OK=true; tel
(113-113/911)