Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / clocks7 / clocks7_4.c @ 6a93d814

History | View | Annotate | Download (4.71 KB)

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
/* Scheduling: (toto_1)  d   toto_2   c   b2   b1   z   b3   y
15
                       A   B        C   D    E    F   G    H   I
16
   Death table: c |-> toto_2, z |-> {c, b1, b2}, y |-> {z, b3, d}
17
   Reuse table: b3 |-> b2#, b1  |-> b2#, y |-> b2, z |-> b2
18
 */
19

    
20
/*@ predicate trans_totoA(int x) =
21
    \true;
22
 */
23

    
24
/*@ predicate trans_d(int x,
25
                      choice2 d) =
26
    (x > 0)?(d == Up):(d == Down);
27
*/
28

    
29
/*@ predicate clock_d(int x) =
30
    \true;
31
*/
32

    
33
/*@ predicate trans_totoB(int x, choice2 d) =
34
       trans_totoA(x)
35
    && (clock_d(x) ==> trans_d(x, d));
36
 */
37

    
38
/*@ predicate trans_toto_2(int x, choice2 d,
39
                           _Bool toto_2) =
40
    toto_2 == (0 == x);
41
*/
42

    
43
/*@ predicate clock_toto_2(int x, choice2 d) =
44
    (d == Up);
45
*/
46

    
47
/*@ predicate trans_totoC(int x, choice2 d, _Bool toto_2) =
48
       trans_totoB(x, d)
49
    && (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
50
 */
51

    
52
/*@ predicate trans_c(_Bool toto_2,
53
                      choice1 c) =
54
    (toto_2)?(c == Off):(c == On);
55
*/
56

    
57
/*@ predicate clock_c(int x, choice2 d) =
58
    (d == Up);
59
*/
60

    
61
/*@ predicate trans_totoD(int x, choice2 d, choice1 c) =
62
    \exists _Bool toto_2;
63
       trans_totoC(x, d, toto_2)
64
    && (clock_c(x, d) ==> trans_c(toto_2, c));
65
 */
66

    
67
/*@ predicate trans_b2(choice1 c, int b2) =
68
    (b2 == 2);
69
*/
70

    
71
/*@ predicate clock_b2(int x, choice2 d, choice1 c) =
72
    (c == Off) && clock_c(x, d);
73
*/
74

    
75
/*@ predicate trans_totoE(int x, choice2 d, choice1 c, int b2) =
76
       trans_totoD(x, d, c)
77
    && (clock_b2(x, d, c) ==> trans_b2(c, b2));
78
*/
79

    
80
/*@ predicate trans_b1(choice1 c, int b1) =
81
    (b1 == 1);
82
*/
83

    
84
/*@ predicate clock_b1(int x, choice2 d, choice1 c) =
85
    (c == On) && clock_c(x, d);
86
*/
87

    
88
/*@ predicate trans_totoF(int x, choice2 d, choice1 c, int b2, int b1) =
89
       trans_totoE(x, d, c, b2)
90
    && (clock_b1(x, d, c) ==> trans_b1(c, b1));
91
*/
92

    
93
/*@ predicate trans_z(choice1 c, int b1, int b2,
94
                      int z) =
95
       ((c == On)  ==> (z == b1))
96
    && ((c == Off) ==> (z == b2));
97
*/
98

    
99
/*@ predicate clock_z(choice1 c, int b1, int b2, int x, choice2 d) =
100
    clock_c(x, d);
101
*/
102

    
103
/*@ predicate trans_totoG(int x, choice2 d, int z) =
104
    \exists choice1 c, int b2, int b1;
105
       trans_totoF(x, d, c, b2, b1)
106
    && (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
107
*/
108

    
109
/*@ predicate trans_b3(choice2 d, int b3) =
110
    (b3 == 3);
111
*/
112

    
113
/*@ predicate clock_b3(choice2 d) =
114
    (d == Down);
115
*/
116

    
117
/*@ predicate trans_totoH(int x, choice2 d, int z, int b3) =
118
       trans_totoG(x, d, z)
119
    && (clock_b3(d) ==> trans_b3(d, b3));
120
*/
121

    
122
/*@ predicate trans_y(choice2 d, int b3, int z,
123
                      int y) =
124
       ((d == Up)   ==> (y == z))
125
    && ((d == Down) ==> (y == b3));
126
*/
127

    
128
/*@ predicate clock_y(choice2 d, int b3, int z, int x) =
129
    clock_d(x);
130
*/
131

    
132
/*@ predicate trans_totoI(int x, int y) =
133
    \exists int z, int b3, choice2 d;
134
       trans_totoH(x, d, z, b3)
135
    && (clock_y(d, b3, z, x) ==> trans_y(d, b3, z, y));
136
*/
137

    
138

    
139
void toto_step (int x, 
140
                int (*y)
141
                ) {
142
  _Bool toto_2;
143
  int b1;
144
  int b2;
145
  int b3;
146
  choice1 c;
147
  choice2 d;
148
  int z;
149
  //@ assert trans_totoA(x);
150
  if ((x > 0)) {
151
    d = Up;
152
    //@ assert (clock_d(x) ==> trans_d(x, d));
153
  } else {
154
    d = Down;
155
    //@ assert (clock_d(x) ==> trans_d(x, d));
156
  }
157
  //@ assert trans_totoB(x, d);
158
  switch(d) {
159
    case Down:
160
      b3 = 3;
161
      //@ assert (clock_b3(d) ==> trans_b3(d, b3));
162
      //@ assert trans_totoH(x, d, z, b3);
163
      *y = b3;
164
      //@ assert (clock_y(d, b3, z, x) ==> trans_y(d, b3, z, *y));
165
      break;
166
    case Up:
167
      toto_2 = (0 == x);
168
      //@ assert (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
169
      //@ assert trans_totoC(x, d, toto_2);
170
      if (toto_2) {
171
        c = Off;
172
        //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
173
      } else {
174
        c = On;
175
        //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
176
      }
177
     //@ assert trans_totoD(x, d, c);
178
      switch(c) {
179
        case Off:
180
          b2 = 2;
181
          //@ assert (clock_b2(x, d, c) ==> trans_b2(c, b2));
182
          //@ assert trans_totoE(x, d, c, b2);
183
          z = b2;  
184
          //@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
185
          break;
186
        case On:
187
          b1 = 1;
188
          //@ assert (clock_b1(x, d, c) ==> trans_b1(c, b1));
189
          //@ assert trans_totoF(x, d, c, b2, b1);
190
          z = b1; 
191
          //@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
192
          break;
193
        }
194
      //@ assert trans_totoG(x, d, z);
195
      *y = z; 
196
      //@ assert (clock_y(d,b3,z,x) ==> trans_y(d, b3, z, *y));
197
      break;
198
  }
199
  //@ assert trans_totoI(x, *y);
200
  return;
201
}
202