CristalCaveGem » LustreC » Lustrec-Tests

--

-- Source: David Merchat (node voiture + property v6)

--

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

let

    Sofar = X -> X and pre Sofar;

tel

node excludes2( X1, X2 : bool ) returns ( excludes : bool );

let

    excludes = not ( X1 and X2 );

tel

node voiture(m,s: bool) returns

(   toofast, stop, bump: bool;

    dist, speed, time: int;

    move: bool; second, meter: bool );

let

  meter = false -> (m and not s);

  second = false -> s;

  move = true -> pre(move and not stop and not toofast and not bump);

  dist = 0 -> if move and meter then pre(dist)+1

			   else pre(dist);

  speed = 0 -> if not move or second then 0

		else if move and meter then pre(speed) + 1

		else pre(speed);

  time = 0 -> if second then pre(time) + 1

		else pre(time);

  toofast = speed >= 3;

  stop = time >= 4;

  bump = dist = 10;

tel

-- Can't prove in luke-bitvec, luke-hybrid, nbac

node top(m, s : bool) returns (OK : bool);

--@ contract guarantees OK;

var toofast, stop, bump: bool;

    dist, speed, time: int;

    move: bool; second, meter: bool;

    env : bool;

let

  (toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s);

  env = Sofar( excludes2( m, s ) );

  OK = env => (dist > 9 => not( move and meter));

  --%PROPERTY OK=true;

  --%MAIN;

tel