CristalCaveGem » LustreC » Lustrec-Tests

node top(input1, input2, input3: real) returns (output: real);

var

  equalized1, equalized2, equalized3 : real;

  equalization1, equalization2, equalization3 : real;

  satCentering, centering : real;

  df1, df2, df3 : real;

  st1, st2, st3 : real;

  c1, c2, c3 : bool;

  d1, d2, d3 : bool;

--  check: bool;

  pre_equalization1, pre_equalization2, pre_equalization3 : real; -- mem

  pre_st1, pre_st2, pre_st3 : real;                               -- mem 

  pre_satCentering : real;                                        -- mem

let

  assert (input1 <  0.2); 

  assert (input1 > -0.2); 

  assert (input2 <  0.2); 

  assert (input2 > -0.2); 

  assert (input3 <  0.2); 

  assert (input3 > -0.2);

 --! /salsa/ranges/input1/: (-0.2, 0.2);

 --! /salsa/ranges/input2/: (-0.2, 0.2);

 --! /salsa/ranges/input3/: (-0.2, 0.2);

 --! /salsa/ranges/output/: (-0.6, 0.6);

 --! /salsa/ranges/pre_equalization1/: (-0.4, 0.4);

 --! /salsa/ranges/pre_st1/: (-0.5, 0.5);

 --! /salsa/ranges/pre_equalization2/: (-0.4, 0.4);

 --! /salsa/ranges/pre_st2/: (-0.5, 0.5);

 --! /salsa/ranges/pre_equalization3/: (-0.4, 0.4);

 --! /salsa/ranges/pre_st3/: (-0.5, 0.5);

 --! /salsa/ranges/pre_satCentering/: (-0.25, 0.25);

  pre_equalization1 = pre equalization1;

  pre_st1 =           pre st1;

  pre_equalization2 = pre equalization2;

  pre_st2 =           pre st2;

  pre_equalization3 = pre equalization3;

  pre_st3 =           pre st3;

  pre_satCentering =  pre satCentering;

  equalized1 = input1 - equalization1;

  df1 = equalized1 - output;

  st1 = if (df1 > 0.5) then 0.5 else (if (df1 < -0.5) then -0.5 else df1);

  equalization1 = 0.0 -> pre_equalization1 + (pre_st1 - pre_satCentering) * 0.05;

  equalized2 = input2 - equalization2;

  df2 = equalized2 - output;

  st2 = if (df2 > 0.5) then 0.5 else (if (df2 < -0.5) then -0.5 else df2);

  equalization2 = 0.0 -> pre_equalization2 + (pre_st2 - pre_satCentering) * 0.05;

  equalized3 = input3 - equalization3;

  df3 = equalized3 - output;

  st3 = if (df3 > 0.5) then 0.5 else (if (df3 < -0.5) then -0.5 else df3);

  equalization3 = 0.0 -> pre_equalization3 + (pre_st3 - pre_satCentering) * 0.05;

  c1 = equalized1 > equalized2;

  c2 = equalized2 > equalized3;

  c3 = equalized3 > equalized1;

  output = if (c1 = c2) then equalized2 else (if (c2 = c3) then equalized3 else equalized1);

  d1 = equalization1 > equalization2;

  d2 = equalization2 > equalization3;

  d3 = equalization3 > equalization1;

  centering = if (d1 = d2) then equalization2 else (if (d2 = d3) then equalization3 else equalization1);

  satCentering = if (centering > 0.25) then 0.25 else (if (centering < -0.25) then -0.25 else centering);

  -- check = ( equalization1 <=  2.0 * 0.2) and

  --         ( equalization1 >= -2.0 * 0.2) and

  --         ( equalization2 <=  2.0 * 0.2) and

  --         ( equalization2 >= -2.0 * 0.2) and

  --         ( equalization3 <=  2.0 * 0.2) and

  --         ( equalization3 >= -2.0 * 0.2);

--% prove(check);

--%MAIN;

tel