CristalCaveGem » LustreC » Lustrec-Tests

node Sofar( X : bool ) returns ( Sofar : bool );

let

    Sofar = X -> X and pre Sofar;

tel

node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool );

let

    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 and not X7 and not X8 and not X9 or

              not X1 and not X2 and not X3 and not X4 and not X5 and     X6 and not X7 and not X8 and not X9 or

              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and     X7 and not X8 and not X9 or

              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and     X8 and not X9 or

              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and     X9;

tel

node ticket3i(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;

init_a1, init_a2, init_a3, init_t : int) returns (

p1, p2, p3, t, s, a1, a2, a3 : int; erreur_ticket3i : bool);

var

   g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool;

let

   erreur_ticket3i = if((p1>=3) or (p2>=3) or (p3>=3)) then true else false;

   g1 = pre p1 = 0;

   g2 = pre p1 = 1 and pre s >= a1;

   g3 = pre p1 = 2;

   g4 = pre p2 = 0;

   g5 = pre p2 = 1 and pre s >= a2;

   g6 = pre p2 = 2;

   g7 = pre p3 = 0;

   g8 = pre p3 = 1 and pre s >= a3;

   g9 = pre p3 = 2;

   p1 = 0 -> 

   if(e1) then if(g1) then 1 else pre p1 else 

   if(e2) then if(g2) then 2 else pre p1 else 

   if(e3) then if(g3) then 0 else pre p1 else 

   pre p1;

   p2 = 0 -> 

   if(e4) then if(g4) then 1 else pre p2 else 

   if(e5) then if(g5) then 2 else pre p2 else 

   if(e6) then if(g6) then 0 else pre p2 else 

   pre p2;

   p3 = 0 -> 

   if(e7) then if(g7) then 1 else pre p3 else 

   if(e8) then if(g8) then 2 else pre p3 else 

   if(e9) then if(g9) then 0 else pre p3 else 

   pre p3;

   t = init_t -> 

   if(e1) then if(g1) then pre t+1 else pre t else 

   if(e4) then if(g4) then pre t+1 else pre t else 

   if(e7) then if(g7) then pre t+1 else pre t else 

   pre t;

   s = t -> 

   if(e3) then if(g3) then pre s+1 else pre s else 

   if(e6) then if(g6) then pre s+1 else pre s else 

   if(e9) then if(g9) then pre s+1 else pre s else 

   pre s;

   a1 = init_a1 -> 

   if(e1) then if(g1) then pre t else pre a1 else 

   pre a1;

   a2 = init_a2 -> 

   if(e4) then if(g4) then pre t else pre a2 else 

   pre a2;

   a3 = init_a3 -> 

   if(e7) then if(g7) then pre t else pre a3 else 

   pre a3;

tel

--@ ensures OK;

node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;

         init_a1, init_a2, init_a3, init_t : int )

returns ( OK : bool );

    var p1, p2, p3, t, s, a1, a2, a3 : int;

        erreur_ticket3i : bool;

        env : bool;

let

    ( p1, p2, p3, t, s, a1, a2, a3 , erreur_ticket3i ) =

        ticket3i( e1, e2, e3, e4, e5, e6, e7, e8, e9,

                  init_a1, init_a2, init_a3, init_t );

    env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and

                 init_a1 >= 0 and

                 init_a2 >= 0 and

                 init_a3 >= 0 and

                 init_t >= 0 );

    OK = env => not erreur_ticket3i and

                  0 <= p1 and p1 <= 3 and

                  0 <= p2 and p2 <= 3 and

                  0 <= p3 and p3 <= 3 and

                  p1 + p2 + p3 <= 9;

    --%PROPERTY OK=true;

    --%MAIN;

tel