|
1
|
#include <assert.h>
|
|
2
|
#include "clocks7.h"
|
|
3
|
|
|
4
|
/* C code generated by lustrec
|
|
5
|
SVN version number 0.1-382M
|
|
6
|
Code is C99 compliant */
|
|
7
|
|
|
8
|
/* Import dependencies */
|
|
9
|
|
|
10
|
/* Global constants (definitions) */
|
|
11
|
|
|
12
|
/* Struct definitions */
|
|
13
|
|
|
14
|
/*@ predicate trans_d(int x,
|
|
15
|
choice2 d) =
|
|
16
|
(x > 0)?(d == Up):(d == Down);
|
|
17
|
*/
|
|
18
|
|
|
19
|
/*@ predicate clock_d(int x) =
|
|
20
|
\true;
|
|
21
|
*/
|
|
22
|
|
|
23
|
/*@ predicate trans_toto_2(int x, choice2 d,
|
|
24
|
_Bool toto_2) =
|
|
25
|
toto_2 == (0 == x);
|
|
26
|
*/
|
|
27
|
|
|
28
|
/*@ predicate clock_toto_2(int x, choice2 d) =
|
|
29
|
(d == Up);
|
|
30
|
*/
|
|
31
|
|
|
32
|
/*@ predicate trans_c(_Bool toto_2,
|
|
33
|
choice1 c) =
|
|
34
|
(toto_2)?(c == Off):(c == On);
|
|
35
|
*/
|
|
36
|
|
|
37
|
/*@ predicate clock_c(int x, choice2 d) =
|
|
38
|
(d == Up);
|
|
39
|
*/
|
|
40
|
|
|
41
|
/*@ predicate trans_b1(choice1 c, int b1) =
|
|
42
|
(b1 == 1);
|
|
43
|
*/
|
|
44
|
|
|
45
|
/*@ predicate clock_b1(choice1 c) =
|
|
46
|
(c == On);
|
|
47
|
*/
|
|
48
|
|
|
49
|
/*@ predicate trans_b2(choice1 c, int b2) =
|
|
50
|
(b2 == 2);
|
|
51
|
*/
|
|
52
|
|
|
53
|
/*@ predicate clock_b2(choice1 c) =
|
|
54
|
(c == Off);
|
|
55
|
*/
|
|
56
|
|
|
57
|
/*@ predicate trans_b3(choice2 d, int b3) =
|
|
58
|
(b3 == 3);
|
|
59
|
*/
|
|
60
|
|
|
61
|
/*@ predicate clock_b3(choice2 d) =
|
|
62
|
(d == Down);
|
|
63
|
*/
|
|
64
|
|
|
65
|
/*@ predicate trans_y(choice2 d, int b3, int z,
|
|
66
|
int y) =
|
|
67
|
((d == Up) ==> (y == z))
|
|
68
|
&& ((d == Down) ==> (y == b3));
|
|
69
|
*/
|
|
70
|
|
|
71
|
/*@ predicate clock_y(choice2 d, int b3, int z, int x) =
|
|
72
|
clock_d(x);
|
|
73
|
*/
|
|
74
|
|
|
75
|
/*@ predicate trans_z(choice1 c, int b1, int b2,
|
|
76
|
int z) =
|
|
77
|
((c == On) ==> (z == b1))
|
|
78
|
&& ((c == Off) ==> (z == b2));
|
|
79
|
*/
|
|
80
|
|
|
81
|
/*@ predicate clock_z(choice1 c, int b1, int b2, int x, choice2 d) =
|
|
82
|
clock_c(x, d);
|
|
83
|
*/
|
|
84
|
|
|
85
|
|
|
86
|
void toto_step (int x,
|
|
87
|
int (*y)
|
|
88
|
) {
|
|
89
|
_Bool toto_2;
|
|
90
|
int b1;
|
|
91
|
int b2;
|
|
92
|
int b3;
|
|
93
|
choice1 c;
|
|
94
|
choice2 d;
|
|
95
|
int z;
|
|
96
|
|
|
97
|
if ((x > 0)) {
|
|
98
|
d = Up;
|
|
99
|
} else {
|
|
100
|
d = Down;
|
|
101
|
}
|
|
102
|
//@ assert (clock_d(x) ==> trans_d(x, d));
|
|
103
|
switch(d) {
|
|
104
|
case Down:
|
|
105
|
b3 = 3;
|
|
106
|
*y = b3;
|
|
107
|
break;
|
|
108
|
case Up:
|
|
109
|
toto_2 = (0 == x);
|
|
110
|
//@ assert (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
|
|
111
|
if (toto_2) {
|
|
112
|
c = Off;
|
|
113
|
} else {
|
|
114
|
c = On;
|
|
115
|
}
|
|
116
|
//@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
|
|
117
|
switch(c) {
|
|
118
|
case Off:
|
|
119
|
b2 = 2;
|
|
120
|
z = b2;
|
|
121
|
break;
|
|
122
|
case On:
|
|
123
|
b1 = 1;
|
|
124
|
z = b1;
|
|
125
|
break;
|
|
126
|
}
|
|
127
|
//@ assert (clock_b1(c) ==> trans_b1(c, b1));
|
|
128
|
//@ assert (clock_b2(c) ==> trans_b2(c, b2));
|
|
129
|
//@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
|
|
130
|
*y = z;
|
|
131
|
break;
|
|
132
|
}
|
|
133
|
//@ assert (clock_b3(d) ==> trans_b3(d, b3));
|
|
134
|
//@ assert (clock_y(d,b3,z,x) ==> trans_y(d, b3, z, *y));
|
|
135
|
return;
|
|
136
|
}
|
|
137
|
|