Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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
}