Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / sandbox / extraction / piecewise_lin / triplex.lus @ 43460259

History | View | Annotate | Download (2.91 KB)

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