Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / memory1 / DRAGON_1_e2_1997_e7_3613_e2_3409.lus @ 22fe1c93

History | View | Annotate | Download (5.8 KB)

1
node Sofar( X : bool ) returns ( Sofar : bool );
2
let
3
    Sofar = X -> X or pre Sofar;
4
tel
5
node excludes12( X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12 : bool ) returns ( excludes : bool );
6
let
7
    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 and not X10 and not X11 and not X12 or
8
                  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 and not X10 and not X11 and not X12 or
9
              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 and not X10 and not X11 and not X12 or
10
              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 and not X10 and not X11 and not X12 or
11
              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 and not X10 and not X11 and not X12 or
12
              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 and not X10 and not X11 and not X12 or
13
              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 and not X10 and not X11 and not X12 or
14
              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 and not X10 and not X11 and not X12 or
15
              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 and not X10 and not X11 and not X12 or
16
              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 and not X10 and not X11 and not X12 or
17
              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 and     X10 and not X11 and not X12 or
18
              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 and not X10 and     X11 and not X12 or
19
              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 and not X10 and not X11 and     X12;
20
tel
21
node DRAGON(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
22
init_invalid : int)
23
returns(exclusive, shared, shared_dirty, dirty, invalid : int; erreur : bool);
24
var
25
   g01, g02, g03, g04, g05, g06, g07, g08, g09, g10, g11, g12 : bool;
26
   mem_init : int;
27
let
28
   mem_init = init_invalid -> pre mem_init;
29
   erreur = if(exclusive >= 2) then true else false;
30
   g01 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 and pre shared_dirty=0;
31
   g02 = pre invalid>=1 and pre dirty -1+ pre shared -1+ pre exclusive + pre shared_dirty>=1;
32
   g03 = pre exclusive>=1;
33
   g04 = pre shared_dirty=1 and pre shared=0;
34
   g05 = pre shared_dirty=0 and pre shared=1;
35
   g06 = pre shared_dirty + pre shared>=2;
36
   g07 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 and pre shared_dirty=0;
37
   g08 = pre invalid>=1 and pre dirty + pre shared + pre exclusive + pre shared_dirty>=1;
38
   g09 = pre dirty>=1;
39
   g10 = pre shared>=1;
40
   g11 = pre shared_dirty>=1;
41
   g12 = pre exclusive>=1;
42
   exclusive = 0 -> 
43
   if(e01) then if(g01) then pre exclusive+1 else pre exclusive else 
44
   if(e02) then if(g02) then 0 else pre exclusive else 
45
   if(e03) then if(g03) then pre exclusive-1 else pre exclusive else 
46
   if(e08) then if(g08) then 0 else pre exclusive else 
47
   if(e12) then if(g12) then pre exclusive-1 else pre exclusive else 
48
   pre exclusive;
49
   shared = 0 -> 
50
   if(e02) then if(g02) then pre shared+pre exclusive+1 else pre shared else 
51
   if(e05) then if(g05) then 0 else pre shared else 
52
   if(e06) then if(g06) then pre shared+pre shared_dirty-1 else pre shared else
53
   if(e08) then if(g08) then pre shared+pre exclusive+pre shared_dirty+pre dirty else pre shared else 
54
   if(e10) then if(g10) then pre shared-1 else pre shared else 
55
   pre shared;
56
   shared_dirty = 0 -> 
57
   if(e02) then if(g02) then pre shared_dirty+pre dirty else pre shared_dirty else 
58
   if(e04) then if(g04) then 0 else pre shared_dirty else 
59
   if(e06) then if(g06) then 1 else pre shared_dirty else 
60
   if(e08) then if(g08) then 1 else pre shared_dirty else 
61
   if(e11) then if(g11) then pre shared_dirty-1 else pre shared_dirty else 
62
   pre shared_dirty;
63
   dirty = 0 -> 
64
   if(e02) then if(g02) then 0 else pre dirty else 
65
   if(e03) then if(g03) then pre dirty+1 else pre dirty else 
66
   if(e04) then if(g04) then pre dirty+1 else pre dirty else 
67
   if(e05) then if(g05) then pre dirty+1 else pre dirty else 
68
   if(e07) then if(g07) then pre dirty+1 else pre dirty else 
69
   if(e08) then if(g08) then 0 else pre dirty else 
70
   if(e09) then if(g09) then pre dirty-1 else pre dirty else 
71
   pre dirty;
72
   invalid = mem_init -> 
73
   if(e01) then if(g01) then pre invalid-1 else pre invalid else 
74
   if(e02) then if(g02) then pre invalid-1 else pre invalid else 
75
   if(e07) then if(g07) then pre invalid-1 else pre invalid else 
76
   if(e08) then if(g08) then pre invalid-1 else pre invalid else 
77
   if(e09) then if(g09) then pre invalid+1 else pre invalid else 
78
   if(e10) then if(g10) then pre invalid+1 else pre invalid else 
79
   if(e11) then if(g11) then pre invalid+1 else pre invalid else 
80
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
81
   pre invalid;
82
tel
83
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
84
         init_invalid : int ) returns ( OK : bool );
85
    var exclusive, shared, shared_dirty, dirty, invalid : int;
86
        erreur : bool;
87
let
88
    ( exclusive, shared, shared_dirty, dirty, invalid, erreur ) =
89
        DRAGON( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12,
90
                init_invalid );
91
    OK = Sofar( excludes12( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10,
92
                            e11, e12 ) and
93
                init_invalid > 0 )
94
         => not erreur;
95
  --%MAIN;
96
  --%PROPERTY  OK=true;
97
tel