Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Events7 / Events7.smt2 @ eb639349

History | View | Annotate | Download (207 KB)

1
(declare-datatypes () ((events7_t1__type POINTEvents7_T1 POINT__TO__T1_A_1 T1_A__TO__T1_B_1 T1_B__TO__T1_A_1 T1_A_IDL T1_B_IDL)));
2

    
3
(declare-datatypes () ((events7_events7__type POINTEvents7_Events7 EVENTS7_EVENTS7_PARALLEL_ENTRY EVENTS7_EVENTS7_PARALLEL_IDL)));
4

    
5
(declare-datatypes () ((events7_t2__type POINTEvents7_T2 POINT__TO__T2_C_1 T2_C__TO__T2_D_1 T2_D__TO__T2_C_1 T2_C_IDL T2_D_IDL)));
6

    
7
; T1_A_en
8
(declare-var T1_A_en.idEvents7_T1_1 Int)
9
(declare-var T1_A_en.sT1_1 Real)
10
(declare-var T1_A_en.isInner Bool)
11
(declare-var T1_A_en.idEvents7_T1 Int)
12
(declare-var T1_A_en.sT1 Real)
13
(declare-var T1_A_en.sT1_2 Real)
14
(declare-rel T1_A_en (Int Real Bool Int Real))
15
(rule (=> 
16
  (and (and (or (not (= (not T1_A_en.isInner) true))
17
               (= T1_A_en.sT1_2 1.))
18
            (or (not (= (not T1_A_en.isInner) false))
19
               (= T1_A_en.sT1_2 T1_A_en.sT1_1))
20
       )
21
       (= T1_A_en.sT1 T1_A_en.sT1_2)
22
       (= T1_A_en.idEvents7_T1 676)
23
       )
24
  (T1_A_en T1_A_en.idEvents7_T1_1 T1_A_en.sT1_1 T1_A_en.isInner T1_A_en.idEvents7_T1 T1_A_en.sT1)
25
))
26

    
27
; T1_A_ex
28
(declare-var T1_A_ex.idEvents7_T1_1 Int)
29
(declare-var T1_A_ex.isInner Bool)
30
(declare-var T1_A_ex.idEvents7_T1 Int)
31
(declare-var T1_A_ex.idEvents7_T1_2 Int)
32
(declare-rel T1_A_ex (Int Bool Int))
33
(rule (=> 
34
  (and (and (or (not (= (not T1_A_ex.isInner) true))
35
               (= T1_A_ex.idEvents7_T1_2 0))
36
            (or (not (= (not T1_A_ex.isInner) false))
37
               (= T1_A_ex.idEvents7_T1_2 T1_A_ex.idEvents7_T1_1))
38
       )
39
       (= T1_A_ex.idEvents7_T1 T1_A_ex.idEvents7_T1_1)
40
       )
41
  (T1_A_ex T1_A_ex.idEvents7_T1_1 T1_A_ex.isInner T1_A_ex.idEvents7_T1)
42
))
43

    
44
; T1_B_en
45
(declare-var T1_B_en.idEvents7_T1_1 Int)
46
(declare-var T1_B_en.sT1_1 Real)
47
(declare-var T1_B_en.isInner Bool)
48
(declare-var T1_B_en.idEvents7_T1 Int)
49
(declare-var T1_B_en.sT1 Real)
50
(declare-var T1_B_en.sT1_2 Real)
51
(declare-rel T1_B_en (Int Real Bool Int Real))
52
(rule (=> 
53
  (and (and (or (not (= (not T1_B_en.isInner) true))
54
               (= T1_B_en.sT1_2 2.))
55
            (or (not (= (not T1_B_en.isInner) false))
56
               (= T1_B_en.sT1_2 T1_B_en.sT1_1))
57
       )
58
       (= T1_B_en.sT1 T1_B_en.sT1_2)
59
       (= T1_B_en.idEvents7_T1 677)
60
       )
61
  (T1_B_en T1_B_en.idEvents7_T1_1 T1_B_en.sT1_1 T1_B_en.isInner T1_B_en.idEvents7_T1 T1_B_en.sT1)
62
))
63

    
64
; T1_B_ex
65
(declare-var T1_B_ex.idEvents7_T1_1 Int)
66
(declare-var T1_B_ex.isInner Bool)
67
(declare-var T1_B_ex.idEvents7_T1 Int)
68
(declare-var T1_B_ex.idEvents7_T1_2 Int)
69
(declare-rel T1_B_ex (Int Bool Int))
70
(rule (=> 
71
  (and (and (or (not (= (not T1_B_ex.isInner) true))
72
               (= T1_B_ex.idEvents7_T1_2 0))
73
            (or (not (= (not T1_B_ex.isInner) false))
74
               (= T1_B_ex.idEvents7_T1_2 T1_B_ex.idEvents7_T1_1))
75
       )
76
       (= T1_B_ex.idEvents7_T1 T1_B_ex.idEvents7_T1_1)
77
       )
78
  (T1_B_ex T1_B_ex.idEvents7_T1_1 T1_B_ex.isInner T1_B_ex.idEvents7_T1)
79
))
80

    
81
; T2_C_en
82
(declare-var T2_C_en.idEvents7_T2_1 Int)
83
(declare-var T2_C_en.sT2_1 Real)
84
(declare-var T2_C_en.isInner Bool)
85
(declare-var T2_C_en.idEvents7_T2 Int)
86
(declare-var T2_C_en.sT2 Real)
87
(declare-var T2_C_en.sT2_2 Real)
88
(declare-rel T2_C_en (Int Real Bool Int Real))
89
(rule (=> 
90
  (and (and (or (not (= (not T2_C_en.isInner) true))
91
               (= T2_C_en.sT2_2 1.))
92
            (or (not (= (not T2_C_en.isInner) false))
93
               (= T2_C_en.sT2_2 T2_C_en.sT2_1))
94
       )
95
       (= T2_C_en.sT2 T2_C_en.sT2_2)
96
       (= T2_C_en.idEvents7_T2 679)
97
       )
98
  (T2_C_en T2_C_en.idEvents7_T2_1 T2_C_en.sT2_1 T2_C_en.isInner T2_C_en.idEvents7_T2 T2_C_en.sT2)
99
))
100

    
101
; T2_C_ex
102
(declare-var T2_C_ex.idEvents7_T2_1 Int)
103
(declare-var T2_C_ex.isInner Bool)
104
(declare-var T2_C_ex.idEvents7_T2 Int)
105
(declare-var T2_C_ex.idEvents7_T2_2 Int)
106
(declare-rel T2_C_ex (Int Bool Int))
107
(rule (=> 
108
  (and (and (or (not (= (not T2_C_ex.isInner) true))
109
               (= T2_C_ex.idEvents7_T2_2 0))
110
            (or (not (= (not T2_C_ex.isInner) false))
111
               (= T2_C_ex.idEvents7_T2_2 T2_C_ex.idEvents7_T2_1))
112
       )
113
       (= T2_C_ex.idEvents7_T2 T2_C_ex.idEvents7_T2_1)
114
       )
115
  (T2_C_ex T2_C_ex.idEvents7_T2_1 T2_C_ex.isInner T2_C_ex.idEvents7_T2)
116
))
117

    
118
; T2_D_en
119
(declare-var T2_D_en.idEvents7_T2_1 Int)
120
(declare-var T2_D_en.sT2_1 Real)
121
(declare-var T2_D_en.isInner Bool)
122
(declare-var T2_D_en.idEvents7_T2 Int)
123
(declare-var T2_D_en.sT2 Real)
124
(declare-var T2_D_en.sT2_2 Real)
125
(declare-rel T2_D_en (Int Real Bool Int Real))
126
(rule (=> 
127
  (and (and (or (not (= (not T2_D_en.isInner) true))
128
               (= T2_D_en.sT2_2 2.))
129
            (or (not (= (not T2_D_en.isInner) false))
130
               (= T2_D_en.sT2_2 T2_D_en.sT2_1))
131
       )
132
       (= T2_D_en.sT2 T2_D_en.sT2_2)
133
       (= T2_D_en.idEvents7_T2 680)
134
       )
135
  (T2_D_en T2_D_en.idEvents7_T2_1 T2_D_en.sT2_1 T2_D_en.isInner T2_D_en.idEvents7_T2 T2_D_en.sT2)
136
))
137

    
138
; T2_D_ex
139
(declare-var T2_D_ex.idEvents7_T2_1 Int)
140
(declare-var T2_D_ex.isInner Bool)
141
(declare-var T2_D_ex.idEvents7_T2 Int)
142
(declare-var T2_D_ex.idEvents7_T2_2 Int)
143
(declare-rel T2_D_ex (Int Bool Int))
144
(rule (=> 
145
  (and (and (or (not (= (not T2_D_ex.isInner) true))
146
               (= T2_D_ex.idEvents7_T2_2 0))
147
            (or (not (= (not T2_D_ex.isInner) false))
148
               (= T2_D_ex.idEvents7_T2_2 T2_D_ex.idEvents7_T2_1))
149
       )
150
       (= T2_D_ex.idEvents7_T2 T2_D_ex.idEvents7_T2_1)
151
       )
152
  (T2_D_ex T2_D_ex.idEvents7_T2_1 T2_D_ex.isInner T2_D_ex.idEvents7_T2)
153
))
154

    
155
; events7_t1__POINTEvents7_T1_handler_until
156
(declare-var events7_t1__POINTEvents7_T1_handler_until.idEvents7_T1_1 Int)
157
(declare-var events7_t1__POINTEvents7_T1_handler_until.sT1_1 Real)
158
(declare-var events7_t1__POINTEvents7_T1_handler_until.events7_t1__restart_in Bool)
159
(declare-var events7_t1__POINTEvents7_T1_handler_until.events7_t1__state_in events7_t1__type)
160
(declare-var events7_t1__POINTEvents7_T1_handler_until.idEvents7_T1_out Int)
161
(declare-var events7_t1__POINTEvents7_T1_handler_until.sT1_out Real)
162
(declare-rel events7_t1__POINTEvents7_T1_handler_until (Int Real Bool events7_t1__type Int Real))
163
(rule (=> 
164
  (and (= events7_t1__POINTEvents7_T1_handler_until.sT1_out events7_t1__POINTEvents7_T1_handler_until.sT1_1)
165
       (= events7_t1__POINTEvents7_T1_handler_until.idEvents7_T1_out events7_t1__POINTEvents7_T1_handler_until.idEvents7_T1_1)
166
       (= events7_t1__POINTEvents7_T1_handler_until.events7_t1__state_in POINTEvents7_T1)
167
       (= events7_t1__POINTEvents7_T1_handler_until.events7_t1__restart_in false)
168
       )
169
  (events7_t1__POINTEvents7_T1_handler_until events7_t1__POINTEvents7_T1_handler_until.idEvents7_T1_1 events7_t1__POINTEvents7_T1_handler_until.sT1_1 events7_t1__POINTEvents7_T1_handler_until.events7_t1__restart_in events7_t1__POINTEvents7_T1_handler_until.events7_t1__state_in events7_t1__POINTEvents7_T1_handler_until.idEvents7_T1_out events7_t1__POINTEvents7_T1_handler_until.sT1_out)
170
))
171

    
172
; events7_t1__POINTEvents7_T1_unless
173
(declare-var events7_t1__POINTEvents7_T1_unless.events7_t1__restart_in Bool)
174
(declare-var events7_t1__POINTEvents7_T1_unless.events7_t1__state_in events7_t1__type)
175
(declare-var events7_t1__POINTEvents7_T1_unless.idEvents7_T1_1 Int)
176
(declare-var events7_t1__POINTEvents7_T1_unless.E Bool)
177
(declare-var events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act Bool)
178
(declare-var events7_t1__POINTEvents7_T1_unless.events7_t1__state_act events7_t1__type)
179
(declare-var events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_1 Bool)
180
(declare-var events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_2 Bool)
181
(declare-var events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_3 Bool)
182
(declare-var events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_4 Bool)
183
(declare-var events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_5 Bool)
184
(declare-rel events7_t1__POINTEvents7_T1_unless (Bool events7_t1__type Int Bool Bool events7_t1__type))
185
(rule (=> 
186
  (and (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_5 (= events7_t1__POINTEvents7_T1_unless.idEvents7_T1_1 677))
187
       (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_4 (= events7_t1__POINTEvents7_T1_unless.idEvents7_T1_1 676))
188
       (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_3 (and (= events7_t1__POINTEvents7_T1_unless.idEvents7_T1_1 677) events7_t1__POINTEvents7_T1_unless.E))
189
       (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_2 (and (= events7_t1__POINTEvents7_T1_unless.idEvents7_T1_1 676) events7_t1__POINTEvents7_T1_unless.E))
190
       (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_1 (= events7_t1__POINTEvents7_T1_unless.idEvents7_T1_1 0))
191
       (and (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_1 false))
192
               (and (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_2 false))
193
                       (and (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_3 false))
194
                               (and (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_4 false))
195
                                       (and (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_5 false))
196
                                               (and (= events7_t1__POINTEvents7_T1_unless.events7_t1__state_act events7_t1__POINTEvents7_T1_unless.events7_t1__state_in)
197
                                                    (= events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act events7_t1__POINTEvents7_T1_unless.events7_t1__restart_in)
198
                                                    ))
199
                                            (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_5 true))
200
                                               (and (= events7_t1__POINTEvents7_T1_unless.events7_t1__state_act T1_B_IDL)
201
                                                    (= events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act true)
202
                                                    ))
203
                                       ))
204
                                    (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_4 true))
205
                                       (and (= events7_t1__POINTEvents7_T1_unless.events7_t1__state_act T1_A_IDL)
206
                                            (= events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act true)
207
                                            ))
208
                               ))
209
                            (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_3 true))
210
                               (and (= events7_t1__POINTEvents7_T1_unless.events7_t1__state_act T1_B__TO__T1_A_1)
211
                                    (= events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act true)
212
                                    ))
213
                       ))
214
                    (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_2 true))
215
                       (and (= events7_t1__POINTEvents7_T1_unless.events7_t1__state_act T1_A__TO__T1_B_1)
216
                            (= events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act true)
217
                            ))
218
               ))
219
            (or (not (= events7_t1__POINTEvents7_T1_unless.__events7_t1__POINTEvents7_T1_unless_1 true))
220
               (and (= events7_t1__POINTEvents7_T1_unless.events7_t1__state_act POINT__TO__T1_A_1)
221
                    (= events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act true)
222
                    ))
223
       )
224
       )
225
  (events7_t1__POINTEvents7_T1_unless events7_t1__POINTEvents7_T1_unless.events7_t1__restart_in events7_t1__POINTEvents7_T1_unless.events7_t1__state_in events7_t1__POINTEvents7_T1_unless.idEvents7_T1_1 events7_t1__POINTEvents7_T1_unless.E events7_t1__POINTEvents7_T1_unless.events7_t1__restart_act events7_t1__POINTEvents7_T1_unless.events7_t1__state_act)
226
))
227

    
228
; events7_t1__POINT__TO__T1_A_1_handler_until
229
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_1 Int)
230
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.sT1_1 Real)
231
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.events7_t1__restart_in Bool)
232
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.events7_t1__state_in events7_t1__type)
233
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_out Int)
234
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.sT1_out Real)
235
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_2 Int)
236
(declare-var events7_t1__POINT__TO__T1_A_1_handler_until.sT1_2 Real)
237
(declare-rel events7_t1__POINT__TO__T1_A_1_handler_until (Int Real Bool events7_t1__type Int Real))
238
(rule (=> 
239
  (and (T1_A_en events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_1
240
                events7_t1__POINT__TO__T1_A_1_handler_until.sT1_1
241
                false
242
                events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_2
243
                events7_t1__POINT__TO__T1_A_1_handler_until.sT1_2)
244
       (= events7_t1__POINT__TO__T1_A_1_handler_until.sT1_out events7_t1__POINT__TO__T1_A_1_handler_until.sT1_2)
245
       (= events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_out events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_2)
246
       (= events7_t1__POINT__TO__T1_A_1_handler_until.events7_t1__state_in POINTEvents7_T1)
247
       (= events7_t1__POINT__TO__T1_A_1_handler_until.events7_t1__restart_in true)
248
       )
249
  (events7_t1__POINT__TO__T1_A_1_handler_until events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_1 events7_t1__POINT__TO__T1_A_1_handler_until.sT1_1 events7_t1__POINT__TO__T1_A_1_handler_until.events7_t1__restart_in events7_t1__POINT__TO__T1_A_1_handler_until.events7_t1__state_in events7_t1__POINT__TO__T1_A_1_handler_until.idEvents7_T1_out events7_t1__POINT__TO__T1_A_1_handler_until.sT1_out)
250
))
251

    
252
; events7_t1__POINT__TO__T1_A_1_unless
253
(declare-var events7_t1__POINT__TO__T1_A_1_unless.events7_t1__restart_in Bool)
254
(declare-var events7_t1__POINT__TO__T1_A_1_unless.events7_t1__state_in events7_t1__type)
255
(declare-var events7_t1__POINT__TO__T1_A_1_unless.events7_t1__restart_act Bool)
256
(declare-var events7_t1__POINT__TO__T1_A_1_unless.events7_t1__state_act events7_t1__type)
257
(declare-rel events7_t1__POINT__TO__T1_A_1_unless (Bool events7_t1__type Bool events7_t1__type))
258
(rule (=> 
259
  (and (= events7_t1__POINT__TO__T1_A_1_unless.events7_t1__state_act events7_t1__POINT__TO__T1_A_1_unless.events7_t1__state_in)
260
       (= events7_t1__POINT__TO__T1_A_1_unless.events7_t1__restart_act events7_t1__POINT__TO__T1_A_1_unless.events7_t1__restart_in)
261
       )
262
  (events7_t1__POINT__TO__T1_A_1_unless events7_t1__POINT__TO__T1_A_1_unless.events7_t1__restart_in events7_t1__POINT__TO__T1_A_1_unless.events7_t1__state_in events7_t1__POINT__TO__T1_A_1_unless.events7_t1__restart_act events7_t1__POINT__TO__T1_A_1_unless.events7_t1__state_act)
263
))
264

    
265
; events7_t1__T1_A_IDL_handler_until
266
(declare-var events7_t1__T1_A_IDL_handler_until.idEvents7_T1_1 Int)
267
(declare-var events7_t1__T1_A_IDL_handler_until.sT1_1 Real)
268
(declare-var events7_t1__T1_A_IDL_handler_until.events7_t1__restart_in Bool)
269
(declare-var events7_t1__T1_A_IDL_handler_until.events7_t1__state_in events7_t1__type)
270
(declare-var events7_t1__T1_A_IDL_handler_until.idEvents7_T1_out Int)
271
(declare-var events7_t1__T1_A_IDL_handler_until.sT1_out Real)
272
(declare-rel events7_t1__T1_A_IDL_handler_until (Int Real Bool events7_t1__type Int Real))
273
(rule (=> 
274
  (and (= events7_t1__T1_A_IDL_handler_until.sT1_out events7_t1__T1_A_IDL_handler_until.sT1_1)
275
       (= events7_t1__T1_A_IDL_handler_until.idEvents7_T1_out events7_t1__T1_A_IDL_handler_until.idEvents7_T1_1)
276
       (= events7_t1__T1_A_IDL_handler_until.events7_t1__state_in POINTEvents7_T1)
277
       (= events7_t1__T1_A_IDL_handler_until.events7_t1__restart_in true)
278
       )
279
  (events7_t1__T1_A_IDL_handler_until events7_t1__T1_A_IDL_handler_until.idEvents7_T1_1 events7_t1__T1_A_IDL_handler_until.sT1_1 events7_t1__T1_A_IDL_handler_until.events7_t1__restart_in events7_t1__T1_A_IDL_handler_until.events7_t1__state_in events7_t1__T1_A_IDL_handler_until.idEvents7_T1_out events7_t1__T1_A_IDL_handler_until.sT1_out)
280
))
281

    
282
; events7_t1__T1_A_IDL_unless
283
(declare-var events7_t1__T1_A_IDL_unless.events7_t1__restart_in Bool)
284
(declare-var events7_t1__T1_A_IDL_unless.events7_t1__state_in events7_t1__type)
285
(declare-var events7_t1__T1_A_IDL_unless.events7_t1__restart_act Bool)
286
(declare-var events7_t1__T1_A_IDL_unless.events7_t1__state_act events7_t1__type)
287
(declare-rel events7_t1__T1_A_IDL_unless (Bool events7_t1__type Bool events7_t1__type))
288
(rule (=> 
289
  (and (= events7_t1__T1_A_IDL_unless.events7_t1__state_act events7_t1__T1_A_IDL_unless.events7_t1__state_in)
290
       (= events7_t1__T1_A_IDL_unless.events7_t1__restart_act events7_t1__T1_A_IDL_unless.events7_t1__restart_in)
291
       )
292
  (events7_t1__T1_A_IDL_unless events7_t1__T1_A_IDL_unless.events7_t1__restart_in events7_t1__T1_A_IDL_unless.events7_t1__state_in events7_t1__T1_A_IDL_unless.events7_t1__restart_act events7_t1__T1_A_IDL_unless.events7_t1__state_act)
293
))
294

    
295
; events7_t1__T1_A__TO__T1_B_1_handler_until
296
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_1 Int)
297
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_1 Real)
298
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.events7_t1__restart_in Bool)
299
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.events7_t1__state_in events7_t1__type)
300
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_out Int)
301
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_out Real)
302
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_2 Int)
303
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_3 Int)
304
(declare-var events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_2 Real)
305
(declare-rel events7_t1__T1_A__TO__T1_B_1_handler_until (Int Real Bool events7_t1__type Int Real))
306
(rule (=> 
307
  (and (T1_A_ex events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_1
308
                false
309
                events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_2)
310
       (T1_B_en events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_2
311
                events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_1
312
                false
313
                events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_3
314
                events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_2)
315
       (= events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_out events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_2)
316
       (= events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_out events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_3)
317
       (= events7_t1__T1_A__TO__T1_B_1_handler_until.events7_t1__state_in POINTEvents7_T1)
318
       (= events7_t1__T1_A__TO__T1_B_1_handler_until.events7_t1__restart_in true)
319
       )
320
  (events7_t1__T1_A__TO__T1_B_1_handler_until events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_1 events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_1 events7_t1__T1_A__TO__T1_B_1_handler_until.events7_t1__restart_in events7_t1__T1_A__TO__T1_B_1_handler_until.events7_t1__state_in events7_t1__T1_A__TO__T1_B_1_handler_until.idEvents7_T1_out events7_t1__T1_A__TO__T1_B_1_handler_until.sT1_out)
321
))
322

    
323
; events7_t1__T1_A__TO__T1_B_1_unless
324
(declare-var events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__restart_in Bool)
325
(declare-var events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__state_in events7_t1__type)
326
(declare-var events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__restart_act Bool)
327
(declare-var events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__state_act events7_t1__type)
328
(declare-rel events7_t1__T1_A__TO__T1_B_1_unless (Bool events7_t1__type Bool events7_t1__type))
329
(rule (=> 
330
  (and (= events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__state_act events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__state_in)
331
       (= events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__restart_act events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__restart_in)
332
       )
333
  (events7_t1__T1_A__TO__T1_B_1_unless events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__restart_in events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__state_in events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__restart_act events7_t1__T1_A__TO__T1_B_1_unless.events7_t1__state_act)
334
))
335

    
336
; events7_t1__T1_B_IDL_handler_until
337
(declare-var events7_t1__T1_B_IDL_handler_until.idEvents7_T1_1 Int)
338
(declare-var events7_t1__T1_B_IDL_handler_until.sT1_1 Real)
339
(declare-var events7_t1__T1_B_IDL_handler_until.events7_t1__restart_in Bool)
340
(declare-var events7_t1__T1_B_IDL_handler_until.events7_t1__state_in events7_t1__type)
341
(declare-var events7_t1__T1_B_IDL_handler_until.idEvents7_T1_out Int)
342
(declare-var events7_t1__T1_B_IDL_handler_until.sT1_out Real)
343
(declare-rel events7_t1__T1_B_IDL_handler_until (Int Real Bool events7_t1__type Int Real))
344
(rule (=> 
345
  (and (= events7_t1__T1_B_IDL_handler_until.sT1_out events7_t1__T1_B_IDL_handler_until.sT1_1)
346
       (= events7_t1__T1_B_IDL_handler_until.idEvents7_T1_out events7_t1__T1_B_IDL_handler_until.idEvents7_T1_1)
347
       (= events7_t1__T1_B_IDL_handler_until.events7_t1__state_in POINTEvents7_T1)
348
       (= events7_t1__T1_B_IDL_handler_until.events7_t1__restart_in true)
349
       )
350
  (events7_t1__T1_B_IDL_handler_until events7_t1__T1_B_IDL_handler_until.idEvents7_T1_1 events7_t1__T1_B_IDL_handler_until.sT1_1 events7_t1__T1_B_IDL_handler_until.events7_t1__restart_in events7_t1__T1_B_IDL_handler_until.events7_t1__state_in events7_t1__T1_B_IDL_handler_until.idEvents7_T1_out events7_t1__T1_B_IDL_handler_until.sT1_out)
351
))
352

    
353
; events7_t1__T1_B_IDL_unless
354
(declare-var events7_t1__T1_B_IDL_unless.events7_t1__restart_in Bool)
355
(declare-var events7_t1__T1_B_IDL_unless.events7_t1__state_in events7_t1__type)
356
(declare-var events7_t1__T1_B_IDL_unless.events7_t1__restart_act Bool)
357
(declare-var events7_t1__T1_B_IDL_unless.events7_t1__state_act events7_t1__type)
358
(declare-rel events7_t1__T1_B_IDL_unless (Bool events7_t1__type Bool events7_t1__type))
359
(rule (=> 
360
  (and (= events7_t1__T1_B_IDL_unless.events7_t1__state_act events7_t1__T1_B_IDL_unless.events7_t1__state_in)
361
       (= events7_t1__T1_B_IDL_unless.events7_t1__restart_act events7_t1__T1_B_IDL_unless.events7_t1__restart_in)
362
       )
363
  (events7_t1__T1_B_IDL_unless events7_t1__T1_B_IDL_unless.events7_t1__restart_in events7_t1__T1_B_IDL_unless.events7_t1__state_in events7_t1__T1_B_IDL_unless.events7_t1__restart_act events7_t1__T1_B_IDL_unless.events7_t1__state_act)
364
))
365

    
366
; events7_t1__T1_B__TO__T1_A_1_handler_until
367
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_1 Int)
368
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_1 Real)
369
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.events7_t1__restart_in Bool)
370
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.events7_t1__state_in events7_t1__type)
371
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_out Int)
372
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_out Real)
373
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_2 Int)
374
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_3 Int)
375
(declare-var events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_2 Real)
376
(declare-rel events7_t1__T1_B__TO__T1_A_1_handler_until (Int Real Bool events7_t1__type Int Real))
377
(rule (=> 
378
  (and (T1_B_ex events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_1
379
                false
380
                events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_2)
381
       (T1_A_en events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_2
382
                events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_1
383
                false
384
                events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_3
385
                events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_2)
386
       (= events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_out events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_2)
387
       (= events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_out events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_3)
388
       (= events7_t1__T1_B__TO__T1_A_1_handler_until.events7_t1__state_in POINTEvents7_T1)
389
       (= events7_t1__T1_B__TO__T1_A_1_handler_until.events7_t1__restart_in true)
390
       )
391
  (events7_t1__T1_B__TO__T1_A_1_handler_until events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_1 events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_1 events7_t1__T1_B__TO__T1_A_1_handler_until.events7_t1__restart_in events7_t1__T1_B__TO__T1_A_1_handler_until.events7_t1__state_in events7_t1__T1_B__TO__T1_A_1_handler_until.idEvents7_T1_out events7_t1__T1_B__TO__T1_A_1_handler_until.sT1_out)
392
))
393

    
394
; events7_t1__T1_B__TO__T1_A_1_unless
395
(declare-var events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__restart_in Bool)
396
(declare-var events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__state_in events7_t1__type)
397
(declare-var events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__restart_act Bool)
398
(declare-var events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__state_act events7_t1__type)
399
(declare-rel events7_t1__T1_B__TO__T1_A_1_unless (Bool events7_t1__type Bool events7_t1__type))
400
(rule (=> 
401
  (and (= events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__state_act events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__state_in)
402
       (= events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__restart_act events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__restart_in)
403
       )
404
  (events7_t1__T1_B__TO__T1_A_1_unless events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__restart_in events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__state_in events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__restart_act events7_t1__T1_B__TO__T1_A_1_unless.events7_t1__state_act)
405
))
406

    
407
; events7_t2__POINTEvents7_T2_handler_until
408
(declare-var events7_t2__POINTEvents7_T2_handler_until.idEvents7_T2_1 Int)
409
(declare-var events7_t2__POINTEvents7_T2_handler_until.sT2_1 Real)
410
(declare-var events7_t2__POINTEvents7_T2_handler_until.events7_t2__restart_in Bool)
411
(declare-var events7_t2__POINTEvents7_T2_handler_until.events7_t2__state_in events7_t2__type)
412
(declare-var events7_t2__POINTEvents7_T2_handler_until.idEvents7_T2_out Int)
413
(declare-var events7_t2__POINTEvents7_T2_handler_until.sT2_out Real)
414
(declare-rel events7_t2__POINTEvents7_T2_handler_until (Int Real Bool events7_t2__type Int Real))
415
(rule (=> 
416
  (and (= events7_t2__POINTEvents7_T2_handler_until.sT2_out events7_t2__POINTEvents7_T2_handler_until.sT2_1)
417
       (= events7_t2__POINTEvents7_T2_handler_until.idEvents7_T2_out events7_t2__POINTEvents7_T2_handler_until.idEvents7_T2_1)
418
       (= events7_t2__POINTEvents7_T2_handler_until.events7_t2__state_in POINTEvents7_T2)
419
       (= events7_t2__POINTEvents7_T2_handler_until.events7_t2__restart_in false)
420
       )
421
  (events7_t2__POINTEvents7_T2_handler_until events7_t2__POINTEvents7_T2_handler_until.idEvents7_T2_1 events7_t2__POINTEvents7_T2_handler_until.sT2_1 events7_t2__POINTEvents7_T2_handler_until.events7_t2__restart_in events7_t2__POINTEvents7_T2_handler_until.events7_t2__state_in events7_t2__POINTEvents7_T2_handler_until.idEvents7_T2_out events7_t2__POINTEvents7_T2_handler_until.sT2_out)
422
))
423

    
424
; events7_t2__POINTEvents7_T2_unless
425
(declare-var events7_t2__POINTEvents7_T2_unless.events7_t2__restart_in Bool)
426
(declare-var events7_t2__POINTEvents7_T2_unless.events7_t2__state_in events7_t2__type)
427
(declare-var events7_t2__POINTEvents7_T2_unless.idEvents7_T2_1 Int)
428
(declare-var events7_t2__POINTEvents7_T2_unless.idEvents7_T1_1 Int)
429
(declare-var events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act Bool)
430
(declare-var events7_t2__POINTEvents7_T2_unless.events7_t2__state_act events7_t2__type)
431
(declare-var events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_1 Bool)
432
(declare-var events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_2 Bool)
433
(declare-var events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_3 Bool)
434
(declare-var events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_4 Bool)
435
(declare-var events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_5 Bool)
436
(declare-rel events7_t2__POINTEvents7_T2_unless (Bool events7_t2__type Int Int Bool events7_t2__type))
437
(rule (=> 
438
  (and (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_5 (= events7_t2__POINTEvents7_T2_unless.idEvents7_T2_1 680))
439
       (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_4 (= events7_t2__POINTEvents7_T2_unless.idEvents7_T2_1 679))
440
       (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_3 (and (= events7_t2__POINTEvents7_T2_unless.idEvents7_T2_1 680) (= events7_t2__POINTEvents7_T2_unless.idEvents7_T1_1 676)))
441
       (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_2 (and (= events7_t2__POINTEvents7_T2_unless.idEvents7_T2_1 679) (= events7_t2__POINTEvents7_T2_unless.idEvents7_T1_1 677)))
442
       (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_1 (= events7_t2__POINTEvents7_T2_unless.idEvents7_T2_1 0))
443
       (and (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_1 false))
444
               (and (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_2 false))
445
                       (and (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_3 false))
446
                               (and (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_4 false))
447
                                       (and (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_5 false))
448
                                               (and (= events7_t2__POINTEvents7_T2_unless.events7_t2__state_act events7_t2__POINTEvents7_T2_unless.events7_t2__state_in)
449
                                                    (= events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act events7_t2__POINTEvents7_T2_unless.events7_t2__restart_in)
450
                                                    ))
451
                                            (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_5 true))
452
                                               (and (= events7_t2__POINTEvents7_T2_unless.events7_t2__state_act T2_D_IDL)
453
                                                    (= events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act true)
454
                                                    ))
455
                                       ))
456
                                    (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_4 true))
457
                                       (and (= events7_t2__POINTEvents7_T2_unless.events7_t2__state_act T2_C_IDL)
458
                                            (= events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act true)
459
                                            ))
460
                               ))
461
                            (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_3 true))
462
                               (and (= events7_t2__POINTEvents7_T2_unless.events7_t2__state_act T2_D__TO__T2_C_1)
463
                                    (= events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act true)
464
                                    ))
465
                       ))
466
                    (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_2 true))
467
                       (and (= events7_t2__POINTEvents7_T2_unless.events7_t2__state_act T2_C__TO__T2_D_1)
468
                            (= events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act true)
469
                            ))
470
               ))
471
            (or (not (= events7_t2__POINTEvents7_T2_unless.__events7_t2__POINTEvents7_T2_unless_1 true))
472
               (and (= events7_t2__POINTEvents7_T2_unless.events7_t2__state_act POINT__TO__T2_C_1)
473
                    (= events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act true)
474
                    ))
475
       )
476
       )
477
  (events7_t2__POINTEvents7_T2_unless events7_t2__POINTEvents7_T2_unless.events7_t2__restart_in events7_t2__POINTEvents7_T2_unless.events7_t2__state_in events7_t2__POINTEvents7_T2_unless.idEvents7_T2_1 events7_t2__POINTEvents7_T2_unless.idEvents7_T1_1 events7_t2__POINTEvents7_T2_unless.events7_t2__restart_act events7_t2__POINTEvents7_T2_unless.events7_t2__state_act)
478
))
479

    
480
; events7_t2__POINT__TO__T2_C_1_handler_until
481
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_1 Int)
482
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.sT2_1 Real)
483
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.events7_t2__restart_in Bool)
484
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.events7_t2__state_in events7_t2__type)
485
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_out Int)
486
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.sT2_out Real)
487
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_2 Int)
488
(declare-var events7_t2__POINT__TO__T2_C_1_handler_until.sT2_2 Real)
489
(declare-rel events7_t2__POINT__TO__T2_C_1_handler_until (Int Real Bool events7_t2__type Int Real))
490
(rule (=> 
491
  (and (T2_C_en events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_1
492
                events7_t2__POINT__TO__T2_C_1_handler_until.sT2_1
493
                false
494
                events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_2
495
                events7_t2__POINT__TO__T2_C_1_handler_until.sT2_2)
496
       (= events7_t2__POINT__TO__T2_C_1_handler_until.sT2_out events7_t2__POINT__TO__T2_C_1_handler_until.sT2_2)
497
       (= events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_out events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_2)
498
       (= events7_t2__POINT__TO__T2_C_1_handler_until.events7_t2__state_in POINTEvents7_T2)
499
       (= events7_t2__POINT__TO__T2_C_1_handler_until.events7_t2__restart_in true)
500
       )
501
  (events7_t2__POINT__TO__T2_C_1_handler_until events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_1 events7_t2__POINT__TO__T2_C_1_handler_until.sT2_1 events7_t2__POINT__TO__T2_C_1_handler_until.events7_t2__restart_in events7_t2__POINT__TO__T2_C_1_handler_until.events7_t2__state_in events7_t2__POINT__TO__T2_C_1_handler_until.idEvents7_T2_out events7_t2__POINT__TO__T2_C_1_handler_until.sT2_out)
502
))
503

    
504
; events7_t2__POINT__TO__T2_C_1_unless
505
(declare-var events7_t2__POINT__TO__T2_C_1_unless.events7_t2__restart_in Bool)
506
(declare-var events7_t2__POINT__TO__T2_C_1_unless.events7_t2__state_in events7_t2__type)
507
(declare-var events7_t2__POINT__TO__T2_C_1_unless.events7_t2__restart_act Bool)
508
(declare-var events7_t2__POINT__TO__T2_C_1_unless.events7_t2__state_act events7_t2__type)
509
(declare-rel events7_t2__POINT__TO__T2_C_1_unless (Bool events7_t2__type Bool events7_t2__type))
510
(rule (=> 
511
  (and (= events7_t2__POINT__TO__T2_C_1_unless.events7_t2__state_act events7_t2__POINT__TO__T2_C_1_unless.events7_t2__state_in)
512
       (= events7_t2__POINT__TO__T2_C_1_unless.events7_t2__restart_act events7_t2__POINT__TO__T2_C_1_unless.events7_t2__restart_in)
513
       )
514
  (events7_t2__POINT__TO__T2_C_1_unless events7_t2__POINT__TO__T2_C_1_unless.events7_t2__restart_in events7_t2__POINT__TO__T2_C_1_unless.events7_t2__state_in events7_t2__POINT__TO__T2_C_1_unless.events7_t2__restart_act events7_t2__POINT__TO__T2_C_1_unless.events7_t2__state_act)
515
))
516

    
517
; events7_t2__T2_C_IDL_handler_until
518
(declare-var events7_t2__T2_C_IDL_handler_until.idEvents7_T2_1 Int)
519
(declare-var events7_t2__T2_C_IDL_handler_until.sT2_1 Real)
520
(declare-var events7_t2__T2_C_IDL_handler_until.events7_t2__restart_in Bool)
521
(declare-var events7_t2__T2_C_IDL_handler_until.events7_t2__state_in events7_t2__type)
522
(declare-var events7_t2__T2_C_IDL_handler_until.idEvents7_T2_out Int)
523
(declare-var events7_t2__T2_C_IDL_handler_until.sT2_out Real)
524
(declare-rel events7_t2__T2_C_IDL_handler_until (Int Real Bool events7_t2__type Int Real))
525
(rule (=> 
526
  (and (= events7_t2__T2_C_IDL_handler_until.sT2_out events7_t2__T2_C_IDL_handler_until.sT2_1)
527
       (= events7_t2__T2_C_IDL_handler_until.idEvents7_T2_out events7_t2__T2_C_IDL_handler_until.idEvents7_T2_1)
528
       (= events7_t2__T2_C_IDL_handler_until.events7_t2__state_in POINTEvents7_T2)
529
       (= events7_t2__T2_C_IDL_handler_until.events7_t2__restart_in true)
530
       )
531
  (events7_t2__T2_C_IDL_handler_until events7_t2__T2_C_IDL_handler_until.idEvents7_T2_1 events7_t2__T2_C_IDL_handler_until.sT2_1 events7_t2__T2_C_IDL_handler_until.events7_t2__restart_in events7_t2__T2_C_IDL_handler_until.events7_t2__state_in events7_t2__T2_C_IDL_handler_until.idEvents7_T2_out events7_t2__T2_C_IDL_handler_until.sT2_out)
532
))
533

    
534
; events7_t2__T2_C_IDL_unless
535
(declare-var events7_t2__T2_C_IDL_unless.events7_t2__restart_in Bool)
536
(declare-var events7_t2__T2_C_IDL_unless.events7_t2__state_in events7_t2__type)
537
(declare-var events7_t2__T2_C_IDL_unless.events7_t2__restart_act Bool)
538
(declare-var events7_t2__T2_C_IDL_unless.events7_t2__state_act events7_t2__type)
539
(declare-rel events7_t2__T2_C_IDL_unless (Bool events7_t2__type Bool events7_t2__type))
540
(rule (=> 
541
  (and (= events7_t2__T2_C_IDL_unless.events7_t2__state_act events7_t2__T2_C_IDL_unless.events7_t2__state_in)
542
       (= events7_t2__T2_C_IDL_unless.events7_t2__restart_act events7_t2__T2_C_IDL_unless.events7_t2__restart_in)
543
       )
544
  (events7_t2__T2_C_IDL_unless events7_t2__T2_C_IDL_unless.events7_t2__restart_in events7_t2__T2_C_IDL_unless.events7_t2__state_in events7_t2__T2_C_IDL_unless.events7_t2__restart_act events7_t2__T2_C_IDL_unless.events7_t2__state_act)
545
))
546

    
547
; events7_t2__T2_C__TO__T2_D_1_handler_until
548
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_1 Int)
549
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_1 Real)
550
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.events7_t2__restart_in Bool)
551
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.events7_t2__state_in events7_t2__type)
552
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_out Int)
553
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_out Real)
554
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_2 Int)
555
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_3 Int)
556
(declare-var events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_2 Real)
557
(declare-rel events7_t2__T2_C__TO__T2_D_1_handler_until (Int Real Bool events7_t2__type Int Real))
558
(rule (=> 
559
  (and (T2_C_ex events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_1
560
                false
561
                events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_2)
562
       (T2_D_en events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_2
563
                events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_1
564
                false
565
                events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_3
566
                events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_2)
567
       (= events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_out events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_2)
568
       (= events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_out events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_3)
569
       (= events7_t2__T2_C__TO__T2_D_1_handler_until.events7_t2__state_in POINTEvents7_T2)
570
       (= events7_t2__T2_C__TO__T2_D_1_handler_until.events7_t2__restart_in true)
571
       )
572
  (events7_t2__T2_C__TO__T2_D_1_handler_until events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_1 events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_1 events7_t2__T2_C__TO__T2_D_1_handler_until.events7_t2__restart_in events7_t2__T2_C__TO__T2_D_1_handler_until.events7_t2__state_in events7_t2__T2_C__TO__T2_D_1_handler_until.idEvents7_T2_out events7_t2__T2_C__TO__T2_D_1_handler_until.sT2_out)
573
))
574

    
575
; events7_t2__T2_C__TO__T2_D_1_unless
576
(declare-var events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__restart_in Bool)
577
(declare-var events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__state_in events7_t2__type)
578
(declare-var events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__restart_act Bool)
579
(declare-var events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__state_act events7_t2__type)
580
(declare-rel events7_t2__T2_C__TO__T2_D_1_unless (Bool events7_t2__type Bool events7_t2__type))
581
(rule (=> 
582
  (and (= events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__state_act events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__state_in)
583
       (= events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__restart_act events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__restart_in)
584
       )
585
  (events7_t2__T2_C__TO__T2_D_1_unless events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__restart_in events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__state_in events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__restart_act events7_t2__T2_C__TO__T2_D_1_unless.events7_t2__state_act)
586
))
587

    
588
; events7_t2__T2_D_IDL_handler_until
589
(declare-var events7_t2__T2_D_IDL_handler_until.idEvents7_T2_1 Int)
590
(declare-var events7_t2__T2_D_IDL_handler_until.sT2_1 Real)
591
(declare-var events7_t2__T2_D_IDL_handler_until.events7_t2__restart_in Bool)
592
(declare-var events7_t2__T2_D_IDL_handler_until.events7_t2__state_in events7_t2__type)
593
(declare-var events7_t2__T2_D_IDL_handler_until.idEvents7_T2_out Int)
594
(declare-var events7_t2__T2_D_IDL_handler_until.sT2_out Real)
595
(declare-rel events7_t2__T2_D_IDL_handler_until (Int Real Bool events7_t2__type Int Real))
596
(rule (=> 
597
  (and (= events7_t2__T2_D_IDL_handler_until.sT2_out events7_t2__T2_D_IDL_handler_until.sT2_1)
598
       (= events7_t2__T2_D_IDL_handler_until.idEvents7_T2_out events7_t2__T2_D_IDL_handler_until.idEvents7_T2_1)
599
       (= events7_t2__T2_D_IDL_handler_until.events7_t2__state_in POINTEvents7_T2)
600
       (= events7_t2__T2_D_IDL_handler_until.events7_t2__restart_in true)
601
       )
602
  (events7_t2__T2_D_IDL_handler_until events7_t2__T2_D_IDL_handler_until.idEvents7_T2_1 events7_t2__T2_D_IDL_handler_until.sT2_1 events7_t2__T2_D_IDL_handler_until.events7_t2__restart_in events7_t2__T2_D_IDL_handler_until.events7_t2__state_in events7_t2__T2_D_IDL_handler_until.idEvents7_T2_out events7_t2__T2_D_IDL_handler_until.sT2_out)
603
))
604

    
605
; events7_t2__T2_D_IDL_unless
606
(declare-var events7_t2__T2_D_IDL_unless.events7_t2__restart_in Bool)
607
(declare-var events7_t2__T2_D_IDL_unless.events7_t2__state_in events7_t2__type)
608
(declare-var events7_t2__T2_D_IDL_unless.events7_t2__restart_act Bool)
609
(declare-var events7_t2__T2_D_IDL_unless.events7_t2__state_act events7_t2__type)
610
(declare-rel events7_t2__T2_D_IDL_unless (Bool events7_t2__type Bool events7_t2__type))
611
(rule (=> 
612
  (and (= events7_t2__T2_D_IDL_unless.events7_t2__state_act events7_t2__T2_D_IDL_unless.events7_t2__state_in)
613
       (= events7_t2__T2_D_IDL_unless.events7_t2__restart_act events7_t2__T2_D_IDL_unless.events7_t2__restart_in)
614
       )
615
  (events7_t2__T2_D_IDL_unless events7_t2__T2_D_IDL_unless.events7_t2__restart_in events7_t2__T2_D_IDL_unless.events7_t2__state_in events7_t2__T2_D_IDL_unless.events7_t2__restart_act events7_t2__T2_D_IDL_unless.events7_t2__state_act)
616
))
617

    
618
; events7_t2__T2_D__TO__T2_C_1_handler_until
619
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_1 Int)
620
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_1 Real)
621
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.events7_t2__restart_in Bool)
622
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.events7_t2__state_in events7_t2__type)
623
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_out Int)
624
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_out Real)
625
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_2 Int)
626
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_3 Int)
627
(declare-var events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_2 Real)
628
(declare-rel events7_t2__T2_D__TO__T2_C_1_handler_until (Int Real Bool events7_t2__type Int Real))
629
(rule (=> 
630
  (and (T2_D_ex events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_1
631
                false
632
                events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_2)
633
       (T2_C_en events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_2
634
                events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_1
635
                false
636
                events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_3
637
                events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_2)
638
       (= events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_out events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_2)
639
       (= events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_out events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_3)
640
       (= events7_t2__T2_D__TO__T2_C_1_handler_until.events7_t2__state_in POINTEvents7_T2)
641
       (= events7_t2__T2_D__TO__T2_C_1_handler_until.events7_t2__restart_in true)
642
       )
643
  (events7_t2__T2_D__TO__T2_C_1_handler_until events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_1 events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_1 events7_t2__T2_D__TO__T2_C_1_handler_until.events7_t2__restart_in events7_t2__T2_D__TO__T2_C_1_handler_until.events7_t2__state_in events7_t2__T2_D__TO__T2_C_1_handler_until.idEvents7_T2_out events7_t2__T2_D__TO__T2_C_1_handler_until.sT2_out)
644
))
645

    
646
; events7_t2__T2_D__TO__T2_C_1_unless
647
(declare-var events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__restart_in Bool)
648
(declare-var events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__state_in events7_t2__type)
649
(declare-var events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__restart_act Bool)
650
(declare-var events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__state_act events7_t2__type)
651
(declare-rel events7_t2__T2_D__TO__T2_C_1_unless (Bool events7_t2__type Bool events7_t2__type))
652
(rule (=> 
653
  (and (= events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__state_act events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__state_in)
654
       (= events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__restart_act events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__restart_in)
655
       )
656
  (events7_t2__T2_D__TO__T2_C_1_unless events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__restart_in events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__state_in events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__restart_act events7_t2__T2_D__TO__T2_C_1_unless.events7_t2__state_act)
657
))
658

    
659
; Events7_T1_en
660
(declare-var Events7_T1_en.idEvents7_T1_1 Int)
661
(declare-var Events7_T1_en.idEvents7_Events7_1 Int)
662
(declare-var Events7_T1_en.sT1_1 Real)
663
(declare-var Events7_T1_en.isInner Bool)
664
(declare-var Events7_T1_en.idEvents7_T1 Int)
665
(declare-var Events7_T1_en.idEvents7_Events7 Int)
666
(declare-var Events7_T1_en.sT1 Real)
667
(declare-var Events7_T1_en.__Events7_T1_en_1 Bool)
668
(declare-var Events7_T1_en.__Events7_T1_en_2 Bool)
669
(declare-var Events7_T1_en.__Events7_T1_en_3 Bool)
670
(declare-var Events7_T1_en.__Events7_T1_en_4 Int)
671
(declare-var Events7_T1_en.__Events7_T1_en_5 Real)
672
(declare-var Events7_T1_en.__Events7_T1_en_6 Int)
673
(declare-var Events7_T1_en.__Events7_T1_en_7 Real)
674
(declare-var Events7_T1_en.idEvents7_Events7_3 Int)
675
(declare-var Events7_T1_en.idEvents7_Events7_4 Int)
676
(declare-var Events7_T1_en.idEvents7_T1_2 Int)
677
(declare-var Events7_T1_en.idEvents7_T1_3 Int)
678
(declare-var Events7_T1_en.idEvents7_T1_4 Int)
679
(declare-var Events7_T1_en.idEvents7_T1_5 Int)
680
(declare-var Events7_T1_en.idEvents7_T1_6 Int)
681
(declare-var Events7_T1_en.sT1_2 Real)
682
(declare-var Events7_T1_en.sT1_3 Real)
683
(declare-var Events7_T1_en.sT1_4 Real)
684
(declare-var Events7_T1_en.sT1_5 Real)
685
(declare-var Events7_T1_en.sT1_6 Real)
686
(declare-rel Events7_T1_en (Int Int Real Bool Int Int Real))
687
(rule (=> 
688
  (and (T1_B_en Events7_T1_en.idEvents7_T1_1
689
                Events7_T1_en.sT1_1
690
                false
691
                Events7_T1_en.__Events7_T1_en_4
692
                Events7_T1_en.__Events7_T1_en_5)
693
       (= Events7_T1_en.__Events7_T1_en_3 (= Events7_T1_en.idEvents7_T1_1 677))
694
       (and (or (not (= Events7_T1_en.__Events7_T1_en_3 false))
695
               (and (= Events7_T1_en.sT1_5 Events7_T1_en.sT1_1)
696
                    (= Events7_T1_en.idEvents7_T1_5 Events7_T1_en.idEvents7_T1_1)
697
                    ))
698
            (or (not (= Events7_T1_en.__Events7_T1_en_3 true))
699
               (and (= Events7_T1_en.sT1_5 Events7_T1_en.__Events7_T1_en_5)
700
                    (= Events7_T1_en.idEvents7_T1_5 Events7_T1_en.__Events7_T1_en_4)
701
                    ))
702
       )
703
       (T1_A_en Events7_T1_en.idEvents7_T1_1
704
                Events7_T1_en.sT1_1
705
                false
706
                Events7_T1_en.__Events7_T1_en_6
707
                Events7_T1_en.__Events7_T1_en_7)
708
       (= Events7_T1_en.__Events7_T1_en_2 (= Events7_T1_en.idEvents7_T1_1 676))
709
       (and (or (not (= Events7_T1_en.__Events7_T1_en_2 false))
710
               (and (= Events7_T1_en.sT1_4 Events7_T1_en.sT1_1)
711
                    (= Events7_T1_en.idEvents7_T1_4 Events7_T1_en.idEvents7_T1_1)
712
                    ))
713
            (or (not (= Events7_T1_en.__Events7_T1_en_2 true))
714
               (and (= Events7_T1_en.sT1_4 Events7_T1_en.__Events7_T1_en_7)
715
                    (= Events7_T1_en.idEvents7_T1_4 Events7_T1_en.__Events7_T1_en_6)
716
                    ))
717
       )
718
       (T1_A_en Events7_T1_en.idEvents7_T1_1
719
                Events7_T1_en.sT1_1
720
                false
721
                Events7_T1_en.idEvents7_T1_2
722
                Events7_T1_en.sT1_2)
723
       (= Events7_T1_en.__Events7_T1_en_1 (= Events7_T1_en.idEvents7_T1_1 0))
724
       (and (or (not (= Events7_T1_en.__Events7_T1_en_1 false))
725
               (and (= Events7_T1_en.sT1_3 Events7_T1_en.sT1_1)
726
                    (= Events7_T1_en.idEvents7_T1_3 Events7_T1_en.idEvents7_T1_1)
727
                    (= Events7_T1_en.idEvents7_Events7_3 675)
728
                    (and (or (not (= Events7_T1_en.__Events7_T1_en_2 false))
729
                            (and (or (not (= Events7_T1_en.__Events7_T1_en_3 false))
730
                                    (and (= Events7_T1_en.sT1_6 Events7_T1_en.sT1_1)
731
                                         (= Events7_T1_en.idEvents7_T1_6 Events7_T1_en.idEvents7_T1_1)
732
                                         (= Events7_T1_en.idEvents7_Events7_4 675)
733
                                         ))
734
                                 (or (not (= Events7_T1_en.__Events7_T1_en_3 true))
735
                                    (and (= Events7_T1_en.sT1_6 Events7_T1_en.sT1_5)
736
                                         (= Events7_T1_en.idEvents7_T1_6 Events7_T1_en.idEvents7_T1_5)
737
                                         (= Events7_T1_en.idEvents7_Events7_4 Events7_T1_en.idEvents7_Events7_3)
738
                                         ))
739
                            ))
740
                         (or (not (= Events7_T1_en.__Events7_T1_en_2 true))
741
                            (and (= Events7_T1_en.sT1_6 Events7_T1_en.sT1_4)
742
                                 (= Events7_T1_en.idEvents7_T1_6 Events7_T1_en.idEvents7_T1_4)
743
                                 (= Events7_T1_en.idEvents7_Events7_4 Events7_T1_en.idEvents7_Events7_3)
744
                                 ))
745
                    )
746
                    ))
747
            (or (not (= Events7_T1_en.__Events7_T1_en_1 true))
748
               (and (= Events7_T1_en.sT1_3 Events7_T1_en.sT1_2)
749
                    (= Events7_T1_en.idEvents7_T1_3 Events7_T1_en.idEvents7_T1_2)
750
                    (= Events7_T1_en.idEvents7_Events7_3 675)
751
                    (= Events7_T1_en.sT1_6 Events7_T1_en.sT1_3)
752
                    (= Events7_T1_en.idEvents7_T1_6 Events7_T1_en.idEvents7_T1_3)
753
                    (= Events7_T1_en.idEvents7_Events7_4 Events7_T1_en.idEvents7_Events7_3)
754
                    ))
755
       )
756
       (= Events7_T1_en.sT1 Events7_T1_en.sT1_6)
757
       (= Events7_T1_en.idEvents7_T1 Events7_T1_en.idEvents7_T1_6)
758
       (= Events7_T1_en.idEvents7_Events7 Events7_T1_en.idEvents7_Events7_4)
759
       )
760
  (Events7_T1_en Events7_T1_en.idEvents7_T1_1 Events7_T1_en.idEvents7_Events7_1 Events7_T1_en.sT1_1 Events7_T1_en.isInner Events7_T1_en.idEvents7_T1 Events7_T1_en.idEvents7_Events7 Events7_T1_en.sT1)
761
))
762

    
763
; Events7_T2_en
764
(declare-var Events7_T2_en.idEvents7_T2_1 Int)
765
(declare-var Events7_T2_en.idEvents7_Events7_1 Int)
766
(declare-var Events7_T2_en.sT2_1 Real)
767
(declare-var Events7_T2_en.isInner Bool)
768
(declare-var Events7_T2_en.idEvents7_T2 Int)
769
(declare-var Events7_T2_en.idEvents7_Events7 Int)
770
(declare-var Events7_T2_en.sT2 Real)
771
(declare-var Events7_T2_en.__Events7_T2_en_1 Bool)
772
(declare-var Events7_T2_en.__Events7_T2_en_2 Bool)
773
(declare-var Events7_T2_en.__Events7_T2_en_3 Bool)
774
(declare-var Events7_T2_en.__Events7_T2_en_4 Int)
775
(declare-var Events7_T2_en.__Events7_T2_en_5 Real)
776
(declare-var Events7_T2_en.__Events7_T2_en_6 Int)
777
(declare-var Events7_T2_en.__Events7_T2_en_7 Real)
778
(declare-var Events7_T2_en.idEvents7_Events7_3 Int)
779
(declare-var Events7_T2_en.idEvents7_Events7_4 Int)
780
(declare-var Events7_T2_en.idEvents7_T2_2 Int)
781
(declare-var Events7_T2_en.idEvents7_T2_3 Int)
782
(declare-var Events7_T2_en.idEvents7_T2_4 Int)
783
(declare-var Events7_T2_en.idEvents7_T2_5 Int)
784
(declare-var Events7_T2_en.idEvents7_T2_6 Int)
785
(declare-var Events7_T2_en.sT2_2 Real)
786
(declare-var Events7_T2_en.sT2_3 Real)
787
(declare-var Events7_T2_en.sT2_4 Real)
788
(declare-var Events7_T2_en.sT2_5 Real)
789
(declare-var Events7_T2_en.sT2_6 Real)
790
(declare-rel Events7_T2_en (Int Int Real Bool Int Int Real))
791
(rule (=> 
792
  (and (T2_D_en Events7_T2_en.idEvents7_T2_1
793
                Events7_T2_en.sT2_1
794
                false
795
                Events7_T2_en.__Events7_T2_en_4
796
                Events7_T2_en.__Events7_T2_en_5)
797
       (= Events7_T2_en.__Events7_T2_en_3 (= Events7_T2_en.idEvents7_T2_1 680))
798
       (and (or (not (= Events7_T2_en.__Events7_T2_en_3 false))
799
               (and (= Events7_T2_en.sT2_5 Events7_T2_en.sT2_1)
800
                    (= Events7_T2_en.idEvents7_T2_5 Events7_T2_en.idEvents7_T2_1)
801
                    ))
802
            (or (not (= Events7_T2_en.__Events7_T2_en_3 true))
803
               (and (= Events7_T2_en.sT2_5 Events7_T2_en.__Events7_T2_en_5)
804
                    (= Events7_T2_en.idEvents7_T2_5 Events7_T2_en.__Events7_T2_en_4)
805
                    ))
806
       )
807
       (T2_C_en Events7_T2_en.idEvents7_T2_1
808
                Events7_T2_en.sT2_1
809
                false
810
                Events7_T2_en.__Events7_T2_en_6
811
                Events7_T2_en.__Events7_T2_en_7)
812
       (= Events7_T2_en.__Events7_T2_en_2 (= Events7_T2_en.idEvents7_T2_1 679))
813
       (and (or (not (= Events7_T2_en.__Events7_T2_en_2 false))
814
               (and (= Events7_T2_en.sT2_4 Events7_T2_en.sT2_1)
815
                    (= Events7_T2_en.idEvents7_T2_4 Events7_T2_en.idEvents7_T2_1)
816
                    ))
817
            (or (not (= Events7_T2_en.__Events7_T2_en_2 true))
818
               (and (= Events7_T2_en.sT2_4 Events7_T2_en.__Events7_T2_en_7)
819
                    (= Events7_T2_en.idEvents7_T2_4 Events7_T2_en.__Events7_T2_en_6)
820
                    ))
821
       )
822
       (T2_C_en Events7_T2_en.idEvents7_T2_1
823
                Events7_T2_en.sT2_1
824
                false
825
                Events7_T2_en.idEvents7_T2_2
826
                Events7_T2_en.sT2_2)
827
       (= Events7_T2_en.__Events7_T2_en_1 (= Events7_T2_en.idEvents7_T2_1 0))
828
       (and (or (not (= Events7_T2_en.__Events7_T2_en_1 false))
829
               (and (= Events7_T2_en.sT2_3 Events7_T2_en.sT2_1)
830
                    (= Events7_T2_en.idEvents7_T2_3 Events7_T2_en.idEvents7_T2_1)
831
                    (= Events7_T2_en.idEvents7_Events7_3 678)
832
                    (and (or (not (= Events7_T2_en.__Events7_T2_en_2 false))
833
                            (and (or (not (= Events7_T2_en.__Events7_T2_en_3 false))
834
                                    (and (= Events7_T2_en.sT2_6 Events7_T2_en.sT2_1)
835
                                         (= Events7_T2_en.idEvents7_T2_6 Events7_T2_en.idEvents7_T2_1)
836
                                         (= Events7_T2_en.idEvents7_Events7_4 678)
837
                                         ))
838
                                 (or (not (= Events7_T2_en.__Events7_T2_en_3 true))
839
                                    (and (= Events7_T2_en.sT2_6 Events7_T2_en.sT2_5)
840
                                         (= Events7_T2_en.idEvents7_T2_6 Events7_T2_en.idEvents7_T2_5)
841
                                         (= Events7_T2_en.idEvents7_Events7_4 Events7_T2_en.idEvents7_Events7_3)
842
                                         ))
843
                            ))
844
                         (or (not (= Events7_T2_en.__Events7_T2_en_2 true))
845
                            (and (= Events7_T2_en.sT2_6 Events7_T2_en.sT2_4)
846
                                 (= Events7_T2_en.idEvents7_T2_6 Events7_T2_en.idEvents7_T2_4)
847
                                 (= Events7_T2_en.idEvents7_Events7_4 Events7_T2_en.idEvents7_Events7_3)
848
                                 ))
849
                    )
850
                    ))
851
            (or (not (= Events7_T2_en.__Events7_T2_en_1 true))
852
               (and (= Events7_T2_en.sT2_3 Events7_T2_en.sT2_2)
853
                    (= Events7_T2_en.idEvents7_T2_3 Events7_T2_en.idEvents7_T2_2)
854
                    (= Events7_T2_en.idEvents7_Events7_3 678)
855
                    (= Events7_T2_en.sT2_6 Events7_T2_en.sT2_3)
856
                    (= Events7_T2_en.idEvents7_T2_6 Events7_T2_en.idEvents7_T2_3)
857
                    (= Events7_T2_en.idEvents7_Events7_4 Events7_T2_en.idEvents7_Events7_3)
858
                    ))
859
       )
860
       (= Events7_T2_en.sT2 Events7_T2_en.sT2_6)
861
       (= Events7_T2_en.idEvents7_T2 Events7_T2_en.idEvents7_T2_6)
862
       (= Events7_T2_en.idEvents7_Events7 Events7_T2_en.idEvents7_Events7_4)
863
       )
864
  (Events7_T2_en Events7_T2_en.idEvents7_T2_1 Events7_T2_en.idEvents7_Events7_1 Events7_T2_en.sT2_1 Events7_T2_en.isInner Events7_T2_en.idEvents7_T2 Events7_T2_en.idEvents7_Events7 Events7_T2_en.sT2)
865
))
866

    
867
; Events7_T1_node
868
(declare-var Events7_T1_node.idEvents7_T1_1 Int)
869
(declare-var Events7_T1_node.sT1_1 Real)
870
(declare-var Events7_T1_node.E Bool)
871
(declare-var Events7_T1_node.idEvents7_T1 Int)
872
(declare-var Events7_T1_node.sT1 Real)
873
(declare-var Events7_T1_node.__Events7_T1_node_38_c Bool)
874
(declare-var Events7_T1_node.__Events7_T1_node_39_c events7_t1__type)
875
(declare-var Events7_T1_node.ni_9._arrow._first_c Bool)
876
(declare-var Events7_T1_node.__Events7_T1_node_38_m Bool)
877
(declare-var Events7_T1_node.__Events7_T1_node_39_m events7_t1__type)
878
(declare-var Events7_T1_node.ni_9._arrow._first_m Bool)
879
(declare-var Events7_T1_node.__Events7_T1_node_38_x Bool)
880
(declare-var Events7_T1_node.__Events7_T1_node_39_x events7_t1__type)
881
(declare-var Events7_T1_node.ni_9._arrow._first_x Bool)
882
(declare-var Events7_T1_node.__Events7_T1_node_1 Bool)
883
(declare-var Events7_T1_node.__Events7_T1_node_10 events7_t1__type)
884
(declare-var Events7_T1_node.__Events7_T1_node_11 Bool)
885
(declare-var Events7_T1_node.__Events7_T1_node_12 events7_t1__type)
886
(declare-var Events7_T1_node.__Events7_T1_node_13 Bool)
887
(declare-var Events7_T1_node.__Events7_T1_node_14 events7_t1__type)
888
(declare-var Events7_T1_node.__Events7_T1_node_15 Int)
889
(declare-var Events7_T1_node.__Events7_T1_node_16 Real)
890
(declare-var Events7_T1_node.__Events7_T1_node_17 Bool)
891
(declare-var Events7_T1_node.__Events7_T1_node_18 events7_t1__type)
892
(declare-var Events7_T1_node.__Events7_T1_node_19 Int)
893
(declare-var Events7_T1_node.__Events7_T1_node_2 events7_t1__type)
894
(declare-var Events7_T1_node.__Events7_T1_node_20 Real)
895
(declare-var Events7_T1_node.__Events7_T1_node_21 Bool)
896
(declare-var Events7_T1_node.__Events7_T1_node_22 events7_t1__type)
897
(declare-var Events7_T1_node.__Events7_T1_node_23 Int)
898
(declare-var Events7_T1_node.__Events7_T1_node_24 Real)
899
(declare-var Events7_T1_node.__Events7_T1_node_25 Bool)
900
(declare-var Events7_T1_node.__Events7_T1_node_26 events7_t1__type)
901
(declare-var Events7_T1_node.__Events7_T1_node_27 Int)
902
(declare-var Events7_T1_node.__Events7_T1_node_28 Real)
903
(declare-var Events7_T1_node.__Events7_T1_node_29 Bool)
904
(declare-var Events7_T1_node.__Events7_T1_node_3 Bool)
905
(declare-var Events7_T1_node.__Events7_T1_node_30 events7_t1__type)
906
(declare-var Events7_T1_node.__Events7_T1_node_31 Int)
907
(declare-var Events7_T1_node.__Events7_T1_node_32 Real)
908
(declare-var Events7_T1_node.__Events7_T1_node_33 Bool)
909
(declare-var Events7_T1_node.__Events7_T1_node_34 events7_t1__type)
910
(declare-var Events7_T1_node.__Events7_T1_node_35 Int)
911
(declare-var Events7_T1_node.__Events7_T1_node_36 Real)
912
(declare-var Events7_T1_node.__Events7_T1_node_37 Bool)
913
(declare-var Events7_T1_node.__Events7_T1_node_4 events7_t1__type)
914
(declare-var Events7_T1_node.__Events7_T1_node_5 Bool)
915
(declare-var Events7_T1_node.__Events7_T1_node_6 events7_t1__type)
916
(declare-var Events7_T1_node.__Events7_T1_node_7 Bool)
917
(declare-var Events7_T1_node.__Events7_T1_node_8 events7_t1__type)
918
(declare-var Events7_T1_node.__Events7_T1_node_9 Bool)
919
(declare-var Events7_T1_node.events7_t1__next_restart_in Bool)
920
(declare-var Events7_T1_node.events7_t1__next_state_in events7_t1__type)
921
(declare-var Events7_T1_node.events7_t1__restart_act Bool)
922
(declare-var Events7_T1_node.events7_t1__restart_in Bool)
923
(declare-var Events7_T1_node.events7_t1__state_act events7_t1__type)
924
(declare-var Events7_T1_node.events7_t1__state_in events7_t1__type)
925
(declare-rel Events7_T1_node_reset (Bool events7_t1__type Bool Bool events7_t1__type Bool))
926
(declare-rel Events7_T1_node_step (Int Real Bool Int Real Bool events7_t1__type Bool Bool events7_t1__type Bool))
927

    
928
(rule (=> 
929
  (and 
930
       (= Events7_T1_node.__Events7_T1_node_38_m Events7_T1_node.__Events7_T1_node_38_c)
931
       (= Events7_T1_node.__Events7_T1_node_39_m Events7_T1_node.__Events7_T1_node_39_c)
932
       (= Events7_T1_node.ni_9._arrow._first_m true)
933
  )
934
  (Events7_T1_node_reset Events7_T1_node.__Events7_T1_node_38_c
935
                         Events7_T1_node.__Events7_T1_node_39_c
936
                         Events7_T1_node.ni_9._arrow._first_c
937
                         Events7_T1_node.__Events7_T1_node_38_m
938
                         Events7_T1_node.__Events7_T1_node_39_m
939
                         Events7_T1_node.ni_9._arrow._first_m)
940
))
941

    
942
(rule (=> 
943
  (and (= Events7_T1_node.ni_9._arrow._first_m Events7_T1_node.ni_9._arrow._first_c)
944
       (and (= Events7_T1_node.__Events7_T1_node_37 (ite Events7_T1_node.ni_9._arrow._first_m true false))
945
            (= Events7_T1_node.ni_9._arrow._first_x false))
946
       (and (or (not (= Events7_T1_node.__Events7_T1_node_37 false))
947
               (and (= Events7_T1_node.events7_t1__state_in Events7_T1_node.__Events7_T1_node_39_c)
948
                    (= Events7_T1_node.events7_t1__restart_in Events7_T1_node.__Events7_T1_node_38_c)
949
                    ))
950
            (or (not (= Events7_T1_node.__Events7_T1_node_37 true))
951
               (and (= Events7_T1_node.events7_t1__state_in POINTEvents7_T1)
952
                    (= Events7_T1_node.events7_t1__restart_in false)
953
                    ))
954
       )
955
       (and (or (not (= Events7_T1_node.events7_t1__state_in POINTEvents7_T1))
956
               (and (events7_t1__POINTEvents7_T1_unless Events7_T1_node.events7_t1__restart_in
957
                                                        Events7_T1_node.events7_t1__state_in
958
                                                        Events7_T1_node.idEvents7_T1_1
959
                                                        Events7_T1_node.E
960
                                                        Events7_T1_node.__Events7_T1_node_11
961
                                                        Events7_T1_node.__Events7_T1_node_12)
962
                    (= Events7_T1_node.events7_t1__state_act Events7_T1_node.__Events7_T1_node_12)
963
                    (= Events7_T1_node.events7_t1__restart_act Events7_T1_node.__Events7_T1_node_11)
964
                    ))
965
            (or (not (= Events7_T1_node.events7_t1__state_in POINT__TO__T1_A_1))
966
               (and (events7_t1__POINT__TO__T1_A_1_unless Events7_T1_node.events7_t1__restart_in
967
                                                          Events7_T1_node.events7_t1__state_in
968
                                                          Events7_T1_node.__Events7_T1_node_9
969
                                                          Events7_T1_node.__Events7_T1_node_10)
970
                    (= Events7_T1_node.events7_t1__state_act Events7_T1_node.__Events7_T1_node_10)
971
                    (= Events7_T1_node.events7_t1__restart_act Events7_T1_node.__Events7_T1_node_9)
972
                    ))
973
            (or (not (= Events7_T1_node.events7_t1__state_in T1_A_IDL))
974
               (and (events7_t1__T1_A_IDL_unless Events7_T1_node.events7_t1__restart_in
975
                                                 Events7_T1_node.events7_t1__state_in
976
                                                 Events7_T1_node.__Events7_T1_node_3
977
                                                 Events7_T1_node.__Events7_T1_node_4)
978
                    (= Events7_T1_node.events7_t1__state_act Events7_T1_node.__Events7_T1_node_4)
979
                    (= Events7_T1_node.events7_t1__restart_act Events7_T1_node.__Events7_T1_node_3)
980
                    ))
981
            (or (not (= Events7_T1_node.events7_t1__state_in T1_A__TO__T1_B_1))
982
               (and (events7_t1__T1_A__TO__T1_B_1_unless Events7_T1_node.events7_t1__restart_in
983
                                                         Events7_T1_node.events7_t1__state_in
984
                                                         Events7_T1_node.__Events7_T1_node_7
985
                                                         Events7_T1_node.__Events7_T1_node_8)
986
                    (= Events7_T1_node.events7_t1__state_act Events7_T1_node.__Events7_T1_node_8)
987
                    (= Events7_T1_node.events7_t1__restart_act Events7_T1_node.__Events7_T1_node_7)
988
                    ))
989
            (or (not (= Events7_T1_node.events7_t1__state_in T1_B_IDL))
990
               (and (events7_t1__T1_B_IDL_unless Events7_T1_node.events7_t1__restart_in
991
                                                 Events7_T1_node.events7_t1__state_in
992
                                                 Events7_T1_node.__Events7_T1_node_1
993
                                                 Events7_T1_node.__Events7_T1_node_2)
994
                    (= Events7_T1_node.events7_t1__state_act Events7_T1_node.__Events7_T1_node_2)
995
                    (= Events7_T1_node.events7_t1__restart_act Events7_T1_node.__Events7_T1_node_1)
996
                    ))
997
            (or (not (= Events7_T1_node.events7_t1__state_in T1_B__TO__T1_A_1))
998
               (and (events7_t1__T1_B__TO__T1_A_1_unless Events7_T1_node.events7_t1__restart_in
999
                                                         Events7_T1_node.events7_t1__state_in
1000
                                                         Events7_T1_node.__Events7_T1_node_5
1001
                                                         Events7_T1_node.__Events7_T1_node_6)
1002
                    (= Events7_T1_node.events7_t1__state_act Events7_T1_node.__Events7_T1_node_6)
1003
                    (= Events7_T1_node.events7_t1__restart_act Events7_T1_node.__Events7_T1_node_5)
1004
                    ))
1005
       )
1006
       (and (or (not (= Events7_T1_node.events7_t1__state_act POINTEvents7_T1))
1007
               (and (events7_t1__POINTEvents7_T1_handler_until Events7_T1_node.idEvents7_T1_1
1008
                                                               Events7_T1_node.sT1_1
1009
                                                               Events7_T1_node.__Events7_T1_node_33
1010
                                                               Events7_T1_node.__Events7_T1_node_34
1011
                                                               Events7_T1_node.__Events7_T1_node_35
1012
                                                               Events7_T1_node.__Events7_T1_node_36)
1013
                    (= Events7_T1_node.sT1 Events7_T1_node.__Events7_T1_node_36)
1014
                    (= Events7_T1_node.idEvents7_T1 Events7_T1_node.__Events7_T1_node_35)
1015
                    (= Events7_T1_node.events7_t1__next_state_in Events7_T1_node.__Events7_T1_node_34)
1016
                    (= Events7_T1_node.events7_t1__next_restart_in Events7_T1_node.__Events7_T1_node_33)
1017
                    ))
1018
            (or (not (= Events7_T1_node.events7_t1__state_act POINT__TO__T1_A_1))
1019
               (and (events7_t1__POINT__TO__T1_A_1_handler_until Events7_T1_node.idEvents7_T1_1
1020
                                                                 Events7_T1_node.sT1_1
1021
                                                                 Events7_T1_node.__Events7_T1_node_29
1022
                                                                 Events7_T1_node.__Events7_T1_node_30
1023
                                                                 Events7_T1_node.__Events7_T1_node_31
1024
                                                                 Events7_T1_node.__Events7_T1_node_32)
1025
                    (= Events7_T1_node.sT1 Events7_T1_node.__Events7_T1_node_32)
1026
                    (= Events7_T1_node.idEvents7_T1 Events7_T1_node.__Events7_T1_node_31)
1027
                    (= Events7_T1_node.events7_t1__next_state_in Events7_T1_node.__Events7_T1_node_30)
1028
                    (= Events7_T1_node.events7_t1__next_restart_in Events7_T1_node.__Events7_T1_node_29)
1029
                    ))
1030
            (or (not (= Events7_T1_node.events7_t1__state_act T1_A_IDL))
1031
               (and (events7_t1__T1_A_IDL_handler_until Events7_T1_node.idEvents7_T1_1
1032
                                                        Events7_T1_node.sT1_1
1033
                                                        Events7_T1_node.__Events7_T1_node_17
1034
                                                        Events7_T1_node.__Events7_T1_node_18
1035
                                                        Events7_T1_node.__Events7_T1_node_19
1036
                                                        Events7_T1_node.__Events7_T1_node_20)
1037
                    (= Events7_T1_node.sT1 Events7_T1_node.__Events7_T1_node_20)
1038
                    (= Events7_T1_node.idEvents7_T1 Events7_T1_node.__Events7_T1_node_19)
1039
                    (= Events7_T1_node.events7_t1__next_state_in Events7_T1_node.__Events7_T1_node_18)
1040
                    (= Events7_T1_node.events7_t1__next_restart_in Events7_T1_node.__Events7_T1_node_17)
1041
                    ))
1042
            (or (not (= Events7_T1_node.events7_t1__state_act T1_A__TO__T1_B_1))
1043
               (and (events7_t1__T1_A__TO__T1_B_1_handler_until Events7_T1_node.idEvents7_T1_1
1044
                                                                Events7_T1_node.sT1_1
1045
                                                                Events7_T1_node.__Events7_T1_node_25
1046
                                                                Events7_T1_node.__Events7_T1_node_26
1047
                                                                Events7_T1_node.__Events7_T1_node_27
1048
                                                                Events7_T1_node.__Events7_T1_node_28)
1049
                    (= Events7_T1_node.sT1 Events7_T1_node.__Events7_T1_node_28)
1050
                    (= Events7_T1_node.idEvents7_T1 Events7_T1_node.__Events7_T1_node_27)
1051
                    (= Events7_T1_node.events7_t1__next_state_in Events7_T1_node.__Events7_T1_node_26)
1052
                    (= Events7_T1_node.events7_t1__next_restart_in Events7_T1_node.__Events7_T1_node_25)
1053
                    ))
1054
            (or (not (= Events7_T1_node.events7_t1__state_act T1_B_IDL))
1055
               (and (events7_t1__T1_B_IDL_handler_until Events7_T1_node.idEvents7_T1_1
1056
                                                        Events7_T1_node.sT1_1
1057
                                                        Events7_T1_node.__Events7_T1_node_13
1058
                                                        Events7_T1_node.__Events7_T1_node_14
1059
                                                        Events7_T1_node.__Events7_T1_node_15
1060
                                                        Events7_T1_node.__Events7_T1_node_16)
1061
                    (= Events7_T1_node.sT1 Events7_T1_node.__Events7_T1_node_16)
1062
                    (= Events7_T1_node.idEvents7_T1 Events7_T1_node.__Events7_T1_node_15)
1063
                    (= Events7_T1_node.events7_t1__next_state_in Events7_T1_node.__Events7_T1_node_14)
1064
                    (= Events7_T1_node.events7_t1__next_restart_in Events7_T1_node.__Events7_T1_node_13)
1065
                    ))
1066
            (or (not (= Events7_T1_node.events7_t1__state_act T1_B__TO__T1_A_1))
1067
               (and (events7_t1__T1_B__TO__T1_A_1_handler_until Events7_T1_node.idEvents7_T1_1
1068
                                                                Events7_T1_node.sT1_1
1069
                                                                Events7_T1_node.__Events7_T1_node_21
1070
                                                                Events7_T1_node.__Events7_T1_node_22
1071
                                                                Events7_T1_node.__Events7_T1_node_23
1072
                                                                Events7_T1_node.__Events7_T1_node_24)
1073
                    (= Events7_T1_node.sT1 Events7_T1_node.__Events7_T1_node_24)
1074
                    (= Events7_T1_node.idEvents7_T1 Events7_T1_node.__Events7_T1_node_23)
1075
                    (= Events7_T1_node.events7_t1__next_state_in Events7_T1_node.__Events7_T1_node_22)
1076
                    (= Events7_T1_node.events7_t1__next_restart_in Events7_T1_node.__Events7_T1_node_21)
1077
                    ))
1078
       )
1079
       (= Events7_T1_node.__Events7_T1_node_39_x Events7_T1_node.events7_t1__next_state_in)
1080
       (= Events7_T1_node.__Events7_T1_node_38_x Events7_T1_node.events7_t1__next_restart_in)
1081
       )
1082
  (Events7_T1_node_step Events7_T1_node.idEvents7_T1_1
1083
                        Events7_T1_node.sT1_1
1084
                        Events7_T1_node.E
1085
                        Events7_T1_node.idEvents7_T1
1086
                        Events7_T1_node.sT1
1087
                        Events7_T1_node.__Events7_T1_node_38_c
1088
                        Events7_T1_node.__Events7_T1_node_39_c
1089
                        Events7_T1_node.ni_9._arrow._first_c
1090
                        Events7_T1_node.__Events7_T1_node_38_x
1091
                        Events7_T1_node.__Events7_T1_node_39_x
1092
                        Events7_T1_node.ni_9._arrow._first_x)
1093
))
1094

    
1095
; Events7_T2_node
1096
(declare-var Events7_T2_node.idEvents7_T2_1 Int)
1097
(declare-var Events7_T2_node.sT2_1 Real)
1098
(declare-var Events7_T2_node.idEvents7_T1_1 Int)
1099
(declare-var Events7_T2_node.idEvents7_T2 Int)
1100
(declare-var Events7_T2_node.sT2 Real)
1101
(declare-var Events7_T2_node.__Events7_T2_node_38_c Bool)
1102
(declare-var Events7_T2_node.__Events7_T2_node_39_c events7_t2__type)
1103
(declare-var Events7_T2_node.ni_8._arrow._first_c Bool)
1104
(declare-var Events7_T2_node.__Events7_T2_node_38_m Bool)
1105
(declare-var Events7_T2_node.__Events7_T2_node_39_m events7_t2__type)
1106
(declare-var Events7_T2_node.ni_8._arrow._first_m Bool)
1107
(declare-var Events7_T2_node.__Events7_T2_node_38_x Bool)
1108
(declare-var Events7_T2_node.__Events7_T2_node_39_x events7_t2__type)
1109
(declare-var Events7_T2_node.ni_8._arrow._first_x Bool)
1110
(declare-var Events7_T2_node.__Events7_T2_node_1 Bool)
1111
(declare-var Events7_T2_node.__Events7_T2_node_10 events7_t2__type)
1112
(declare-var Events7_T2_node.__Events7_T2_node_11 Bool)
1113
(declare-var Events7_T2_node.__Events7_T2_node_12 events7_t2__type)
1114
(declare-var Events7_T2_node.__Events7_T2_node_13 Bool)
1115
(declare-var Events7_T2_node.__Events7_T2_node_14 events7_t2__type)
1116
(declare-var Events7_T2_node.__Events7_T2_node_15 Int)
1117
(declare-var Events7_T2_node.__Events7_T2_node_16 Real)
1118
(declare-var Events7_T2_node.__Events7_T2_node_17 Bool)
1119
(declare-var Events7_T2_node.__Events7_T2_node_18 events7_t2__type)
1120
(declare-var Events7_T2_node.__Events7_T2_node_19 Int)
1121
(declare-var Events7_T2_node.__Events7_T2_node_2 events7_t2__type)
1122
(declare-var Events7_T2_node.__Events7_T2_node_20 Real)
1123
(declare-var Events7_T2_node.__Events7_T2_node_21 Bool)
1124
(declare-var Events7_T2_node.__Events7_T2_node_22 events7_t2__type)
1125
(declare-var Events7_T2_node.__Events7_T2_node_23 Int)
1126
(declare-var Events7_T2_node.__Events7_T2_node_24 Real)
1127
(declare-var Events7_T2_node.__Events7_T2_node_25 Bool)
1128
(declare-var Events7_T2_node.__Events7_T2_node_26 events7_t2__type)
1129
(declare-var Events7_T2_node.__Events7_T2_node_27 Int)
1130
(declare-var Events7_T2_node.__Events7_T2_node_28 Real)
1131
(declare-var Events7_T2_node.__Events7_T2_node_29 Bool)
1132
(declare-var Events7_T2_node.__Events7_T2_node_3 Bool)
1133
(declare-var Events7_T2_node.__Events7_T2_node_30 events7_t2__type)
1134
(declare-var Events7_T2_node.__Events7_T2_node_31 Int)
1135
(declare-var Events7_T2_node.__Events7_T2_node_32 Real)
1136
(declare-var Events7_T2_node.__Events7_T2_node_33 Bool)
1137
(declare-var Events7_T2_node.__Events7_T2_node_34 events7_t2__type)
1138
(declare-var Events7_T2_node.__Events7_T2_node_35 Int)
1139
(declare-var Events7_T2_node.__Events7_T2_node_36 Real)
1140
(declare-var Events7_T2_node.__Events7_T2_node_37 Bool)
1141
(declare-var Events7_T2_node.__Events7_T2_node_4 events7_t2__type)
1142
(declare-var Events7_T2_node.__Events7_T2_node_5 Bool)
1143
(declare-var Events7_T2_node.__Events7_T2_node_6 events7_t2__type)
1144
(declare-var Events7_T2_node.__Events7_T2_node_7 Bool)
1145
(declare-var Events7_T2_node.__Events7_T2_node_8 events7_t2__type)
1146
(declare-var Events7_T2_node.__Events7_T2_node_9 Bool)
1147
(declare-var Events7_T2_node.events7_t2__next_restart_in Bool)
1148
(declare-var Events7_T2_node.events7_t2__next_state_in events7_t2__type)
1149
(declare-var Events7_T2_node.events7_t2__restart_act Bool)
1150
(declare-var Events7_T2_node.events7_t2__restart_in Bool)
1151
(declare-var Events7_T2_node.events7_t2__state_act events7_t2__type)
1152
(declare-var Events7_T2_node.events7_t2__state_in events7_t2__type)
1153
(declare-rel Events7_T2_node_reset (Bool events7_t2__type Bool Bool events7_t2__type Bool))
1154
(declare-rel Events7_T2_node_step (Int Real Int Int Real Bool events7_t2__type Bool Bool events7_t2__type Bool))
1155

    
1156
(rule (=> 
1157
  (and 
1158
       (= Events7_T2_node.__Events7_T2_node_38_m Events7_T2_node.__Events7_T2_node_38_c)
1159
       (= Events7_T2_node.__Events7_T2_node_39_m Events7_T2_node.__Events7_T2_node_39_c)
1160
       (= Events7_T2_node.ni_8._arrow._first_m true)
1161
  )
1162
  (Events7_T2_node_reset Events7_T2_node.__Events7_T2_node_38_c
1163
                         Events7_T2_node.__Events7_T2_node_39_c
1164
                         Events7_T2_node.ni_8._arrow._first_c
1165
                         Events7_T2_node.__Events7_T2_node_38_m
1166
                         Events7_T2_node.__Events7_T2_node_39_m
1167
                         Events7_T2_node.ni_8._arrow._first_m)
1168
))
1169

    
1170
(rule (=> 
1171
  (and (= Events7_T2_node.ni_8._arrow._first_m Events7_T2_node.ni_8._arrow._first_c)
1172
       (and (= Events7_T2_node.__Events7_T2_node_37 (ite Events7_T2_node.ni_8._arrow._first_m true false))
1173
            (= Events7_T2_node.ni_8._arrow._first_x false))
1174
       (and (or (not (= Events7_T2_node.__Events7_T2_node_37 false))
1175
               (and (= Events7_T2_node.events7_t2__state_in Events7_T2_node.__Events7_T2_node_39_c)
1176
                    (= Events7_T2_node.events7_t2__restart_in Events7_T2_node.__Events7_T2_node_38_c)
1177
                    ))
1178
            (or (not (= Events7_T2_node.__Events7_T2_node_37 true))
1179
               (and (= Events7_T2_node.events7_t2__state_in POINTEvents7_T2)
1180
                    (= Events7_T2_node.events7_t2__restart_in false)
1181
                    ))
1182
       )
1183
       (and (or (not (= Events7_T2_node.events7_t2__state_in POINTEvents7_T2))
1184
               (and (events7_t2__POINTEvents7_T2_unless Events7_T2_node.events7_t2__restart_in
1185
                                                        Events7_T2_node.events7_t2__state_in
1186
                                                        Events7_T2_node.idEvents7_T2_1
1187
                                                        Events7_T2_node.idEvents7_T1_1
1188
                                                        Events7_T2_node.__Events7_T2_node_11
1189
                                                        Events7_T2_node.__Events7_T2_node_12)
1190
                    (= Events7_T2_node.events7_t2__state_act Events7_T2_node.__Events7_T2_node_12)
1191
                    (= Events7_T2_node.events7_t2__restart_act Events7_T2_node.__Events7_T2_node_11)
1192
                    ))
1193
            (or (not (= Events7_T2_node.events7_t2__state_in POINT__TO__T2_C_1))
1194
               (and (events7_t2__POINT__TO__T2_C_1_unless Events7_T2_node.events7_t2__restart_in
1195
                                                          Events7_T2_node.events7_t2__state_in
1196
                                                          Events7_T2_node.__Events7_T2_node_9
1197
                                                          Events7_T2_node.__Events7_T2_node_10)
1198
                    (= Events7_T2_node.events7_t2__state_act Events7_T2_node.__Events7_T2_node_10)
1199
                    (= Events7_T2_node.events7_t2__restart_act Events7_T2_node.__Events7_T2_node_9)
1200
                    ))
1201
            (or (not (= Events7_T2_node.events7_t2__state_in T2_C_IDL))
1202
               (and (events7_t2__T2_C_IDL_unless Events7_T2_node.events7_t2__restart_in
1203
                                                 Events7_T2_node.events7_t2__state_in
1204
                                                 Events7_T2_node.__Events7_T2_node_3
1205
                                                 Events7_T2_node.__Events7_T2_node_4)
1206
                    (= Events7_T2_node.events7_t2__state_act Events7_T2_node.__Events7_T2_node_4)
1207
                    (= Events7_T2_node.events7_t2__restart_act Events7_T2_node.__Events7_T2_node_3)
1208
                    ))
1209
            (or (not (= Events7_T2_node.events7_t2__state_in T2_C__TO__T2_D_1))
1210
               (and (events7_t2__T2_C__TO__T2_D_1_unless Events7_T2_node.events7_t2__restart_in
1211
                                                         Events7_T2_node.events7_t2__state_in
1212
                                                         Events7_T2_node.__Events7_T2_node_7
1213
                                                         Events7_T2_node.__Events7_T2_node_8)
1214
                    (= Events7_T2_node.events7_t2__state_act Events7_T2_node.__Events7_T2_node_8)
1215
                    (= Events7_T2_node.events7_t2__restart_act Events7_T2_node.__Events7_T2_node_7)
1216
                    ))
1217
            (or (not (= Events7_T2_node.events7_t2__state_in T2_D_IDL))
1218
               (and (events7_t2__T2_D_IDL_unless Events7_T2_node.events7_t2__restart_in
1219
                                                 Events7_T2_node.events7_t2__state_in
1220
                                                 Events7_T2_node.__Events7_T2_node_1
1221
                                                 Events7_T2_node.__Events7_T2_node_2)
1222
                    (= Events7_T2_node.events7_t2__state_act Events7_T2_node.__Events7_T2_node_2)
1223
                    (= Events7_T2_node.events7_t2__restart_act Events7_T2_node.__Events7_T2_node_1)
1224
                    ))
1225
            (or (not (= Events7_T2_node.events7_t2__state_in T2_D__TO__T2_C_1))
1226
               (and (events7_t2__T2_D__TO__T2_C_1_unless Events7_T2_node.events7_t2__restart_in
1227
                                                         Events7_T2_node.events7_t2__state_in
1228
                                                         Events7_T2_node.__Events7_T2_node_5
1229
                                                         Events7_T2_node.__Events7_T2_node_6)
1230
                    (= Events7_T2_node.events7_t2__state_act Events7_T2_node.__Events7_T2_node_6)
1231
                    (= Events7_T2_node.events7_t2__restart_act Events7_T2_node.__Events7_T2_node_5)
1232
                    ))
1233
       )
1234
       (and (or (not (= Events7_T2_node.events7_t2__state_act POINTEvents7_T2))
1235
               (and (events7_t2__POINTEvents7_T2_handler_until Events7_T2_node.idEvents7_T2_1
1236
                                                               Events7_T2_node.sT2_1
1237
                                                               Events7_T2_node.__Events7_T2_node_33
1238
                                                               Events7_T2_node.__Events7_T2_node_34
1239
                                                               Events7_T2_node.__Events7_T2_node_35
1240
                                                               Events7_T2_node.__Events7_T2_node_36)
1241
                    (= Events7_T2_node.sT2 Events7_T2_node.__Events7_T2_node_36)
1242
                    (= Events7_T2_node.idEvents7_T2 Events7_T2_node.__Events7_T2_node_35)
1243
                    (= Events7_T2_node.events7_t2__next_state_in Events7_T2_node.__Events7_T2_node_34)
1244
                    (= Events7_T2_node.events7_t2__next_restart_in Events7_T2_node.__Events7_T2_node_33)
1245
                    ))
1246
            (or (not (= Events7_T2_node.events7_t2__state_act POINT__TO__T2_C_1))
1247
               (and (events7_t2__POINT__TO__T2_C_1_handler_until Events7_T2_node.idEvents7_T2_1
1248
                                                                 Events7_T2_node.sT2_1
1249
                                                                 Events7_T2_node.__Events7_T2_node_29
1250
                                                                 Events7_T2_node.__Events7_T2_node_30
1251
                                                                 Events7_T2_node.__Events7_T2_node_31
1252
                                                                 Events7_T2_node.__Events7_T2_node_32)
1253
                    (= Events7_T2_node.sT2 Events7_T2_node.__Events7_T2_node_32)
1254
                    (= Events7_T2_node.idEvents7_T2 Events7_T2_node.__Events7_T2_node_31)
1255
                    (= Events7_T2_node.events7_t2__next_state_in Events7_T2_node.__Events7_T2_node_30)
1256
                    (= Events7_T2_node.events7_t2__next_restart_in Events7_T2_node.__Events7_T2_node_29)
1257
                    ))
1258
            (or (not (= Events7_T2_node.events7_t2__state_act T2_C_IDL))
1259
               (and (events7_t2__T2_C_IDL_handler_until Events7_T2_node.idEvents7_T2_1
1260
                                                        Events7_T2_node.sT2_1
1261
                                                        Events7_T2_node.__Events7_T2_node_17
1262
                                                        Events7_T2_node.__Events7_T2_node_18
1263
                                                        Events7_T2_node.__Events7_T2_node_19
1264
                                                        Events7_T2_node.__Events7_T2_node_20)
1265
                    (= Events7_T2_node.sT2 Events7_T2_node.__Events7_T2_node_20)
1266
                    (= Events7_T2_node.idEvents7_T2 Events7_T2_node.__Events7_T2_node_19)
1267
                    (= Events7_T2_node.events7_t2__next_state_in Events7_T2_node.__Events7_T2_node_18)
1268
                    (= Events7_T2_node.events7_t2__next_restart_in Events7_T2_node.__Events7_T2_node_17)
1269
                    ))
1270
            (or (not (= Events7_T2_node.events7_t2__state_act T2_C__TO__T2_D_1))
1271
               (and (events7_t2__T2_C__TO__T2_D_1_handler_until Events7_T2_node.idEvents7_T2_1
1272
                                                                Events7_T2_node.sT2_1
1273
                                                                Events7_T2_node.__Events7_T2_node_25
1274
                                                                Events7_T2_node.__Events7_T2_node_26
1275
                                                                Events7_T2_node.__Events7_T2_node_27
1276
                                                                Events7_T2_node.__Events7_T2_node_28)
1277
                    (= Events7_T2_node.sT2 Events7_T2_node.__Events7_T2_node_28)
1278
                    (= Events7_T2_node.idEvents7_T2 Events7_T2_node.__Events7_T2_node_27)
1279
                    (= Events7_T2_node.events7_t2__next_state_in Events7_T2_node.__Events7_T2_node_26)
1280
                    (= Events7_T2_node.events7_t2__next_restart_in Events7_T2_node.__Events7_T2_node_25)
1281
                    ))
1282
            (or (not (= Events7_T2_node.events7_t2__state_act T2_D_IDL))
1283
               (and (events7_t2__T2_D_IDL_handler_until Events7_T2_node.idEvents7_T2_1
1284
                                                        Events7_T2_node.sT2_1
1285
                                                        Events7_T2_node.__Events7_T2_node_13
1286
                                                        Events7_T2_node.__Events7_T2_node_14
1287
                                                        Events7_T2_node.__Events7_T2_node_15
1288
                                                        Events7_T2_node.__Events7_T2_node_16)
1289
                    (= Events7_T2_node.sT2 Events7_T2_node.__Events7_T2_node_16)
1290
                    (= Events7_T2_node.idEvents7_T2 Events7_T2_node.__Events7_T2_node_15)
1291
                    (= Events7_T2_node.events7_t2__next_state_in Events7_T2_node.__Events7_T2_node_14)
1292
                    (= Events7_T2_node.events7_t2__next_restart_in Events7_T2_node.__Events7_T2_node_13)
1293
                    ))
1294
            (or (not (= Events7_T2_node.events7_t2__state_act T2_D__TO__T2_C_1))
1295
               (and (events7_t2__T2_D__TO__T2_C_1_handler_until Events7_T2_node.idEvents7_T2_1
1296
                                                                Events7_T2_node.sT2_1
1297
                                                                Events7_T2_node.__Events7_T2_node_21
1298
                                                                Events7_T2_node.__Events7_T2_node_22
1299
                                                                Events7_T2_node.__Events7_T2_node_23
1300
                                                                Events7_T2_node.__Events7_T2_node_24)
1301
                    (= Events7_T2_node.sT2 Events7_T2_node.__Events7_T2_node_24)
1302
                    (= Events7_T2_node.idEvents7_T2 Events7_T2_node.__Events7_T2_node_23)
1303
                    (= Events7_T2_node.events7_t2__next_state_in Events7_T2_node.__Events7_T2_node_22)
1304
                    (= Events7_T2_node.events7_t2__next_restart_in Events7_T2_node.__Events7_T2_node_21)
1305
                    ))
1306
       )
1307
       (= Events7_T2_node.__Events7_T2_node_39_x Events7_T2_node.events7_t2__next_state_in)
1308
       (= Events7_T2_node.__Events7_T2_node_38_x Events7_T2_node.events7_t2__next_restart_in)
1309
       )
1310
  (Events7_T2_node_step Events7_T2_node.idEvents7_T2_1
1311
                        Events7_T2_node.sT2_1
1312
                        Events7_T2_node.idEvents7_T1_1
1313
                        Events7_T2_node.idEvents7_T2
1314
                        Events7_T2_node.sT2
1315
                        Events7_T2_node.__Events7_T2_node_38_c
1316
                        Events7_T2_node.__Events7_T2_node_39_c
1317
                        Events7_T2_node.ni_8._arrow._first_c
1318
                        Events7_T2_node.__Events7_T2_node_38_x
1319
                        Events7_T2_node.__Events7_T2_node_39_x
1320
                        Events7_T2_node.ni_8._arrow._first_x)
1321
))
1322

    
1323
; events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until
1324
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_1 Int)
1325
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_1 Int)
1326
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_1 Real)
1327
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_1 Int)
1328
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_1 Real)
1329
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.events7_events7__restart_in Bool)
1330
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.events7_events7__state_in events7_events7__type)
1331
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_out Int)
1332
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_out Int)
1333
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_out Int)
1334
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_out Real)
1335
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_out Real)
1336
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_2 Int)
1337
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_3 Int)
1338
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_2 Int)
1339
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_2 Int)
1340
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_2 Real)
1341
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_2 Real)
1342
(declare-rel events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until (Int Int Real Int Real Bool events7_events7__type Int Int Int Real Real))
1343
(rule (=> 
1344
  (and (Events7_T1_en events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_1
1345
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_1
1346
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_1
1347
                      false
1348
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_2
1349
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_2
1350
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_2)
1351
       (Events7_T2_en events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_1
1352
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_2
1353
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_1
1354
                      false
1355
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_2
1356
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_3
1357
                      events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_2)
1358
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_2)
1359
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_2)
1360
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_2)
1361
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_2)
1362
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_3)
1363
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.events7_events7__state_in POINTEvents7_Events7)
1364
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.events7_events7__restart_in true)
1365
       )
1366
  (events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_1 events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_1 events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_1 events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_1 events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_1 events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.events7_events7__restart_in events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.events7_events7__state_in events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_Events7_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T1_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.idEvents7_T2_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT1_out events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until.sT2_out)
1367
))
1368

    
1369
; events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless
1370
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__restart_in Bool)
1371
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__state_in events7_events7__type)
1372
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__restart_act Bool)
1373
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__state_act events7_events7__type)
1374
(declare-rel events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless (Bool events7_events7__type Bool events7_events7__type))
1375
(rule (=> 
1376
  (and (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__state_act events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__state_in)
1377
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__restart_act events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__restart_in)
1378
       )
1379
  (events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__restart_in events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__state_in events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__restart_act events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless.events7_events7__state_act)
1380
))
1381

    
1382
; events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until
1383
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_Events7_1 Int)
1384
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_1 Int)
1385
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_1 Real)
1386
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_1 Int)
1387
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_1 Real)
1388
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.E Bool)
1389
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.events7_events7__restart_in Bool)
1390
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.events7_events7__state_in events7_events7__type)
1391
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_Events7_out Int)
1392
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_out Int)
1393
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_out Int)
1394
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_out Real)
1395
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_out Real)
1396
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c Bool)
1397
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c events7_t2__type)
1398
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c Bool)
1399
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c Bool)
1400
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c events7_t1__type)
1401
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c Bool)
1402
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Bool)
1403
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m events7_t2__type)
1404
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Bool)
1405
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Bool)
1406
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m events7_t1__type)
1407
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Bool)
1408
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x Bool)
1409
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x events7_t2__type)
1410
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x Bool)
1411
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x Bool)
1412
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x events7_t1__type)
1413
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x Bool)
1414
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_1 Bool)
1415
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_2 Int)
1416
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_3 Real)
1417
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_4 Bool)
1418
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_5 Int)
1419
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_6 Real)
1420
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_2 Int)
1421
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_2 Int)
1422
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_2 Real)
1423
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_2 Real)
1424
(declare-rel events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_reset (Bool events7_t2__type Bool Bool events7_t1__type Bool Bool events7_t2__type Bool Bool events7_t1__type Bool))
1425
(declare-rel events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_step (Int Int Real Int Real Bool Bool events7_events7__type Int Int Int Real Real Bool events7_t2__type Bool Bool events7_t1__type Bool Bool events7_t2__type Bool Bool events7_t1__type Bool))
1426

    
1427
(rule (=> 
1428
  (and 
1429
       
1430
       (Events7_T1_node_reset events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1431
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1432
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1433
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1434
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1435
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m)
1436
       (Events7_T2_node_reset events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1437
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1438
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1439
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1440
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1441
                              events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m)
1442
  )
1443
  (events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_reset 
1444
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1445
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1446
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1447
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1448
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1449
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1450
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1451
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1452
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
1453
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1454
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1455
  events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m)
1456
))
1457

    
1458
(rule (=> 
1459
  (and (and (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c)
1460
            (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c)
1461
            (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c)
1462
            )
1463
       (Events7_T1_node_step events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_1
1464
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_1
1465
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.E
1466
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_5
1467
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_6
1468
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1469
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1470
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
1471
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
1472
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
1473
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x)
1474
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_4 (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_1 0)))
1475
       (and (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_4 true))
1476
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_5))
1477
            (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_4 false))
1478
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_1))
1479
       )
1480
       (and (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c)
1481
            (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c)
1482
            (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c)
1483
            )
1484
       (Events7_T2_node_step events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_1
1485
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_1
1486
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_2
1487
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_2
1488
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_3
1489
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1490
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1491
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
1492
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
1493
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
1494
                             events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x)
1495
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_1 (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_1 0)))
1496
       (and (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_1 true))
1497
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_3))
1498
            (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_1 false))
1499
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_1))
1500
       )
1501
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_out events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_2)
1502
       (and (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_4 true))
1503
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_6))
1504
            (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_4 false))
1505
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_1))
1506
       )
1507
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_out events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_2)
1508
       (and (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_1 true))
1509
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_2))
1510
            (or (not (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.__events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_1 false))
1511
               (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_2 events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_1))
1512
       )
1513
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_out events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_2)
1514
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_out events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_2)
1515
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_Events7_out events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_Events7_1)
1516
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.events7_events7__state_in POINTEvents7_Events7)
1517
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.events7_events7__restart_in true)
1518
       )
1519
  (events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_step events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_Events7_1
1520
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_1
1521
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_1
1522
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_1
1523
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_1
1524
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.E
1525
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.events7_events7__restart_in
1526
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.events7_events7__state_in
1527
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_Events7_out
1528
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T1_out
1529
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.idEvents7_T2_out
1530
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT1_out
1531
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.sT2_out
1532
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1533
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1534
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1535
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1536
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1537
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1538
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
1539
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
1540
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x
1541
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
1542
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
1543
                                                                    events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x)
1544
))
1545

    
1546
; events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless
1547
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__restart_in Bool)
1548
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__state_in events7_events7__type)
1549
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__restart_act Bool)
1550
(declare-var events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__state_act events7_events7__type)
1551
(declare-rel events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless (Bool events7_events7__type Bool events7_events7__type))
1552
(rule (=> 
1553
  (and (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__state_act events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__state_in)
1554
       (= events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__restart_act events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__restart_in)
1555
       )
1556
  (events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__restart_in events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__state_in events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__restart_act events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless.events7_events7__state_act)
1557
))
1558

    
1559
; events7_events7__POINTEvents7_Events7_handler_until
1560
(declare-var events7_events7__POINTEvents7_Events7_handler_until.idEvents7_Events7_1 Int)
1561
(declare-var events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T1_1 Int)
1562
(declare-var events7_events7__POINTEvents7_Events7_handler_until.sT1_1 Real)
1563
(declare-var events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T2_1 Int)
1564
(declare-var events7_events7__POINTEvents7_Events7_handler_until.sT2_1 Real)
1565
(declare-var events7_events7__POINTEvents7_Events7_handler_until.events7_events7__restart_in Bool)
1566
(declare-var events7_events7__POINTEvents7_Events7_handler_until.events7_events7__state_in events7_events7__type)
1567
(declare-var events7_events7__POINTEvents7_Events7_handler_until.idEvents7_Events7_out Int)
1568
(declare-var events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T1_out Int)
1569
(declare-var events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T2_out Int)
1570
(declare-var events7_events7__POINTEvents7_Events7_handler_until.sT1_out Real)
1571
(declare-var events7_events7__POINTEvents7_Events7_handler_until.sT2_out Real)
1572
(declare-rel events7_events7__POINTEvents7_Events7_handler_until (Int Int Real Int Real Bool events7_events7__type Int Int Int Real Real))
1573
(rule (=> 
1574
  (and (= events7_events7__POINTEvents7_Events7_handler_until.sT2_out events7_events7__POINTEvents7_Events7_handler_until.sT2_1)
1575
       (= events7_events7__POINTEvents7_Events7_handler_until.sT1_out events7_events7__POINTEvents7_Events7_handler_until.sT1_1)
1576
       (= events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T2_out events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T2_1)
1577
       (= events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T1_out events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T1_1)
1578
       (= events7_events7__POINTEvents7_Events7_handler_until.idEvents7_Events7_out events7_events7__POINTEvents7_Events7_handler_until.idEvents7_Events7_1)
1579
       (= events7_events7__POINTEvents7_Events7_handler_until.events7_events7__state_in POINTEvents7_Events7)
1580
       (= events7_events7__POINTEvents7_Events7_handler_until.events7_events7__restart_in false)
1581
       )
1582
  (events7_events7__POINTEvents7_Events7_handler_until events7_events7__POINTEvents7_Events7_handler_until.idEvents7_Events7_1 events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T1_1 events7_events7__POINTEvents7_Events7_handler_until.sT1_1 events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T2_1 events7_events7__POINTEvents7_Events7_handler_until.sT2_1 events7_events7__POINTEvents7_Events7_handler_until.events7_events7__restart_in events7_events7__POINTEvents7_Events7_handler_until.events7_events7__state_in events7_events7__POINTEvents7_Events7_handler_until.idEvents7_Events7_out events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T1_out events7_events7__POINTEvents7_Events7_handler_until.idEvents7_T2_out events7_events7__POINTEvents7_Events7_handler_until.sT1_out events7_events7__POINTEvents7_Events7_handler_until.sT2_out)
1583
))
1584

    
1585
; events7_events7__POINTEvents7_Events7_unless
1586
(declare-var events7_events7__POINTEvents7_Events7_unless.events7_events7__restart_in Bool)
1587
(declare-var events7_events7__POINTEvents7_Events7_unless.events7_events7__state_in events7_events7__type)
1588
(declare-var events7_events7__POINTEvents7_Events7_unless.idEvents7_Events7_1 Int)
1589
(declare-var events7_events7__POINTEvents7_Events7_unless.events7_events7__restart_act Bool)
1590
(declare-var events7_events7__POINTEvents7_Events7_unless.events7_events7__state_act events7_events7__type)
1591
(declare-var events7_events7__POINTEvents7_Events7_unless.__events7_events7__POINTEvents7_Events7_unless_1 Bool)
1592
(declare-rel events7_events7__POINTEvents7_Events7_unless (Bool events7_events7__type Int Bool events7_events7__type))
1593
(rule (=> 
1594
  (and (= events7_events7__POINTEvents7_Events7_unless.__events7_events7__POINTEvents7_Events7_unless_1 (= events7_events7__POINTEvents7_Events7_unless.idEvents7_Events7_1 0))
1595
       (and (or (not (= events7_events7__POINTEvents7_Events7_unless.__events7_events7__POINTEvents7_Events7_unless_1 false))
1596
               (and (= events7_events7__POINTEvents7_Events7_unless.events7_events7__state_act EVENTS7_EVENTS7_PARALLEL_IDL)
1597
                    (= events7_events7__POINTEvents7_Events7_unless.events7_events7__restart_act true)
1598
                    ))
1599
            (or (not (= events7_events7__POINTEvents7_Events7_unless.__events7_events7__POINTEvents7_Events7_unless_1 true))
1600
               (and (= events7_events7__POINTEvents7_Events7_unless.events7_events7__state_act EVENTS7_EVENTS7_PARALLEL_ENTRY)
1601
                    (= events7_events7__POINTEvents7_Events7_unless.events7_events7__restart_act true)
1602
                    ))
1603
       )
1604
       )
1605
  (events7_events7__POINTEvents7_Events7_unless events7_events7__POINTEvents7_Events7_unless.events7_events7__restart_in events7_events7__POINTEvents7_Events7_unless.events7_events7__state_in events7_events7__POINTEvents7_Events7_unless.idEvents7_Events7_1 events7_events7__POINTEvents7_Events7_unless.events7_events7__restart_act events7_events7__POINTEvents7_Events7_unless.events7_events7__state_act)
1606
))
1607

    
1608
; Events7_Events7_node
1609
(declare-var Events7_Events7_node.idEvents7_Events7_1 Int)
1610
(declare-var Events7_Events7_node.idEvents7_T1_1 Int)
1611
(declare-var Events7_Events7_node.sT1_1 Real)
1612
(declare-var Events7_Events7_node.idEvents7_T2_1 Int)
1613
(declare-var Events7_Events7_node.sT2_1 Real)
1614
(declare-var Events7_Events7_node.E Bool)
1615
(declare-var Events7_Events7_node.idEvents7_Events7 Int)
1616
(declare-var Events7_Events7_node.idEvents7_T1 Int)
1617
(declare-var Events7_Events7_node.sT1 Real)
1618
(declare-var Events7_Events7_node.idEvents7_T2 Int)
1619
(declare-var Events7_Events7_node.sT2 Real)
1620
(declare-var Events7_Events7_node.__Events7_Events7_node_29_c Bool)
1621
(declare-var Events7_Events7_node.__Events7_Events7_node_30_c events7_events7__type)
1622
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c Bool)
1623
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c events7_t2__type)
1624
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c Bool)
1625
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c Bool)
1626
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c events7_t1__type)
1627
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c Bool)
1628
(declare-var Events7_Events7_node.ni_5._arrow._first_c Bool)
1629
(declare-var Events7_Events7_node.__Events7_Events7_node_29_m Bool)
1630
(declare-var Events7_Events7_node.__Events7_Events7_node_30_m events7_events7__type)
1631
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Bool)
1632
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m events7_t2__type)
1633
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Bool)
1634
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Bool)
1635
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m events7_t1__type)
1636
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Bool)
1637
(declare-var Events7_Events7_node.ni_5._arrow._first_m Bool)
1638
(declare-var Events7_Events7_node.__Events7_Events7_node_29_x Bool)
1639
(declare-var Events7_Events7_node.__Events7_Events7_node_30_x events7_events7__type)
1640
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x Bool)
1641
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x events7_t2__type)
1642
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x Bool)
1643
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x Bool)
1644
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x events7_t1__type)
1645
(declare-var Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x Bool)
1646
(declare-var Events7_Events7_node.ni_5._arrow._first_x Bool)
1647
(declare-var Events7_Events7_node.__Events7_Events7_node_1 Bool)
1648
(declare-var Events7_Events7_node.__Events7_Events7_node_10 Int)
1649
(declare-var Events7_Events7_node.__Events7_Events7_node_11 Int)
1650
(declare-var Events7_Events7_node.__Events7_Events7_node_12 Real)
1651
(declare-var Events7_Events7_node.__Events7_Events7_node_13 Real)
1652
(declare-var Events7_Events7_node.__Events7_Events7_node_14 Bool)
1653
(declare-var Events7_Events7_node.__Events7_Events7_node_15 events7_events7__type)
1654
(declare-var Events7_Events7_node.__Events7_Events7_node_16 Int)
1655
(declare-var Events7_Events7_node.__Events7_Events7_node_17 Int)
1656
(declare-var Events7_Events7_node.__Events7_Events7_node_18 Int)
1657
(declare-var Events7_Events7_node.__Events7_Events7_node_19 Real)
1658
(declare-var Events7_Events7_node.__Events7_Events7_node_2 events7_events7__type)
1659
(declare-var Events7_Events7_node.__Events7_Events7_node_20 Real)
1660
(declare-var Events7_Events7_node.__Events7_Events7_node_21 Bool)
1661
(declare-var Events7_Events7_node.__Events7_Events7_node_22 events7_events7__type)
1662
(declare-var Events7_Events7_node.__Events7_Events7_node_23 Int)
1663
(declare-var Events7_Events7_node.__Events7_Events7_node_24 Int)
1664
(declare-var Events7_Events7_node.__Events7_Events7_node_25 Int)
1665
(declare-var Events7_Events7_node.__Events7_Events7_node_26 Real)
1666
(declare-var Events7_Events7_node.__Events7_Events7_node_27 Real)
1667
(declare-var Events7_Events7_node.__Events7_Events7_node_28 Bool)
1668
(declare-var Events7_Events7_node.__Events7_Events7_node_3 Bool)
1669
(declare-var Events7_Events7_node.__Events7_Events7_node_4 events7_events7__type)
1670
(declare-var Events7_Events7_node.__Events7_Events7_node_5 Bool)
1671
(declare-var Events7_Events7_node.__Events7_Events7_node_6 events7_events7__type)
1672
(declare-var Events7_Events7_node.__Events7_Events7_node_7 Bool)
1673
(declare-var Events7_Events7_node.__Events7_Events7_node_8 events7_events7__type)
1674
(declare-var Events7_Events7_node.__Events7_Events7_node_9 Int)
1675
(declare-var Events7_Events7_node.events7_events7__next_restart_in Bool)
1676
(declare-var Events7_Events7_node.events7_events7__next_state_in events7_events7__type)
1677
(declare-var Events7_Events7_node.events7_events7__restart_act Bool)
1678
(declare-var Events7_Events7_node.events7_events7__restart_in Bool)
1679
(declare-var Events7_Events7_node.events7_events7__state_act events7_events7__type)
1680
(declare-var Events7_Events7_node.events7_events7__state_in events7_events7__type)
1681
(declare-rel Events7_Events7_node_reset (Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool))
1682
(declare-rel Events7_Events7_node_step (Int Int Real Int Real Bool Int Int Real Int Real Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool))
1683

    
1684
(rule (=> 
1685
  (and 
1686
       (= Events7_Events7_node.__Events7_Events7_node_29_m Events7_Events7_node.__Events7_Events7_node_29_c)
1687
       (= Events7_Events7_node.__Events7_Events7_node_30_m Events7_Events7_node.__Events7_Events7_node_30_c)
1688
       (= Events7_Events7_node.ni_5._arrow._first_m true)
1689
       (events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_reset 
1690
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1691
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1692
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1693
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1694
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1695
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1696
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1697
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1698
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
1699
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1700
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1701
       Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m)
1702
  )
1703
  (Events7_Events7_node_reset Events7_Events7_node.__Events7_Events7_node_29_c
1704
                              Events7_Events7_node.__Events7_Events7_node_30_c
1705
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1706
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1707
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1708
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1709
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1710
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1711
                              Events7_Events7_node.ni_5._arrow._first_c
1712
                              Events7_Events7_node.__Events7_Events7_node_29_m
1713
                              Events7_Events7_node.__Events7_Events7_node_30_m
1714
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1715
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1716
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
1717
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1718
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1719
                              Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
1720
                              Events7_Events7_node.ni_5._arrow._first_m)
1721
))
1722

    
1723
(rule (=> 
1724
  (and (= Events7_Events7_node.ni_5._arrow._first_m Events7_Events7_node.ni_5._arrow._first_c)
1725
       (and (= Events7_Events7_node.__Events7_Events7_node_28 (ite Events7_Events7_node.ni_5._arrow._first_m true false))
1726
            (= Events7_Events7_node.ni_5._arrow._first_x false))
1727
       (and (or (not (= Events7_Events7_node.__Events7_Events7_node_28 false))
1728
               (and (= Events7_Events7_node.events7_events7__state_in Events7_Events7_node.__Events7_Events7_node_30_c)
1729
                    (= Events7_Events7_node.events7_events7__restart_in Events7_Events7_node.__Events7_Events7_node_29_c)
1730
                    ))
1731
            (or (not (= Events7_Events7_node.__Events7_Events7_node_28 true))
1732
               (and (= Events7_Events7_node.events7_events7__state_in POINTEvents7_Events7)
1733
                    (= Events7_Events7_node.events7_events7__restart_in false)
1734
                    ))
1735
       )
1736
       (and (or (not (= Events7_Events7_node.events7_events7__state_in EVENTS7_EVENTS7_PARALLEL_ENTRY))
1737
               (and (events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_unless 
1738
                    Events7_Events7_node.events7_events7__restart_in
1739
                    Events7_Events7_node.events7_events7__state_in
1740
                    Events7_Events7_node.__Events7_Events7_node_3
1741
                    Events7_Events7_node.__Events7_Events7_node_4)
1742
                    (= Events7_Events7_node.events7_events7__state_act Events7_Events7_node.__Events7_Events7_node_4)
1743
                    (= Events7_Events7_node.events7_events7__restart_act Events7_Events7_node.__Events7_Events7_node_3)
1744
                    ))
1745
            (or (not (= Events7_Events7_node.events7_events7__state_in EVENTS7_EVENTS7_PARALLEL_IDL))
1746
               (and (events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_unless 
1747
                    Events7_Events7_node.events7_events7__restart_in
1748
                    Events7_Events7_node.events7_events7__state_in
1749
                    Events7_Events7_node.__Events7_Events7_node_1
1750
                    Events7_Events7_node.__Events7_Events7_node_2)
1751
                    (= Events7_Events7_node.events7_events7__state_act Events7_Events7_node.__Events7_Events7_node_2)
1752
                    (= Events7_Events7_node.events7_events7__restart_act Events7_Events7_node.__Events7_Events7_node_1)
1753
                    ))
1754
            (or (not (= Events7_Events7_node.events7_events7__state_in POINTEvents7_Events7))
1755
               (and (events7_events7__POINTEvents7_Events7_unless Events7_Events7_node.events7_events7__restart_in
1756
                                                                  Events7_Events7_node.events7_events7__state_in
1757
                                                                  Events7_Events7_node.idEvents7_Events7_1
1758
                                                                  Events7_Events7_node.__Events7_Events7_node_5
1759
                                                                  Events7_Events7_node.__Events7_Events7_node_6)
1760
                    (= Events7_Events7_node.events7_events7__state_act Events7_Events7_node.__Events7_Events7_node_6)
1761
                    (= Events7_Events7_node.events7_events7__restart_act Events7_Events7_node.__Events7_Events7_node_5)
1762
                    ))
1763
       )
1764
       (and (or (not (= Events7_Events7_node.events7_events7__state_act EVENTS7_EVENTS7_PARALLEL_ENTRY))
1765
               (and (events7_events7__EVENTS7_EVENTS7_PARALLEL_ENTRY_handler_until 
1766
                    Events7_Events7_node.idEvents7_Events7_1
1767
                    Events7_Events7_node.idEvents7_T1_1
1768
                    Events7_Events7_node.sT1_1
1769
                    Events7_Events7_node.idEvents7_T2_1
1770
                    Events7_Events7_node.sT2_1
1771
                    Events7_Events7_node.__Events7_Events7_node_14
1772
                    Events7_Events7_node.__Events7_Events7_node_15
1773
                    Events7_Events7_node.__Events7_Events7_node_16
1774
                    Events7_Events7_node.__Events7_Events7_node_17
1775
                    Events7_Events7_node.__Events7_Events7_node_18
1776
                    Events7_Events7_node.__Events7_Events7_node_19
1777
                    Events7_Events7_node.__Events7_Events7_node_20)
1778
                    (= Events7_Events7_node.sT2 Events7_Events7_node.__Events7_Events7_node_20)
1779
                    (= Events7_Events7_node.sT1 Events7_Events7_node.__Events7_Events7_node_19)
1780
                    (= Events7_Events7_node.idEvents7_T2 Events7_Events7_node.__Events7_Events7_node_18)
1781
                    (= Events7_Events7_node.idEvents7_T1 Events7_Events7_node.__Events7_Events7_node_17)
1782
                    (= Events7_Events7_node.idEvents7_Events7 Events7_Events7_node.__Events7_Events7_node_16)
1783
                    (= Events7_Events7_node.events7_events7__next_state_in Events7_Events7_node.__Events7_Events7_node_15)
1784
                    (= Events7_Events7_node.events7_events7__next_restart_in Events7_Events7_node.__Events7_Events7_node_14)
1785
                    ))
1786
            (or (not (= Events7_Events7_node.events7_events7__state_act EVENTS7_EVENTS7_PARALLEL_IDL))
1787
               (and (and (or (not (= Events7_Events7_node.events7_events7__restart_act true))
1788
                            (events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_reset 
1789
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1790
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1791
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1792
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1793
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1794
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1795
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1796
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1797
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
1798
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1799
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1800
                            Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m))
1801
                         (or (not (= Events7_Events7_node.events7_events7__restart_act false))
1802
                            (and (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c)
1803
                                 (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c)
1804
                                 (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c)
1805
                                 (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c)
1806
                                 (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c)
1807
                                 (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c)
1808
                                 )
1809
                            )
1810
                    )
1811
                    (and (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c)
1812
                         (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c)
1813
                         (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c)
1814
                         (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c)
1815
                         (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c)
1816
                         (= Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c)
1817
                         )
1818
                    (events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until_step 
1819
                    Events7_Events7_node.idEvents7_Events7_1
1820
                    Events7_Events7_node.idEvents7_T1_1
1821
                    Events7_Events7_node.sT1_1
1822
                    Events7_Events7_node.idEvents7_T2_1
1823
                    Events7_Events7_node.sT2_1
1824
                    Events7_Events7_node.E
1825
                    Events7_Events7_node.__Events7_Events7_node_7
1826
                    Events7_Events7_node.__Events7_Events7_node_8
1827
                    Events7_Events7_node.__Events7_Events7_node_9
1828
                    Events7_Events7_node.__Events7_Events7_node_10
1829
                    Events7_Events7_node.__Events7_Events7_node_11
1830
                    Events7_Events7_node.__Events7_Events7_node_12
1831
                    Events7_Events7_node.__Events7_Events7_node_13
1832
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1833
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1834
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
1835
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1836
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1837
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
1838
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
1839
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
1840
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x
1841
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
1842
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
1843
                    Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x)
1844
                    (= Events7_Events7_node.sT2 Events7_Events7_node.__Events7_Events7_node_13)
1845
                    (= Events7_Events7_node.sT1 Events7_Events7_node.__Events7_Events7_node_12)
1846
                    (= Events7_Events7_node.idEvents7_T2 Events7_Events7_node.__Events7_Events7_node_11)
1847
                    (= Events7_Events7_node.idEvents7_T1 Events7_Events7_node.__Events7_Events7_node_10)
1848
                    (= Events7_Events7_node.idEvents7_Events7 Events7_Events7_node.__Events7_Events7_node_9)
1849
                    (= Events7_Events7_node.events7_events7__next_state_in Events7_Events7_node.__Events7_Events7_node_8)
1850
                    (= Events7_Events7_node.events7_events7__next_restart_in Events7_Events7_node.__Events7_Events7_node_7)
1851
                    ))
1852
            (or (not (= Events7_Events7_node.events7_events7__state_act POINTEvents7_Events7))
1853
               (and (events7_events7__POINTEvents7_Events7_handler_until 
1854
                    Events7_Events7_node.idEvents7_Events7_1
1855
                    Events7_Events7_node.idEvents7_T1_1
1856
                    Events7_Events7_node.sT1_1
1857
                    Events7_Events7_node.idEvents7_T2_1
1858
                    Events7_Events7_node.sT2_1
1859
                    Events7_Events7_node.__Events7_Events7_node_21
1860
                    Events7_Events7_node.__Events7_Events7_node_22
1861
                    Events7_Events7_node.__Events7_Events7_node_23
1862
                    Events7_Events7_node.__Events7_Events7_node_24
1863
                    Events7_Events7_node.__Events7_Events7_node_25
1864
                    Events7_Events7_node.__Events7_Events7_node_26
1865
                    Events7_Events7_node.__Events7_Events7_node_27)
1866
                    (= Events7_Events7_node.sT2 Events7_Events7_node.__Events7_Events7_node_27)
1867
                    (= Events7_Events7_node.sT1 Events7_Events7_node.__Events7_Events7_node_26)
1868
                    (= Events7_Events7_node.idEvents7_T2 Events7_Events7_node.__Events7_Events7_node_25)
1869
                    (= Events7_Events7_node.idEvents7_T1 Events7_Events7_node.__Events7_Events7_node_24)
1870
                    (= Events7_Events7_node.idEvents7_Events7 Events7_Events7_node.__Events7_Events7_node_23)
1871
                    (= Events7_Events7_node.events7_events7__next_state_in Events7_Events7_node.__Events7_Events7_node_22)
1872
                    (= Events7_Events7_node.events7_events7__next_restart_in Events7_Events7_node.__Events7_Events7_node_21)
1873
                    ))
1874
       )
1875
       (= Events7_Events7_node.__Events7_Events7_node_30_x Events7_Events7_node.events7_events7__next_state_in)
1876
       (= Events7_Events7_node.__Events7_Events7_node_29_x Events7_Events7_node.events7_events7__next_restart_in)
1877
       )
1878
  (Events7_Events7_node_step Events7_Events7_node.idEvents7_Events7_1
1879
                             Events7_Events7_node.idEvents7_T1_1
1880
                             Events7_Events7_node.sT1_1
1881
                             Events7_Events7_node.idEvents7_T2_1
1882
                             Events7_Events7_node.sT2_1
1883
                             Events7_Events7_node.E
1884
                             Events7_Events7_node.idEvents7_Events7
1885
                             Events7_Events7_node.idEvents7_T1
1886
                             Events7_Events7_node.sT1
1887
                             Events7_Events7_node.idEvents7_T2
1888
                             Events7_Events7_node.sT2
1889
                             Events7_Events7_node.__Events7_Events7_node_29_c
1890
                             Events7_Events7_node.__Events7_Events7_node_30_c
1891
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1892
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1893
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1894
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1895
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1896
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1897
                             Events7_Events7_node.ni_5._arrow._first_c
1898
                             Events7_Events7_node.__Events7_Events7_node_29_x
1899
                             Events7_Events7_node.__Events7_Events7_node_30_x
1900
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
1901
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
1902
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x
1903
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
1904
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
1905
                             Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x
1906
                             Events7_Events7_node.ni_5._arrow._first_x)
1907
))
1908

    
1909
; Events7_Events7
1910
(declare-var Events7_Events7.E Bool)
1911
(declare-var Events7_Events7.sT1 Real)
1912
(declare-var Events7_Events7.sT2 Real)
1913
(declare-var Events7_Events7.__Events7_Events7_10_c Real)
1914
(declare-var Events7_Events7.__Events7_Events7_11_c Real)
1915
(declare-var Events7_Events7.__Events7_Events7_7_c Int)
1916
(declare-var Events7_Events7.__Events7_Events7_8_c Int)
1917
(declare-var Events7_Events7.__Events7_Events7_9_c Int)
1918
(declare-var Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c Bool)
1919
(declare-var Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c events7_events7__type)
1920
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c Bool)
1921
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c events7_t2__type)
1922
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c Bool)
1923
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c Bool)
1924
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c events7_t1__type)
1925
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c Bool)
1926
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c Bool)
1927
(declare-var Events7_Events7.ni_3._arrow._first_c Bool)
1928
(declare-var Events7_Events7.__Events7_Events7_10_m Real)
1929
(declare-var Events7_Events7.__Events7_Events7_11_m Real)
1930
(declare-var Events7_Events7.__Events7_Events7_7_m Int)
1931
(declare-var Events7_Events7.__Events7_Events7_8_m Int)
1932
(declare-var Events7_Events7.__Events7_Events7_9_m Int)
1933
(declare-var Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m Bool)
1934
(declare-var Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m events7_events7__type)
1935
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Bool)
1936
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m events7_t2__type)
1937
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Bool)
1938
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Bool)
1939
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m events7_t1__type)
1940
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Bool)
1941
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m Bool)
1942
(declare-var Events7_Events7.ni_3._arrow._first_m Bool)
1943
(declare-var Events7_Events7.__Events7_Events7_10_x Real)
1944
(declare-var Events7_Events7.__Events7_Events7_11_x Real)
1945
(declare-var Events7_Events7.__Events7_Events7_7_x Int)
1946
(declare-var Events7_Events7.__Events7_Events7_8_x Int)
1947
(declare-var Events7_Events7.__Events7_Events7_9_x Int)
1948
(declare-var Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_x Bool)
1949
(declare-var Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_x events7_events7__type)
1950
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x Bool)
1951
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x events7_t2__type)
1952
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x Bool)
1953
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x Bool)
1954
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x events7_t1__type)
1955
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x Bool)
1956
(declare-var Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_x Bool)
1957
(declare-var Events7_Events7.ni_3._arrow._first_x Bool)
1958
(declare-var Events7_Events7.__Events7_Events7_1 Int)
1959
(declare-var Events7_Events7.__Events7_Events7_2 Int)
1960
(declare-var Events7_Events7.__Events7_Events7_3 Real)
1961
(declare-var Events7_Events7.__Events7_Events7_4 Int)
1962
(declare-var Events7_Events7.__Events7_Events7_5 Real)
1963
(declare-var Events7_Events7.__Events7_Events7_6 Bool)
1964
(declare-var Events7_Events7.idEvents7_Events7 Int)
1965
(declare-var Events7_Events7.idEvents7_Events7_1 Int)
1966
(declare-var Events7_Events7.idEvents7_T1 Int)
1967
(declare-var Events7_Events7.idEvents7_T1_1 Int)
1968
(declare-var Events7_Events7.idEvents7_T2 Int)
1969
(declare-var Events7_Events7.idEvents7_T2_1 Int)
1970
(declare-var Events7_Events7.sT1_1 Real)
1971
(declare-var Events7_Events7.sT2_1 Real)
1972
(declare-rel Events7_Events7_reset (Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool))
1973
(declare-rel Events7_Events7_step (Bool Real Real Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool))
1974

    
1975
(rule (=> 
1976
  (and 
1977
       (= Events7_Events7.__Events7_Events7_10_m Events7_Events7.__Events7_Events7_10_c)
1978
       (= Events7_Events7.__Events7_Events7_11_m Events7_Events7.__Events7_Events7_11_c)
1979
       (= Events7_Events7.__Events7_Events7_7_m Events7_Events7.__Events7_Events7_7_c)
1980
       (= Events7_Events7.__Events7_Events7_8_m Events7_Events7.__Events7_Events7_8_c)
1981
       (= Events7_Events7.__Events7_Events7_9_m Events7_Events7.__Events7_Events7_9_c)
1982
       (= Events7_Events7.ni_3._arrow._first_m true)
1983
       (Events7_Events7_node_reset Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c
1984
                                   Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c
1985
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
1986
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
1987
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
1988
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
1989
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
1990
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
1991
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c
1992
                                   Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m
1993
                                   Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m
1994
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
1995
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
1996
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
1997
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
1998
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
1999
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
2000
                                   Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m)
2001
  )
2002
  (Events7_Events7_reset Events7_Events7.__Events7_Events7_10_c
2003
                         Events7_Events7.__Events7_Events7_11_c
2004
                         Events7_Events7.__Events7_Events7_7_c
2005
                         Events7_Events7.__Events7_Events7_8_c
2006
                         Events7_Events7.__Events7_Events7_9_c
2007
                         Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c
2008
                         Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c
2009
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
2010
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
2011
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
2012
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
2013
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
2014
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
2015
                         Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c
2016
                         Events7_Events7.ni_3._arrow._first_c
2017
                         Events7_Events7.__Events7_Events7_10_m
2018
                         Events7_Events7.__Events7_Events7_11_m
2019
                         Events7_Events7.__Events7_Events7_7_m
2020
                         Events7_Events7.__Events7_Events7_8_m
2021
                         Events7_Events7.__Events7_Events7_9_m
2022
                         Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m
2023
                         Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m
2024
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
2025
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
2026
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
2027
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
2028
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
2029
                         Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
2030
                         Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m
2031
                         Events7_Events7.ni_3._arrow._first_m)
2032
))
2033

    
2034
(rule (=> 
2035
  (and (= Events7_Events7.ni_3._arrow._first_m Events7_Events7.ni_3._arrow._first_c)
2036
       (and (= Events7_Events7.__Events7_Events7_6 (ite Events7_Events7.ni_3._arrow._first_m true false))
2037
            (= Events7_Events7.ni_3._arrow._first_x false))
2038
       (and (or (not (= Events7_Events7.__Events7_Events7_6 false))
2039
               (and (= Events7_Events7.sT2_1 Events7_Events7.__Events7_Events7_10_c)
2040
                    (= Events7_Events7.sT1_1 Events7_Events7.__Events7_Events7_11_c)
2041
                    (= Events7_Events7.idEvents7_T2_1 Events7_Events7.__Events7_Events7_8_c)
2042
                    (= Events7_Events7.idEvents7_T1_1 Events7_Events7.__Events7_Events7_7_c)
2043
                    (= Events7_Events7.idEvents7_Events7_1 Events7_Events7.__Events7_Events7_9_c)
2044
                    ))
2045
            (or (not (= Events7_Events7.__Events7_Events7_6 true))
2046
               (and (= Events7_Events7.sT2_1 0.)
2047
                    (= Events7_Events7.sT1_1 0.)
2048
                    (= Events7_Events7.idEvents7_T2_1 0)
2049
                    (= Events7_Events7.idEvents7_T1_1 0)
2050
                    (= Events7_Events7.idEvents7_Events7_1 0)
2051
                    ))
2052
       )
2053
       (and (= Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c)
2054
            (= Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c)
2055
            (= Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c)
2056
            (= Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c)
2057
            (= Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c)
2058
            (= Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c)
2059
            (= Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c)
2060
            (= Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c)
2061
            (= Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c)
2062
            )
2063
       (Events7_Events7_node_step Events7_Events7.idEvents7_Events7_1
2064
                                  Events7_Events7.idEvents7_T1_1
2065
                                  Events7_Events7.sT1_1
2066
                                  Events7_Events7.idEvents7_T2_1
2067
                                  Events7_Events7.sT2_1
2068
                                  Events7_Events7.E
2069
                                  Events7_Events7.__Events7_Events7_1
2070
                                  Events7_Events7.__Events7_Events7_2
2071
                                  Events7_Events7.__Events7_Events7_3
2072
                                  Events7_Events7.__Events7_Events7_4
2073
                                  Events7_Events7.__Events7_Events7_5
2074
                                  Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m
2075
                                  Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m
2076
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
2077
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
2078
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
2079
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
2080
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
2081
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
2082
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m
2083
                                  Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_x
2084
                                  Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_x
2085
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
2086
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
2087
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x
2088
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
2089
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
2090
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x
2091
                                  Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_x)
2092
       (and (or (not (= Events7_Events7.E false))
2093
               (and (= Events7_Events7.sT2 Events7_Events7.sT2_1)
2094
                    (= Events7_Events7.sT1 Events7_Events7.sT1_1)
2095
                    (= Events7_Events7.idEvents7_T2 Events7_Events7.idEvents7_T2_1)
2096
                    (= Events7_Events7.idEvents7_T1 Events7_Events7.idEvents7_T1_1)
2097
                    (= Events7_Events7.idEvents7_Events7 Events7_Events7.idEvents7_Events7_1)
2098
                    ))
2099
            (or (not (= Events7_Events7.E true))
2100
               (and (= Events7_Events7.sT2 Events7_Events7.__Events7_Events7_5)
2101
                    (= Events7_Events7.sT1 Events7_Events7.__Events7_Events7_3)
2102
                    (= Events7_Events7.idEvents7_T2 Events7_Events7.__Events7_Events7_4)
2103
                    (= Events7_Events7.idEvents7_T1 Events7_Events7.__Events7_Events7_2)
2104
                    (= Events7_Events7.idEvents7_Events7 Events7_Events7.__Events7_Events7_1)
2105
                    ))
2106
       )
2107
       (= Events7_Events7.__Events7_Events7_9_x Events7_Events7.idEvents7_Events7)
2108
       (= Events7_Events7.__Events7_Events7_8_x Events7_Events7.idEvents7_T2)
2109
       (= Events7_Events7.__Events7_Events7_7_x Events7_Events7.idEvents7_T1)
2110
       (= Events7_Events7.__Events7_Events7_11_x Events7_Events7.sT1)
2111
       (= Events7_Events7.__Events7_Events7_10_x Events7_Events7.sT2)
2112
       )
2113
  (Events7_Events7_step Events7_Events7.E
2114
                        Events7_Events7.sT1
2115
                        Events7_Events7.sT2
2116
                        Events7_Events7.__Events7_Events7_10_c
2117
                        Events7_Events7.__Events7_Events7_11_c
2118
                        Events7_Events7.__Events7_Events7_7_c
2119
                        Events7_Events7.__Events7_Events7_8_c
2120
                        Events7_Events7.__Events7_Events7_9_c
2121
                        Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c
2122
                        Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c
2123
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
2124
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
2125
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
2126
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
2127
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
2128
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
2129
                        Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c
2130
                        Events7_Events7.ni_3._arrow._first_c
2131
                        Events7_Events7.__Events7_Events7_10_x
2132
                        Events7_Events7.__Events7_Events7_11_x
2133
                        Events7_Events7.__Events7_Events7_7_x
2134
                        Events7_Events7.__Events7_Events7_8_x
2135
                        Events7_Events7.__Events7_Events7_9_x
2136
                        Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_x
2137
                        Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_x
2138
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
2139
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
2140
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x
2141
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
2142
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
2143
                        Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x
2144
                        Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_x
2145
                        Events7_Events7.ni_3._arrow._first_x)
2146
))
2147

    
2148
; Events7_T1_ex
2149
(declare-var Events7_T1_ex.idEvents7_T1_1 Int)
2150
(declare-var Events7_T1_ex.idEvents7_Events7_1 Int)
2151
(declare-var Events7_T1_ex.isInner Bool)
2152
(declare-var Events7_T1_ex.idEvents7_T1 Int)
2153
(declare-var Events7_T1_ex.idEvents7_Events7 Int)
2154
(declare-var Events7_T1_ex.__Events7_T1_ex_2 Bool)
2155
(declare-var Events7_T1_ex.__Events7_T1_ex_3 Bool)
2156
(declare-var Events7_T1_ex.__Events7_T1_ex_4 Int)
2157
(declare-var Events7_T1_ex.__Events7_T1_ex_5 Int)
2158
(declare-var Events7_T1_ex.idEvents7_Events7_2 Int)
2159
(declare-var Events7_T1_ex.idEvents7_T1_2 Int)
2160
(declare-var Events7_T1_ex.idEvents7_T1_3 Int)
2161
(declare-var Events7_T1_ex.idEvents7_T1_4 Int)
2162
(declare-rel Events7_T1_ex (Int Int Bool Int Int))
2163
(rule (=> 
2164
  (and (T1_B_ex Events7_T1_ex.idEvents7_T1_1
2165
                false
2166
                Events7_T1_ex.__Events7_T1_ex_4)
2167
       (= Events7_T1_ex.__Events7_T1_ex_3 (= Events7_T1_ex.idEvents7_T1_1 677))
2168
       (and (or (not (= Events7_T1_ex.__Events7_T1_ex_3 true))
2169
               (= Events7_T1_ex.idEvents7_T1_3 Events7_T1_ex.__Events7_T1_ex_4))
2170
            (or (not (= Events7_T1_ex.__Events7_T1_ex_3 false))
2171
               (= Events7_T1_ex.idEvents7_T1_3 Events7_T1_ex.idEvents7_T1_1))
2172
       )
2173
       (T1_A_ex Events7_T1_ex.idEvents7_T1_1
2174
                false
2175
                Events7_T1_ex.__Events7_T1_ex_5)
2176
       (= Events7_T1_ex.__Events7_T1_ex_2 (= Events7_T1_ex.idEvents7_T1_1 676))
2177
       (and (or (not (= Events7_T1_ex.__Events7_T1_ex_2 false))
2178
               (and (= Events7_T1_ex.idEvents7_T1_2 Events7_T1_ex.idEvents7_T1_1)
2179
                    (and (or (not (= Events7_T1_ex.__Events7_T1_ex_3 true))
2180
                            (= Events7_T1_ex.idEvents7_T1_4 Events7_T1_ex.idEvents7_T1_3))
2181
                         (or (not (= Events7_T1_ex.__Events7_T1_ex_3 false))
2182
                            (= Events7_T1_ex.idEvents7_T1_4 Events7_T1_ex.idEvents7_T1_1))
2183
                    )
2184
                    ))
2185
            (or (not (= Events7_T1_ex.__Events7_T1_ex_2 true))
2186
               (and (= Events7_T1_ex.idEvents7_T1_2 Events7_T1_ex.__Events7_T1_ex_5)
2187
                    (= Events7_T1_ex.idEvents7_T1_4 Events7_T1_ex.idEvents7_T1_2)
2188
                    ))
2189
       )
2190
       (and (or (not (= (not Events7_T1_ex.isInner) true))
2191
               (= Events7_T1_ex.idEvents7_Events7_2 0))
2192
            (or (not (= (not Events7_T1_ex.isInner) false))
2193
               (= Events7_T1_ex.idEvents7_Events7_2 Events7_T1_ex.idEvents7_Events7_1))
2194
       )
2195
       (= Events7_T1_ex.idEvents7_T1 0)
2196
       (= Events7_T1_ex.idEvents7_Events7 Events7_T1_ex.idEvents7_Events7_1)
2197
       )
2198
  (Events7_T1_ex Events7_T1_ex.idEvents7_T1_1 Events7_T1_ex.idEvents7_Events7_1 Events7_T1_ex.isInner Events7_T1_ex.idEvents7_T1 Events7_T1_ex.idEvents7_Events7)
2199
))
2200

    
2201
; Events7
2202
(declare-var Events7.E_1_1 Real)
2203
(declare-var Events7.sT1_1_1 Real)
2204
(declare-var Events7.sT2_2_1 Real)
2205
(declare-var Events7.__Events7_2_c Real)
2206
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_10_c Real)
2207
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_11_c Real)
2208
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_7_c Int)
2209
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_8_c Int)
2210
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_9_c Int)
2211
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c Bool)
2212
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c events7_events7__type)
2213
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c Bool)
2214
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c events7_t2__type)
2215
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c Bool)
2216
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c Bool)
2217
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c events7_t1__type)
2218
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c Bool)
2219
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c Bool)
2220
(declare-var Events7.ni_0.Events7_Events7.ni_3._arrow._first_c Bool)
2221
(declare-var Events7.ni_1._arrow._first_c Bool)
2222
(declare-var Events7.__Events7_2_m Real)
2223
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_10_m Real)
2224
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_11_m Real)
2225
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_7_m Int)
2226
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_8_m Int)
2227
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_9_m Int)
2228
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m Bool)
2229
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m events7_events7__type)
2230
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Bool)
2231
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m events7_t2__type)
2232
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Bool)
2233
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Bool)
2234
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m events7_t1__type)
2235
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Bool)
2236
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m Bool)
2237
(declare-var Events7.ni_0.Events7_Events7.ni_3._arrow._first_m Bool)
2238
(declare-var Events7.ni_1._arrow._first_m Bool)
2239
(declare-var Events7.__Events7_2_x Real)
2240
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_10_x Real)
2241
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_11_x Real)
2242
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_7_x Int)
2243
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_8_x Int)
2244
(declare-var Events7.ni_0.Events7_Events7.__Events7_Events7_9_x Int)
2245
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_x Bool)
2246
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_x events7_events7__type)
2247
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x Bool)
2248
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x events7_t2__type)
2249
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x Bool)
2250
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x Bool)
2251
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x events7_t1__type)
2252
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x Bool)
2253
(declare-var Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_x Bool)
2254
(declare-var Events7.ni_0.Events7_Events7.ni_3._arrow._first_x Bool)
2255
(declare-var Events7.ni_1._arrow._first_x Bool)
2256
(declare-var Events7.Events7E_1_1_event Bool)
2257
(declare-var Events7.Events7_1_1 Real)
2258
(declare-var Events7.Events7_2_1 Real)
2259
(declare-var Events7.__Events7_1 Bool)
2260
(declare-var Events7.i_virtual_local Real)
2261
(declare-rel Events7_reset (Real Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool Bool Real Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool Bool))
2262
(declare-rel Events7_step (Real Real Real Real Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool Bool Real Real Real Int Int Int Bool events7_events7__type Bool events7_t2__type Bool Bool events7_t1__type Bool Bool Bool Bool))
2263

    
2264
(rule (=> 
2265
  (and 
2266
       (= Events7.__Events7_2_m Events7.__Events7_2_c)
2267
       (= Events7.ni_1._arrow._first_m true)
2268
       (Events7_Events7_reset Events7.ni_0.Events7_Events7.__Events7_Events7_10_c
2269
                              Events7.ni_0.Events7_Events7.__Events7_Events7_11_c
2270
                              Events7.ni_0.Events7_Events7.__Events7_Events7_7_c
2271
                              Events7.ni_0.Events7_Events7.__Events7_Events7_8_c
2272
                              Events7.ni_0.Events7_Events7.__Events7_Events7_9_c
2273
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c
2274
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c
2275
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
2276
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
2277
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
2278
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
2279
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
2280
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
2281
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c
2282
                              Events7.ni_0.Events7_Events7.ni_3._arrow._first_c
2283
                              Events7.ni_0.Events7_Events7.__Events7_Events7_10_m
2284
                              Events7.ni_0.Events7_Events7.__Events7_Events7_11_m
2285
                              Events7.ni_0.Events7_Events7.__Events7_Events7_7_m
2286
                              Events7.ni_0.Events7_Events7.__Events7_Events7_8_m
2287
                              Events7.ni_0.Events7_Events7.__Events7_Events7_9_m
2288
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m
2289
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m
2290
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
2291
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
2292
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
2293
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
2294
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
2295
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
2296
                              Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m
2297
                              Events7.ni_0.Events7_Events7.ni_3._arrow._first_m)
2298
  )
2299
  (Events7_reset Events7.__Events7_2_c
2300
                 Events7.ni_0.Events7_Events7.__Events7_Events7_10_c
2301
                 Events7.ni_0.Events7_Events7.__Events7_Events7_11_c
2302
                 Events7.ni_0.Events7_Events7.__Events7_Events7_7_c
2303
                 Events7.ni_0.Events7_Events7.__Events7_Events7_8_c
2304
                 Events7.ni_0.Events7_Events7.__Events7_Events7_9_c
2305
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c
2306
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c
2307
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
2308
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
2309
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
2310
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
2311
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
2312
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
2313
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c
2314
                 Events7.ni_0.Events7_Events7.ni_3._arrow._first_c
2315
                 Events7.ni_1._arrow._first_c
2316
                 Events7.__Events7_2_m
2317
                 Events7.ni_0.Events7_Events7.__Events7_Events7_10_m
2318
                 Events7.ni_0.Events7_Events7.__Events7_Events7_11_m
2319
                 Events7.ni_0.Events7_Events7.__Events7_Events7_7_m
2320
                 Events7.ni_0.Events7_Events7.__Events7_Events7_8_m
2321
                 Events7.ni_0.Events7_Events7.__Events7_Events7_9_m
2322
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m
2323
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m
2324
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
2325
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
2326
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
2327
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
2328
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
2329
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
2330
                 Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m
2331
                 Events7.ni_0.Events7_Events7.ni_3._arrow._first_m
2332
                 Events7.ni_1._arrow._first_m)
2333
))
2334

    
2335
(rule (=> 
2336
  (and (= Events7.ni_1._arrow._first_m Events7.ni_1._arrow._first_c)(and (= Events7.__Events7_1 (ite Events7.ni_1._arrow._first_m true false))
2337
                                                                    (= Events7.ni_1._arrow._first_x false))
2338
       (and (or (not (= Events7.__Events7_1 true))
2339
               (= Events7.Events7E_1_1_event false))
2340
            (or (not (= Events7.__Events7_1 false))
2341
               (= Events7.Events7E_1_1_event (or (and (> Events7.__Events7_2_c 0.) (<= Events7.E_1_1 0.)) (and (<= Events7.__Events7_2_c 0.) (> Events7.E_1_1 0.)))))
2342
       )
2343
       (and (= Events7.ni_0.Events7_Events7.__Events7_Events7_10_m Events7.ni_0.Events7_Events7.__Events7_Events7_10_c)
2344
            (= Events7.ni_0.Events7_Events7.__Events7_Events7_11_m Events7.ni_0.Events7_Events7.__Events7_Events7_11_c)
2345
            (= Events7.ni_0.Events7_Events7.__Events7_Events7_7_m Events7.ni_0.Events7_Events7.__Events7_Events7_7_c)
2346
            (= Events7.ni_0.Events7_Events7.__Events7_Events7_8_m Events7.ni_0.Events7_Events7.__Events7_Events7_8_c)
2347
            (= Events7.ni_0.Events7_Events7.__Events7_Events7_9_m Events7.ni_0.Events7_Events7.__Events7_Events7_9_c)
2348
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c)
2349
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c)
2350
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c)
2351
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c)
2352
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c)
2353
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c)
2354
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c)
2355
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c)
2356
            (= Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c)
2357
            (= Events7.ni_0.Events7_Events7.ni_3._arrow._first_m Events7.ni_0.Events7_Events7.ni_3._arrow._first_c)
2358
            )
2359
       (Events7_Events7_step Events7.Events7E_1_1_event
2360
                             Events7.Events7_1_1
2361
                             Events7.Events7_2_1
2362
                             Events7.ni_0.Events7_Events7.__Events7_Events7_10_m
2363
                             Events7.ni_0.Events7_Events7.__Events7_Events7_11_m
2364
                             Events7.ni_0.Events7_Events7.__Events7_Events7_7_m
2365
                             Events7.ni_0.Events7_Events7.__Events7_Events7_8_m
2366
                             Events7.ni_0.Events7_Events7.__Events7_Events7_9_m
2367
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_m
2368
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_m
2369
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_m
2370
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_m
2371
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_m
2372
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_m
2373
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_m
2374
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_m
2375
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_m
2376
                             Events7.ni_0.Events7_Events7.ni_3._arrow._first_m
2377
                             Events7.ni_0.Events7_Events7.__Events7_Events7_10_x
2378
                             Events7.ni_0.Events7_Events7.__Events7_Events7_11_x
2379
                             Events7.ni_0.Events7_Events7.__Events7_Events7_7_x
2380
                             Events7.ni_0.Events7_Events7.__Events7_Events7_8_x
2381
                             Events7.ni_0.Events7_Events7.__Events7_Events7_9_x
2382
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_x
2383
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_x
2384
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
2385
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
2386
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x
2387
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
2388
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
2389
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x
2390
                             Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_x
2391
                             Events7.ni_0.Events7_Events7.ni_3._arrow._first_x)
2392
       (= Events7.sT2_2_1 Events7.Events7_2_1)
2393
       (= Events7.sT1_1_1 Events7.Events7_1_1)
2394
       (and (or (not (= Events7.__Events7_1 true))
2395
               (= Events7.i_virtual_local 0.))
2396
            (or (not (= Events7.__Events7_1 false))
2397
               (= Events7.i_virtual_local 1.))
2398
       )
2399
       (= Events7.__Events7_2_x Events7.E_1_1)
2400
       )
2401
  (Events7_step Events7.E_1_1
2402
                Events7.sT1_1_1
2403
                Events7.sT2_2_1
2404
                Events7.__Events7_2_c
2405
                Events7.ni_0.Events7_Events7.__Events7_Events7_10_c
2406
                Events7.ni_0.Events7_Events7.__Events7_Events7_11_c
2407
                Events7.ni_0.Events7_Events7.__Events7_Events7_7_c
2408
                Events7.ni_0.Events7_Events7.__Events7_Events7_8_c
2409
                Events7.ni_0.Events7_Events7.__Events7_Events7_9_c
2410
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_c
2411
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_c
2412
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_c
2413
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_c
2414
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_c
2415
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_c
2416
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_c
2417
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_c
2418
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_c
2419
                Events7.ni_0.Events7_Events7.ni_3._arrow._first_c
2420
                Events7.ni_1._arrow._first_c
2421
                Events7.__Events7_2_x
2422
                Events7.ni_0.Events7_Events7.__Events7_Events7_10_x
2423
                Events7.ni_0.Events7_Events7.__Events7_Events7_11_x
2424
                Events7.ni_0.Events7_Events7.__Events7_Events7_7_x
2425
                Events7.ni_0.Events7_Events7.__Events7_Events7_8_x
2426
                Events7.ni_0.Events7_Events7.__Events7_Events7_9_x
2427
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_29_x
2428
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.__Events7_Events7_node_30_x
2429
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_38_x
2430
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.__Events7_T2_node_39_x
2431
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_6.Events7_T2_node.ni_8._arrow._first_x
2432
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_38_x
2433
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.__Events7_T1_node_39_x
2434
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_4.events7_events7__EVENTS7_EVENTS7_PARALLEL_IDL_handler_until.ni_7.Events7_T1_node.ni_9._arrow._first_x
2435
                Events7.ni_0.Events7_Events7.ni_2.Events7_Events7_node.ni_5._arrow._first_x
2436
                Events7.ni_0.Events7_Events7.ni_3._arrow._first_x
2437
                Events7.ni_1._arrow._first_x)
2438
))
2439

    
2440
; Events7_T2_ex
2441
(declare-var Events7_T2_ex.idEvents7_T2_1 Int)
2442
(declare-var Events7_T2_ex.idEvents7_Events7_1 Int)
2443
(declare-var Events7_T2_ex.isInner Bool)
2444
(declare-var Events7_T2_ex.idEvents7_T2 Int)
2445
(declare-var Events7_T2_ex.idEvents7_Events7 Int)
2446
(declare-var Events7_T2_ex.__Events7_T2_ex_2 Bool)
2447
(declare-var Events7_T2_ex.__Events7_T2_ex_3 Bool)
2448
(declare-var Events7_T2_ex.__Events7_T2_ex_4 Int)
2449
(declare-var Events7_T2_ex.__Events7_T2_ex_5 Int)
2450
(declare-var Events7_T2_ex.idEvents7_Events7_2 Int)
2451
(declare-var Events7_T2_ex.idEvents7_T2_2 Int)
2452
(declare-var Events7_T2_ex.idEvents7_T2_3 Int)
2453
(declare-var Events7_T2_ex.idEvents7_T2_4 Int)
2454
(declare-rel Events7_T2_ex (Int Int Bool Int Int))
2455
(rule (=> 
2456
  (and (T2_D_ex Events7_T2_ex.idEvents7_T2_1
2457
                false
2458
                Events7_T2_ex.__Events7_T2_ex_4)
2459
       (= Events7_T2_ex.__Events7_T2_ex_3 (= Events7_T2_ex.idEvents7_T2_1 680))
2460
       (and (or (not (= Events7_T2_ex.__Events7_T2_ex_3 true))
2461
               (= Events7_T2_ex.idEvents7_T2_3 Events7_T2_ex.__Events7_T2_ex_4))
2462
            (or (not (= Events7_T2_ex.__Events7_T2_ex_3 false))
2463
               (= Events7_T2_ex.idEvents7_T2_3 Events7_T2_ex.idEvents7_T2_1))
2464
       )
2465
       (T2_C_ex Events7_T2_ex.idEvents7_T2_1
2466
                false
2467
                Events7_T2_ex.__Events7_T2_ex_5)
2468
       (= Events7_T2_ex.__Events7_T2_ex_2 (= Events7_T2_ex.idEvents7_T2_1 679))
2469
       (and (or (not (= Events7_T2_ex.__Events7_T2_ex_2 false))
2470
               (and (= Events7_T2_ex.idEvents7_T2_2 Events7_T2_ex.idEvents7_T2_1)
2471
                    (and (or (not (= Events7_T2_ex.__Events7_T2_ex_3 true))
2472
                            (= Events7_T2_ex.idEvents7_T2_4 Events7_T2_ex.idEvents7_T2_3))
2473
                         (or (not (= Events7_T2_ex.__Events7_T2_ex_3 false))
2474
                            (= Events7_T2_ex.idEvents7_T2_4 Events7_T2_ex.idEvents7_T2_1))
2475
                    )
2476
                    ))
2477
            (or (not (= Events7_T2_ex.__Events7_T2_ex_2 true))
2478
               (and (= Events7_T2_ex.idEvents7_T2_2 Events7_T2_ex.__Events7_T2_ex_5)
2479
                    (= Events7_T2_ex.idEvents7_T2_4 Events7_T2_ex.idEvents7_T2_2)
2480
                    ))
2481
       )
2482
       (and (or (not (= (not Events7_T2_ex.isInner) true))
2483
               (= Events7_T2_ex.idEvents7_Events7_2 0))
2484
            (or (not (= (not Events7_T2_ex.isInner) false))
2485
               (= Events7_T2_ex.idEvents7_Events7_2 Events7_T2_ex.idEvents7_Events7_1))
2486
       )
2487
       (= Events7_T2_ex.idEvents7_T2 0)
2488
       (= Events7_T2_ex.idEvents7_Events7 Events7_T2_ex.idEvents7_Events7_1)
2489
       )
2490
  (Events7_T2_ex Events7_T2_ex.idEvents7_T2_1 Events7_T2_ex.idEvents7_Events7_1 Events7_T2_ex.isInner Events7_T2_ex.idEvents7_T2 Events7_T2_ex.idEvents7_Events7)
2491
))
2492