CristalCaveGem » LustreC

node top

  (beacon: bool;

  second: bool)

returns

  (OK: bool);

var

  V19_late: bool;

  V20_early: bool;

  V63_diff: int;

  V64_incr: int;

  V65_PC: int;

  V54_second: bool;

let

  OK = (true -> ((not V19_late) and (pre V20_early)));

  V19_late = (false -> (if (pre V19_late) then (V63_diff < 0) else (V63_diff <= 

  -10)));

  V20_early = (false -> (if (pre V20_early) then (V63_diff > 0) else (V63_diff 

  >= 10)));

  V63_diff = (if false then 0 else (if (beacon and V54_second) then (V65_PC + 

  V64_incr) else V65_PC));

  V64_incr = (if (beacon and (not V54_second)) then 1 else (if (V54_second and 

  (not beacon)) then 2 else 0));

  V65_PC = (0 -> (pre V63_diff));

  V54_second = (not second);

tel