CristalCaveGem » LustreC

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 readwrite(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool)

returns(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int);

var

   garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8, garde9 : bool;

let

   garde1 = pre x0>=1;

   garde2 = pre x1>=1 and pre x4>=1;

   garde3 = pre x2>=1 and pre x11>=1;

   garde4 = pre x1>=1;

   garde5 = pre x6>=1;

   garde6 = pre x3>=1 and pre x7>=1;

   garde7 = pre x8>=1 and pre x12>=1;

   garde8 = pre x4>=5 and pre x5>=1 and pre x7>=1;

   garde9 = pre x9>=1 and pre x10>=1;

   x0 = 0 -> 

   if(etat1) then if(garde1) then pre x0-1 else pre x0 else 

   if(etat2) then if(garde2) then pre x0+1 else pre x0 else 

   pre x0;

   x1 = 0 -> 

   if(etat1) then if(garde1) then pre x1+1 else pre x1 else 

   if(etat2) then if(garde2) then pre x1-1 else pre x1 else 

   if(etat3) then if(garde3) then pre x1+1 else pre x1 else 

   if(etat4) then if(garde4) then pre x1-1 else pre x1 else 

   pre x1;

   x2 = 1 -> 

   if(etat3) then if(garde3) then pre x2-1 else pre x2 else 

   if(etat4) then if(garde4) then pre x2+1 else pre x2 else 

   pre x2;

   x3 = 0 -> 

   if(etat2) then if(garde2) then pre x3+1 else pre x3 else 

   if(etat6) then if(garde6) then pre x3-1 else pre x3 else

   pre x3;

   x4 = 0 -> 

   if(etat2) then if(garde2) then pre x4-1 else pre x4 else 

   if(etat6) then if(garde6) then pre x4+1 else pre x4 else 

   if(etat7) then if(garde7) then pre x4+5 else pre x4 else 

   if(etat8) then if(garde8) then pre x4-5 else pre x4 else 

   pre x4;

   x5 = 0 -> 

   if(etat4) then if(garde5) then pre x5+1 else pre x5 else 

   if(etat8) then if(garde8) then pre x5-1 else pre x5 else 

   pre x5;

   x6 = 0 -> 

   if(etat5) then if(garde5) then pre x6-1 else pre x6 else 

   if(etat6) then if(garde6) then pre x6+1 else pre x6 else 

   pre x6;

   x7 = 0 -> 

   if(etat5) then if(garde5) then pre x7+1 else pre x7 else 

   if(etat6) then if(garde6) then pre x7-1 else pre x7 else 

   if(etat7) then if(garde7) then pre x7+1 else pre x7 else 

   if(etat8) then if(garde8) then pre x7-1 else pre x7 else 

   pre x7;

   x8 = 1 -> 

   if(etat7) then if(garde7) then pre x8-1 else pre x8 else 

   if(etat8) then if(garde8) then pre x8+1 else pre x8 else 

   pre x8;

   x9 = 0 -> 

   if(etat4) then if(garde4) then pre x9+1 else pre x9 else 

   if(etat9) then if(garde9) then pre x9-1 else pre x9 else 

   pre x9;

   x10 = 0 -> 

   if(etat8) then if(garde8) then pre x10+1 else pre x10 else 

   if(etat9) then if(garde9) then pre x10-1 else pre x10 else 

   pre x10;

   x11 = 1 -> 

   if(etat3) then if(garde3) then pre x11-1 else pre x11 else 

   if(etat9) then if(garde9) then pre x11+1 else pre x11 else 

   pre x11;

   x12 = 1 -> 

   if(etat7) then if(garde7) then pre x12-1 else pre x12 else 

   if(etat9) then if(garde9) then pre x12+1 else pre x12 else 

   pre x12;

tel

node top(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9 : bool)

returns ( OK : bool );

   var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 : int;

       env : bool;

let

   (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) =

      readwrite(etat1, etat2, etat3, etat4, etat5, etat6, etat7, etat8, etat9);

   env =  Sofar( excludes9(etat1, etat2, etat3, etat4, etat5,

                           etat6, etat7, etat8, etat9) and

                 x0 > -32768 and x1 > -32768 and x2 > -32768 and

                 x3 > -32768 and x4 > -32768 and x5 > -32768 and

                 x6 > -32768 and x7 > -32768 and x8 > -32768 and

                 x0 < 32767 and x1 < 32767 and x3 < 32767 and x4 < 32767 and

                 x5 < 32767 and x6 < 32767 and x7 < 32767 and x8 < 32767 and

                 x9 < 32767 and x10 < 32767 and x11 < 32767 and x12 < 32767);

   OK = x0 >= 0;

   --%PROPERTY OK=true;

   --%MAIN;

tel