CristalCaveGem » LustreC » Lustrec-Tests

node b2i (b: bool) returns (i: int);

-- 0

let i = if b then 1 else 0;  tel;

node Since (p: bool) returns (r: int);

-- 0

var __abs_1: int; __abs_0: bool;

let

  (__abs_1) = b2i(__abs_0);

  __abs_0 = p;

  r = (__abs_1 -> if p then 1 else if (pre(r) = 0) then 0 else (pre(r) + 1));

tel;

node SinceGTOrZero (in: bool; min: int) returns (out: bool);

-- 1

var __abs_1: int; __abs_0: bool;

let

  (__abs_1) = Since(__abs_0);

  __abs_0 = in;

  out = ((__abs_1 > min) or (__abs_1 = 0));

tel;

node Changed (p: bool) returns (r: bool);

-- 0

let r = (false -> (not (p = pre(p))));  tel;

node SinceLENotZero (in: bool; max: int) returns (out: bool);

-- 1

var __abs_1: int; __abs_0: bool;

let

  (__abs_1) = Since(__abs_0);

  __abs_0 = in;

  out = ((__abs_1 <= max) and (__abs_1 > 0));

tel;

node Rise (p: bool) returns (r: bool);

-- 0

let r = (false -> ((not pre(p)) and p));  tel;

node Fall (p: bool) returns (r: bool);

-- 0

let r = (false -> ((not p) and pre(p)));  tel;

node PFS_oracle

  (TS: bool; LPFS: bool; RPFS: bool)

returns

  (output_global: bool;

   output_inhibited_R2_R3: bool;

   output_unchanged_nop_R5: bool;

   output_change_R3_Rise: bool;

   output_change_R3_Fall: bool);

-- 2 1

-- 

-- 

-- 

-- 

var

  __abs_1: bool;

  __abs_3: bool;

  __abs_5: int;

  __abs_7: bool;

  __abs_9: bool;

  __abs_12: bool;

  __abs_13: bool;

  __abs_14: bool;

  __abs_17: bool;

  __abs_18: bool;

  __abs_19: bool;

  __abs_23: bool;

  __abs_24: bool;

  __abs_25: bool;

  __abs_28: bool;

  __abs_33: bool;

  __abs_0: bool;

  __abs_2: bool;

  __abs_4: bool;

  __abs_6: bool;

  __abs_8: bool;

  __abs_11: bool;

  __abs_15: int;

  __abs_16: bool;

  __abs_21: int;

  __abs_22: bool;

  __abs_26: int;

  __abs_27: bool;

  __abs_32: int;

let

  (__abs_3) = Rise(__abs_2);

  (__abs_1) = Rise(__abs_0);

  (__abs_14) = Fall(__abs_0);

  (__abs_13) = Fall(__abs_2);

  (__abs_9) = Fall(__abs_8);

  (__abs_7) = Fall(__abs_6);

  (__abs_5) = Since(__abs_4);

  (__abs_19) = Rise(__abs_8);

  (__abs_18) = Rise(__abs_6);

  (__abs_17) = SinceGTOrZero(__abs_16, __abs_15);

  (__abs_12) = Rise(__abs_11);

  (__abs_23) = SinceGTOrZero(__abs_22, __abs_21);

  (__abs_28) = SinceLENotZero(__abs_27, __abs_26);

  (__abs_25) = Changed(__abs_8);

  (__abs_24) = Changed(__abs_6);

  (__abs_33) = SinceGTOrZero(__abs_22, __abs_32);

  __abs_8 = LPFS;

  __abs_6 = RPFS;

  __abs_2 = (false -> pre(RPFS));

  __abs_0 = (true -> pre(LPFS));

  __abs_4 = (__abs_1 or __abs_3);

  output_change_R3_Fall =

    ((__abs_5 = 1) => (__abs_7 or (__abs_9 and (not (__abs_7 and __abs_9)))));

  __abs_15 = 4;

  __abs_11 = TS;

  output_change_R3_Rise =

    ((__abs_17 and __abs_12) =>

      (__abs_18 or (__abs_19 and (not (__abs_18 and __abs_19)))));

  __abs_21 = 3;

  output_unchanged_nop_R5 = (__abs_23 => (not (__abs_24 or __abs_25)));

  __abs_26 = 2;

  output_inhibited_R2_R3 =

    (true -> (__abs_28 => (not (__abs_24 or __abs_25))));

  __abs_32 = 1;

  output_global =

    ((((__abs_33 => (LPFS = (not RPFS))) and (LPFS or RPFS)) and

       (LPFS and (not RPFS)))

     ->

     ((__abs_33 => (LPFS = (not RPFS))) and (LPFS or RPFS)));

  __abs_22 = __abs_12;

  __abs_27 = (__abs_14 or __abs_13);

  __abs_16 = (__abs_13 or __abs_14);

  --%MAIN

tel;