CristalCaveGem » LustreC

node First( X : int ) returns ( First : int );

let

    First = X -> pre First;

tel

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

let

    Sofar = X -> X or pre Sofar;

tel

node excludes6( X1, X2, X3, X4, X5, X6 : bool ) returns ( excludes : bool );

let

    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 or

                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 or

              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 or

              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 or

              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 or

              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 or

              not X1 and not X2 and not X3 and not X4 and not X5 and     X6;

tel

node swimingpool(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)returns 

(x1, x2, x3, x4, x5, x6, x7, p1, p2 : int);

var

	g1, g2, g3, g4, g5, g6 : bool;

let

	g1 = false -> pre x6>=1;

	g2 = false -> pre x1>=1 and pre x7>=1;

	g3 = false -> pre x2>=1;

	g4 = false -> pre x3>=1 and pre x6>=1;

	g5 = false -> pre x4>=1;

	g6 = false -> pre x5>=1;

	x1 = 0 -> 

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

	if(e2) then if(g2) then pre x1-1 else pre x1 else 

	pre x1;

	x2 = 0 -> 

	if(e2) then if(g2) then pre x2+1 else pre x2 else 

	if(e3) then if(g3) then pre x2-1 else pre x2 else 

	pre x2;

	x3 = 0 -> 

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

	if(e4) then if(g4) then pre x3-1 else pre x3 else 

	pre x3;

	x4 = 0 -> 

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

	if(e5) then if(g4) then pre x4-1 else pre x4 else 

	pre x4;

	x5 = 0 -> 

	if(e5) then if(g5) then pre x5+1 else pre x5 else 

	if(e6) then if(g6) then pre x5-1 else pre x5 else 

	pre x5;

	x6 = p1 -> 

	if(e1) then if(g1) then pre x6-1 else pre x6 else 

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

	if(e4) then if(g4) then pre x6-1 else pre x6 else 

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

	pre x6;

	x7 = p2 -> 

	if(e2) then if(g2) then pre x7-1 else pre x7 else 

	if(e5) then if(g5) then pre x7+1 else pre x7 else 

	pre x7;

	p1 = init_p1 -> 

	pre p1;

	p2 = init_p2 -> 

	pre p2;

tel

node top(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)

returns ( OK : bool );

    var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int;

        env : bool;

let

    (x1, x2, x3, x4, x5, x6, x7, p1, p2) =

        swimingpool(e1, e2, e3, e4, e5, e6, init_p1, init_p2);

    env = Sofar( excludes6( e1, e2, e3, e4, e5, e6 ) ) and

          0 <= First(init_p1) and 0 <= First(init_p2) and First(init_p1) < 1000 and First(init_p2) < 1000;

    OK = env => x5 < 1;

  --%MAIN;

  --%PROPERTY  OK=true;

tel