## lustrec / optim / clocks7 / clocks7_3.c @ 6a93d814

History | View | Annotate | Download (4.74 KB)

1 | 6a93d814 | xthirioux | #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 | ```
/* Scheduling: (toto_1) d toto_2 c b2 b1 z b3 y
``` |
||

15 | ```
*/
``` |
||

16 | |||

17 | ```
/*@ predicate trans_totoA(int x) =
``` |
||

18 | ```
\true;
``` |
||

19 | ```
*/
``` |
||

20 | |||

21 | ```
/*@ predicate trans_d(int x,
``` |
||

22 | ```
choice2 d) =
``` |
||

23 | ```
(x > 0)?(d == Up):(d == Down);
``` |
||

24 | ```
*/
``` |
||

25 | |||

26 | ```
/*@ predicate clock_d(int x) =
``` |
||

27 | ```
\true;
``` |
||

28 | ```
*/
``` |
||

29 | |||

30 | ```
/*@ predicate trans_totoB(int x, choice2 d) =
``` |
||

31 | ```
trans_totoA(x)
``` |
||

32 | ```
&& (clock_d(x) ==> trans_d(x, d));
``` |
||

33 | ```
*/
``` |
||

34 | |||

35 | ```
/*@ predicate trans_toto_2(int x, choice2 d,
``` |
||

36 | ```
_Bool toto_2) =
``` |
||

37 | ```
toto_2 == (0 == x);
``` |
||

38 | ```
*/
``` |
||

39 | |||

40 | ```
/*@ predicate clock_toto_2(int x, choice2 d) =
``` |
||

41 | ```
(d == Up);
``` |
||

42 | ```
*/
``` |
||

43 | |||

44 | ```
/*@ predicate trans_totoC(int x, choice2 d, _Bool toto_2) =
``` |
||

45 | ```
trans_totoB(x, d)
``` |
||

46 | ```
&& (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
``` |
||

47 | ```
*/
``` |
||

48 | |||

49 | ```
/*@ predicate trans_c(_Bool toto_2,
``` |
||

50 | ```
choice1 c) =
``` |
||

51 | ```
(toto_2)?(c == Off):(c == On);
``` |
||

52 | ```
*/
``` |
||

53 | |||

54 | ```
/*@ predicate clock_c(int x, choice2 d) =
``` |
||

55 | ```
(d == Up);
``` |
||

56 | ```
*/
``` |
||

57 | |||

58 | ```
/*@ predicate trans_totoD(int x, choice2 d, _Bool toto_2, choice1 c) =
``` |
||

59 | ```
trans_totoC(x, d, toto_2)
``` |
||

60 | ```
&& (clock_c(x, d) ==> trans_c(toto_2, c));
``` |
||

61 | ```
*/
``` |
||

62 | |||

63 | ```
/*@ predicate trans_b2(choice1 c, int b2) =
``` |
||

64 | ```
(b2 == 2);
``` |
||

65 | ```
*/
``` |
||

66 | |||

67 | ```
/*@ predicate clock_b2(int x, choice2 d, choice1 c) =
``` |
||

68 | ```
(c == Off) && clock_c(x, d);
``` |
||

69 | ```
*/
``` |
||

70 | |||

71 | ```
/*@ predicate trans_totoE(int x, choice2 d, _Bool toto_2, choice1 c, int b2) =
``` |
||

72 | ```
trans_totoD(x, d, toto_2, c)
``` |
||

73 | ```
&& (clock_b2(x, d, c) ==> trans_b2(c, b2));
``` |
||

74 | ```
*/
``` |
||

75 | |||

76 | ```
/*@ predicate trans_b1(choice1 c, int b1) =
``` |
||

77 | ```
(b1 == 1);
``` |
||

78 | ```
*/
``` |
||

79 | |||

80 | ```
/*@ predicate clock_b1(int x, choice2 d, choice1 c) =
``` |
||

81 | ```
(c == On) && clock_c(x, d);
``` |
||

82 | ```
*/
``` |
||

83 | |||

84 | ```
/*@ predicate trans_totoF(int x, choice2 d, _Bool toto_2, choice1 c, int b2, int b1) =
``` |
||

85 | ```
trans_totoE(x, d, toto_2, c, b2)
``` |
||

86 | ```
&& (clock_b1(x, d, c) ==> trans_b1(c, b1));
``` |
||

87 | ```
*/
``` |
||

88 | |||

89 | ```
/*@ predicate trans_z(choice1 c, int b1, int b2,
``` |
||

90 | ```
int z) =
``` |
||

91 | ```
((c == On) ==> (z == b1))
``` |
||

92 | ```
&& ((c == Off) ==> (z == b2));
``` |
||

93 | ```
*/
``` |
||

94 | |||

95 | ```
/*@ predicate clock_z(choice1 c, int b1, int b2, int x, choice2 d) =
``` |
||

96 | ```
clock_c(x, d);
``` |
||

97 | ```
*/
``` |
||

98 | |||

99 | ```
/*@ predicate trans_totoG(int x, choice2 d, _Bool toto_2, choice1 c, int b2, int b1, int z) =
``` |
||

100 | ```
trans_totoF(x, d, toto_2, c, b2, b1)
``` |
||

101 | ```
&& (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
``` |
||

102 | ```
*/
``` |
||

103 | |||

104 | ```
/*@ predicate trans_b3(choice2 d, int b3) =
``` |
||

105 | ```
(b3 == 3);
``` |
||

106 | ```
*/
``` |
||

107 | |||

108 | ```
/*@ predicate clock_b3(choice2 d) =
``` |
||

109 | ```
(d == Down);
``` |
||

110 | ```
*/
``` |
||

111 | |||

112 | ```
/*@ predicate trans_totoH(int x, choice2 d, _Bool toto_2, choice1 c, int b2, int b1, int z, int b3) =
``` |
||

113 | ```
trans_totoG(x, d, toto_2, c, b2, b1, z)
``` |
||

114 | ```
&& (clock_b3(d) ==> trans_b3(d, b3));
``` |
||

115 | ```
*/
``` |
||

116 | |||

117 | ```
/*@ predicate trans_y(choice2 d, int b3, int z,
``` |
||

118 | ```
int y) =
``` |
||

119 | ```
((d == Up) ==> (y == z))
``` |
||

120 | ```
&& ((d == Down) ==> (y == b3));
``` |
||

121 | ```
*/
``` |
||

122 | |||

123 | ```
/*@ predicate clock_y(choice2 d, int b3, int z, int x) =
``` |
||

124 | ```
clock_d(x);
``` |
||

125 | ```
*/
``` |
||

126 | |||

127 | ```
/*@ predicate trans_totoI(int x, choice2 d, _Bool toto_2, choice1 c, int b2, int b1, int z, int b3, int y) =
``` |
||

128 | ```
trans_totoH(x, d, toto_2, c, b2, b1, z, b3)
``` |
||

129 | ```
&& (clock_y(d, b3, z, x) ==> trans_y(d, b3, z, y));
``` |
||

130 | ```
*/
``` |
||

131 | |||

132 | |||

133 | void toto_step (int x, |
||

134 | ```
int (*y)
``` |
||

135 | ) { |
||

136 | _Bool toto_2; |
||

137 | ```
int b1;
``` |
||

138 | ```
int b2;
``` |
||

139 | ```
int b3;
``` |
||

140 | choice1 c; |
||

141 | choice2 d; |
||

142 | ```
int z;
``` |
||

143 | ```
//@ assert trans_totoA(x);
``` |
||

144 | if ((x > 0)) { |
||

145 | d = Up; |
||

146 | ```
//@ assert (clock_d(x) ==> trans_d(x, d));
``` |
||

147 | ```
} else {
``` |
||

148 | d = Down; |
||

149 | ```
//@ assert (clock_d(x) ==> trans_d(x, d));
``` |
||

150 | } |
||

151 | ```
//@ assert trans_totoB(x, d);
``` |
||

152 | ```
switch(d) {
``` |
||

153 | ```
case Down:
``` |
||

154 | ```
b3 = 3;
``` |
||

155 | ```
//@ assert (clock_b3(d) ==> trans_b3(d, b3));
``` |
||

156 | ```
//@ assert trans_totoH(x, d, toto_2, c, b2, b1, z, b3);
``` |
||

157 | *y = b3; |
||

158 | ```
//@ assert (clock_y(d, b3, z, x) ==> trans_y(d, b3, z, *y));
``` |
||

159 | ```
break;
``` |
||

160 | ```
case Up:
``` |
||

161 | ```
toto_2 = (0 == x);
``` |
||

162 | ```
//@ assert (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
``` |
||

163 | ```
//@ assert trans_totoC(x, d, toto_2);
``` |
||

164 | ```
if (toto_2) {
``` |
||

165 | c = Off; |
||

166 | ```
//@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
``` |
||

167 | ```
} else {
``` |
||

168 | c = On; |
||

169 | ```
//@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
``` |
||

170 | } |
||

171 | ```
//@ assert trans_totoD(x, d, toto_2, c);
``` |
||

172 | ```
switch(c) {
``` |
||

173 | ```
case Off:
``` |
||

174 | ```
b2 = 2;
``` |
||

175 | ```
//@ assert (clock_b2(x, d, c) ==> trans_b2(c, b2));
``` |
||

176 | ```
//@ assert trans_totoE(x, d, toto_2, c, b2);
``` |
||

177 | z = b2; |
||

178 | ```
//@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
``` |
||

179 | ```
break;
``` |
||

180 | ```
case On:
``` |
||

181 | ```
b1 = 1;
``` |
||

182 | ```
//@ assert (clock_b1(x, d, c) ==> trans_b1(c, b1));
``` |
||

183 | ```
//@ assert trans_totoF(x, d, toto_2, c, b2, b1);
``` |
||

184 | z = b1; |
||

185 | ```
//@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
``` |
||

186 | ```
break;
``` |
||

187 | } |
||

188 | ```
//@ assert trans_totoG(x, d, toto_2, c, b2, b1, z);
``` |
||

189 | *y = z; |
||

190 | ```
//@ assert (clock_y(d,b3,z,x) ==> trans_y(d, b3, z, *y));
``` |
||

191 | ```
break;
``` |
||

192 | } |
||

193 | ```
//@ assert trans_totoI(x, d, toto_2, c, b2, b1, z, b3, *y);
``` |
||

194 | ```
return;
``` |
||

195 | } |