Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.79 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
/*@ predicate trans_d(int x,
15
                      choice2 d) =
16
    (x > 0)?(d == Up):(d == Down);
17
*/
18

    
19
/*@ predicate clock_d(int x) =
20
    \true;
21
*/
22

    
23
/*@ predicate trans_toto_2(int x, choice2 d,
24
                           _Bool toto_2) =
25
    toto_2 == (0 == x);
26
*/
27

    
28
/*@ predicate clock_toto_2(int x, choice2 d) =
29
    (d == Up);
30
*/
31

    
32
/*@ predicate trans_c(_Bool toto_2,
33
                      choice1 c) =
34
    (toto_2)?(c == Off):(c == On);
35
*/
36

    
37
/*@ predicate clock_c(int x, choice2 d) =
38
    (d == Up);
39
*/
40

    
41
/*@ predicate trans_b1(choice1 c, int b1) =
42
    (b1 == 1);
43
*/
44

    
45
/*@ predicate clock_b1(choice1 c) =
46
    (c == On);
47
*/
48

    
49
/*@ predicate trans_b2(choice1 c, int b2) =
50
    (b2 == 2);
51
*/
52

    
53
/*@ predicate clock_b2(choice1 c) =
54
    (c == Off);
55
*/
56

    
57
/*@ predicate trans_b3(choice2 d, int b3) =
58
    (b3 == 3);
59
*/
60

    
61
/*@ predicate clock_b3(choice2 d) =
62
    (d == Down);
63
*/
64

    
65
/*@ predicate trans_y(choice2 d, int b3, int z,
66
                      int y) =
67
       ((d == Up)   ==> (y == z))
68
    && ((d == Down) ==> (y == b3));
69
*/
70

    
71
/*@ predicate clock_y(choice2 d, int b3, int z, int x) =
72
    clock_d(x);
73
*/
74

    
75
/*@ predicate trans_z(choice1 c, int b1, int b2,
76
                      int z) =
77
       ((c == On)  ==> (z == b1))
78
    && ((c == Off) ==> (z == b2));
79
*/
80

    
81
/*@ predicate clock_z(choice1 c, int b1, int b2, int x, choice2 d) =
82
    clock_c(x, d);
83
*/
84

    
85

    
86
void toto_step (int x, 
87
                int (*y)
88
                ) {
89
  _Bool toto_2;
90
  int b1;
91
  int b2;
92
  int b3;
93
  choice1 c;
94
  choice2 d;
95
  int z;
96
  
97
  if ((x > 0)) {
98
    d = Up;
99
    //@ assert (clock_d(x) ==> trans_d(x, d));
100
  } else {
101
    d = Down;
102
    //@ assert (clock_d(x) ==> trans_d(x, d));
103
  }
104
  switch(d) {
105
    case Down:
106
      b3 = 3;
107
      //@ assert (clock_b3(d) ==> trans_b3(d, b3));
108
      *y = b3;
109
      //@ assert (clock_y(d,b3,z,x) ==> trans_y(d, b3, z, *y));
110
      break;
111
    case Up:
112
      toto_2 = (0 == x);
113
      //@ assert (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
114
      if (toto_2) {
115
        c = Off;
116
        //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
117
      } else {
118
        c = On;
119
        //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
120
      }
121
      switch(c) {
122
        case Off:
123
          b2 = 2;
124
          //@ assert (clock_b2(c) ==> trans_b2(c, b2));
125
          z = b2;  
126
          //@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
127
          break;
128
        case On:
129
          b1 = 1;
130
          //@ assert (clock_b1(c) ==> trans_b1(c, b1));
131
          z = b1; 
132
          //@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
133
          break;
134
        }
135
      *y = z; 
136
      //@ assert (clock_y(d,b3,z,x) ==> trans_y(d, b3, z, *y));
137
      break;
138
  }
139
  return;
140
}
141