Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_saturationdynamic_param_test / saturationdynamic_param_test.smt2 @ 6c3ea955

History | View | Annotate | Download (20.6 KB)

1
; saturationdynamic_param_test
2
(declare-var saturationdynamic_param_test.In1_1_1 Real)
3
(declare-var saturationdynamic_param_test.In2_1_1 Real)
4
(declare-var saturationdynamic_param_test.In3_1_1 Real)
5
(declare-var saturationdynamic_param_test.In4_1_1 Int)
6
(declare-var saturationdynamic_param_test.In5_1_1 Int)
7
(declare-var saturationdynamic_param_test.In6_1_1 Int)
8
(declare-var saturationdynamic_param_test.In7_1_1 Real)
9
(declare-var saturationdynamic_param_test.In7_1_2 Real)
10
(declare-var saturationdynamic_param_test.In8_1_1 Real)
11
(declare-var saturationdynamic_param_test.In8_1_2 Real)
12
(declare-var saturationdynamic_param_test.In9_1_1 Real)
13
(declare-var saturationdynamic_param_test.In9_1_2 Real)
14
(declare-var saturationdynamic_param_test.In10_1_1 Real)
15
(declare-var saturationdynamic_param_test.In10_1_2 Real)
16
(declare-var saturationdynamic_param_test.In10_1_3 Real)
17
(declare-var saturationdynamic_param_test.In10_1_4 Real)
18
(declare-var saturationdynamic_param_test.In10_1_5 Real)
19
(declare-var saturationdynamic_param_test.In10_1_6 Real)
20
(declare-var saturationdynamic_param_test.In11_1_1 Real)
21
(declare-var saturationdynamic_param_test.In11_1_2 Real)
22
(declare-var saturationdynamic_param_test.In11_1_3 Real)
23
(declare-var saturationdynamic_param_test.In11_1_4 Real)
24
(declare-var saturationdynamic_param_test.In11_1_5 Real)
25
(declare-var saturationdynamic_param_test.In11_1_6 Real)
26
(declare-var saturationdynamic_param_test.In12_1_1 Real)
27
(declare-var saturationdynamic_param_test.In12_1_2 Real)
28
(declare-var saturationdynamic_param_test.In12_1_3 Real)
29
(declare-var saturationdynamic_param_test.In12_1_4 Real)
30
(declare-var saturationdynamic_param_test.In12_1_5 Real)
31
(declare-var saturationdynamic_param_test.In12_1_6 Real)
32
(declare-var saturationdynamic_param_test.Out1_1_1 Real)
33
(declare-var saturationdynamic_param_test.Out2_2_1 Int)
34
(declare-var saturationdynamic_param_test.Out3_3_1 Real)
35
(declare-var saturationdynamic_param_test.Out3_3_2 Real)
36
(declare-var saturationdynamic_param_test.Out4_4_1 Real)
37
(declare-var saturationdynamic_param_test.Out4_4_2 Real)
38
(declare-var saturationdynamic_param_test.Out4_4_3 Real)
39
(declare-var saturationdynamic_param_test.Out4_4_4 Real)
40
(declare-var saturationdynamic_param_test.Out4_4_5 Real)
41
(declare-var saturationdynamic_param_test.Out4_4_6 Real)
42
(declare-var saturationdynamic_param_test.ni_0._arrow._first_c Bool)
43
(declare-var saturationdynamic_param_test.ni_0._arrow._first_m Bool)
44
(declare-var saturationdynamic_param_test.ni_0._arrow._first_x Bool)
45
(declare-var saturationdynamic_param_test.SaturationDynamic1_1_1 Int)
46
(declare-var saturationdynamic_param_test.SaturationDynamic2_1_1 Real)
47
(declare-var saturationdynamic_param_test.SaturationDynamic2_1_2 Real)
48
(declare-var saturationdynamic_param_test.SaturationDynamic3_1_1 Real)
49
(declare-var saturationdynamic_param_test.SaturationDynamic3_1_2 Real)
50
(declare-var saturationdynamic_param_test.SaturationDynamic3_1_3 Real)
51
(declare-var saturationdynamic_param_test.SaturationDynamic3_1_4 Real)
52
(declare-var saturationdynamic_param_test.SaturationDynamic3_1_5 Real)
53
(declare-var saturationdynamic_param_test.SaturationDynamic3_1_6 Real)
54
(declare-var saturationdynamic_param_test.SaturationDynamic_1_1 Real)
55
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_1 Bool)
56
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_10 Bool)
57
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_11 Bool)
58
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_12 Bool)
59
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_13 Bool)
60
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_14 Bool)
61
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_15 Bool)
62
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_16 Bool)
63
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_17 Bool)
64
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_18 Bool)
65
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_19 Bool)
66
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_2 Bool)
67
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_20 Bool)
68
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_21 Bool)
69
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_3 Bool)
70
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_4 Bool)
71
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_5 Bool)
72
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_6 Bool)
73
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_7 Bool)
74
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_8 Bool)
75
(declare-var saturationdynamic_param_test.__saturationdynamic_param_test_9 Bool)
76
(declare-var saturationdynamic_param_test.i_virtual_local Real)
77
(declare-rel saturationdynamic_param_test_reset (Bool Bool))
78
(declare-rel saturationdynamic_param_test_step (Real Real Real Int Int Int Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Int Real Real Real Real Real Real Real Real Bool Bool))
79

    
80
(rule (=> 
81
  (and 
82
       
83
       (= saturationdynamic_param_test.ni_0._arrow._first_m true)
84
  )
85
  (saturationdynamic_param_test_reset saturationdynamic_param_test.ni_0._arrow._first_c
86
                                      saturationdynamic_param_test.ni_0._arrow._first_m)
87
))
88

    
89
(rule (=> 
90
  (and (= saturationdynamic_param_test.ni_0._arrow._first_m saturationdynamic_param_test.ni_0._arrow._first_c)
91
       (and (= saturationdynamic_param_test.__saturationdynamic_param_test_1 (ite saturationdynamic_param_test.ni_0._arrow._first_m true false))
92
            (= saturationdynamic_param_test.ni_0._arrow._first_x false))
93
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_1 true))
94
               (= saturationdynamic_param_test.i_virtual_local 0.0))
95
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_1 false))
96
               (= saturationdynamic_param_test.i_virtual_local 1.0))
97
       )
98
       (= saturationdynamic_param_test.__saturationdynamic_param_test_9 (< saturationdynamic_param_test.In11_1_3 saturationdynamic_param_test.In12_1_3))
99
       (= saturationdynamic_param_test.__saturationdynamic_param_test_8 (> saturationdynamic_param_test.In11_1_3 saturationdynamic_param_test.In10_1_3))
100
       (= saturationdynamic_param_test.__saturationdynamic_param_test_7 (< saturationdynamic_param_test.In11_1_4 saturationdynamic_param_test.In12_1_4))
101
       (= saturationdynamic_param_test.__saturationdynamic_param_test_6 (> saturationdynamic_param_test.In11_1_4 saturationdynamic_param_test.In10_1_4))
102
       (= saturationdynamic_param_test.__saturationdynamic_param_test_5 (< saturationdynamic_param_test.In11_1_5 saturationdynamic_param_test.In12_1_5))
103
       (= saturationdynamic_param_test.__saturationdynamic_param_test_4 (> saturationdynamic_param_test.In11_1_5 saturationdynamic_param_test.In10_1_5))
104
       (= saturationdynamic_param_test.__saturationdynamic_param_test_3 (< saturationdynamic_param_test.In11_1_6 saturationdynamic_param_test.In12_1_6))
105
       (= saturationdynamic_param_test.__saturationdynamic_param_test_21 (< saturationdynamic_param_test.In2_1_1 saturationdynamic_param_test.In3_1_1))
106
       (= saturationdynamic_param_test.__saturationdynamic_param_test_20 (> saturationdynamic_param_test.In2_1_1 saturationdynamic_param_test.In1_1_1))
107
       (= saturationdynamic_param_test.__saturationdynamic_param_test_2 (> saturationdynamic_param_test.In11_1_6 saturationdynamic_param_test.In10_1_6))
108
       (= saturationdynamic_param_test.__saturationdynamic_param_test_19 (< saturationdynamic_param_test.In5_1_1 saturationdynamic_param_test.In6_1_1))
109
       (= saturationdynamic_param_test.__saturationdynamic_param_test_18 (> saturationdynamic_param_test.In5_1_1 saturationdynamic_param_test.In4_1_1))
110
       (= saturationdynamic_param_test.__saturationdynamic_param_test_17 (< saturationdynamic_param_test.In8_1_1 saturationdynamic_param_test.In9_1_1))
111
       (= saturationdynamic_param_test.__saturationdynamic_param_test_16 (> saturationdynamic_param_test.In8_1_1 saturationdynamic_param_test.In7_1_1))
112
       (= saturationdynamic_param_test.__saturationdynamic_param_test_15 (< saturationdynamic_param_test.In8_1_2 saturationdynamic_param_test.In9_1_2))
113
       (= saturationdynamic_param_test.__saturationdynamic_param_test_14 (> saturationdynamic_param_test.In8_1_2 saturationdynamic_param_test.In7_1_2))
114
       (= saturationdynamic_param_test.__saturationdynamic_param_test_13 (< saturationdynamic_param_test.In11_1_1 saturationdynamic_param_test.In12_1_1))
115
       (= saturationdynamic_param_test.__saturationdynamic_param_test_12 (> saturationdynamic_param_test.In11_1_1 saturationdynamic_param_test.In10_1_1))
116
       (= saturationdynamic_param_test.__saturationdynamic_param_test_11 (< saturationdynamic_param_test.In11_1_2 saturationdynamic_param_test.In12_1_2))
117
       (= saturationdynamic_param_test.__saturationdynamic_param_test_10 (> saturationdynamic_param_test.In11_1_2 saturationdynamic_param_test.In10_1_2))
118
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_20 true))
119
               (= saturationdynamic_param_test.SaturationDynamic_1_1 saturationdynamic_param_test.In1_1_1))
120
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_20 false))
121
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_21 true))
122
                       (= saturationdynamic_param_test.SaturationDynamic_1_1 saturationdynamic_param_test.In3_1_1))
123
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_21 false))
124
                       (= saturationdynamic_param_test.SaturationDynamic_1_1 saturationdynamic_param_test.In2_1_1))
125
               ))
126
       )
127
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_2 true))
128
               (= saturationdynamic_param_test.SaturationDynamic3_1_6 saturationdynamic_param_test.In10_1_6))
129
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_2 false))
130
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_3 true))
131
                       (= saturationdynamic_param_test.SaturationDynamic3_1_6 saturationdynamic_param_test.In12_1_6))
132
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_3 false))
133
                       (= saturationdynamic_param_test.SaturationDynamic3_1_6 saturationdynamic_param_test.In11_1_6))
134
               ))
135
       )
136
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_4 true))
137
               (= saturationdynamic_param_test.SaturationDynamic3_1_5 saturationdynamic_param_test.In10_1_5))
138
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_4 false))
139
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_5 true))
140
                       (= saturationdynamic_param_test.SaturationDynamic3_1_5 saturationdynamic_param_test.In12_1_5))
141
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_5 false))
142
                       (= saturationdynamic_param_test.SaturationDynamic3_1_5 saturationdynamic_param_test.In11_1_5))
143
               ))
144
       )
145
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_6 true))
146
               (= saturationdynamic_param_test.SaturationDynamic3_1_4 saturationdynamic_param_test.In10_1_4))
147
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_6 false))
148
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_7 true))
149
                       (= saturationdynamic_param_test.SaturationDynamic3_1_4 saturationdynamic_param_test.In12_1_4))
150
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_7 false))
151
                       (= saturationdynamic_param_test.SaturationDynamic3_1_4 saturationdynamic_param_test.In11_1_4))
152
               ))
153
       )
154
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_8 true))
155
               (= saturationdynamic_param_test.SaturationDynamic3_1_3 saturationdynamic_param_test.In10_1_3))
156
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_8 false))
157
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_9 true))
158
                       (= saturationdynamic_param_test.SaturationDynamic3_1_3 saturationdynamic_param_test.In12_1_3))
159
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_9 false))
160
                       (= saturationdynamic_param_test.SaturationDynamic3_1_3 saturationdynamic_param_test.In11_1_3))
161
               ))
162
       )
163
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_10 true))
164
               (= saturationdynamic_param_test.SaturationDynamic3_1_2 saturationdynamic_param_test.In10_1_2))
165
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_10 false))
166
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_11 true))
167
                       (= saturationdynamic_param_test.SaturationDynamic3_1_2 saturationdynamic_param_test.In12_1_2))
168
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_11 false))
169
                       (= saturationdynamic_param_test.SaturationDynamic3_1_2 saturationdynamic_param_test.In11_1_2))
170
               ))
171
       )
172
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_12 true))
173
               (= saturationdynamic_param_test.SaturationDynamic3_1_1 saturationdynamic_param_test.In10_1_1))
174
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_12 false))
175
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_13 true))
176
                       (= saturationdynamic_param_test.SaturationDynamic3_1_1 saturationdynamic_param_test.In12_1_1))
177
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_13 false))
178
                       (= saturationdynamic_param_test.SaturationDynamic3_1_1 saturationdynamic_param_test.In11_1_1))
179
               ))
180
       )
181
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_14 true))
182
               (= saturationdynamic_param_test.SaturationDynamic2_1_2 saturationdynamic_param_test.In7_1_2))
183
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_14 false))
184
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_15 true))
185
                       (= saturationdynamic_param_test.SaturationDynamic2_1_2 saturationdynamic_param_test.In9_1_2))
186
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_15 false))
187
                       (= saturationdynamic_param_test.SaturationDynamic2_1_2 saturationdynamic_param_test.In8_1_2))
188
               ))
189
       )
190
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_16 true))
191
               (= saturationdynamic_param_test.SaturationDynamic2_1_1 saturationdynamic_param_test.In7_1_1))
192
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_16 false))
193
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_17 true))
194
                       (= saturationdynamic_param_test.SaturationDynamic2_1_1 saturationdynamic_param_test.In9_1_1))
195
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_17 false))
196
                       (= saturationdynamic_param_test.SaturationDynamic2_1_1 saturationdynamic_param_test.In8_1_1))
197
               ))
198
       )
199
       (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_18 true))
200
               (= saturationdynamic_param_test.SaturationDynamic1_1_1 saturationdynamic_param_test.In4_1_1))
201
            (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_18 false))
202
               (and (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_19 true))
203
                       (= saturationdynamic_param_test.SaturationDynamic1_1_1 saturationdynamic_param_test.In6_1_1))
204
                    (or (not (= saturationdynamic_param_test.__saturationdynamic_param_test_19 false))
205
                       (= saturationdynamic_param_test.SaturationDynamic1_1_1 saturationdynamic_param_test.In5_1_1))
206
               ))
207
       )
208
       (= saturationdynamic_param_test.Out4_4_6 saturationdynamic_param_test.SaturationDynamic3_1_6)
209
       (= saturationdynamic_param_test.Out4_4_5 saturationdynamic_param_test.SaturationDynamic3_1_5)
210
       (= saturationdynamic_param_test.Out4_4_4 saturationdynamic_param_test.SaturationDynamic3_1_4)
211
       (= saturationdynamic_param_test.Out4_4_3 saturationdynamic_param_test.SaturationDynamic3_1_3)
212
       (= saturationdynamic_param_test.Out4_4_2 saturationdynamic_param_test.SaturationDynamic3_1_2)
213
       (= saturationdynamic_param_test.Out4_4_1 saturationdynamic_param_test.SaturationDynamic3_1_1)
214
       (= saturationdynamic_param_test.Out3_3_2 saturationdynamic_param_test.SaturationDynamic2_1_2)
215
       (= saturationdynamic_param_test.Out3_3_1 saturationdynamic_param_test.SaturationDynamic2_1_1)
216
       (= saturationdynamic_param_test.Out2_2_1 saturationdynamic_param_test.SaturationDynamic1_1_1)
217
       (= saturationdynamic_param_test.Out1_1_1 saturationdynamic_param_test.SaturationDynamic_1_1)
218
       )
219
  (saturationdynamic_param_test_step saturationdynamic_param_test.In1_1_1
220
                                     saturationdynamic_param_test.In2_1_1
221
                                     saturationdynamic_param_test.In3_1_1
222
                                     saturationdynamic_param_test.In4_1_1
223
                                     saturationdynamic_param_test.In5_1_1
224
                                     saturationdynamic_param_test.In6_1_1
225
                                     saturationdynamic_param_test.In7_1_1
226
                                     saturationdynamic_param_test.In7_1_2
227
                                     saturationdynamic_param_test.In8_1_1
228
                                     saturationdynamic_param_test.In8_1_2
229
                                     saturationdynamic_param_test.In9_1_1
230
                                     saturationdynamic_param_test.In9_1_2
231
                                     saturationdynamic_param_test.In10_1_1
232
                                     saturationdynamic_param_test.In10_1_2
233
                                     saturationdynamic_param_test.In10_1_3
234
                                     saturationdynamic_param_test.In10_1_4
235
                                     saturationdynamic_param_test.In10_1_5
236
                                     saturationdynamic_param_test.In10_1_6
237
                                     saturationdynamic_param_test.In11_1_1
238
                                     saturationdynamic_param_test.In11_1_2
239
                                     saturationdynamic_param_test.In11_1_3
240
                                     saturationdynamic_param_test.In11_1_4
241
                                     saturationdynamic_param_test.In11_1_5
242
                                     saturationdynamic_param_test.In11_1_6
243
                                     saturationdynamic_param_test.In12_1_1
244
                                     saturationdynamic_param_test.In12_1_2
245
                                     saturationdynamic_param_test.In12_1_3
246
                                     saturationdynamic_param_test.In12_1_4
247
                                     saturationdynamic_param_test.In12_1_5
248
                                     saturationdynamic_param_test.In12_1_6
249
                                     saturationdynamic_param_test.Out1_1_1
250
                                     saturationdynamic_param_test.Out2_2_1
251
                                     saturationdynamic_param_test.Out3_3_1
252
                                     saturationdynamic_param_test.Out3_3_2
253
                                     saturationdynamic_param_test.Out4_4_1
254
                                     saturationdynamic_param_test.Out4_4_2
255
                                     saturationdynamic_param_test.Out4_4_3
256
                                     saturationdynamic_param_test.Out4_4_4
257
                                     saturationdynamic_param_test.Out4_4_5
258
                                     saturationdynamic_param_test.Out4_4_6
259
                                     saturationdynamic_param_test.ni_0._arrow._first_c
260
                                     saturationdynamic_param_test.ni_0._arrow._first_x)
261
))
262