## Revision 43460259

View differences:

1
```* Available examples:
```
2
```- linear cases: Pierre Roux's examples as well as YAsmine Seladji ones
```
3
```- piecewise lin cases:
```
4
```  - Saturations or reset of the former category
```
5
```  - Triplex voter (Honeywell/Rockwell)
```
6

7
```TODO:
```
8
```- extract lustre modeling of the matlab code of Assale:
```
9
```  - svn/numericaltools/PiecewiseLyapunov/code/matlab/Code2/Examples/
```
10
```    - running_example.m
```
11
```    - exampleMignoneinvariance1.m (or variants)
```
12
```- same thing for the work with Assale + Victor:
```
13
```  - git/laas/progcertsos/script/example
```
14
```- last, the examples of the paper with Victor
```
15
```- Why not building examples with non polynomial computations and
```
16
```  extract the proper math. model?
```
17

18
```* Run
```
19
```source `lustrev -version | grep "Standard lib"| sed "s/.*: //"`/z3librc
```
20
```lustrev -seal -node top linear/ex1.lus
```
21

sandbox/extraction/linear/chain4_1.lus
1
```node top(in4_0 : real) returns (x4_0, x4_1, x4_2, in1_0, x1_0, x1_1 : real);
```
2
```let
```
3
```  assert(in4_0 >= -1. and in4_0 <= 1.);
```
4
```  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;
```
5
```  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;
```
6
```  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;
```
7
```  in1_0 = in4_0 -> 0.3 * x4_1;
```
8
```  x1_0 = 0. -> 1.5 * pre x1_0 - 0.7 * pre x1_1 + 1.6 * in1_0;
```
9
```  x1_1 = 0. -> pre x1_0;
```
10
```tel
```
sandbox/extraction/linear/chain4_4.lus
1
```node top(in4_0 : real) returns (x4_0, x4_1, x4_2, in42_0, x42_0, x42_1, x42_2 : real);
```
2
```let
```
3
```  assert(in4_0 >= -1. and in4_0 <= 1.);
```
4
```  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;
```
5
```  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;
```
6
```  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;
```
7
```  in42_0 = in4_0 -> 0.3 * x4_1;
```
8
```  x42_0 = 0. -> 0.9371 * pre x42_0 - 0.0377 * pre x42_1 - 0.0411 * pre x42_2 + 0.0237 * in42_0;
```
9
```  x42_1 = 0. -> -0.0399 * pre x42_0 + 0.960 * pre x42_1 - 0.0172 * pre x42_2 + 0.0143 * in42_0;
```
10
```  x42_2 = 0. -> 0.0140 * pre x42_0 - 0.0193 * pre x42_1 + 0.9821 * pre x42_2 + 0.0077 * in42_0;
```
11
```tel
```
sandbox/extraction/linear/chain4_l2.lus
1
```node top(in4_0 : real) returns (x4_0, x4_1, x4_2, inl2_0, yn, ynm1, xnm1, xnm2 : real);
```
2
```let
```
3
```  assert(in4_0 >= -1. and in4_0 <= 1.);
```
4
```  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;
```
5
```  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;
```
6
```  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;
```
7
```  inl2_0 = in4_0 -> 0.3 * x4_1;
```
8
```  yn = 0. -> 0.21875*inl2_0 + 0.40625*pre xnm1 + 0.21875*pre xnm2 + 0.375*pre yn - 0.1875*pre ynm1;
```
9
```  ynm1 = 0. -> pre yn;
```
10
```  xnm1 = 0. -> inl2_0;
```
11
```  xnm2 = 0. -> pre xnm1;
```
12
```tel
```
sandbox/extraction/linear/chain5_4.lus
1
```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);
```
2
```let
```
3
```  assert(in5_0 >= -1. and in5_0 <= 1.);
```
4
```  assert(in5_1 >= -1. and in5_1 <= 1.);
```
5
```  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;
```
6
```  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;
```
7
```  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;
```
8
```  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;
```
9
```  in4_0 = in5_0 -> 0.3 * x5_2;
```
10
```  x4_0 = 0. -> 0.9379 * pre x4_0 - 0.0381 * pre x4_1 - 0.0414 * pre x4_2 + 0.0237 * in4_0;
```
11
```  x4_1 = 0. -> -0.0404 * pre x4_0 + 0.968 * pre x4_1 - 0.0179 * pre x4_2 + 0.0143 * in4_0;
```
12
```  x4_2 = 0. -> 0.0142 * pre x4_0 - 0.0197 * pre x4_1 + 0.9823 * pre x4_2 + 0.0077 * in4_0;
```
13
```tel
```
sandbox/extraction/linear/chain5_6.lus
1
```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);
```
2
```let
```
3
```  assert(in5_0 >= -1. and in5_0 <= 1.);
```
4
```  assert(in5_1 >= -1. and in5_1 <= 1.);
```
5
```  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;
```
6
```  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;
```
7
```  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;
```
8
```  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;
```
9
```  in6_0 = in5_0 -> 0.3 * x5_1;
```
10
```  x6_0 = 0. -> 0.4250 * pre x6_0 + 0.8131 * in6_0;
```
11
```  x6_1 = 0. -> 0.3167 * pre x6_0 + 0.1016 * pre x6_1 - 0.4444 * pre x6_2 + 0.1807 * in6_0;
```
12
```  x6_2 = 0. -> 0.1278 * pre x6_0 + 0.4444 * pre x6_1 + 0.8207 * pre x6_2 + 0.0729 * in6_0;
```
13
```  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;
```
14
```  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;
```
15
```tel
```
sandbox/extraction/linear/chain6_l2.lus
1
```node top(in6_0 : real) returns (x6_0, x6_1, x6_2, x6_3, x6_4, inl2_0, yn, ynm1, xnm1, xnm2 : real);
```
2
```let
```
3
```  assert(in6_0 >= -1. and in6_0 <= 1.);
```
4
```  x6_0 = 0. -> 0.4250 * pre x6_0 + 0.8131 * in6_0;
```
5
```  x6_1 = 0. -> 0.3167 * pre x6_0 + 0.1016 * pre x6_1 - 0.4444 * pre x6_2 + 0.1807 * in6_0;
```
6
```  x6_2 = 0. -> 0.1278 * pre x6_0 + 0.4444 * pre x6_1 + 0.8207 * pre x6_2 + 0.0729 * in6_0;
```
7
```  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;
```
8
```  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;
```
9
```  inl2_0 = in6_0 -> 0.3 * x6_2;
```
10
```  yn = 0. -> 0.21875*inl2_0 + 0.40625*pre xnm1 + 0.21875*pre xnm2 + 0.375*pre yn - 0.1875*pre ynm1;
```
11
```  ynm1 = 0. -> pre yn;
```
12
```  xnm1 = 0. -> inl2_0;
```
13
```  xnm2 = 0. -> pre xnm1;
```
14
```tel
```
sandbox/extraction/linear/ex1.lus
1
```node top(in0 : real) returns (x, y : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x = 0. -> 1.5 * pre x - 0.7 * pre y + 1.6 * in0;
```
5
```  y = 0. -> pre x;
```
6
```tel
```
7

sandbox/extraction/linear/ex1_mat.lus
1
```#open "libarrays"
```
2

3
```node ctl(in0 : real^1^1) returns (mem : real^2^1);
```
4
```var _A:  real^2^2;
```
5
```    _B:  real^2^1;
```
6
```let
```
7
```  _A = [[1.5, 1.],  [-0.7, 0.]];
```
8
```  _B = [[1.6, 0.]];
```
9
```   assert(in0[0][0] >= -1. and in0[0][0] <= 1.);
```
10
```   mem = [[0., 0.]] -> _MatMul_real(2, 2, 1,  _A,  pre mem) + _MatMul_real(2, 1, 1, _B,  in0);
```
11
```
```
12
```tel
```
13

14
```node top(in0 : real) returns (x,  y:  real);
```
15
```var res:  real^2^1;
```
16
```let
```
17
```  res = ctl([[in0]]);
```
18
```  x = res[0][0];
```
19
```  y = res[0][1];
```
20
```tel
```
21

sandbox/extraction/linear/ex2.lus
1
```node top(in0 : real) returns (x0, x1, x2, x3 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 1.5 * pre x0 - 0.7 * pre x1 - 0.7 * pre x2 + 0.4 * pre x3 + 0.5 * in0;
```
5
```  x1 = 0. -> pre x0;
```
6
```  x2 = 0. -> in0;
```
7
```  x3 = 0. -> pre x2;
```
8
```tel
```
sandbox/extraction/linear/ex3.lus
1
```node top(in0 : real) returns (x0, x1 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 0.499 * pre x0 - 0.05 * pre x1 + in0;
```
5
```  x1 = 0. -> 0.01 * pre x0 + pre x1;
```
6
```tel
```
sandbox/extraction/linear/ex4.lus
1
```node top(in0 : real) returns (x0, x1, x2 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 0.9379 * pre x0 - 0.0381 * pre x1 - 0.0414 * pre x2 + 0.0237 * in0;
```
5
```  x1 = 0. -> -0.0404 * pre x0 + 0.968 * pre x1 - 0.0179 * pre x2 + 0.0143 * in0;
```
6
```  x2 = 0. -> 0.0142 * pre x0 - 0.0197 * pre x1 + 0.9823 * pre x2 + 0.0077 * in0;
```
7
```tel
```
sandbox/extraction/linear/ex5.lus
1
```node top(in0, in1 : real) returns (x0, x1, x2, x3 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  assert(in1 >= -1. and in1 <= 1.);
```
5
```  x0 = 0. -> 0.6227 * pre x0 + 0.3871 * pre x1 - 0.113 * pre x2 + 0.0102 * pre x3 + 0.3064 * in0 + 0.1826 * in1;
```
6
```  x1 = 0. -> -0.3407 * pre x0 + 0.9103 * pre x1 - 0.3388 * pre x2 + 0.0649 * pre x3 - 0.0054 * in0 + 0.6731 * in1;
```
7
```  x2 = 0. -> 0.0918 * pre x0 - 0.0265 * pre x1 - 0.7319 * pre x2 + 0.2669 * pre x3 + 0.0494 * in0 + 1.6138 * in1;
```
8
```  x3 = 0. -> 0.2643 * pre x0 - 0.1298 * pre x1 - 0.9903 * pre x2 + 0.3331 * pre x3 - 0.0531 * in0 + 0.4012 * in1;
```
9
```tel
```
sandbox/extraction/linear/ex6.lus
1
```node top(in0 : real) returns (x0, x1, x2, x3, x4 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 0.4250 * pre x0 + 0.8131 * in0;
```
5
```  x1 = 0. -> 0.3167 * pre x0 + 0.1016 * pre x1 - 0.4444 * pre x2 + 0.1807 * in0;
```
6
```  x2 = 0. -> 0.1278 * pre x0 + 0.4444 * pre x1 + 0.8207 * pre x2 + 0.0729 * in0;
```
7
```  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;
```
8
```  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;
```
9
```tel
```
sandbox/extraction/linear/ex7.lus
1
```node top(ix0, ix1 : real) returns (x0, x1 : real);
```
2
```let
```
3
```  assert(ix0 > 0. and ix0 < 1.);
```
4
```  assert(ix1 > 0. and ix1 < 1.);
```
5
```  x0 = ix0 -> pre x0 + 0.01 * pre x1;
```
6
```  x1 = ix1 -> -0.01 * pre x0 + 0.99 * pre x1;
```
7
```tel
```
sandbox/extraction/linear/ex8.lus
1
```node top(ix0, ix1 : real) returns (x0, x1 : real);
```
2
```let
```
3
```  assert(ix0 > 0. and ix0 < 1.);
```
4
```  assert(ix1 > 0. and ix1 < 1.);
```
5
```  x0 = ix0 -> 0.95 * pre x0 + 0.09975 * pre x1;
```
6
```  x1 = ix1 -> -0.1 * pre x0 + 0.95 * pre x1;
```
7
```tel
```
sandbox/extraction/linear/lp_iir_9600_2.lus
1
```node top(xn : real) returns (yn, xnm1, xnm2, ynm1 : real);
```
2
```let
```
3
```  assert(xn >= -1.6 and xn <= 1.6);
```
4
```  yn = 0. -> 0.21875*xn + 0.40625*pre xnm1 + 0.21875*pre xnm2 + 0.375*pre yn - 0.1875*pre ynm1;
```
5
```  ynm1 = 0. -> pre yn;
```
6
```  xnm1 = 0. -> xn;
```
7
```  xnm2 = 0. -> pre xnm1;
```
8
```tel
```
sandbox/extraction/linear/lp_iir_9600_4.lus
1
```node top(xn : real) returns (yn, ynm1, ynm2, ynm3, xnm1, xnm2, xnm3, xnm4 : real);
```
2
```let
```
3
```  assert(xn >= -1.0 and xn <= 1.0);
```
4
```  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;
```
5
```  ynm1 = 0. -> pre yn;
```
6
```  ynm2 = 0. -> pre ynm1;
```
7
```  ynm3 = 0. -> pre ynm2;
```
8
```  xnm1 = 0. -> xn;
```
9
```  xnm2 = 0. -> pre xnm1;
```
10
```  xnm3 = 0. -> pre xnm2;
```
11
```  xnm4 = 0. -> pre xnm3;
```
12
```tel
```
sandbox/extraction/linear/lp_iir_9600_4_elliptic.lus
1
```node top(xn : real) returns (yn, ynm1, ynm2, ynm3, xnm1, xnm2, xnm3, xnm4 : real);
```
2
```let
```
3
```  assert(xn >= -1.0 and xn <= 1.0);
```
4
```  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;
```
5
```  ynm1 = 0. -> pre yn;
```
6
```  ynm2 = 0. -> pre ynm1;
```
7
```  ynm3 = 0. -> pre ynm2;
```
8
```  xnm1 = 0. -> xn;
```
9
```  xnm2 = 0. -> pre xnm1;
```
10
```  xnm3 = 0. -> pre xnm2;
```
11
```  xnm4 = 0. -> pre xnm3;
```
12
```tel
```
sandbox/extraction/linear/lp_iir_9600_6_elliptic.lus
1
```node top(xn : real) returns (yn, ynm1, ynm2, ynm3, ynm4, ynm5, xnm1, xnm2, xnm3, xnm4, xnm5, xnm6 : real);
```
2
```let
```
3
```  assert(xn >= -1.0 and xn <= 1.0);
```
4
```  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;
```
5
```  ynm1 = 0. -> pre yn;
```
6
```  ynm2 = 0. -> pre ynm1;
```
7
```  ynm3 = 0. -> pre ynm2;
```
8
```  ynm4 = 0. -> pre ynm3;
```
9
```  ynm5 = 0. -> pre ynm4;
```
10
```  xnm1 = 0. -> xn;
```
11
```  xnm2 = 0. -> pre xnm1;
```
12
```  xnm3 = 0. -> pre xnm2;
```
13
```  xnm4 = 0. -> pre xnm3;
```
14
```  xnm5 = 0. -> pre xnm4;
```
15
```  xnm6 = 0. -> pre xnm5;
```
16
```tel
```
sandbox/extraction/piecewise_lin/ex1reset.lus
1
```node top(r : bool; in0 : real) returns (x, y : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x = 0. -> if r then 1. else 1.5 * pre x - 0.7 * pre y + 1.6 * in0;
```
5
```  y = 0. -> if r then 1. else pre x;
```
6
```tel
```
7

sandbox/extraction/piecewise_lin/ex1sat.lus
1
```node top(in0 : real) returns (sx, x, y : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x = 0. -> 1.5 * pre sx - 0.7 * pre y + 1.6 * in0;
```
5
```  y = 0. -> pre x;
```
6
```  sx = if x > 10. then 10. else if x < -10. then -10. else in0 + x;
```
7
```tel
```
sandbox/extraction/piecewise_lin/ex2reset.lus
1
```node top(r : bool; in0 : real) returns (x0, x1, x2, x3 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  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;
```
5
```  x1 = 0. -> if r then 1. else pre x0;
```
6
```  x2 = 0. -> if r then 1. else in0;
```
7
```  x3 = 0. -> if r then 1. else pre x2;
```
8
```tel
```
sandbox/extraction/piecewise_lin/ex2sat.lus
1
```node top(in0 : real) returns (sx0, x0, x1, x2, x3 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 1.5 * pre sx0 - 0.7 * pre x1 - 0.7 * pre x2 + 0.4 * pre x3 + 0.5 * in0;
```
5
```  x1 = 0. -> pre sx0;
```
6
```  x2 = 0. -> in0;
```
7
```  x3 = 0. -> pre x2;
```
8
```  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;
```
9
```tel
```
sandbox/extraction/piecewise_lin/ex3reset.lus
1
```node top(r : bool; in0 : real) returns (x0, x1 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> if r then 1. else 0.499 * pre x0 - 0.05 * pre x1 + in0;
```
5
```  x1 = 0. -> if r then 1. else 0.01 * pre x0 + pre x1;
```
6
```tel
```
sandbox/extraction/piecewise_lin/ex3sat.lus
1
```node top(in0 : real) returns (sx0, x0, x1 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 0.499 * pre sx0 - 0.05 * pre x1 + in0;
```
5
```  x1 = 0. -> 0.01 * pre sx0 + pre x1;
```
6
```  sx0 = if x0 > 50. then 50. else if x0 < -50. then -50. else x0;
```
7
```tel
```
sandbox/extraction/piecewise_lin/ex4reset.lus
1
```node top(r : bool; in0 : real) returns (x0, x1, x2 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> if r then 1. else 0.9379 * pre x0 - 0.0381 * pre x1 - 0.0414 * pre x2 + 0.0237 * in0;
```
5
```  x1 = 0. -> if r then 1. else -0.0404 * pre x0 + 0.968 * pre x1 - 0.0179 * pre x2 + 0.0143 * in0;
```
6
```  x2 = 0. -> if r then 1. else 0.0142 * pre x0 - 0.0197 * pre x1 + 0.9823 * pre x2 + 0.0077 * in0;
```
7
```tel
```
sandbox/extraction/piecewise_lin/ex4sat.lus
1
```node top(in0 : real) returns (sx0, x0, x1, x2 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 0.9379 * pre sx0 - 0.0381 * pre x1 - 0.0414 * pre x2 + 0.0237 * in0;
```
5
```  x1 = 0. -> -0.0404 * pre sx0 + 0.968 * pre x1 - 0.0179 * pre x2 + 0.0143 * in0;
```
6
```  x2 = 0. -> 0.0142 * pre sx0 - 0.0197 * pre x1 + 0.9823 * pre x2 + 0.0077 * in0;
```
7
```  sx0 = if x0 > 50. then 50. else if x0 < -50. then -50. else x0;
```
8
```tel
```
sandbox/extraction/piecewise_lin/ex5reset.lus
1
```node top(r : bool; in0, in1 : real) returns (x0, x1, x2, x3 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  assert(in1 >= -1. and in1 <= 1.);
```
5
```  x0 = 0. -> if r then 1. else
```
6
```    0.6227 * pre x0 + 0.3871 * pre x1 - 0.113 * pre x2 + 0.0102 * pre x3 + 0.3064 * in0 + 0.1826 * in1;
```
7
```  x1 = 0. -> if r then 1. else
```
8
```    -0.3407 * pre x0 + 0.9103 * pre x1 - 0.3388 * pre x2 + 0.0649 * pre x3 - 0.0054 * in0 + 0.6731 * in1;
```
9
```  x2 = 0. -> if r then 1. else
```
10
```    0.0918 * pre x0 - 0.0265 * pre x1 - 0.7319 * pre x2 + 0.2669 * pre x3 + 0.0494 * in0 + 1.6138 * in1;
```
11
```  x3 = 0. -> if r then 1. else
```
12
```    0.2643 * pre x0 - 0.1298 * pre x1 - 0.9903 * pre x2 + 0.3331 * pre x3 - 0.0531 * in0 + 0.4012 * in1;
```
13
```tel
```
sandbox/extraction/piecewise_lin/ex5sat.lus
1
```node top(in0, in1 : real) returns (sx0, x0, x1, x2, x3 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  assert(in1 >= -1. and in1 <= 1.);
```
5
```  x0 = 0. -> 0.6227 * pre sx0 + 0.3871 * pre x1 - 0.113 * pre x2 + 0.0102 * pre x3 + 0.3064 * in0 + 0.1826 * in1;
```
6
```  x1 = 0. -> -0.3407 * pre sx0 + 0.9103 * pre x1 - 0.3388 * pre x2 + 0.0649 * pre x3 - 0.0054 * in0 + 0.6731 * in1;
```
7
```  x2 = 0. -> 0.0918 * pre sx0 - 0.0265 * pre x1 - 0.7319 * pre x2 + 0.2669 * pre x3 + 0.0494 * in0 + 1.6138 * in1;
```
8
```  x3 = 0. -> 0.2643 * pre sx0 - 0.1298 * pre x1 - 0.9903 * pre x2 + 0.3331 * pre x3 - 0.0531 * in0 + 0.4012 * in1;
```
9
```  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;
```
10
```tel
```
sandbox/extraction/piecewise_lin/ex6reset.lus
1
```node top(r : bool; in0 : real) returns (x0, x1, x2, x3, x4 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> if r then 1. else 0.4250 * pre x0 + 0.8131 * in0;
```
5
```  x1 = 0. -> if r then 1. else
```
6
```    0.3167 * pre x0 + 0.1016 * pre x1 - 0.4444 * pre x2 + 0.1807 * in0;
```
7
```  x2 = 0. -> if r then 1. else
```
8
```    0.1278 * pre x0 + 0.4444 * pre x1 + 0.8207 * pre x2 + 0.0729 * in0;
```
9
```  x3 = 0. -> if r then 1. else
```
10
```    0.0365 * pre x0 + 0.1270 * pre x1 + 0.5202 * pre x2 + 0.4163 * pre x3 - 0.5714 * pre x4 + 0.0208 * in0;
```
11
```  x4 = 0. -> if r then 1. else
```
12
```    0.0147 * pre x0 + 0.0512 * pre x1 + 0.2099 * pre x2 + 0.57104 * pre x3 + 0.7694 * pre x4 + 0.0084 * in0;
```
13
```tel
```
sandbox/extraction/piecewise_lin/ex6sat.lus
1
```node top(in0 : real) returns (sx0, x0, x1, x2, x3, x4 : real);
```
2
```let
```
3
```  assert(in0 >= -1. and in0 <= 1.);
```
4
```  x0 = 0. -> 0.4250 * pre sx0 + 0.8131 * in0;
```
5
```  x1 = 0. -> 0.3167 * pre sx0 + 0.1016 * pre x1 - 0.4444 * pre x2 + 0.1807 * in0;
```
6
```  x2 = 0. -> 0.1278 * pre sx0 + 0.4444 * pre x1 + 0.8207 * pre x2 + 0.0729 * in0;
```
7
```  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;
```
8
```  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;
```
9
```  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;
```
10
```tel;
```
sandbox/extraction/piecewise_lin/ex7reset.lus
1
```node top(r : bool; ix0, ix1 : real) returns (x0, x1 : real);
```
2
```let
```
3
```  assert(ix0 > 0. and ix0 < 1.);
```
4
```  assert(ix1 > 0. and ix1 < 1.);
```
5
```  x0 = ix0 -> if r then 1. else pre x0 + 0.01 * pre x1;
```
6
```  x1 = ix1 -> if r then 1. else -0.01 * pre x0 + 0.99 * pre x1;
```
7
```tel
```
sandbox/extraction/piecewise_lin/ex7sat.lus
1
```node top(ix0, ix1 : real) returns (sx0, x0, x1 : real);
```
2
```let
```
3
```  assert(ix0 > 0. and ix0 < 1.);
```
4
```  assert(ix1 > 0. and ix1 < 1.);
```
5
```  x0 = ix0 -> pre sx0 + 0.01 * pre x1;
```
6
```  x1 = ix1 -> -0.01 * pre sx0 + 0.99 * pre x1;
```
7
```  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;
```
8
```tel
```
sandbox/extraction/piecewise_lin/ex8reset.lus
1
```node top(r : bool; ix0, ix1 : real) returns (x0, x1 : real);
```
2
```let
```
3
```  assert(ix0 > 0. and ix0 < 1.);
```
4
```  assert(ix1 > 0. and ix1 < 1.);
```
5
```  x0 = ix0 -> if r then 1. else 0.95 * pre x0 + 0.09975 * pre x1;
```
6
```  x1 = ix1 -> if r then 1. else -0.1 * pre x0 + 0.95 * pre x1;
```
7
```tel
```
sandbox/extraction/piecewise_lin/ex8sat.lus
1
```node top(ix0, ix1 : real) returns (sx0, x0, x1 : real);
```
2
```let
```
3
```  assert(ix0 > 0. and ix0 < 1.);
```
4
```  assert(ix1 > 0. and ix1 < 1.);
```
5
```  x0 = ix0 -> 0.95 * pre sx0 + 0.09975 * pre x1;
```
6
```  x1 = ix1 -> -0.1 * pre sx0 + 0.95 * pre x1;
```
7
```  sx0 = if x0 > 0.5 then 0.5 else if x0 < -0.5 then -0.5 else x0;
```
8
```tel
```
sandbox/extraction/piecewise_lin/triplex.lus
1
```node top(input1, input2, input3: real) returns (output: real);
```
2
```var
```
3
```  equalized1, equalized2, equalized3 : real;
```
4
```  equalization1, equalization2, equalization3 : real;
```
5
```  satCentering, centering : real;
```
6
```  df1, df2, df3 : real;
```
7
```  st1, st2, st3 : real;
```
8
```  c1, c2, c3 : bool;
```
9
```  d1, d2, d3 : bool;
```
10
```--  check: bool;
```
11
```  pre_equalization1, pre_equalization2, pre_equalization3 : real; -- mem
```
12
```  pre_st1, pre_st2, pre_st3 : real;                               -- mem
```
13
```  pre_satCentering : real;                                        -- mem
```
14
```let
```
15

16
```  assert (input1 <  0.2);
```
17
```  assert (input1 > -0.2);
```
18
```  assert (input2 <  0.2);
```
19
```  assert (input2 > -0.2);
```
20
```  assert (input3 <  0.2);
```
21
```  assert (input3 > -0.2);
```
22

23
``` --! /salsa/ranges/input1/: (-0.2, 0.2);
```
24
``` --! /salsa/ranges/input2/: (-0.2, 0.2);
```
25
``` --! /salsa/ranges/input3/: (-0.2, 0.2);
```
26

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

29
``` --! /salsa/ranges/pre_equalization1/: (-0.4, 0.4);
```
30
``` --! /salsa/ranges/pre_st1/: (-0.5, 0.5);
```
31
``` --! /salsa/ranges/pre_equalization2/: (-0.4, 0.4);
```
32
``` --! /salsa/ranges/pre_st2/: (-0.5, 0.5);
```
33
``` --! /salsa/ranges/pre_equalization3/: (-0.4, 0.4);
```
34
``` --! /salsa/ranges/pre_st3/: (-0.5, 0.5);
```
35
``` --! /salsa/ranges/pre_satCentering/: (-0.25, 0.25);
```
36

37

38
```  pre_equalization1 = pre equalization1;
```
39
```  pre_st1 =           pre st1;
```
40
```  pre_equalization2 = pre equalization2;
```
41
```  pre_st2 =           pre st2;
```
42
```  pre_equalization3 = pre equalization3;
```
43
```  pre_st3 =           pre st3;
```
44

45
```  pre_satCentering =  pre satCentering;
```
46

47
```  equalized1 = input1 - equalization1;
```
48
```  df1 = equalized1 - output;
```
49
```  st1 = if (df1 > 0.5) then 0.5 else (if (df1 < -0.5) then -0.5 else df1);
```
50
```  equalization1 = 0.0 -> pre_equalization1 + (pre_st1 - pre_satCentering) * 0.05;
```
51
```
```
52
```  equalized2 = input2 - equalization2;
```
53
```  df2 = equalized2 - output;
```
54
```  st2 = if (df2 > 0.5) then 0.5 else (if (df2 < -0.5) then -0.5 else df2);
```
55
```  equalization2 = 0.0 -> pre_equalization2 + (pre_st2 - pre_satCentering) * 0.05;
```
56

57
```  equalized3 = input3 - equalization3;
```
58
```  df3 = equalized3 - output;
```
59
```  st3 = if (df3 > 0.5) then 0.5 else (if (df3 < -0.5) then -0.5 else df3);
```
60
```  equalization3 = 0.0 -> pre_equalization3 + (pre_st3 - pre_satCentering) * 0.05;
```
61

62
```  c1 = equalized1 > equalized2;
```
63
```  c2 = equalized2 > equalized3;
```
64
```  c3 = equalized3 > equalized1;
```
65

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

68
```  d1 = equalization1 > equalization2;
```
69
```  d2 = equalization2 > equalization3;
```
70
```  d3 = equalization3 > equalization1;
```
71

72
```  centering = if (d1 = d2) then equalization2 else (if (d2 = d3) then equalization3 else equalization1);
```
73
```  satCentering = if (centering > 0.25) then 0.25 else (if (centering < -0.25) then -0.25 else centering);
```
74

75
```  -- check = ( equalization1 <=  2.0 * 0.2) and
```
76
```  --         ( equalization1 >= -2.0 * 0.2) and
```
77
```  --         ( equalization2 <=  2.0 * 0.2) and
```
78
```  --         ( equalization2 >= -2.0 * 0.2) and
```
79
```  --         ( equalization3 <=  2.0 * 0.2) and
```
80
```  --         ( equalization3 >= -2.0 * 0.2);
```
81

82
```--% prove(check);
```
83
```--%MAIN;
```
84

85
```tel
```
86

87

88

89

90

Also available in: Unified diff