CristalCaveGem » LustreC

-- From

-- Production Cell in Lustre: A Case Study, by Leszek Holenderski

-- Published in Formal Development of Reactive Systems, Claus Lewerentz and

-- Thomas Lindner (eds.), Springer-Verlag, LNCS 891, 1995.

node redge (signal: bool) returns (r: bool);

let

  r = signal -> (signal and pre(not signal));

tel

node fedge (signal: bool) returns (f: bool);

let

  f = redge(not signal);

tel

node sustain (on, off: bool) returns (s: bool);

let

  s = on -> if on then true else if off then false else pre(s);

tel

--@ ensures OK;

node top (MaySafelyMove, TryToMove1, TryToMove2: bool)

returns (OK: bool);

var

  MayMove1, MayMove2: bool;

  start1, start2, stop, moving: bool;

let

  MayMove1 = TryToMove1 and MaySafelyMove;

  MayMove2 = TryToMove2 and MaySafelyMove;

  moving = sustain(start1 or start2, stop);

  start1 = redge(MayMove1 and (true -> pre(not TryToMove2)));

  start2 = redge(MayMove2 and (true -> pre(not TryToMove1)));

  stop = fedge(MayMove1) or fedge(MayMove2);

  OK = true -> if (not redge(TryToMove1) or not redge(TryToMove2)) then (

         ((not start1 and not start2) or (not start2 and not stop) 

            or (not start1 and not stop))

         and not (start1 and start2 and stop) 

         and if moving then MaySafelyMove else true)

         else true;

  --%MAIN;

  --%PROPERTY OK=true;

--  assert #(redge(TryToMove1), redge(TryToMove2));

--  OK = #(start1, start2, stop) and

--         if moving then MaySafelyMove else true;

tel