lustrec / test / src / kind_fmcad08 / memory1 / FIREFLY_luke_2_e2_1375_e1_418.lus @ 65f71d05
History | View | Annotate | Download (3.56 KB)
1 | 22fe1c93 | ploc | |
---|---|---|---|
2 | node Sofar( X : bool ) returns ( Sofar : bool ); |
||
3 | let |
||
4 | Sofar = X -> X and pre Sofar; |
||
5 | tel |
||
6 | node excludes8( X1, X2, X3, X4, X5, X6, X7, X8 : bool ) returns ( excludes : bool ); |
||
7 | let |
||
8 | 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 |
||
9 | X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or |
||
10 | not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or |
||
11 | not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 or |
||
12 | not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 or |
||
13 | not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 or |
||
14 | not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 or |
||
15 | not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 or |
||
16 | not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8; |
||
17 | tel |
||
18 | node firefly(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) |
||
19 | returns(invalid, dirty, exclusive, shared : int); |
||
20 | var |
||
21 | garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8 : bool; |
||
22 | mem_invalid : int; |
||
23 | let |
||
24 | mem_invalid = i_invalid -> pre mem_invalid; |
||
25 | garde1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 ; |
||
26 | garde2 = pre invalid>=1 and pre dirty>=1; |
||
27 | garde3 = pre invalid>=1 and pre shared+pre exclusive>=1; |
||
28 | garde4 = pre exclusive>=1; |
||
29 | garde5 = pre shared=1; |
||
30 | garde6 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0; |
||
31 | garde7 = pre invalid>=1 and pre dirty>=1; |
||
32 | garde8 = pre invalid>=1 and pre shared+pre exclusive>=1; |
||
33 | invalid = mem_invalid -> |
||
34 | if(e1) then if(garde1) then pre invalid-1 else pre invalid else |
||
35 | if(e2) then if(garde2) then pre invalid-1 else pre invalid else |
||
36 | if(e3) then if(garde3) then pre invalid-1 else pre invalid else |
||
37 | if(e6) then if(garde6) then pre invalid-1 else pre invalid else |
||
38 | if(e7) then if(garde7) then pre invalid-1 else pre invalid else |
||
39 | if(e8) then if(garde8) then pre invalid-1 else pre invalid else |
||
40 | pre invalid; |
||
41 | dirty = 0 -> |
||
42 | if(e2) then if(garde2) then pre dirty-1 else pre dirty else |
||
43 | if(e4) then if(garde4) then pre dirty+1 else pre dirty else |
||
44 | if(e6) then if(garde6) then 1 else pre dirty else |
||
45 | if(e7) then if(garde7) then pre dirty-1 else pre dirty else |
||
46 | pre dirty; |
||
47 | exclusive = 0 -> |
||
48 | if(e1) then if(garde1) then pre exclusive+1 else pre exclusive else |
||
49 | if(e3) then if(garde3) then 0 else pre exclusive else |
||
50 | if(e4) then if(garde4) then pre exclusive-1 else pre exclusive else |
||
51 | if(e5) then if(garde5) then pre exclusive+1 else pre exclusive else |
||
52 | if(e8) then if(garde8) then 0 else pre exclusive else |
||
53 | pre exclusive; |
||
54 | shared = 0 -> |
||
55 | if(e2) then if(garde2) then pre shared+2 else pre shared else |
||
56 | if(e3) then if(garde3) then pre shared -1+ pre exclusive +1+ 1 else pre shared else |
||
57 | if(e5) then if(garde5) then pre 0 else pre shared else |
||
58 | if(e7) then if(garde7) then pre shared+2 else pre shared else |
||
59 | if(e8) then if(garde8) then pre shared + pre exclusive + 1 else pre shared else |
||
60 | pre shared; |
||
61 | tel |
||
62 | 65f71d05 | ploc | --@ ensures OK; |
63 | 22fe1c93 | ploc | node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) |
64 | returns( OK : bool ); |
||
65 | var invalid, dirty, exclusive, shared : int; |
||
66 | env : bool; |
||
67 | let |
||
68 | ( invalid, dirty, exclusive, shared ) = |
||
69 | firefly( e1, e2, e3, e4, e5, e6, e7, e8, i_invalid ); |
||
70 | env = Sofar( excludes8( e1, e2, e3, e4, e5, e6, e7, e8 ) and |
||
71 | i_invalid >= 0 ); |
||
72 | OK = env => dirty < 2; |
||
73 | --%MAIN; |
||
74 | --%PROPERTY OK=true; |
||
75 | tel |