Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.56 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
/*@ 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
  } else {
100
    d = Down;
101
  }
102
  //@ assert (clock_d(x) ==> trans_d(x, d));
103
  switch(d) {
104
    case Down:
105
      b3 = 3;
106
      *y = b3;
107
      break;
108
    case Up:
109
      toto_2 = (0 == x);
110
      //@ assert (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));
111
      if (toto_2) {
112
        c = Off;
113
      } else {
114
        c = On;
115
      }
116
      //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));
117
      switch(c) {
118
        case Off:
119
          b2 = 2;
120
          z = b2;
121
          break;
122
        case On:
123
          b1 = 1;
124
          z = b1;
125
          break;
126
        }
127
      //@ assert (clock_b1(c) ==> trans_b1(c, b1));
128
      //@ assert (clock_b2(c) ==> trans_b2(c, b2));
129
      //@ assert (clock_z(c, b1, b2, x, d) ==> trans_z(c, b1, b2, z));
130
      *y = z;
131
      break;
132
  }
133
  //@ assert (clock_b3(d) ==> trans_b3(d, b3));
134
  //@ assert (clock_y(d,b3,z,x) ==> trans_y(d, b3, z, *y));
135
  return;
136
}