Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_trigger_test / trigger_test.smt2 @ 6c3ea955

History | View | Annotate | Download (34.7 KB)

1
; trigger_test_TriggeredSubsystem
2
(declare-var trigger_test_TriggeredSubsystem.In1_1_1 Real)
3
(declare-var trigger_test_TriggeredSubsystem.Out1_1_1 Bool)
4
(declare-var trigger_test_TriggeredSubsystem.LogicalOperator_1_1 Bool)
5
(declare-var trigger_test_TriggeredSubsystem.Trigger_1_1 Real)
6
(declare-rel trigger_test_TriggeredSubsystem (Real Bool))
7
(rule (=> 
8
  (and (= trigger_test_TriggeredSubsystem.Trigger_1_1 1.0)
9
       (= trigger_test_TriggeredSubsystem.LogicalOperator_1_1 (and (not (= trigger_test_TriggeredSubsystem.Trigger_1_1 0.0)) (not (= trigger_test_TriggeredSubsystem.In1_1_1 0.0))))
10
       (= trigger_test_TriggeredSubsystem.Out1_1_1 trigger_test_TriggeredSubsystem.LogicalOperator_1_1)
11
       )
12
  (trigger_test_TriggeredSubsystem trigger_test_TriggeredSubsystem.In1_1_1 trigger_test_TriggeredSubsystem.Out1_1_1)
13
))
14

    
15
; trigger_test_TriggeredSubsystem1
16
(declare-var trigger_test_TriggeredSubsystem1.In2_1_1 Real)
17
(declare-var trigger_test_TriggeredSubsystem1.Out2_1_1 Real)
18
(declare-var trigger_test_TriggeredSubsystem1.Add_1_1 Real)
19
(declare-var trigger_test_TriggeredSubsystem1.Trigger_1_1 Real)
20
(declare-rel trigger_test_TriggeredSubsystem1 (Real Real))
21
(rule (=> 
22
  (and (= trigger_test_TriggeredSubsystem1.Trigger_1_1 (- 1.0))
23
       (= trigger_test_TriggeredSubsystem1.Add_1_1 (+ trigger_test_TriggeredSubsystem1.Trigger_1_1 trigger_test_TriggeredSubsystem1.In2_1_1))
24
       (= trigger_test_TriggeredSubsystem1.Out2_1_1 trigger_test_TriggeredSubsystem1.Add_1_1)
25
       )
26
  (trigger_test_TriggeredSubsystem1 trigger_test_TriggeredSubsystem1.In2_1_1 trigger_test_TriggeredSubsystem1.Out2_1_1)
27
))
28

    
29
; trigger_test_TriggeredSubsystem2
30
(declare-var trigger_test_TriggeredSubsystem2.In1_1_1 Real)
31
(declare-var trigger_test_TriggeredSubsystem2.trigger_test_TriggeredSubsystem2_Trigger_1_1 Bool)
32
(declare-var trigger_test_TriggeredSubsystem2.trigger_test_TriggeredSubsystem2_Trigger_pre_1_1 Bool)
33
(declare-var trigger_test_TriggeredSubsystem2.Out1_1_1 Real)
34
(declare-var trigger_test_TriggeredSubsystem2.Add_1_1 Real)
35
(declare-var trigger_test_TriggeredSubsystem2.Trigger_1_1 Real)
36
(declare-var trigger_test_TriggeredSubsystem2.__trigger_test_TriggeredSubsystem2_1 Bool)
37
(declare-rel trigger_test_TriggeredSubsystem2 (Real Bool Bool Real))
38
(rule (=> 
39
  (and (= trigger_test_TriggeredSubsystem2.__trigger_test_TriggeredSubsystem2_1 (and trigger_test_TriggeredSubsystem2.trigger_test_TriggeredSubsystem2_Trigger_pre_1_1 (not trigger_test_TriggeredSubsystem2.trigger_test_TriggeredSubsystem2_Trigger_1_1)))
40
       (and (or (not (= trigger_test_TriggeredSubsystem2.__trigger_test_TriggeredSubsystem2_1 true))
41
               (= trigger_test_TriggeredSubsystem2.Trigger_1_1 (- 1.0)))
42
            (or (not (= trigger_test_TriggeredSubsystem2.__trigger_test_TriggeredSubsystem2_1 false))
43
               (= trigger_test_TriggeredSubsystem2.Trigger_1_1 1.0))
44
       )
45
       (= trigger_test_TriggeredSubsystem2.Add_1_1 (+ trigger_test_TriggeredSubsystem2.Trigger_1_1 trigger_test_TriggeredSubsystem2.In1_1_1))
46
       (= trigger_test_TriggeredSubsystem2.Out1_1_1 trigger_test_TriggeredSubsystem2.Add_1_1)
47
       )
48
  (trigger_test_TriggeredSubsystem2 trigger_test_TriggeredSubsystem2.In1_1_1 trigger_test_TriggeredSubsystem2.trigger_test_TriggeredSubsystem2_Trigger_1_1 trigger_test_TriggeredSubsystem2.trigger_test_TriggeredSubsystem2_Trigger_pre_1_1 trigger_test_TriggeredSubsystem2.Out1_1_1)
49
))
50

    
51
; trigger_test_TriggeredSubsystem3
52
(declare-var trigger_test_TriggeredSubsystem3.In1_1_1 Real)
53
(declare-var trigger_test_TriggeredSubsystem3.Out1_1_1 Real)
54
(declare-rel trigger_test_TriggeredSubsystem3 (Real Real))
55
(rule (=> 
56
  (= trigger_test_TriggeredSubsystem3.Out1_1_1 trigger_test_TriggeredSubsystem3.In1_1_1)
57
  (trigger_test_TriggeredSubsystem3 trigger_test_TriggeredSubsystem3.In1_1_1 trigger_test_TriggeredSubsystem3.Out1_1_1)
58
))
59

    
60
; trigger_test_TriggeredSubsystem4
61
(declare-var trigger_test_TriggeredSubsystem4.In1_1_1 Real)
62
(declare-var trigger_test_TriggeredSubsystem4.Out1_1_1 Real)
63
(declare-rel trigger_test_TriggeredSubsystem4 (Real Real))
64
(rule (=> 
65
  (= trigger_test_TriggeredSubsystem4.Out1_1_1 trigger_test_TriggeredSubsystem4.In1_1_1)
66
  (trigger_test_TriggeredSubsystem4 trigger_test_TriggeredSubsystem4.In1_1_1 trigger_test_TriggeredSubsystem4.Out1_1_1)
67
))
68

    
69
; trigger_test_TriggeredSubsystem5
70
(declare-var trigger_test_TriggeredSubsystem5.In1_1_1 Real)
71
(declare-var trigger_test_TriggeredSubsystem5.trigger_test_TriggeredSubsystem5_Trigger_1_1 Int)
72
(declare-var trigger_test_TriggeredSubsystem5.trigger_test_TriggeredSubsystem5_Trigger_pre_1_1 Int)
73
(declare-var trigger_test_TriggeredSubsystem5.Out1_1_1 Real)
74
(declare-var trigger_test_TriggeredSubsystem5.Add_1_1 Real)
75
(declare-var trigger_test_TriggeredSubsystem5.Trigger_1_1 Real)
76
(declare-var trigger_test_TriggeredSubsystem5.__trigger_test_TriggeredSubsystem5_1 Bool)
77
(declare-rel trigger_test_TriggeredSubsystem5 (Real Int Int Real))
78
(rule (=> 
79
  (and (= trigger_test_TriggeredSubsystem5.__trigger_test_TriggeredSubsystem5_1 (> trigger_test_TriggeredSubsystem5.trigger_test_TriggeredSubsystem5_Trigger_pre_1_1 trigger_test_TriggeredSubsystem5.trigger_test_TriggeredSubsystem5_Trigger_1_1))
80
       (and (or (not (= trigger_test_TriggeredSubsystem5.__trigger_test_TriggeredSubsystem5_1 true))
81
               (= trigger_test_TriggeredSubsystem5.Trigger_1_1 (- 1.0)))
82
            (or (not (= trigger_test_TriggeredSubsystem5.__trigger_test_TriggeredSubsystem5_1 false))
83
               (= trigger_test_TriggeredSubsystem5.Trigger_1_1 1.0))
84
       )
85
       (= trigger_test_TriggeredSubsystem5.Add_1_1 (+ trigger_test_TriggeredSubsystem5.Trigger_1_1 trigger_test_TriggeredSubsystem5.In1_1_1))
86
       (= trigger_test_TriggeredSubsystem5.Out1_1_1 trigger_test_TriggeredSubsystem5.Add_1_1)
87
       )
88
  (trigger_test_TriggeredSubsystem5 trigger_test_TriggeredSubsystem5.In1_1_1 trigger_test_TriggeredSubsystem5.trigger_test_TriggeredSubsystem5_Trigger_1_1 trigger_test_TriggeredSubsystem5.trigger_test_TriggeredSubsystem5_Trigger_pre_1_1 trigger_test_TriggeredSubsystem5.Out1_1_1)
89
))
90

    
91
; trigger_test_TriggeredSubsystem6
92
(declare-var trigger_test_TriggeredSubsystem6.In1_1_1 Real)
93
(declare-var trigger_test_TriggeredSubsystem6.Out1_1_1 Real)
94
(declare-rel trigger_test_TriggeredSubsystem6 (Real Real))
95
(rule (=> 
96
  (= trigger_test_TriggeredSubsystem6.Out1_1_1 trigger_test_TriggeredSubsystem6.In1_1_1)
97
  (trigger_test_TriggeredSubsystem6 trigger_test_TriggeredSubsystem6.In1_1_1 trigger_test_TriggeredSubsystem6.Out1_1_1)
98
))
99

    
100
; trigger_test_TriggeredSubsystem7
101
(declare-var trigger_test_TriggeredSubsystem7.In1_1_1 Real)
102
(declare-var trigger_test_TriggeredSubsystem7.Out1_1_1 Real)
103
(declare-rel trigger_test_TriggeredSubsystem7 (Real Real))
104
(rule (=> 
105
  (= trigger_test_TriggeredSubsystem7.Out1_1_1 trigger_test_TriggeredSubsystem7.In1_1_1)
106
  (trigger_test_TriggeredSubsystem7 trigger_test_TriggeredSubsystem7.In1_1_1 trigger_test_TriggeredSubsystem7.Out1_1_1)
107
))
108

    
109
; trigger_test_TriggeredSubsystem8
110
(declare-var trigger_test_TriggeredSubsystem8.In1_1_1 Real)
111
(declare-var trigger_test_TriggeredSubsystem8.Out1_1_1 Real)
112
(declare-rel trigger_test_TriggeredSubsystem8 (Real Real))
113
(rule (=> 
114
  (= trigger_test_TriggeredSubsystem8.Out1_1_1 trigger_test_TriggeredSubsystem8.In1_1_1)
115
  (trigger_test_TriggeredSubsystem8 trigger_test_TriggeredSubsystem8.In1_1_1 trigger_test_TriggeredSubsystem8.Out1_1_1)
116
))
117

    
118
; trigger_test_TriggeredSubsystem9
119
(declare-var trigger_test_TriggeredSubsystem9.In1_1_1 Real)
120
(declare-var trigger_test_TriggeredSubsystem9.In1_1_2 Real)
121
(declare-var trigger_test_TriggeredSubsystem9.In1_1_3 Real)
122
(declare-var trigger_test_TriggeredSubsystem9.trigger_test_TriggeredSubsystem9_Trigger_1_1 Bool)
123
(declare-var trigger_test_TriggeredSubsystem9.trigger_test_TriggeredSubsystem9_Trigger_pre_1_1 Bool)
124
(declare-var trigger_test_TriggeredSubsystem9.Out1_1_1 Real)
125
(declare-var trigger_test_TriggeredSubsystem9.Out1_1_2 Real)
126
(declare-var trigger_test_TriggeredSubsystem9.Out1_1_3 Real)
127
(declare-var trigger_test_TriggeredSubsystem9.Add_1_1 Real)
128
(declare-var trigger_test_TriggeredSubsystem9.Add_1_2 Real)
129
(declare-var trigger_test_TriggeredSubsystem9.Add_1_3 Real)
130
(declare-var trigger_test_TriggeredSubsystem9.Trigger_1_1 Real)
131
(declare-var trigger_test_TriggeredSubsystem9.__trigger_test_TriggeredSubsystem9_1 Bool)
132
(declare-rel trigger_test_TriggeredSubsystem9 (Real Real Real Bool Bool Real Real Real))
133
(rule (=> 
134
  (and (= trigger_test_TriggeredSubsystem9.__trigger_test_TriggeredSubsystem9_1 (and trigger_test_TriggeredSubsystem9.trigger_test_TriggeredSubsystem9_Trigger_pre_1_1 (not trigger_test_TriggeredSubsystem9.trigger_test_TriggeredSubsystem9_Trigger_1_1)))
135
       (and (or (not (= trigger_test_TriggeredSubsystem9.__trigger_test_TriggeredSubsystem9_1 true))
136
               (= trigger_test_TriggeredSubsystem9.Trigger_1_1 (- 1.0)))
137
            (or (not (= trigger_test_TriggeredSubsystem9.__trigger_test_TriggeredSubsystem9_1 false))
138
               (= trigger_test_TriggeredSubsystem9.Trigger_1_1 1.0))
139
       )
140
       (= trigger_test_TriggeredSubsystem9.Add_1_3 (+ trigger_test_TriggeredSubsystem9.Trigger_1_1 trigger_test_TriggeredSubsystem9.In1_1_3))
141
       (= trigger_test_TriggeredSubsystem9.Out1_1_3 trigger_test_TriggeredSubsystem9.Add_1_3)
142
       (= trigger_test_TriggeredSubsystem9.Add_1_2 (+ trigger_test_TriggeredSubsystem9.Trigger_1_1 trigger_test_TriggeredSubsystem9.In1_1_2))
143
       (= trigger_test_TriggeredSubsystem9.Out1_1_2 trigger_test_TriggeredSubsystem9.Add_1_2)
144
       (= trigger_test_TriggeredSubsystem9.Add_1_1 (+ trigger_test_TriggeredSubsystem9.Trigger_1_1 trigger_test_TriggeredSubsystem9.In1_1_1))
145
       (= trigger_test_TriggeredSubsystem9.Out1_1_1 trigger_test_TriggeredSubsystem9.Add_1_1)
146
       )
147
  (trigger_test_TriggeredSubsystem9 trigger_test_TriggeredSubsystem9.In1_1_1 trigger_test_TriggeredSubsystem9.In1_1_2 trigger_test_TriggeredSubsystem9.In1_1_3 trigger_test_TriggeredSubsystem9.trigger_test_TriggeredSubsystem9_Trigger_1_1 trigger_test_TriggeredSubsystem9.trigger_test_TriggeredSubsystem9_Trigger_pre_1_1 trigger_test_TriggeredSubsystem9.Out1_1_1 trigger_test_TriggeredSubsystem9.Out1_1_2 trigger_test_TriggeredSubsystem9.Out1_1_3)
148
))
149

    
150
; trigger_test
151
(declare-var trigger_test.In1_1_1 Real)
152
(declare-var trigger_test.In2_1_1 Bool)
153
(declare-var trigger_test.In3_1_1 Real)
154
(declare-var trigger_test.In4_1_1 Int)
155
(declare-var trigger_test.In5_1_1 Real)
156
(declare-var trigger_test.In6_1_1 Real)
157
(declare-var trigger_test.In7_1_1 Real)
158
(declare-var trigger_test.In7_1_2 Real)
159
(declare-var trigger_test.In7_1_3 Real)
160
(declare-var trigger_test.In8_1_1 Bool)
161
(declare-var trigger_test.Out1_1_1 Bool)
162
(declare-var trigger_test.Out2_2_1 Real)
163
(declare-var trigger_test.Out3_3_1 Real)
164
(declare-var trigger_test.Out4_4_1 Real)
165
(declare-var trigger_test.Out5_5_1 Real)
166
(declare-var trigger_test.Out6_6_1 Real)
167
(declare-var trigger_test.Out7_7_1 Real)
168
(declare-var trigger_test.Out8_8_1 Real)
169
(declare-var trigger_test.Out9_9_1 Real)
170
(declare-var trigger_test.Out10_10_1 Real)
171
(declare-var trigger_test.Out10_10_2 Real)
172
(declare-var trigger_test.Out10_10_3 Real)
173
(declare-var trigger_test.TriggeredSubsystem2pre_In2_1_1_c Bool)
174
(declare-var trigger_test.TriggeredSubsystem5pre_In4_1_1_c Int)
175
(declare-var trigger_test.TriggeredSubsystem9pre_In8_1_1_c Bool)
176
(declare-var trigger_test.__trigger_test_10_c Real)
177
(declare-var trigger_test.__trigger_test_12_c Real)
178
(declare-var trigger_test.__trigger_test_14_c Real)
179
(declare-var trigger_test.__trigger_test_16_c Real)
180
(declare-var trigger_test.__trigger_test_18_c Real)
181
(declare-var trigger_test.__trigger_test_20_c Real)
182
(declare-var trigger_test.__trigger_test_22_c Real)
183
(declare-var trigger_test.__trigger_test_24_c Real)
184
(declare-var trigger_test.__trigger_test_26_c Bool)
185
(declare-var trigger_test.__trigger_test_5_c Real)
186
(declare-var trigger_test.__trigger_test_6_c Real)
187
(declare-var trigger_test.__trigger_test_7_c Real)
188
(declare-var trigger_test.__trigger_test_9_c Real)
189
(declare-var trigger_test.ni_0._arrow._first_c Bool)
190
(declare-var trigger_test.TriggeredSubsystem2pre_In2_1_1_m Bool)
191
(declare-var trigger_test.TriggeredSubsystem5pre_In4_1_1_m Int)
192
(declare-var trigger_test.TriggeredSubsystem9pre_In8_1_1_m Bool)
193
(declare-var trigger_test.__trigger_test_10_m Real)
194
(declare-var trigger_test.__trigger_test_12_m Real)
195
(declare-var trigger_test.__trigger_test_14_m Real)
196
(declare-var trigger_test.__trigger_test_16_m Real)
197
(declare-var trigger_test.__trigger_test_18_m Real)
198
(declare-var trigger_test.__trigger_test_20_m Real)
199
(declare-var trigger_test.__trigger_test_22_m Real)
200
(declare-var trigger_test.__trigger_test_24_m Real)
201
(declare-var trigger_test.__trigger_test_26_m Bool)
202
(declare-var trigger_test.__trigger_test_5_m Real)
203
(declare-var trigger_test.__trigger_test_6_m Real)
204
(declare-var trigger_test.__trigger_test_7_m Real)
205
(declare-var trigger_test.__trigger_test_9_m Real)
206
(declare-var trigger_test.ni_0._arrow._first_m Bool)
207
(declare-var trigger_test.TriggeredSubsystem2pre_In2_1_1_x Bool)
208
(declare-var trigger_test.TriggeredSubsystem5pre_In4_1_1_x Int)
209
(declare-var trigger_test.TriggeredSubsystem9pre_In8_1_1_x Bool)
210
(declare-var trigger_test.__trigger_test_10_x Real)
211
(declare-var trigger_test.__trigger_test_12_x Real)
212
(declare-var trigger_test.__trigger_test_14_x Real)
213
(declare-var trigger_test.__trigger_test_16_x Real)
214
(declare-var trigger_test.__trigger_test_18_x Real)
215
(declare-var trigger_test.__trigger_test_20_x Real)
216
(declare-var trigger_test.__trigger_test_22_x Real)
217
(declare-var trigger_test.__trigger_test_24_x Real)
218
(declare-var trigger_test.__trigger_test_26_x Bool)
219
(declare-var trigger_test.__trigger_test_5_x Real)
220
(declare-var trigger_test.__trigger_test_6_x Real)
221
(declare-var trigger_test.__trigger_test_7_x Real)
222
(declare-var trigger_test.__trigger_test_9_x Real)
223
(declare-var trigger_test.ni_0._arrow._first_x Bool)
224
(declare-var trigger_test.TriggeredSubsystem1In2_1_1_cond_str_trigger Bool)
225
(declare-var trigger_test.TriggeredSubsystem1_1_1 Real)
226
(declare-var trigger_test.TriggeredSubsystem2In2_1_1_cond_str_trigger Bool)
227
(declare-var trigger_test.TriggeredSubsystem2_1_1 Real)
228
(declare-var trigger_test.TriggeredSubsystem3In4_1_1_cond_str_trigger Bool)
229
(declare-var trigger_test.TriggeredSubsystem3_1_1 Real)
230
(declare-var trigger_test.TriggeredSubsystem4In4_1_1_cond_str_trigger Bool)
231
(declare-var trigger_test.TriggeredSubsystem4_1_1 Real)
232
(declare-var trigger_test.TriggeredSubsystem5In4_1_1_cond_str_trigger Bool)
233
(declare-var trigger_test.TriggeredSubsystem5_1_1 Real)
234
(declare-var trigger_test.TriggeredSubsystem6In6_1_1_cond_str_trigger Bool)
235
(declare-var trigger_test.TriggeredSubsystem6_1_1 Real)
236
(declare-var trigger_test.TriggeredSubsystem7In6_1_1_cond_str_trigger Bool)
237
(declare-var trigger_test.TriggeredSubsystem7_1_1 Real)
238
(declare-var trigger_test.TriggeredSubsystem8In6_1_1_cond_str_trigger Bool)
239
(declare-var trigger_test.TriggeredSubsystem8_1_1 Real)
240
(declare-var trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger Bool)
241
(declare-var trigger_test.TriggeredSubsystem9_1_1 Real)
242
(declare-var trigger_test.TriggeredSubsystem9_1_2 Real)
243
(declare-var trigger_test.TriggeredSubsystem9_1_3 Real)
244
(declare-var trigger_test.TriggeredSubsystemIn2_1_1_cond_str_trigger Bool)
245
(declare-var trigger_test.TriggeredSubsystem_1_1 Bool)
246
(declare-var trigger_test.__trigger_test_1 Bool)
247
(declare-var trigger_test.__trigger_test_11 Real)
248
(declare-var trigger_test.__trigger_test_13 Real)
249
(declare-var trigger_test.__trigger_test_15 Real)
250
(declare-var trigger_test.__trigger_test_17 Real)
251
(declare-var trigger_test.__trigger_test_19 Real)
252
(declare-var trigger_test.__trigger_test_2 Real)
253
(declare-var trigger_test.__trigger_test_21 Real)
254
(declare-var trigger_test.__trigger_test_23 Real)
255
(declare-var trigger_test.__trigger_test_25 Bool)
256
(declare-var trigger_test.__trigger_test_3 Real)
257
(declare-var trigger_test.__trigger_test_4 Real)
258
(declare-var trigger_test.__trigger_test_8 Real)
259
(declare-var trigger_test.i_virtual_local Real)
260
(declare-rel trigger_test_reset (Bool Int Bool Real Real Real Real Real Real Real Real Bool Real Real Real Real Bool Bool Int Bool Real Real Real Real Real Real Real Real Bool Real Real Real Real Bool))
261
(declare-rel trigger_test_step (Real Bool Real Int Real Real Real Real Real Bool Bool Real Real Real Real Real Real Real Real Real Real Real Bool Int Bool Real Real Real Real Real Real Real Real Bool Real Real Real Real Bool Bool Int Bool Real Real Real Real Real Real Real Real Bool Real Real Real Real Bool))
262

    
263
(rule (=> 
264
  (and 
265
       (= trigger_test.TriggeredSubsystem2pre_In2_1_1_m trigger_test.TriggeredSubsystem2pre_In2_1_1_c)
266
       (= trigger_test.TriggeredSubsystem5pre_In4_1_1_m trigger_test.TriggeredSubsystem5pre_In4_1_1_c)
267
       (= trigger_test.TriggeredSubsystem9pre_In8_1_1_m trigger_test.TriggeredSubsystem9pre_In8_1_1_c)
268
       (= trigger_test.__trigger_test_10_m trigger_test.__trigger_test_10_c)
269
       (= trigger_test.__trigger_test_12_m trigger_test.__trigger_test_12_c)
270
       (= trigger_test.__trigger_test_14_m trigger_test.__trigger_test_14_c)
271
       (= trigger_test.__trigger_test_16_m trigger_test.__trigger_test_16_c)
272
       (= trigger_test.__trigger_test_18_m trigger_test.__trigger_test_18_c)
273
       (= trigger_test.__trigger_test_20_m trigger_test.__trigger_test_20_c)
274
       (= trigger_test.__trigger_test_22_m trigger_test.__trigger_test_22_c)
275
       (= trigger_test.__trigger_test_24_m trigger_test.__trigger_test_24_c)
276
       (= trigger_test.__trigger_test_26_m trigger_test.__trigger_test_26_c)
277
       (= trigger_test.__trigger_test_5_m trigger_test.__trigger_test_5_c)
278
       (= trigger_test.__trigger_test_6_m trigger_test.__trigger_test_6_c)
279
       (= trigger_test.__trigger_test_7_m trigger_test.__trigger_test_7_c)
280
       (= trigger_test.__trigger_test_9_m trigger_test.__trigger_test_9_c)
281
       (= trigger_test.ni_0._arrow._first_m true)
282
  )
283
  (trigger_test_reset trigger_test.TriggeredSubsystem2pre_In2_1_1_c
284
                      trigger_test.TriggeredSubsystem5pre_In4_1_1_c
285
                      trigger_test.TriggeredSubsystem9pre_In8_1_1_c
286
                      trigger_test.__trigger_test_10_c
287
                      trigger_test.__trigger_test_12_c
288
                      trigger_test.__trigger_test_14_c
289
                      trigger_test.__trigger_test_16_c
290
                      trigger_test.__trigger_test_18_c
291
                      trigger_test.__trigger_test_20_c
292
                      trigger_test.__trigger_test_22_c
293
                      trigger_test.__trigger_test_24_c
294
                      trigger_test.__trigger_test_26_c
295
                      trigger_test.__trigger_test_5_c
296
                      trigger_test.__trigger_test_6_c
297
                      trigger_test.__trigger_test_7_c
298
                      trigger_test.__trigger_test_9_c
299
                      trigger_test.ni_0._arrow._first_c
300
                      trigger_test.TriggeredSubsystem2pre_In2_1_1_m
301
                      trigger_test.TriggeredSubsystem5pre_In4_1_1_m
302
                      trigger_test.TriggeredSubsystem9pre_In8_1_1_m
303
                      trigger_test.__trigger_test_10_m
304
                      trigger_test.__trigger_test_12_m
305
                      trigger_test.__trigger_test_14_m
306
                      trigger_test.__trigger_test_16_m
307
                      trigger_test.__trigger_test_18_m
308
                      trigger_test.__trigger_test_20_m
309
                      trigger_test.__trigger_test_22_m
310
                      trigger_test.__trigger_test_24_m
311
                      trigger_test.__trigger_test_26_m
312
                      trigger_test.__trigger_test_5_m
313
                      trigger_test.__trigger_test_6_m
314
                      trigger_test.__trigger_test_7_m
315
                      trigger_test.__trigger_test_9_m
316
                      trigger_test.ni_0._arrow._first_m)
317
))
318

    
319
(rule (=> 
320
  (and (= trigger_test.ni_0._arrow._first_m trigger_test.ni_0._arrow._first_c)
321
       (and (= trigger_test.__trigger_test_1 (ite trigger_test.ni_0._arrow._first_m true false))
322
            (= trigger_test.ni_0._arrow._first_x false))
323
       (and (or (not (= trigger_test.__trigger_test_1 true))
324
               (= trigger_test.i_virtual_local 0.0))
325
            (or (not (= trigger_test.__trigger_test_1 false))
326
               (= trigger_test.i_virtual_local 1.0))
327
       )
328
       (trigger_test_TriggeredSubsystem8 trigger_test.In5_1_1
329
                                         trigger_test.__trigger_test_8)
330
       (and (or (not (= trigger_test.__trigger_test_1 true))
331
               (= trigger_test.TriggeredSubsystem8In6_1_1_cond_str_trigger false))
332
            (or (not (= trigger_test.__trigger_test_1 false))
333
               (= trigger_test.TriggeredSubsystem8In6_1_1_cond_str_trigger (or (and (> trigger_test.__trigger_test_10_c 0.0) (<= trigger_test.In6_1_1 0.0)) (and (<= trigger_test.__trigger_test_10_c 0.0) (> trigger_test.In6_1_1 0.0)))))
334
       )
335
       (and (or (not (= trigger_test.TriggeredSubsystem8In6_1_1_cond_str_trigger true))
336
               (= trigger_test.TriggeredSubsystem8_1_1 trigger_test.__trigger_test_8))
337
            (or (not (= trigger_test.TriggeredSubsystem8In6_1_1_cond_str_trigger false))
338
               (= trigger_test.TriggeredSubsystem8_1_1 trigger_test.__trigger_test_9_c))
339
       )
340
       (= trigger_test.__trigger_test_9_x trigger_test.TriggeredSubsystem8_1_1)
341
       (trigger_test_TriggeredSubsystem9 trigger_test.In7_1_1
342
                                         trigger_test.In7_1_2
343
                                         trigger_test.In7_1_3
344
                                         trigger_test.In8_1_1
345
                                         trigger_test.TriggeredSubsystem9pre_In8_1_1_c
346
                                         trigger_test.__trigger_test_2
347
                                         trigger_test.__trigger_test_3
348
                                         trigger_test.__trigger_test_4)
349
       (and (or (not (= trigger_test.__trigger_test_1 true))
350
               (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger false))
351
            (or (not (= trigger_test.__trigger_test_1 false))
352
               (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger (not (= trigger_test.TriggeredSubsystem9pre_In8_1_1_c trigger_test.In8_1_1))))
353
       )
354
       (and (or (not (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger true))
355
               (= trigger_test.TriggeredSubsystem9_1_1 trigger_test.__trigger_test_2))
356
            (or (not (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger false))
357
               (= trigger_test.TriggeredSubsystem9_1_1 trigger_test.__trigger_test_7_c))
358
       )
359
       (= trigger_test.__trigger_test_7_x trigger_test.TriggeredSubsystem9_1_1)
360
       (and (or (not (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger true))
361
               (= trigger_test.TriggeredSubsystem9_1_2 trigger_test.__trigger_test_3))
362
            (or (not (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger false))
363
               (= trigger_test.TriggeredSubsystem9_1_2 trigger_test.__trigger_test_6_c))
364
       )
365
       (= trigger_test.__trigger_test_6_x trigger_test.TriggeredSubsystem9_1_2)
366
       (and (or (not (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger true))
367
               (= trigger_test.TriggeredSubsystem9_1_3 trigger_test.__trigger_test_4))
368
            (or (not (= trigger_test.TriggeredSubsystem9In8_1_1_cond_str_trigger false))
369
               (= trigger_test.TriggeredSubsystem9_1_3 trigger_test.__trigger_test_5_c))
370
       )
371
       (= trigger_test.__trigger_test_5_x trigger_test.TriggeredSubsystem9_1_3)
372
       (trigger_test_TriggeredSubsystem trigger_test.In1_1_1
373
                                        trigger_test.__trigger_test_25)
374
       (and (or (not (= trigger_test.__trigger_test_1 true))
375
               (= trigger_test.TriggeredSubsystemIn2_1_1_cond_str_trigger false))
376
            (or (not (= trigger_test.__trigger_test_1 false))
377
               (= trigger_test.TriggeredSubsystemIn2_1_1_cond_str_trigger (and (not trigger_test.TriggeredSubsystem2pre_In2_1_1_c) trigger_test.In2_1_1)))
378
       )
379
       (and (or (not (= trigger_test.TriggeredSubsystemIn2_1_1_cond_str_trigger true))
380
               (= trigger_test.TriggeredSubsystem_1_1 trigger_test.__trigger_test_25))
381
            (or (not (= trigger_test.TriggeredSubsystemIn2_1_1_cond_str_trigger false))
382
               (= trigger_test.TriggeredSubsystem_1_1 trigger_test.__trigger_test_26_c))
383
       )
384
       (= trigger_test.__trigger_test_26_x trigger_test.TriggeredSubsystem_1_1)
385
       (trigger_test_TriggeredSubsystem1 trigger_test.In1_1_1
386
                                         trigger_test.__trigger_test_23)
387
       (and (or (not (= trigger_test.__trigger_test_1 true))
388
               (= trigger_test.TriggeredSubsystem1In2_1_1_cond_str_trigger false))
389
            (or (not (= trigger_test.__trigger_test_1 false))
390
               (= trigger_test.TriggeredSubsystem1In2_1_1_cond_str_trigger (and trigger_test.TriggeredSubsystem2pre_In2_1_1_c (not trigger_test.In2_1_1))))
391
       )
392
       (and (or (not (= trigger_test.TriggeredSubsystem1In2_1_1_cond_str_trigger true))
393
               (= trigger_test.TriggeredSubsystem1_1_1 trigger_test.__trigger_test_23))
394
            (or (not (= trigger_test.TriggeredSubsystem1In2_1_1_cond_str_trigger false))
395
               (= trigger_test.TriggeredSubsystem1_1_1 trigger_test.__trigger_test_24_c))
396
       )
397
       (= trigger_test.__trigger_test_24_x trigger_test.TriggeredSubsystem1_1_1)
398
       (trigger_test_TriggeredSubsystem2 trigger_test.In1_1_1
399
                                         trigger_test.In2_1_1
400
                                         trigger_test.TriggeredSubsystem2pre_In2_1_1_c
401
                                         trigger_test.__trigger_test_21)
402
       (and (or (not (= trigger_test.__trigger_test_1 true))
403
               (= trigger_test.TriggeredSubsystem2In2_1_1_cond_str_trigger false))
404
            (or (not (= trigger_test.__trigger_test_1 false))
405
               (= trigger_test.TriggeredSubsystem2In2_1_1_cond_str_trigger (not (= trigger_test.TriggeredSubsystem2pre_In2_1_1_c trigger_test.In2_1_1))))
406
       )
407
       (and (or (not (= trigger_test.TriggeredSubsystem2In2_1_1_cond_str_trigger true))
408
               (= trigger_test.TriggeredSubsystem2_1_1 trigger_test.__trigger_test_21))
409
            (or (not (= trigger_test.TriggeredSubsystem2In2_1_1_cond_str_trigger false))
410
               (= trigger_test.TriggeredSubsystem2_1_1 trigger_test.__trigger_test_22_c))
411
       )
412
       (= trigger_test.__trigger_test_22_x trigger_test.TriggeredSubsystem2_1_1)
413
       (trigger_test_TriggeredSubsystem3 trigger_test.In3_1_1
414
                                         trigger_test.__trigger_test_19)
415
       (and (or (not (= trigger_test.__trigger_test_1 true))
416
               (= trigger_test.TriggeredSubsystem3In4_1_1_cond_str_trigger false))
417
            (or (not (= trigger_test.__trigger_test_1 false))
418
               (= trigger_test.TriggeredSubsystem3In4_1_1_cond_str_trigger (and (<= trigger_test.TriggeredSubsystem5pre_In4_1_1_c 0) (> trigger_test.In4_1_1 0))))
419
       )
420
       (and (or (not (= trigger_test.TriggeredSubsystem3In4_1_1_cond_str_trigger true))
421
               (= trigger_test.TriggeredSubsystem3_1_1 trigger_test.__trigger_test_19))
422
            (or (not (= trigger_test.TriggeredSubsystem3In4_1_1_cond_str_trigger false))
423
               (= trigger_test.TriggeredSubsystem3_1_1 trigger_test.__trigger_test_20_c))
424
       )
425
       (= trigger_test.__trigger_test_20_x trigger_test.TriggeredSubsystem3_1_1)
426
       (trigger_test_TriggeredSubsystem4 trigger_test.In3_1_1
427
                                         trigger_test.__trigger_test_17)
428
       (and (or (not (= trigger_test.__trigger_test_1 true))
429
               (= trigger_test.TriggeredSubsystem4In4_1_1_cond_str_trigger false))
430
            (or (not (= trigger_test.__trigger_test_1 false))
431
               (= trigger_test.TriggeredSubsystem4In4_1_1_cond_str_trigger (and (> trigger_test.TriggeredSubsystem5pre_In4_1_1_c 0) (<= trigger_test.In4_1_1 0))))
432
       )
433
       (and (or (not (= trigger_test.TriggeredSubsystem4In4_1_1_cond_str_trigger true))
434
               (= trigger_test.TriggeredSubsystem4_1_1 trigger_test.__trigger_test_17))
435
            (or (not (= trigger_test.TriggeredSubsystem4In4_1_1_cond_str_trigger false))
436
               (= trigger_test.TriggeredSubsystem4_1_1 trigger_test.__trigger_test_18_c))
437
       )
438
       (= trigger_test.__trigger_test_18_x trigger_test.TriggeredSubsystem4_1_1)
439
       (trigger_test_TriggeredSubsystem5 trigger_test.In3_1_1
440
                                         trigger_test.In4_1_1
441
                                         trigger_test.TriggeredSubsystem5pre_In4_1_1_c
442
                                         trigger_test.__trigger_test_15)
443
       (and (or (not (= trigger_test.__trigger_test_1 true))
444
               (= trigger_test.TriggeredSubsystem5In4_1_1_cond_str_trigger false))
445
            (or (not (= trigger_test.__trigger_test_1 false))
446
               (= trigger_test.TriggeredSubsystem5In4_1_1_cond_str_trigger (or (and (> trigger_test.TriggeredSubsystem5pre_In4_1_1_c 0) (<= trigger_test.In4_1_1 0)) (and (<= trigger_test.TriggeredSubsystem5pre_In4_1_1_c 0) (> trigger_test.In4_1_1 0)))))
447
       )
448
       (and (or (not (= trigger_test.TriggeredSubsystem5In4_1_1_cond_str_trigger true))
449
               (= trigger_test.TriggeredSubsystem5_1_1 trigger_test.__trigger_test_15))
450
            (or (not (= trigger_test.TriggeredSubsystem5In4_1_1_cond_str_trigger false))
451
               (= trigger_test.TriggeredSubsystem5_1_1 trigger_test.__trigger_test_16_c))
452
       )
453
       (= trigger_test.__trigger_test_16_x trigger_test.TriggeredSubsystem5_1_1)
454
       (trigger_test_TriggeredSubsystem6 trigger_test.In5_1_1
455
                                         trigger_test.__trigger_test_13)
456
       (and (or (not (= trigger_test.__trigger_test_1 true))
457
               (= trigger_test.TriggeredSubsystem6In6_1_1_cond_str_trigger false))
458
            (or (not (= trigger_test.__trigger_test_1 false))
459
               (= trigger_test.TriggeredSubsystem6In6_1_1_cond_str_trigger (and (<= trigger_test.__trigger_test_10_c 0.0) (> trigger_test.In6_1_1 0.0))))
460
       )
461
       (and (or (not (= trigger_test.TriggeredSubsystem6In6_1_1_cond_str_trigger true))
462
               (= trigger_test.TriggeredSubsystem6_1_1 trigger_test.__trigger_test_13))
463
            (or (not (= trigger_test.TriggeredSubsystem6In6_1_1_cond_str_trigger false))
464
               (= trigger_test.TriggeredSubsystem6_1_1 trigger_test.__trigger_test_14_c))
465
       )
466
       (= trigger_test.__trigger_test_14_x trigger_test.TriggeredSubsystem6_1_1)
467
       (trigger_test_TriggeredSubsystem7 trigger_test.In5_1_1
468
                                         trigger_test.__trigger_test_11)
469
       (and (or (not (= trigger_test.__trigger_test_1 true))
470
               (= trigger_test.TriggeredSubsystem7In6_1_1_cond_str_trigger false))
471
            (or (not (= trigger_test.__trigger_test_1 false))
472
               (= trigger_test.TriggeredSubsystem7In6_1_1_cond_str_trigger (and (> trigger_test.__trigger_test_10_c 0.0) (<= trigger_test.In6_1_1 0.0))))
473
       )
474
       (and (or (not (= trigger_test.TriggeredSubsystem7In6_1_1_cond_str_trigger true))
475
               (= trigger_test.TriggeredSubsystem7_1_1 trigger_test.__trigger_test_11))
476
            (or (not (= trigger_test.TriggeredSubsystem7In6_1_1_cond_str_trigger false))
477
               (= trigger_test.TriggeredSubsystem7_1_1 trigger_test.__trigger_test_12_c))
478
       )
479
       (= trigger_test.__trigger_test_12_x trigger_test.TriggeredSubsystem7_1_1)
480
       (= trigger_test.__trigger_test_10_x trigger_test.In6_1_1)
481
       (= trigger_test.TriggeredSubsystem9pre_In8_1_1_x trigger_test.In8_1_1)
482
       (= trigger_test.TriggeredSubsystem5pre_In4_1_1_x trigger_test.In4_1_1)
483
       (= trigger_test.TriggeredSubsystem2pre_In2_1_1_x trigger_test.In2_1_1)
484
       (= trigger_test.Out9_9_1 trigger_test.TriggeredSubsystem8_1_1)
485
       (= trigger_test.Out8_8_1 trigger_test.TriggeredSubsystem7_1_1)
486
       (= trigger_test.Out7_7_1 trigger_test.TriggeredSubsystem6_1_1)
487
       (= trigger_test.Out6_6_1 trigger_test.TriggeredSubsystem5_1_1)
488
       (= trigger_test.Out5_5_1 trigger_test.TriggeredSubsystem4_1_1)
489
       (= trigger_test.Out4_4_1 trigger_test.TriggeredSubsystem3_1_1)
490
       (= trigger_test.Out3_3_1 trigger_test.TriggeredSubsystem2_1_1)
491
       (= trigger_test.Out2_2_1 trigger_test.TriggeredSubsystem1_1_1)
492
       (= trigger_test.Out1_1_1 trigger_test.TriggeredSubsystem_1_1)
493
       (= trigger_test.Out10_10_3 trigger_test.TriggeredSubsystem9_1_3)
494
       (= trigger_test.Out10_10_2 trigger_test.TriggeredSubsystem9_1_2)
495
       (= trigger_test.Out10_10_1 trigger_test.TriggeredSubsystem9_1_1)
496
       )
497
  (trigger_test_step trigger_test.In1_1_1
498
                     trigger_test.In2_1_1
499
                     trigger_test.In3_1_1
500
                     trigger_test.In4_1_1
501
                     trigger_test.In5_1_1
502
                     trigger_test.In6_1_1
503
                     trigger_test.In7_1_1
504
                     trigger_test.In7_1_2
505
                     trigger_test.In7_1_3
506
                     trigger_test.In8_1_1
507
                     trigger_test.Out1_1_1
508
                     trigger_test.Out2_2_1
509
                     trigger_test.Out3_3_1
510
                     trigger_test.Out4_4_1
511
                     trigger_test.Out5_5_1
512
                     trigger_test.Out6_6_1
513
                     trigger_test.Out7_7_1
514
                     trigger_test.Out8_8_1
515
                     trigger_test.Out9_9_1
516
                     trigger_test.Out10_10_1
517
                     trigger_test.Out10_10_2
518
                     trigger_test.Out10_10_3
519
                     trigger_test.TriggeredSubsystem2pre_In2_1_1_c
520
                     trigger_test.TriggeredSubsystem5pre_In4_1_1_c
521
                     trigger_test.TriggeredSubsystem9pre_In8_1_1_c
522
                     trigger_test.__trigger_test_10_c
523
                     trigger_test.__trigger_test_12_c
524
                     trigger_test.__trigger_test_14_c
525
                     trigger_test.__trigger_test_16_c
526
                     trigger_test.__trigger_test_18_c
527
                     trigger_test.__trigger_test_20_c
528
                     trigger_test.__trigger_test_22_c
529
                     trigger_test.__trigger_test_24_c
530
                     trigger_test.__trigger_test_26_c
531
                     trigger_test.__trigger_test_5_c
532
                     trigger_test.__trigger_test_6_c
533
                     trigger_test.__trigger_test_7_c
534
                     trigger_test.__trigger_test_9_c
535
                     trigger_test.ni_0._arrow._first_c
536
                     trigger_test.TriggeredSubsystem2pre_In2_1_1_x
537
                     trigger_test.TriggeredSubsystem5pre_In4_1_1_x
538
                     trigger_test.TriggeredSubsystem9pre_In8_1_1_x
539
                     trigger_test.__trigger_test_10_x
540
                     trigger_test.__trigger_test_12_x
541
                     trigger_test.__trigger_test_14_x
542
                     trigger_test.__trigger_test_16_x
543
                     trigger_test.__trigger_test_18_x
544
                     trigger_test.__trigger_test_20_x
545
                     trigger_test.__trigger_test_22_x
546
                     trigger_test.__trigger_test_24_x
547
                     trigger_test.__trigger_test_26_x
548
                     trigger_test.__trigger_test_5_x
549
                     trigger_test.__trigger_test_6_x
550
                     trigger_test.__trigger_test_7_x
551
                     trigger_test.__trigger_test_9_x
552
                     trigger_test.ni_0._arrow._first_x)
553
))
554