Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / protocol / rtp_8.lus @ 22fe1c93

History | View | Annotate | Download (4.64 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6

    
7
node excludes12( X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12 : bool ) returns ( excludes : bool );
8
let
9
    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
10
                  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
11
              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
12
              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
13
              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
14
              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
15
              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
16
              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
17
              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
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     X9 and not X10 and not 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     X10 and not X11 and not X12 or
20
              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
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 not X9 and not X10 and not X11 and     X12;
22
tel
23

    
24
node rtp(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
25
returns(X1, X2, X3, X4, X5, X6, X7, X8, X9 : int; erreur : bool);
26
var
27
   g01, g02, g03, g04, g05, g06, g07, g08, g09, g10, g11, g12 : bool;
28
let
29

    
30
   g01 = pre X1>=1;
31
   g02 = pre X2>=1;
32
   g03 = pre X3>=1;
33
   g04 = pre X4>=1;
34
   g05 = pre X4>=1;
35
   g06 = pre X5>=1;
36
   g07 = pre X6>=1;
37
   g08 = pre X6>=1;
38
   g09 = pre X6>=1;
39
   g10 = pre X7>=1;
40
   g11 = pre X8>=1;
41
   g12 = pre X9>=1;
42

    
43
   erreur = if(X1>=2) then true else false;
44

    
45
   X1 = 1 ->
46
   if(e01) then if(g01) then pre X1-1 else pre X1 else 
47
   pre X1;
48

    
49
   X2 = 0 ->
50
   if(e01) then if(g01) then pre X2+1 else pre X2 else 
51
   if(e02) then if(g02) then pre X2-1 else pre X2 else 
52
   if(e12) then if(g12) then pre X2+1 else pre X2 else 
53
   pre X2;
54

    
55
   X3 = 0 ->
56
   if(e02) then if(g02) then pre X3+1 else pre X3 else 
57
   if(e03) then if(g03) then pre X3-1 else pre X3 else 
58
   pre X3;
59

    
60
   X4 = 0 ->
61
   if(e03) then if(g03) then pre X4+1 else pre X4 else 
62
   if(e04) then if(g04) then pre X4-1 else pre X4 else 
63
   if(e05) then if(g05) then pre X4-1 else pre X4 else 
64
   pre X4;
65

    
66
   X5 = 0 ->
67
   if(e04) then if(g04) then pre X5+1 else pre X5 else 
68
   if(e06) then if(g06) then pre X5-1 else pre X5 else 
69
   pre X5;
70

    
71
   X6 = 0 ->
72
   if(e06) then if(g06) then pre X6+1 else pre X6 else 
73
   if(e07) then if(g07) then pre X6-1 else pre X6 else 
74
   if(e08) then if(g08) then pre X6-1 else pre X6 else 
75
   if(e09) then if(g09) then pre X6-1 else pre X6 else 
76
   pre X6;
77

    
78
   X7 = 0 ->
79
   if(e08) then if(g08) then pre X7+1 else pre X7 else 
80
   if(e10) then if(g10) then pre X7-1 else pre X7 else 
81
   pre X7;
82

    
83
   X8 = 0 ->
84
   if(e09) then if(g09) then pre X8+1 else pre X8 else 
85
   if(e11) then if(g11) then pre X8-1 else pre X8 else 
86
   pre X8;
87

    
88
   X9 = 0 ->
89
   if(e05) then if(g05) then pre X9+1 else pre X9 else 
90
   if(e07) then if(g07) then pre X9+1 else pre X9 else 
91
   if(e10) then if(g10) then pre X9+1 else pre X9 else 
92
   if(e11) then if(g11) then pre X9+1 else pre X9 else 
93
   if(e12) then if(g12) then pre X9-1 else pre X9 else 
94
   pre X9;
95

    
96
tel
97

    
98
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool )
99
returns ( OK : bool );
100
    var X1, X2, X3, X4, X5, X6, X7, X8, X9 : int;
101
        erreur : bool;
102
        env : bool;
103
let
104
    ( X1, X2, X3, X4, X5, X6, X7, X8, X9, erreur ) =
105
        rtp( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 );
106
    env = Sofar( excludes12( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10,
107
                            e11, e12 ) and
108
                 X6 < 32767);
109
    OK = env => X6 >= 0;
110
    --%PROPERTY OK=true;
111
    --%MAIN;
112
tel