|
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
|
--@ ensures OK;
|
|
111
|
node top(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool)
|
|
112
|
returns ( OK : bool );
|
|
113
|
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int;
|
|
114
|
env : bool;
|
|
115
|
let
|
|
116
|
(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) =
|
|
117
|
readwrite(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9);
|
|
118
|
env = Sofar( excludes9(etat1, etat2, etat3, etat4, etat5,
|
|
119
|
etat6, etat7, etat8, etat9) and
|
|
120
|
x0 > -32768 and x1 > -32768 and x2 > -32768 and
|
|
121
|
x3 > -32768 and x4 > -32768 and x5 > -32768 and
|
|
122
|
x6 > -32768 and x7 > -32768 and x8 > -32768 and
|
|
123
|
x0 < 32767 and x1 < 32767 and x3 < 32767 and x4 < 32767 and
|
|
124
|
x5 < 32767 and x6 < 32767 and x7 < 32767 and x8 < 32767 and
|
|
125
|
x9 < 32767 and x10 < 32767 and x11 < 32767 and x12 < 32767);
|
|
126
|
|
|
127
|
OK = x0 >= 0;
|
|
128
|
--!k:2;
|
|
129
|
--!PROPERTY: OK=true;
|
|
130
|
--%MAIN;
|
|
131
|
tel
|