lustrec / test / src / kind_fmcad08 / memory2 / ILLINOIS_3_e3_2581_e7_3447.lus @ 65f71d05
History | View | Annotate | Download (3.98 KB)
| 1 | 22fe1c93 | ploc | |
|---|---|---|---|
| 2 | node First( X : int ) returns ( First : int ); |
||
| 3 | let |
||
| 4 | First = X -> pre First; |
||
| 5 | tel |
||
| 6 | node Sofar( X : bool ) returns ( Sofar : bool ); |
||
| 7 | let |
||
| 8 | Sofar = X -> X or pre Sofar; |
||
| 9 | tel |
||
| 10 | node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool ); |
||
| 11 | let |
||
| 12 | 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 |
||
| 13 | 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 |
||
| 14 | 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 |
||
| 15 | 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 |
||
| 16 | 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 |
||
| 17 | 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 |
||
| 18 | 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 |
||
| 19 | 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 |
||
| 20 | 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 |
||
| 21 | 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; |
||
| 22 | tel |
||
| 23 | node illinois(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) |
||
| 24 | returns(invalid, dirty, exclusive, shared : int); |
||
| 25 | var |
||
| 26 | g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool; |
||
| 27 | let |
||
| 28 | g1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0; |
||
| 29 | g2 = pre invalid>=1 and pre dirty>=1; |
||
| 30 | g3 = pre invalid>=1 and pre shared+pre exclusive>=1; |
||
| 31 | g4 = pre exclusive>=1; |
||
| 32 | g5 = pre shared>=1; |
||
| 33 | g6 = pre invalid>=1; |
||
| 34 | g7 = pre dirty>=1; |
||
| 35 | g8 = pre shared>=1; |
||
| 36 | g9 = pre exclusive>=1; |
||
| 37 | invalid = (if(init_invalid>0) then init_invalid else 1-init_invalid) -> |
||
| 38 | if(e1) then if(g1) then pre invalid-1 else pre invalid else |
||
| 39 | if(e2) then if(g2) then pre invalid-1 else pre invalid else |
||
| 40 | if(e3) then if(g3) then pre invalid-1 else pre invalid else |
||
| 41 | if(e5) then if(g5) then pre invalid+pre shared-1 else pre invalid else |
||
| 42 | if(e6) then if(g6) then pre invalid+pre dirty+pre shared+pre exclusive-1 else pre invalid else |
||
| 43 | if(e7) then if(g7) then pre invalid+1 else pre invalid else |
||
| 44 | if(e8) then if(g8) then pre invalid+1 else pre invalid else |
||
| 45 | if(e9) then if(g9) then pre invalid+1 else pre invalid else |
||
| 46 | pre invalid; |
||
| 47 | dirty = 0 -> |
||
| 48 | if(e2) then if(g2) then pre dirty-1 else pre dirty else |
||
| 49 | if(e4) then if(g4) then pre dirty+1 else pre dirty else |
||
| 50 | if(e5) then if(g5) then pre dirty+1 else pre dirty else |
||
| 51 | if(e6) then if(g6) then 1 else pre dirty else |
||
| 52 | if(e7) then if(g7) then pre dirty-1 else pre dirty else |
||
| 53 | pre dirty; |
||
| 54 | exclusive = 0 -> |
||
| 55 | if(e1) then if(g1) then pre exclusive+1 else pre exclusive else |
||
| 56 | if(e3) then if(g3) then pre 0 else pre exclusive else |
||
| 57 | if(e4) then if(g4) then pre exclusive-1 else pre exclusive else |
||
| 58 | if(e6) then if(g6) then 0 else pre exclusive else |
||
| 59 | if(e9) then if(g9) then pre exclusive-1 else pre exclusive else |
||
| 60 | pre exclusive; |
||
| 61 | shared = 0 -> |
||
| 62 | if(e2) then if(g2) then pre shared+2 else pre shared else |
||
| 63 | if(e3) then if(g3) then pre shared+pre exclusive+1 else pre shared else |
||
| 64 | if(e5) then if(g5) then 0 else pre shared else |
||
| 65 | if(e6) then if(g6) then 0 else pre shared else |
||
| 66 | if(e8) then if(g8) then pre shared-1 else pre shared else |
||
| 67 | pre shared; |
||
| 68 | tel |
||
| 69 | 65f71d05 | ploc | --@ ensures OK; |
| 70 | 22fe1c93 | ploc | node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) |
| 71 | returns( OK : bool); |
||
| 72 | var invalid, dirty, exclusive, shared : int; |
||
| 73 | env : bool; |
||
| 74 | let |
||
| 75 | ( invalid, dirty, exclusive, shared ) = |
||
| 76 | illinois( e1, e2, e3, e4, e5, e6, e7, e8, e9, init_invalid ); |
||
| 77 | env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and |
||
| 78 | init_invalid > 0 ); |
||
| 79 | OK = env => invalid - dirty + exclusive + shared = First( init_invalid ); |
||
| 80 | --%MAIN; |
||
| 81 | --%PROPERTY OK=true; |
||
| 82 | tel |