Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / memory1 / DRAGON_13.lus @ b8dc00eb

History | View | Annotate | Download (6.03 KB)

1

    
2
-- Source: David Merchat (node DRAGON + property v1)
3

    
4

    
5
node First( X : int ) returns ( First : int );
6
let
7
    First = X -> pre First;
8
tel
9

    
10
node Sofar( X : bool ) returns ( Sofar : bool );
11
let
12
    Sofar = X -> X and pre Sofar;
13
tel
14

    
15
node excludes12( X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12 : bool ) returns ( excludes : bool );
16
let
17
    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
18
                  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
19
              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
20
              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
21
              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
22
              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
23
              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
24
              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
25
              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
26
              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
27
              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
28
              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
29
              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;
30
tel
31

    
32
node DRAGON(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
33
init_invalid : int)
34
returns(exclusive, shared, shared_dirty, dirty, invalid : int; erreur : bool);
35
var
36
   g01, g02, g03, g04, g05, g06, g07, g08, g09, g10, g11, g12 : bool;
37
   mem_init : int;
38
let
39

    
40
   mem_init = init_invalid -> pre mem_init;
41

    
42
   erreur = if(exclusive >= 2) then true else false;
43

    
44
   g01 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 and pre shared_dirty=0;
45
   g02 = pre invalid>=1 and pre dirty + pre shared + pre exclusive + pre shared_dirty>=1;
46
   g03 = pre exclusive>=1;
47
   g04 = pre shared_dirty=1 and pre shared=0;
48
   g05 = pre shared_dirty=0 and pre shared=1;
49
   g06 = pre shared_dirty + pre shared>=2;
50
   g07 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 and pre shared_dirty=0;
51
   g08 = pre invalid>=1 and pre dirty + pre shared + pre exclusive + pre shared_dirty>=1;
52
   g09 = pre dirty>=1;
53
   g10 = pre shared>=1;
54
   g11 = pre shared_dirty>=1;
55
   g12 = pre exclusive>=1;
56

    
57
   exclusive = 0 -> 
58
   if(e01) then if(g01) then pre exclusive+1 else pre exclusive else 
59
   if(e02) then if(g02) then 0 else pre exclusive else 
60
   if(e03) then if(g03) then pre exclusive-1 else pre exclusive else 
61
   if(e08) then if(g08) then 0 else pre exclusive else 
62
   if(e12) then if(g12) then pre exclusive-1 else pre exclusive else 
63
   pre exclusive;
64

    
65
   shared = 0 -> 
66
   if(e02) then if(g02) then pre shared+pre exclusive+1 else pre shared else 
67
   if(e05) then if(g05) then 0 else pre shared else 
68
   if(e06) then if(g06) then pre shared+pre shared_dirty-1 else pre shared else
69
   if(e08) then if(g08) then pre shared+pre exclusive+pre shared_dirty+pre dirty else pre shared else 
70
   if(e10) then if(g10) then pre shared-1 else pre shared else 
71
   pre shared;
72

    
73
   shared_dirty = 0 -> 
74
   if(e02) then if(g02) then pre shared_dirty+pre dirty else pre shared_dirty else 
75
   if(e04) then if(g04) then 0 else pre shared_dirty else 
76
   if(e06) then if(g06) then 1 else pre shared_dirty else 
77
   if(e08) then if(g08) then 1 else pre shared_dirty else 
78
   if(e11) then if(g11) then pre shared_dirty-1 else pre shared_dirty else 
79
   pre shared_dirty;
80

    
81
   dirty = 0 -> 
82
   if(e02) then if(g02) then 0 else pre dirty else 
83
   if(e03) then if(g03) then pre dirty+1 else pre dirty else 
84
   if(e04) then if(g04) then pre dirty+1 else pre dirty else 
85
   if(e05) then if(g05) then pre dirty+1 else pre dirty else 
86
   if(e07) then if(g07) then pre dirty+1 else pre dirty else 
87
   if(e08) then if(g08) then 0 else pre dirty else 
88
   if(e09) then if(g09) then pre dirty-1 else pre dirty else 
89
   pre dirty;
90

    
91
   invalid = mem_init -> 
92
   if(e01) then if(g01) then pre invalid-1 else pre invalid else 
93
   if(e02) then if(g02) then pre invalid-1 else pre invalid else 
94
   if(e07) then if(g07) then pre invalid-1 else pre invalid else 
95
   if(e08) then if(g08) then pre invalid-1 else pre invalid else 
96
   if(e09) then if(g09) then pre invalid+1 else pre invalid else 
97
   if(e10) then if(g10) then pre invalid+1 else pre invalid else 
98
   if(e11) then if(g11) then pre invalid+1 else pre invalid else 
99
   if(e12) then if(g12) then pre invalid+1 else pre invalid else 
100
   pre invalid;
101
tel
102

    
103
-- Only provable in nbac
104
--@ ensures OK;
105
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
106
             init_invalid : int ) returns ( OK : bool );
107
    var exclusive, shared, shared_dirty, dirty, invalid : int;
108
        erreur : bool;
109
        env : bool;
110
let
111
    ( exclusive, shared, shared_dirty, dirty, invalid, erreur ) =
112
        DRAGON( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12,
113
                init_invalid );
114
    env = Sofar( excludes12( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10,
115
                            e11, e12 ) and
116
                init_invalid > 0);
117
    OK = env => dirty <= First( init_invalid );
118
    --%PROPERTY OK=true;
119
    --%MAIN;
120
tel