lustrec / test / src / kind_fmcad08 / protocol / readwrit.lus @ 22fe1c93
History | View | Annotate | Download (5 KB)
1 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
---|---|
2 |
let |
3 |
Sofar = X -> X and pre Sofar; |
4 |
tel |
5 |
|
6 |
node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : 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 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 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 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 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 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 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 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 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 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; |
18 |
tel |
19 |
|
20 |
|
21 |
|
22 |
node readwrite(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool) |
23 |
returns(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int); |
24 |
var |
25 |
garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8, garde9 : bool; |
26 |
let |
27 |
garde1 = pre x0>=1; |
28 |
garde2 = pre x1>=1 and pre x4>=1; |
29 |
garde3 = pre x2>=1 and pre x11>=1; |
30 |
garde4 = pre x1>=1; |
31 |
garde5 = pre x6>=1; |
32 |
garde6 = pre x3>=1 and pre x7>=1; |
33 |
garde7 = pre x8>=1 and pre x12>=1; |
34 |
garde8 = pre x4>=5 and pre x5>=1 and pre x7>=1; |
35 |
garde9 = pre x9>=1 and pre x10>=1; |
36 |
|
37 |
x0 = 0 -> |
38 |
if(etat1) then if(garde1) then pre x0-1 else pre x0 else |
39 |
if(etat2) then if(garde2) then pre x0+1 else pre x0 else |
40 |
pre x0; |
41 |
|
42 |
x1 = 0 -> |
43 |
if(etat1) then if(garde1) then pre x1+1 else pre x1 else |
44 |
if(etat2) then if(garde2) then pre x1-1 else pre x1 else |
45 |
if(etat3) then if(garde3) then pre x1+1 else pre x1 else |
46 |
if(etat4) then if(garde4) then pre x1-1 else pre x1 else |
47 |
pre x1; |
48 |
|
49 |
x2 = 1 -> |
50 |
if(etat3) then if(garde3) then pre x2-1 else pre x2 else |
51 |
if(etat4) then if(garde4) then pre x2+1 else pre x2 else |
52 |
pre x2; |
53 |
|
54 |
x3 = 0 -> |
55 |
if(etat2) then if(garde2) then pre x3+1 else pre x3 else |
56 |
if(etat6) then if(garde6) then pre x3-1 else pre x3 else |
57 |
pre x3; |
58 |
|
59 |
x4 = 0 -> |
60 |
if(etat2) then if(garde2) then pre x4-1 else pre x4 else |
61 |
if(etat6) then if(garde6) then pre x4+1 else pre x4 else |
62 |
if(etat7) then if(garde7) then pre x4+5 else pre x4 else |
63 |
if(etat8) then if(garde8) then pre x4-5 else pre x4 else |
64 |
pre x4; |
65 |
|
66 |
x5 = 0 -> |
67 |
if(etat4) then if(garde5) then pre x5+1 else pre x5 else |
68 |
if(etat8) then if(garde8) then pre x5-1 else pre x5 else |
69 |
pre x5; |
70 |
|
71 |
x6 = 0 -> |
72 |
if(etat5) then if(garde5) then pre x6-1 else pre x6 else |
73 |
if(etat6) then if(garde6) then pre x6+1 else pre x6 else |
74 |
pre x6; |
75 |
|
76 |
x7 = 0 -> |
77 |
if(etat5) then if(garde5) then pre x7+1 else pre x7 else |
78 |
if(etat6) then if(garde6) then pre x7-1 else pre x7 else |
79 |
if(etat7) then if(garde7) then pre x7+1 else pre x7 else |
80 |
if(etat8) then if(garde8) then pre x7-1 else pre x7 else |
81 |
pre x7; |
82 |
|
83 |
x8 = 1 -> |
84 |
if(etat7) then if(garde7) then pre x8-1 else pre x8 else |
85 |
if(etat8) then if(garde8) then pre x8+1 else pre x8 else |
86 |
pre x8; |
87 |
|
88 |
x9 = 0 -> |
89 |
if(etat4) then if(garde4) then pre x9+1 else pre x9 else |
90 |
if(etat9) then if(garde9) then pre x9-1 else pre x9 else |
91 |
pre x9; |
92 |
|
93 |
x10 = 0 -> |
94 |
if(etat8) then if(garde8) then pre x10+1 else pre x10 else |
95 |
if(etat9) then if(garde9) then pre x10-1 else pre x10 else |
96 |
pre x10; |
97 |
|
98 |
x11 = 1 -> |
99 |
if(etat3) then if(garde3) then pre x11-1 else pre x11 else |
100 |
if(etat9) then if(garde9) then pre x11+1 else pre x11 else |
101 |
pre x11; |
102 |
|
103 |
x12 = 1 -> |
104 |
if(etat7) then if(garde7) then pre x12-1 else pre x12 else |
105 |
if(etat9) then if(garde9) then pre x12+1 else pre x12 else |
106 |
pre x12; |
107 |
|
108 |
tel |
109 |
|
110 |
node top(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool) |
111 |
returns ( OK : bool ); |
112 |
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int; |
113 |
env : bool; |
114 |
let |
115 |
(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = |
116 |
readwrite(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9); |
117 |
env = Sofar( excludes9(etat1, etat2, etat3, etat4, etat5, |
118 |
etat6, etat7, etat8, etat9) and |
119 |
x0 > -32768 and x1 > -32768 and x2 > -32768 and |
120 |
x3 > -32768 and x4 > -32768 and x5 > -32768 and |
121 |
x6 > -32768 and x7 > -32768 and x8 > -32768 and |
122 |
x0 < 32767 and x1 < 32767 and x3 < 32767 and x4 < 32767 and |
123 |
x5 < 32767 and x6 < 32767 and x7 < 32767 and x8 < 32767 and |
124 |
x9 < 32767 and x10 < 32767 and x11 < 32767 and x12 < 32767); |
125 |
|
126 |
OK = x0 >= 0; |
127 |
--%PROPERTY OK=true; |
128 |
--%MAIN; |
129 |
tel |