CristalCaveGem » LustreC

node top

  (beacon: bool;

  second: bool)

returns

  (OK: bool);

var

  V19_late: bool;

  V20_early: bool;

  V64_diff: int;

  V65_incr: int;

  V66_PC: int;

let

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

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

  -10)));

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

  >= 11)));

  V64_diff = (if false then 0 else (if (beacon or second) then (V66_PC + 

  V65_incr) else V66_PC));

  V65_incr = (if (beacon and (not second)) then 1 else (if (second and (not 

  beacon)) then 2 else 0));

  V66_PC = (0 -> (pre V64_diff));

tel