Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (5 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
                       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_dead;
63
       trans_totoC(x, d, toto_2_dead)
64
    && (clock_c(x, d) ==> trans_c(toto_2_dead, 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_dead, int b2_dead, int b1_dead;
105
       trans_totoF(x, d, c_dead, b2_dead, b1_dead)
106
    && (clock_z(c_dead, b1_dead, b2_dead, x, d) ==> trans_z(c_dead, b1_dead, b2_dead, 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_dead, int b3_dead, choice2 d_dead;
134
       trans_totoH(x, d_dead, z_dead, b3_dead)
135
    && (clock_y(d_dead, b3_dead, z_dead, x) ==> trans_y(d_dead, b3_dead, z_dead, y));
136
*/
137
138
139
void toto_step (int x, 
140
                int (*b2) /* y |-> b2 */
141
                ) {
142
  _Bool toto_2;
143
  /*int b1; b1 |-> b2 */
144
  /* int b2; y |-> b2 */
145
  /* int b3; b3 |-> b2 */
146
  choice1 c;
147
  choice2 d;
148
  /* int z; z |-> b2 */
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
      *b2 = 3; /* b3 |-> b2, y |-> b2 */
161
      //@ assert (clock_b3(d) ==> trans_b3(d, *b2));
162
      //@ assert trans_totoH(x, d, *b2, *b2);
163
      *b2 = *b2;
164
      //@ assert (clock_y(d, *b2, *b2, x) ==> trans_y(d, *b2, *b2, *b2));
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
          *b2 = *b2;  
184
          //@ assert (clock_z(c, *b2, *b2, x, d) ==> trans_z(c, *b2, *b2, *b2));
185
          break;
186
        case On:
187
          *b2 = 1;
188
          //@ assert (clock_b1(x, d, c) ==> trans_b1(c, *b2));
189
          //@ assert trans_totoF(x, d, c, *b2, *b2);
190
          *b2 = *b2; 
191
          //@ assert (clock_z(c, *b2, *b2, x, d) ==> trans_z(c, *b2, *b2, *b2));
192
          break;
193
        }
194
      //@ assert trans_totoG(x, d, *b2);
195
      *b2 = *b2; 
196
      //@ assert (clock_y(d, *b2, *b2, x) ==> trans_y(d, *b2, *b2, *b2));
197
      break;
198
  }
199
  //@ assert trans_totoI(x, *b2);
200
  return;
201
}