CristalCaveGem » LustreC » Lustrec-Tests

* Available examples:

- linear cases: Pierre Roux's examples as well as YAsmine Seladji ones

- piecewise lin cases:

  - Saturations or reset of the former category

  - Triplex voter (Honeywell/Rockwell)

TODO:

- extract lustre modeling of the matlab code of Assale: 

  - svn/numericaltools/PiecewiseLyapunov/code/matlab/Code2/Examples/

    - running_example.m

    - exampleMignoneinvariance1.m (or variants)

- same thing for the work with Assale + Victor:

  - git/laas/progcertsos/script/example

- last, the examples of the paper with Victor

- Why not building examples with non polynomial computations and

  extract the proper math. model?

* Run

source `lustrev -version | grep "Standard lib"| sed "s/.*: //"`/z3librc

lustrev -seal -node top linear/ex1.lus

node top(in4_0 : real) returns (x4_0, x4_1, x4_2, in1_0, x1_0, x1_1 : real);

let

  assert(in4_0 >= -1. and in4_0 <= 1.);

  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;

  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;

  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;

  in1_0 = in4_0 -> 0.3 * x4_1;

  x1_0 = 0. -> 1.5 * pre x1_0 - 0.7 * pre x1_1 + 1.6 * in1_0;

  x1_1 = 0. -> pre x1_0;

tel

node top(in4_0 : real) returns (x4_0, x4_1, x4_2, in42_0, x42_0, x42_1, x42_2 : real);

let

  assert(in4_0 >= -1. and in4_0 <= 1.);

  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;

  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;

  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;

  in42_0 = in4_0 -> 0.3 * x4_1;

  x42_0 = 0. -> 0.9371 * pre x42_0 - 0.0377 * pre x42_1 - 0.0411 * pre x42_2 + 0.0237 * in42_0;

  x42_1 = 0. -> -0.0399 * pre x42_0 + 0.960 * pre x42_1 - 0.0172 * pre x42_2 + 0.0143 * in42_0;

  x42_2 = 0. -> 0.0140 * pre x42_0 - 0.0193 * pre x42_1 + 0.9821 * pre x42_2 + 0.0077 * in42_0;

tel

node top(in4_0 : real) returns (x4_0, x4_1, x4_2, inl2_0, yn, ynm1, xnm1, xnm2 : real);

let

  assert(in4_0 >= -1. and in4_0 <= 1.);

  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;

  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;

  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;

  inl2_0 = in4_0 -> 0.3 * x4_1;

  yn = 0. -> 0.21875*inl2_0 + 0.40625*pre xnm1 + 0.21875*pre xnm2 + 0.375*pre yn - 0.1875*pre ynm1;

  ynm1 = 0. -> pre yn;

  xnm1 = 0. -> inl2_0;

  xnm2 = 0. -> pre xnm1;

tel

node top(in5_0, in5_1 : real) returns (x5_0, x5_1, x5_2, x5_3, in4_0, x4_0, x4_1, x4_2 : real);

let

  assert(in5_0 >= -1. and in5_0 <= 1.);

  assert(in5_1 >= -1. and in5_1 <= 1.);

  x5_0 = 0. -> 0.6227 * pre x5_0 + 0.3871 * pre x5_1 - 0.113 * pre x5_2 + 0.0102 * pre x5_3 + 0.3064 * in5_0 + 0.1826 * in5_1;

  x5_1 = 0. -> -0.3407 * pre x5_0 + 0.9103 * pre x5_1 - 0.3388 * pre x5_2 + 0.0649 * pre x5_3 - 0.0054 * in5_0 + 0.6731 * in5_1;

  x5_2 = 0. -> 0.0918 * pre x5_0 - 0.0265 * pre x5_1 - 0.7319 * pre x5_2 + 0.2669 * pre x5_3 + 0.0494 * in5_0 + 1.6138 * in5_1;

  x5_3 = 0. -> 0.2643 * pre x5_0 - 0.1298 * pre x5_1 - 0.9903 * pre x5_2 + 0.3331 * pre x5_3 - 0.0531 * in5_0 + 0.4012 * in5_1;

  in4_0 = in5_0 -> 0.3 * x5_2;

  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;

  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;

  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;

tel

node top(in5_0, in5_1 : real) returns (x5_0, x5_1, x5_2, x5_3, in6_0, x6_0, x6_1, x6_2, x6_3, x6_4 : real);

let

  assert(in5_0 >= -1. and in5_0 <= 1.);

  assert(in5_1 >= -1. and in5_1 <= 1.);

  x5_0 = 0. -> 0.6227 * pre x5_0 + 0.3871 * pre x5_1 - 0.113 * pre x5_2 + 0.0102 * pre x5_3 + 0.3064 * in5_0 + 0.1826 * in5_1;

  x5_1 = 0. -> -0.3407 * pre x5_0 + 0.9103 * pre x5_1 - 0.3388 * pre x5_2 + 0.0649 * pre x5_3 - 0.0054 * in5_0 + 0.6731 * in5_1;

  x5_2 = 0. -> 0.0918 * pre x5_0 - 0.0265 * pre x5_1 - 0.7319 * pre x5_2 + 0.2669 * pre x5_3 + 0.0494 * in5_0 + 1.6138 * in5_1;

  x5_3 = 0. -> 0.2643 * pre x5_0 - 0.1298 * pre x5_1 - 0.9903 * pre x5_2 + 0.3331 * pre x5_3 - 0.0531 * in5_0 + 0.4012 * in5_1;

  in6_0 = in5_0 -> 0.3 * x5_1;

  x6_0 = 0. -> 0.4250 * pre x6_0 + 0.8131 * in6_0;

  x6_1 = 0. -> 0.3167 * pre x6_0 + 0.1016 * pre x6_1 - 0.4444 * pre x6_2 + 0.1807 * in6_0;

  x6_2 = 0. -> 0.1278 * pre x6_0 + 0.4444 * pre x6_1 + 0.8207 * pre x6_2 + 0.0729 * in6_0;

  x6_3 = 0. -> 0.0365 * pre x6_0 + 0.1270 * pre x6_1 + 0.5202 * pre x6_2 + 0.4163 * pre x6_3 - 0.5714 * pre x6_4 + 0.0208 * in6_0;

  x6_4 = 0. -> 0.0147 * pre x6_0 + 0.0512 * pre x6_1 + 0.2099 * pre x6_2 + 0.57104 * pre x6_3 + 0.7694 * pre x6_4 + 0.0084 * in6_0;

tel

node top(in6_0 : real) returns (x6_0, x6_1, x6_2, x6_3, x6_4, inl2_0, yn, ynm1, xnm1, xnm2 : real);

let

  assert(in6_0 >= -1. and in6_0 <= 1.);

  x6_0 = 0. -> 0.4250 * pre x6_0 + 0.8131 * in6_0;

  x6_1 = 0. -> 0.3167 * pre x6_0 + 0.1016 * pre x6_1 - 0.4444 * pre x6_2 + 0.1807 * in6_0;

  x6_2 = 0. -> 0.1278 * pre x6_0 + 0.4444 * pre x6_1 + 0.8207 * pre x6_2 + 0.0729 * in6_0;

  x6_3 = 0. -> 0.0365 * pre x6_0 + 0.1270 * pre x6_1 + 0.5202 * pre x6_2 + 0.4163 * pre x6_3 - 0.5714 * pre x6_4 + 0.0208 * in6_0;

  x6_4 = 0. -> 0.0147 * pre x6_0 + 0.0512 * pre x6_1 + 0.2099 * pre x6_2 + 0.57104 * pre x6_3 + 0.7694 * pre x6_4 + 0.0084 * in6_0;

  inl2_0 = in6_0 -> 0.3 * x6_2;

  yn = 0. -> 0.21875*inl2_0 + 0.40625*pre xnm1 + 0.21875*pre xnm2 + 0.375*pre yn - 0.1875*pre ynm1;

  ynm1 = 0. -> pre yn;

  xnm1 = 0. -> inl2_0;

  xnm2 = 0. -> pre xnm1;

tel

node top(in0 : real) returns (x, y : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x = 0. -> 1.5 * pre x - 0.7 * pre y + 1.6 * in0;

  y = 0. -> pre x;

tel

#open "libarrays"

node ctl(in0 : real^1^1) returns (mem : real^2^1);

var _A:  real^2^2;

    _B:  real^2^1;

let

  _A = [[1.5, 1.],  [-0.7, 0.]]; 

  _B = [[1.6, 0.]]; 

   assert(in0[0][0] >= -1. and in0[0][0] <= 1.);

   mem = [[0., 0.]] -> _MatMul_real(2, 2, 1,  _A,  pre mem) + _MatMul_real(2, 1, 1, _B,  in0);

tel

node top(in0 : real) returns (x,  y:  real);

var res:  real^2^1;

let

  res = ctl([[in0]]);

  x = res[0][0];

  y = res[0][1];

tel

node top(in0 : real) returns (x0, x1, x2, x3 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 1.5 * pre x0 - 0.7 * pre x1 - 0.7 * pre x2 + 0.4 * pre x3 + 0.5 * in0;

  x1 = 0. -> pre x0;

  x2 = 0. -> in0;

  x3 = 0. -> pre x2;

tel

node top(in0 : real) returns (x0, x1 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 0.499 * pre x0 - 0.05 * pre x1 + in0;

  x1 = 0. -> 0.01 * pre x0 + pre x1;

tel

node top(in0 : real) returns (x0, x1, x2 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 0.9379 * pre x0 - 0.0381 * pre x1 - 0.0414 * pre x2 + 0.0237 * in0;

  x1 = 0. -> -0.0404 * pre x0 + 0.968 * pre x1 - 0.0179 * pre x2 + 0.0143 * in0;

  x2 = 0. -> 0.0142 * pre x0 - 0.0197 * pre x1 + 0.9823 * pre x2 + 0.0077 * in0;

tel

node top(in0, in1 : real) returns (x0, x1, x2, x3 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  assert(in1 >= -1. and in1 <= 1.);

  x0 = 0. -> 0.6227 * pre x0 + 0.3871 * pre x1 - 0.113 * pre x2 + 0.0102 * pre x3 + 0.3064 * in0 + 0.1826 * in1;

  x1 = 0. -> -0.3407 * pre x0 + 0.9103 * pre x1 - 0.3388 * pre x2 + 0.0649 * pre x3 - 0.0054 * in0 + 0.6731 * in1;

  x2 = 0. -> 0.0918 * pre x0 - 0.0265 * pre x1 - 0.7319 * pre x2 + 0.2669 * pre x3 + 0.0494 * in0 + 1.6138 * in1;

  x3 = 0. -> 0.2643 * pre x0 - 0.1298 * pre x1 - 0.9903 * pre x2 + 0.3331 * pre x3 - 0.0531 * in0 + 0.4012 * in1;

tel

node top(in0 : real) returns (x0, x1, x2, x3, x4 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 0.4250 * pre x0 + 0.8131 * in0;

  x1 = 0. -> 0.3167 * pre x0 + 0.1016 * pre x1 - 0.4444 * pre x2 + 0.1807 * in0;

  x2 = 0. -> 0.1278 * pre x0 + 0.4444 * pre x1 + 0.8207 * pre x2 + 0.0729 * in0;

  x3 = 0. -> 0.0365 * pre x0 + 0.1270 * pre x1 + 0.5202 * pre x2 + 0.4163 * pre x3 - 0.5714 * pre x4 + 0.0208 * in0;

  x4 = 0. -> 0.0147 * pre x0 + 0.0512 * pre x1 + 0.2099 * pre x2 + 0.57104 * pre x3 + 0.7694 * pre x4 + 0.0084 * in0;

tel

node top(ix0, ix1 : real) returns (x0, x1 : real);

let

  assert(ix0 > 0. and ix0 < 1.);

  assert(ix1 > 0. and ix1 < 1.);

  x0 = ix0 -> pre x0 + 0.01 * pre x1;

  x1 = ix1 -> -0.01 * pre x0 + 0.99 * pre x1;

tel

node top(ix0, ix1 : real) returns (x0, x1 : real);

let

  assert(ix0 > 0. and ix0 < 1.);

  assert(ix1 > 0. and ix1 < 1.);

  x0 = ix0 -> 0.95 * pre x0 + 0.09975 * pre x1;

  x1 = ix1 -> -0.1 * pre x0 + 0.95 * pre x1;

tel

node top(xn : real) returns (yn, xnm1, xnm2, ynm1 : real);

let

  assert(xn >= -1.6 and xn <= 1.6);

  yn = 0. -> 0.21875*xn + 0.40625*pre xnm1 + 0.21875*pre xnm2 + 0.375*pre yn - 0.1875*pre ynm1;

  ynm1 = 0. -> pre yn;

  xnm1 = 0. -> xn;

  xnm2 = 0. -> pre xnm1;

tel

node top(xn : real) returns (yn, ynm1, ynm2, ynm3, xnm1, xnm2, xnm3, xnm4 : real);

let

  assert(xn >= -1.0 and xn <= 1.0);

  yn = 0. -> 0.046582906636443676*xn + 0.1863316265457747*pre xnm1 + 0.27949743981866204*pre xnm2 + 0.1863316265457747*pre xnm3 + 0.046582906636443676*pre xnm4 + 0.7820951980233379*pre yn - 0.6799785269162999*pre ynm1 + 0.1826756977530325*pre ynm2 - 0.03011887504316928*pre ynm3;

  ynm1 = 0. -> pre yn;

  ynm2 = 0. -> pre ynm1;

  ynm3 = 0. -> pre ynm2;

  xnm1 = 0. -> xn;

  xnm2 = 0. -> pre xnm1;

  xnm3 = 0. -> pre xnm2;

  xnm4 = 0. -> pre xnm3;

tel

node top(xn : real) returns (yn, ynm1, ynm2, ynm3, xnm1, xnm2, xnm3, xnm4 : real);

let

  assert(xn >= -1.0 and xn <= 1.0);

  yn = 0. -> 0.027571327441965943*xn + 0.09946114577079751*pre xnm1 + 0.14434540411316932*pre xnm2 + 0.09946114577079751*pre xnm3 + 0.027571327441965943*pre xnm4 + 1.5881829830740517*pre yn - 1.7443826804178832*pre ynm1 + 1.0171424112847436*pre ynm2 - 0.3079664796302433*pre ynm3;

  ynm1 = 0. -> pre yn;

  ynm2 = 0. -> pre ynm1;

  ynm3 = 0. -> pre ynm2;

  xnm1 = 0. -> xn;

  xnm2 = 0. -> pre xnm1;

  xnm3 = 0. -> pre xnm2;

  xnm4 = 0. -> pre xnm3;

tel

node top(xn : real) returns (yn, ynm1, ynm2, ynm3, ynm4, ynm5, xnm1, xnm2, xnm3, xnm4, xnm5, xnm6 : real);

let

  assert(xn >= -1.0 and xn <= 1.0);

  yn = 0. -> 0.0071206017131343335*xn + 0.02429729818092203*pre xnm1 + 0.04613413371939573*pre xnm2 + 0.05613064430953349*pre xnm3 + 0.04613413371939573*pre xnm4 + 0.02429729818092203*pre xnm5 + 0.0071206017131343335*pre xnm6 - -2.7445577051566046*pre yn - 4.495158480897364*pre ynm1 - -4.649204375147074*pre ynm2 - 3.2299784258838873*pre ynm3 - -1.4088842648092799*pre ynm4 - 0.31451868286474205*pre ynm5;

  ynm1 = 0. -> pre yn;

  ynm2 = 0. -> pre ynm1;

  ynm3 = 0. -> pre ynm2;

  ynm4 = 0. -> pre ynm3;

  ynm5 = 0. -> pre ynm4;

  xnm1 = 0. -> xn;

  xnm2 = 0. -> pre xnm1;

  xnm3 = 0. -> pre xnm2;

  xnm4 = 0. -> pre xnm3;

  xnm5 = 0. -> pre xnm4;

  xnm6 = 0. -> pre xnm5;

tel

node top(r : bool; in0 : real) returns (x, y : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x = 0. -> if r then 1. else 1.5 * pre x - 0.7 * pre y + 1.6 * in0;

  y = 0. -> if r then 1. else pre x;

tel

node top(in0 : real) returns (sx, x, y : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x = 0. -> 1.5 * pre sx - 0.7 * pre y + 1.6 * in0;

  y = 0. -> pre x;

  sx = if x > 10. then 10. else if x < -10. then -10. else in0 + x;

tel

node top(r : bool; in0 : real) returns (x0, x1, x2, x3 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> if r then 1. else 1.5 * pre x0 - 0.7 * pre x1 - 0.7 * pre x2 + 0.4 * pre x3 + 0.5 * in0;

  x1 = 0. -> if r then 1. else pre x0;

  x2 = 0. -> if r then 1. else in0;

  x3 = 0. -> if r then 1. else pre x2;

tel

node top(in0 : real) returns (sx0, x0, x1, x2, x3 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 1.5 * pre sx0 - 0.7 * pre x1 - 0.7 * pre x2 + 0.4 * pre x3 + 0.5 * in0;

  x1 = 0. -> pre sx0;

  x2 = 0. -> in0;

  x3 = 0. -> pre x2;

  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;

tel

node top(r : bool; in0 : real) returns (x0, x1 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> if r then 1. else 0.499 * pre x0 - 0.05 * pre x1 + in0;

  x1 = 0. -> if r then 1. else 0.01 * pre x0 + pre x1;

tel

node top(in0 : real) returns (sx0, x0, x1 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 0.499 * pre sx0 - 0.05 * pre x1 + in0;

  x1 = 0. -> 0.01 * pre sx0 + pre x1;

  sx0 = if x0 > 50. then 50. else if x0 < -50. then -50. else x0;

tel

node top(r : bool; in0 : real) returns (x0, x1, x2 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> if r then 1. else 0.9379 * pre x0 - 0.0381 * pre x1 - 0.0414 * pre x2 + 0.0237 * in0;

  x1 = 0. -> if r then 1. else -0.0404 * pre x0 + 0.968 * pre x1 - 0.0179 * pre x2 + 0.0143 * in0;

  x2 = 0. -> if r then 1. else 0.0142 * pre x0 - 0.0197 * pre x1 + 0.9823 * pre x2 + 0.0077 * in0;

tel

node top(in0 : real) returns (sx0, x0, x1, x2 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 0.9379 * pre sx0 - 0.0381 * pre x1 - 0.0414 * pre x2 + 0.0237 * in0;

  x1 = 0. -> -0.0404 * pre sx0 + 0.968 * pre x1 - 0.0179 * pre x2 + 0.0143 * in0;

  x2 = 0. -> 0.0142 * pre sx0 - 0.0197 * pre x1 + 0.9823 * pre x2 + 0.0077 * in0;

  sx0 = if x0 > 50. then 50. else if x0 < -50. then -50. else x0;

tel

node top(r : bool; in0, in1 : real) returns (x0, x1, x2, x3 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  assert(in1 >= -1. and in1 <= 1.);

  x0 = 0. -> if r then 1. else

    0.6227 * pre x0 + 0.3871 * pre x1 - 0.113 * pre x2 + 0.0102 * pre x3 + 0.3064 * in0 + 0.1826 * in1;

  x1 = 0. -> if r then 1. else

    -0.3407 * pre x0 + 0.9103 * pre x1 - 0.3388 * pre x2 + 0.0649 * pre x3 - 0.0054 * in0 + 0.6731 * in1;

  x2 = 0. -> if r then 1. else

    0.0918 * pre x0 - 0.0265 * pre x1 - 0.7319 * pre x2 + 0.2669 * pre x3 + 0.0494 * in0 + 1.6138 * in1;

  x3 = 0. -> if r then 1. else

    0.2643 * pre x0 - 0.1298 * pre x1 - 0.9903 * pre x2 + 0.3331 * pre x3 - 0.0531 * in0 + 0.4012 * in1;

tel

node top(in0, in1 : real) returns (sx0, x0, x1, x2, x3 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  assert(in1 >= -1. and in1 <= 1.);

  x0 = 0. -> 0.6227 * pre sx0 + 0.3871 * pre x1 - 0.113 * pre x2 + 0.0102 * pre x3 + 0.3064 * in0 + 0.1826 * in1;

  x1 = 0. -> -0.3407 * pre sx0 + 0.9103 * pre x1 - 0.3388 * pre x2 + 0.0649 * pre x3 - 0.0054 * in0 + 0.6731 * in1;

  x2 = 0. -> 0.0918 * pre sx0 - 0.0265 * pre x1 - 0.7319 * pre x2 + 0.2669 * pre x3 + 0.0494 * in0 + 1.6138 * in1;

  x3 = 0. -> 0.2643 * pre sx0 - 0.1298 * pre x1 - 0.9903 * pre x2 + 0.3331 * pre x3 - 0.0531 * in0 + 0.4012 * in1;

  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;

tel

node top(r : bool; in0 : real) returns (x0, x1, x2, x3, x4 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> if r then 1. else 0.4250 * pre x0 + 0.8131 * in0;

  x1 = 0. -> if r then 1. else

    0.3167 * pre x0 + 0.1016 * pre x1 - 0.4444 * pre x2 + 0.1807 * in0;

  x2 = 0. -> if r then 1. else

    0.1278 * pre x0 + 0.4444 * pre x1 + 0.8207 * pre x2 + 0.0729 * in0;

  x3 = 0. -> if r then 1. else

    0.0365 * pre x0 + 0.1270 * pre x1 + 0.5202 * pre x2 + 0.4163 * pre x3 - 0.5714 * pre x4 + 0.0208 * in0;

  x4 = 0. -> if r then 1. else

    0.0147 * pre x0 + 0.0512 * pre x1 + 0.2099 * pre x2 + 0.57104 * pre x3 + 0.7694 * pre x4 + 0.0084 * in0;

tel

node top(in0 : real) returns (sx0, x0, x1, x2, x3, x4 : real);

let

  assert(in0 >= -1. and in0 <= 1.);

  x0 = 0. -> 0.4250 * pre sx0 + 0.8131 * in0;

  x1 = 0. -> 0.3167 * pre sx0 + 0.1016 * pre x1 - 0.4444 * pre x2 + 0.1807 * in0;

  x2 = 0. -> 0.1278 * pre sx0 + 0.4444 * pre x1 + 0.8207 * pre x2 + 0.0729 * in0;

  x3 = 0. -> 0.0365 * pre sx0 + 0.1270 * pre x1 + 0.5202 * pre x2 + 0.4163 * pre x3 - 0.5714 * pre x4 + 0.0208 * in0;

  x4 = 0. -> 0.0147 * pre sx0 + 0.0512 * pre x1 + 0.2099 * pre x2 + 0.57104 * pre x3 + 0.7694 * pre x4 + 0.0084 * in0;

  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;

tel;

node top(r : bool; ix0, ix1 : real) returns (x0, x1 : real);

let

  assert(ix0 > 0. and ix0 < 1.);

  assert(ix1 > 0. and ix1 < 1.);

  x0 = ix0 -> if r then 1. else pre x0 + 0.01 * pre x1;

  x1 = ix1 -> if r then 1. else -0.01 * pre x0 + 0.99 * pre x1;

tel

node top(ix0, ix1 : real) returns (sx0, x0, x1 : real);

let

  assert(ix0 > 0. and ix0 < 1.);

  assert(ix1 > 0. and ix1 < 1.);

  x0 = ix0 -> pre sx0 + 0.01 * pre x1;

  x1 = ix1 -> -0.01 * pre sx0 + 0.99 * pre x1;

  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;

tel

node top(r : bool; ix0, ix1 : real) returns (x0, x1 : real);

let

  assert(ix0 > 0. and ix0 < 1.);

  assert(ix1 > 0. and ix1 < 1.);

  x0 = ix0 -> if r then 1. else 0.95 * pre x0 + 0.09975 * pre x1;

  x1 = ix1 -> if r then 1. else -0.1 * pre x0 + 0.95 * pre x1;

tel

node top(ix0, ix1 : real) returns (sx0, x0, x1 : real);

let

  assert(ix0 > 0. and ix0 < 1.);

  assert(ix1 > 0. and ix1 < 1.);

  x0 = ix0 -> 0.95 * pre sx0 + 0.09975 * pre x1;

  x1 = ix1 -> -0.1 * pre sx0 + 0.95 * pre x1;

  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;

tel

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