CristalCaveGem » LustreC

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

returns (OK: bool);

var

  MayMove1, MayMove2: bool;

  start1, start2, stop, moving: bool;

let

  MayMove1 = TryToMove1 and MaySafelyMove;

  MayMove2 = TryToMove2 and MaySafelyMove;

  moving = sustain(start1 and start2, stop);

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

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

  stop = fedge(MayMove1) and 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;

tel