Project

General

Profile

Revision 43460259

View differences:

sandbox/extraction/README.org
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