Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (4.89 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_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
    //@ assert trans_totoB(x, d);
154
    toto_2 = (0 == x);
155
    //@ assert (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
156
    //@ assert trans_totoC(x, d, toto_2);
157
    if (toto_2) {
158
      c = Off;
159
      //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
160
      //@ assert trans_totoD(x, d, c);
161
      *b2 = 2;
162
      //@ assert (clock_b2(x, d, c) ==> trans_b2(c, *b2));
163
      //@ assert trans_totoE(x, d, c, *b2);
164
      *b2 = *b2;  
165
      //@ assert (clock_z(c, *b2, *b2, x, d) ==> trans_z(c, *b2, *b2, *b2));
166
    } else {
167
      c = On;
168
      //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
169
      //@ assert trans_totoD(x, d, c);
170
      *b2 = 1;
171
      //@ assert (clock_b1(x, d, c) ==> trans_b1(c, *b2));
172
      //@ assert trans_totoF(x, d, c, *b2, *b2);
173
      *b2 = *b2; 
174
      //@ assert (clock_z(c, *b2, *b2, x, d) ==> trans_z(c, *b2, *b2, *b2));
175
    }
176
    //@ assert trans_totoG(x, d, *b2);
177
    *b2 = *b2; 
178
    //@ assert (clock_y(d, *b2, *b2, x) ==> trans_y(d, *b2, *b2, *b2));
179
  } else {
180
    d = Down;
181
    //@ assert (clock_d(x) ==> trans_d(x, d));
182
    //@ assert trans_totoB(x, d);
183
    *b2 = 3; /* b3 |-> b2, y |-> b2 */
184
    //@ assert (clock_b3(d) ==> trans_b3(d, *b2));
185
    //@ assert trans_totoH(x, d, *b2, *b2);
186
    *b2 = *b2;
187
    //@ assert (clock_y(d, *b2, *b2, x) ==> trans_y(d, *b2, *b2, *b2));
188
  }
189
  //@ assert trans_totoI(x, *b2);
190
  return;
191
}
192