Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_bias_test / bias_test.smt2 @ 6c3ea955

History | View | Annotate | Download (5.4 KB)

1
; bias_test
2
(declare-var bias_test.In1_1_1 Real)
3
(declare-var bias_test.In2_1_1 Real)
4
(declare-var bias_test.In3_1_1 Real)
5
(declare-var bias_test.In4_1_1 Int)
6
(declare-var bias_test.In4_1_2 Int)
7
(declare-var bias_test.In4_1_3 Int)
8
(declare-var bias_test.Out1_1_1 Real)
9
(declare-var bias_test.Out1_1_2 Real)
10
(declare-var bias_test.Out1_1_3 Real)
11
(declare-var bias_test.Out1_1_4 Real)
12
(declare-var bias_test.Out1_1_5 Real)
13
(declare-var bias_test.Out1_1_6 Real)
14
(declare-var bias_test.Out2_2_1 Real)
15
(declare-var bias_test.Out2_2_2 Real)
16
(declare-var bias_test.Out3_3_1 Real)
17
(declare-var bias_test.Out3_3_2 Real)
18
(declare-var bias_test.Out4_4_1 Real)
19
(declare-var bias_test.Out4_4_2 Real)
20
(declare-var bias_test.Out5_5_1 Int)
21
(declare-var bias_test.Out5_5_2 Int)
22
(declare-var bias_test.Out5_5_3 Int)
23
(declare-var bias_test.ni_0._arrow._first_c Bool)
24
(declare-var bias_test.ni_0._arrow._first_m Bool)
25
(declare-var bias_test.ni_0._arrow._first_x Bool)
26
(declare-var bias_test.Bias1_1_1 Real)
27
(declare-var bias_test.Bias1_1_2 Real)
28
(declare-var bias_test.Bias2_1_1 Real)
29
(declare-var bias_test.Bias2_1_2 Real)
30
(declare-var bias_test.Bias3_1_1 Real)
31
(declare-var bias_test.Bias3_1_2 Real)
32
(declare-var bias_test.Bias4_1_1 Int)
33
(declare-var bias_test.Bias4_1_2 Int)
34
(declare-var bias_test.Bias4_1_3 Int)
35
(declare-var bias_test.Bias_1_1 Real)
36
(declare-var bias_test.Bias_1_2 Real)
37
(declare-var bias_test.Bias_1_3 Real)
38
(declare-var bias_test.Bias_1_4 Real)
39
(declare-var bias_test.Bias_1_5 Real)
40
(declare-var bias_test.Bias_1_6 Real)
41
(declare-var bias_test.Constant_1_1 Real)
42
(declare-var bias_test.Constant_1_2 Real)
43
(declare-var bias_test.Constant_1_3 Real)
44
(declare-var bias_test.Constant_1_4 Real)
45
(declare-var bias_test.Constant_1_5 Real)
46
(declare-var bias_test.Constant_1_6 Real)
47
(declare-var bias_test.__bias_test_1 Bool)
48
(declare-var bias_test.i_virtual_local Real)
49
(declare-rel bias_test_reset (Bool Bool))
50
(declare-rel bias_test_step (Real Real Real Int Int Int Real Real Real Real Real Real Real Real Real Real Real Real Int Int Int Bool Bool))
51

    
52
(rule (=> 
53
  (and 
54
       
55
       (= bias_test.ni_0._arrow._first_m true)
56
  )
57
  (bias_test_reset bias_test.ni_0._arrow._first_c
58
                   bias_test.ni_0._arrow._first_m)
59
))
60

    
61
(rule (=> 
62
  (and (= bias_test.ni_0._arrow._first_m bias_test.ni_0._arrow._first_c)
63
       (and (= bias_test.__bias_test_1 (ite bias_test.ni_0._arrow._first_m true false))
64
            (= bias_test.ni_0._arrow._first_x false))
65
       (and (or (not (= bias_test.__bias_test_1 true))
66
               (= bias_test.i_virtual_local 0.0))
67
            (or (not (= bias_test.__bias_test_1 false))
68
               (= bias_test.i_virtual_local 1.0))
69
       )
70
       (= bias_test.Bias4_1_3 (+ bias_test.In4_1_3 6))
71
       (= bias_test.Out5_5_3 bias_test.Bias4_1_3)
72
       (= bias_test.Bias4_1_2 (+ bias_test.In4_1_2 6))
73
       (= bias_test.Out5_5_2 bias_test.Bias4_1_2)
74
       (= bias_test.Bias4_1_1 (+ bias_test.In4_1_1 6))
75
       (= bias_test.Out5_5_1 bias_test.Bias4_1_1)
76
       (= bias_test.Bias3_1_2 (+ bias_test.In3_1_1 4.00000000))
77
       (= bias_test.Out4_4_2 bias_test.Bias3_1_2)
78
       (= bias_test.Bias3_1_1 (+ bias_test.In3_1_1 2.00000000))
79
       (= bias_test.Out4_4_1 bias_test.Bias3_1_1)
80
       (= bias_test.Bias2_1_2 (+ bias_test.In2_1_1 0.00000000))
81
       (= bias_test.Out3_3_2 bias_test.Bias2_1_2)
82
       (= bias_test.Bias2_1_1 (+ bias_test.In2_1_1 1.00000000))
83
       (= bias_test.Out3_3_1 bias_test.Bias2_1_1)
84
       (= bias_test.Bias1_1_2 (+ bias_test.In1_1_1 4.00000000))
85
       (= bias_test.Out2_2_2 bias_test.Bias1_1_2)
86
       (= bias_test.Bias1_1_1 (+ bias_test.In1_1_1 2.00000000))
87
       (= bias_test.Out2_2_1 bias_test.Bias1_1_1)
88
       (= bias_test.Constant_1_6 9.00000000)
89
       (= bias_test.Bias_1_6 (+ bias_test.Constant_1_6 2.00000000))
90
       (= bias_test.Out1_1_6 bias_test.Bias_1_6)
91
       (= bias_test.Constant_1_5 7.00000000)
92
       (= bias_test.Bias_1_5 (+ bias_test.Constant_1_5 2.00000000))
93
       (= bias_test.Out1_1_5 bias_test.Bias_1_5)
94
       (= bias_test.Constant_1_4 5.00000000)
95
       (= bias_test.Bias_1_4 (+ bias_test.Constant_1_4 2.00000000))
96
       (= bias_test.Out1_1_4 bias_test.Bias_1_4)
97
       (= bias_test.Constant_1_3 4.00000000)
98
       (= bias_test.Bias_1_3 (+ bias_test.Constant_1_3 2.00000000))
99
       (= bias_test.Out1_1_3 bias_test.Bias_1_3)
100
       (= bias_test.Constant_1_2 3.00000000)
101
       (= bias_test.Bias_1_2 (+ bias_test.Constant_1_2 2.00000000))
102
       (= bias_test.Out1_1_2 bias_test.Bias_1_2)
103
       (= bias_test.Constant_1_1 2.00000000)
104
       (= bias_test.Bias_1_1 (+ bias_test.Constant_1_1 2.00000000))
105
       (= bias_test.Out1_1_1 bias_test.Bias_1_1)
106
       )
107
  (bias_test_step bias_test.In1_1_1
108
                  bias_test.In2_1_1
109
                  bias_test.In3_1_1
110
                  bias_test.In4_1_1
111
                  bias_test.In4_1_2
112
                  bias_test.In4_1_3
113
                  bias_test.Out1_1_1
114
                  bias_test.Out1_1_2
115
                  bias_test.Out1_1_3
116
                  bias_test.Out1_1_4
117
                  bias_test.Out1_1_5
118
                  bias_test.Out1_1_6
119
                  bias_test.Out2_2_1
120
                  bias_test.Out2_2_2
121
                  bias_test.Out3_3_1
122
                  bias_test.Out3_3_2
123
                  bias_test.Out4_4_1
124
                  bias_test.Out4_4_2
125
                  bias_test.Out5_5_1
126
                  bias_test.Out5_5_2
127
                  bias_test.Out5_5_3
128
                  bias_test.ni_0._arrow._first_c
129
                  bias_test.ni_0._arrow._first_x)
130
))
131