Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (4.96 KB)

1

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