CristalCaveGem » LustreC

#include <assert.h>

#include "clocks7.h"

/* C code generated by lustrec

   SVN version number 0.1-382M

   Code is C99 compliant */

/* Import dependencies */

/* Global constants (definitions) */

/* Struct definitions */

/* Scheduling: (toto_1)  d   toto_2   c   b2   b1   z   b3   y

                       A   B        C   D    E    F   G    H   I

   Death table: c |-> toto_2, z |-> {c, b1, b2}, y |-> {z, b3, d}

   Reuse table: b3 |-> b2#, b1  |-> b2#, y |-> b2, z |-> b2

 */

/*@ predicate trans_totoA(int x) =

    \true;

 */

/*@ predicate trans_d(int x,

                      choice2 d) =

    (x > 0)?(d == Up):(d == Down);

*/

/*@ predicate clock_d(int x) =

    \true;

*/

/*@ predicate trans_totoB(int x, choice2 d) =

       trans_totoA(x)

    && (clock_d(x) ==> trans_d(x, d));

 */

/*@ predicate trans_toto_2(int x, choice2 d,

                           _Bool toto_2) =

    toto_2 == (0 == x);

*/

/*@ predicate clock_toto_2(int x, choice2 d) =

    (d == Up);

*/

/*@ predicate trans_totoC(int x, choice2 d, _Bool toto_2) =

       trans_totoB(x, d)

    && (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));

 */

/*@ predicate trans_c(_Bool toto_2,

                      choice1 c) =

    (toto_2)?(c == Off):(c == On);

*/

/*@ predicate clock_c(int x, choice2 d) =

    (d == Up);

*/

/*@ predicate trans_totoD(int x, choice2 d, choice1 c) =

    \exists _Bool toto_2_dead;

       trans_totoC(x, d, toto_2_dead)

    && (clock_c(x, d) ==> trans_c(toto_2_dead, c));

 */

/*@ predicate trans_b2(choice1 c, int b2) =

    (b2 == 2);

*/

/*@ predicate clock_b2(int x, choice2 d, choice1 c) =

    (c == Off) && clock_c(x, d);

*/

/*@ predicate trans_totoE(int x, choice2 d, choice1 c, int b2) =

       trans_totoD(x, d, c)

    && (clock_b2(x, d, c) ==> trans_b2(c, b2));

*/

/*@ predicate trans_b1(choice1 c, int b1) =

    (b1 == 1);

*/

/*@ predicate clock_b1(int x, choice2 d, choice1 c) =

    (c == On) && clock_c(x, d);

*/

/*@ predicate trans_totoF(int x, choice2 d, choice1 c, int b2, int b1) =

       trans_totoE(x, d, c, b2)

    && (clock_b1(x, d, c) ==> trans_b1(c, b1));

*/

/*@ predicate trans_z(choice1 c, int b1, int b2,

                      int z) =

       ((c == On)  ==> (z == b1))

    && ((c == Off) ==> (z == b2));

*/

/*@ predicate clock_z(choice1 c, int b1, int b2, int x, choice2 d) =

    clock_c(x, d);

*/

/*@ predicate trans_totoG(int x, choice2 d, int z) =

    \exists choice1 c_dead, int b2_dead, int b1_dead;

       trans_totoF(x, d, c_dead, b2_dead, b1_dead)

    && (clock_z(c_dead, b1_dead, b2_dead, x, d) ==> trans_z(c_dead, b1_dead, b2_dead, z));

*/

/*@ predicate trans_b3(choice2 d, int b3) =

    (b3 == 3);

*/

/*@ predicate clock_b3(choice2 d) =

    (d == Down);

*/

/*@ predicate trans_totoH(int x, choice2 d, int z, int b3) =

       trans_totoG(x, d, z)

    && (clock_b3(d) ==> trans_b3(d, b3));

*/

/*@ predicate trans_y(choice2 d, int b3, int z,

                      int y) =

       ((d == Up)   ==> (y == z))

    && ((d == Down) ==> (y == b3));

*/

/*@ predicate clock_y(choice2 d, int b3, int z, int x) =

    clock_d(x);

*/

/*@ predicate trans_totoI(int x, int y) =

    \exists int z_dead, int b3_dead, choice2 d_dead;

       trans_totoH(x, d_dead, z_dead, b3_dead)

    && (clock_y(d_dead, b3_dead, z_dead, x) ==> trans_y(d_dead, b3_dead, z_dead, y));

*/

void toto_step (int x, 

                int (*b2) /* y |-> b2 */

                ) {

  _Bool toto_2;

  /*int b1; b1 |-> b2 */

  /* int b2; y |-> b2 */

  /* int b3; b3 |-> b2 */

  choice1 c;

  choice2 d;

  /* int z; z |-> b2 */

  //@ assert trans_totoA(x);

  if ((x > 0)) {

    d = Up;

    //@ assert (clock_d(x) ==> trans_d(x, d));

    //@ assert trans_totoB(x, d);

    toto_2 = (0 == x);

    //@ assert (clock_toto_2(x, d) ==> trans_toto_2(x, d, toto_2));

    //@ assert trans_totoC(x, d, toto_2);

    if (toto_2) {

      c = Off;

      //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));

      //@ assert trans_totoD(x, d, c);

      *b2 = 2;

      //@ assert (clock_b2(x, d, c) ==> trans_b2(c, *b2));

      //@ assert trans_totoE(x, d, c, *b2);

      *b2 = *b2;  

      //@ assert (clock_z(c, *b2, *b2, x, d) ==> trans_z(c, *b2, *b2, *b2));

    } else {

      c = On;

      //@ assert (clock_c(x, d) ==> trans_c(toto_2, c));

      //@ assert trans_totoD(x, d, c);

      *b2 = 1;

      //@ assert (clock_b1(x, d, c) ==> trans_b1(c, *b2));

      //@ assert trans_totoF(x, d, c, *b2, *b2);

      *b2 = *b2; 

      //@ assert (clock_z(c, *b2, *b2, x, d) ==> trans_z(c, *b2, *b2, *b2));

    }

    //@ assert trans_totoG(x, d, *b2);

    *b2 = *b2; 

    //@ assert (clock_y(d, *b2, *b2, x) ==> trans_y(d, *b2, *b2, *b2));

  } else {

    d = Down;

    //@ assert (clock_d(x) ==> trans_d(x, d));

    //@ assert trans_totoB(x, d);

    *b2 = 3; /* b3 |-> b2, y |-> b2 */

    //@ assert (clock_b3(d) ==> trans_b3(d, *b2));

    //@ assert trans_totoH(x, d, *b2, *b2);

    *b2 = *b2;

    //@ assert (clock_y(d, *b2, *b2, x) ==> trans_y(d, *b2, *b2, *b2));

  }

  //@ assert trans_totoI(x, *b2);

  return;

}