Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Temporal1 / Temporal1.smt2 @ eb639349

History | View | Annotate | Download (94.1 KB)

1
(declare-datatypes () ((temporal1_temporal1__type POINTTemporal1_Temporal1 POINT__TO__TEMPORAL1_A_1 TEMPORAL1_A__TO__TEMPORAL1_B_1 TEMPORAL1_B__TO__TEMPORAL1_A_1 TEMPORAL1_A_IDL TEMPORAL1_B_IDL)));
2

    
3
; Temporal1_A_en
4
(declare-var Temporal1_A_en.idTemporal1_Temporal1_1 Int)
5
(declare-var Temporal1_A_en.x_1 Int)
6
(declare-var Temporal1_A_en.isInner Bool)
7
(declare-var Temporal1_A_en.idTemporal1_Temporal1 Int)
8
(declare-var Temporal1_A_en.x Int)
9
(declare-var Temporal1_A_en.x_2 Int)
10
(declare-rel Temporal1_A_en (Int Int Bool Int Int))
11
(rule (=> 
12
  (and (and (or (not (= (not Temporal1_A_en.isInner) true))
13
               (= Temporal1_A_en.x_2 (+ Temporal1_A_en.x_1 1)))
14
            (or (not (= (not Temporal1_A_en.isInner) false))
15
               (= Temporal1_A_en.x_2 Temporal1_A_en.x_1))
16
       )
17
       (= Temporal1_A_en.x Temporal1_A_en.x_2)
18
       (= Temporal1_A_en.idTemporal1_Temporal1 122)
19
       )
20
  (Temporal1_A_en Temporal1_A_en.idTemporal1_Temporal1_1 Temporal1_A_en.x_1 Temporal1_A_en.isInner Temporal1_A_en.idTemporal1_Temporal1 Temporal1_A_en.x)
21
))
22

    
23
; Temporal1_A_ex
24
(declare-var Temporal1_A_ex.idTemporal1_Temporal1_1 Int)
25
(declare-var Temporal1_A_ex.isInner Bool)
26
(declare-var Temporal1_A_ex.idTemporal1_Temporal1 Int)
27
(declare-var Temporal1_A_ex.idTemporal1_Temporal1_2 Int)
28
(declare-rel Temporal1_A_ex (Int Bool Int))
29
(rule (=> 
30
  (and (and (or (not (= (not Temporal1_A_ex.isInner) true))
31
               (= Temporal1_A_ex.idTemporal1_Temporal1_2 0))
32
            (or (not (= (not Temporal1_A_ex.isInner) false))
33
               (= Temporal1_A_ex.idTemporal1_Temporal1_2 Temporal1_A_ex.idTemporal1_Temporal1_1))
34
       )
35
       (= Temporal1_A_ex.idTemporal1_Temporal1 Temporal1_A_ex.idTemporal1_Temporal1_1)
36
       )
37
  (Temporal1_A_ex Temporal1_A_ex.idTemporal1_Temporal1_1 Temporal1_A_ex.isInner Temporal1_A_ex.idTemporal1_Temporal1)
38
))
39

    
40
; Temporal1_B_en
41
(declare-var Temporal1_B_en.idTemporal1_Temporal1_1 Int)
42
(declare-var Temporal1_B_en.x_1 Int)
43
(declare-var Temporal1_B_en.isInner Bool)
44
(declare-var Temporal1_B_en.idTemporal1_Temporal1 Int)
45
(declare-var Temporal1_B_en.x Int)
46
(declare-var Temporal1_B_en.x_2 Int)
47
(declare-rel Temporal1_B_en (Int Int Bool Int Int))
48
(rule (=> 
49
  (and (and (or (not (= (not Temporal1_B_en.isInner) true))
50
               (= Temporal1_B_en.x_2 (+ Temporal1_B_en.x_1 1)))
51
            (or (not (= (not Temporal1_B_en.isInner) false))
52
               (= Temporal1_B_en.x_2 Temporal1_B_en.x_1))
53
       )
54
       (= Temporal1_B_en.x Temporal1_B_en.x_2)
55
       (= Temporal1_B_en.idTemporal1_Temporal1 123)
56
       )
57
  (Temporal1_B_en Temporal1_B_en.idTemporal1_Temporal1_1 Temporal1_B_en.x_1 Temporal1_B_en.isInner Temporal1_B_en.idTemporal1_Temporal1 Temporal1_B_en.x)
58
))
59

    
60
; Temporal1_B_ex
61
(declare-var Temporal1_B_ex.idTemporal1_Temporal1_1 Int)
62
(declare-var Temporal1_B_ex.isInner Bool)
63
(declare-var Temporal1_B_ex.idTemporal1_Temporal1 Int)
64
(declare-var Temporal1_B_ex.idTemporal1_Temporal1_2 Int)
65
(declare-rel Temporal1_B_ex (Int Bool Int))
66
(rule (=> 
67
  (and (and (or (not (= (not Temporal1_B_ex.isInner) true))
68
               (= Temporal1_B_ex.idTemporal1_Temporal1_2 0))
69
            (or (not (= (not Temporal1_B_ex.isInner) false))
70
               (= Temporal1_B_ex.idTemporal1_Temporal1_2 Temporal1_B_ex.idTemporal1_Temporal1_1))
71
       )
72
       (= Temporal1_B_ex.idTemporal1_Temporal1 Temporal1_B_ex.idTemporal1_Temporal1_1)
73
       )
74
  (Temporal1_B_ex Temporal1_B_ex.idTemporal1_Temporal1_1 Temporal1_B_ex.isInner Temporal1_B_ex.idTemporal1_Temporal1)
75
))
76

    
77
; after
78
(declare-var after.n Int)
79
(declare-var after.E Bool)
80
(declare-var after.id Int)
81
(declare-var after.Y Bool)
82
(declare-var after.__after_2_c Int)
83
(declare-var after.__after_4_c Int)
84
(declare-var after.ni_7._arrow._first_c Bool)
85
(declare-var after.__after_2_m Int)
86
(declare-var after.__after_4_m Int)
87
(declare-var after.ni_7._arrow._first_m Bool)
88
(declare-var after.__after_2_x Int)
89
(declare-var after.__after_4_x Int)
90
(declare-var after.ni_7._arrow._first_x Bool)
91
(declare-var after.__after_1 Bool)
92
(declare-var after.__after_3 Bool)
93
(declare-var after.count Int)
94
(declare-rel after_reset (Int Int Bool Int Int Bool))
95
(declare-rel after_step (Int Bool Int Bool Int Int Bool Int Int Bool))
96

    
97
(rule (=> 
98
  (and 
99
       (= after.__after_2_m after.__after_2_c)
100
       (= after.__after_4_m after.__after_4_c)
101
       (= after.ni_7._arrow._first_m true)
102
  )
103
  (after_reset after.__after_2_c
104
               after.__after_4_c
105
               after.ni_7._arrow._first_c
106
               after.__after_2_m
107
               after.__after_4_m
108
               after.ni_7._arrow._first_m)
109
))
110

    
111
(rule (=> 
112
  (and (= after.__after_3 (not (= after.__after_2_c after.id)))
113
       (= after.ni_7._arrow._first_m after.ni_7._arrow._first_c)(and (= after.__after_1 (ite after.ni_7._arrow._first_m true false))
114
                                                                    (= after.ni_7._arrow._first_x false))
115
       (and (or (not (= after.__after_1 true))
116
               (= after.count 0))
117
            (or (not (= after.__after_1 false))
118
               (and (or (not (= after.__after_3 true))
119
                       (and (or (not (= after.E true))
120
                               (= after.count 1))
121
                            (or (not (= after.E false))
122
                               (= after.count 0))
123
                       ))
124
                    (or (not (= after.__after_3 false))
125
                       (and (or (not (= after.E true))
126
                               (= after.count (+ after.__after_4_c 1)))
127
                            (or (not (= after.E false))
128
                               (= after.count after.__after_4_c))
129
                       ))
130
               ))
131
       )
132
       (= after.__after_4_x after.count)
133
       (= after.__after_2_x after.id)
134
       (= after.Y (>= after.count after.n))
135
       )
136
  (after_step after.n
137
              after.E
138
              after.id
139
              after.Y
140
              after.__after_2_c
141
              after.__after_4_c
142
              after.ni_7._arrow._first_c
143
              after.__after_2_x
144
              after.__after_4_x
145
              after.ni_7._arrow._first_x)
146
))
147

    
148
; temporal1_temporal1__POINTTemporal1_Temporal1_handler_until
149
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.idTemporal1_Temporal1_1 Int)
150
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.x_1 Int)
151
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.temporal1_temporal1__restart_in Bool)
152
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__type)
153
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.idTemporal1_Temporal1_out Int)
154
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.x_out Int)
155
(declare-rel temporal1_temporal1__POINTTemporal1_Temporal1_handler_until (Int Int Bool temporal1_temporal1__type Int Int))
156
(rule (=> 
157
  (and (= temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.x_out temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.x_1)
158
       (= temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.temporal1_temporal1__state_in POINTTemporal1_Temporal1)
159
       (= temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.temporal1_temporal1__restart_in false)
160
       (= temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.idTemporal1_Temporal1_1)
161
       )
162
  (temporal1_temporal1__POINTTemporal1_Temporal1_handler_until temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.idTemporal1_Temporal1_1 temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.x_1 temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.temporal1_temporal1__restart_in temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__POINTTemporal1_Temporal1_handler_until.x_out)
163
))
164

    
165
; temporal1_temporal1__POINTTemporal1_Temporal1_unless
166
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_in Bool)
167
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_in temporal1_temporal1__type)
168
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.idTemporal1_Temporal1_1 Int)
169
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.E Bool)
170
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.after_E_2_output Bool)
171
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.after_E_3_output Bool)
172
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act Bool)
173
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act temporal1_temporal1__type)
174
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_1 Bool)
175
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_2 Bool)
176
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_3 Bool)
177
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_4 Bool)
178
(declare-var temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_5 Bool)
179
(declare-rel temporal1_temporal1__POINTTemporal1_Temporal1_unless (Bool temporal1_temporal1__type Int Bool Bool Bool Bool temporal1_temporal1__type))
180
(rule (=> 
181
  (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_5 (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.idTemporal1_Temporal1_1 123))
182
       (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_4 (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.idTemporal1_Temporal1_1 122))
183
       (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_3 (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.idTemporal1_Temporal1_1 123) temporal1_temporal1__POINTTemporal1_Temporal1_unless.after_E_3_output))
184
       (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_2 (and (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.idTemporal1_Temporal1_1 122) temporal1_temporal1__POINTTemporal1_Temporal1_unless.E) temporal1_temporal1__POINTTemporal1_Temporal1_unless.after_E_2_output))
185
       (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_1 (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.idTemporal1_Temporal1_1 0))
186
       (and (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_1 false))
187
               (and (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_2 false))
188
                       (and (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_3 false))
189
                               (and (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_4 false))
190
                                       (and (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_5 false))
191
                                               (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_in)
192
                                                    (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_in)
193
                                                    ))
194
                                            (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_5 true))
195
                                               (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act TEMPORAL1_B_IDL)
196
                                                    (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act true)
197
                                                    ))
198
                                       ))
199
                                    (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_4 true))
200
                                       (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act TEMPORAL1_A_IDL)
201
                                            (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act true)
202
                                            ))
203
                               ))
204
                            (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_3 true))
205
                               (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act TEMPORAL1_B__TO__TEMPORAL1_A_1)
206
                                    (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act true)
207
                                    ))
208
                       ))
209
                    (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_2 true))
210
                       (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act TEMPORAL1_A__TO__TEMPORAL1_B_1)
211
                            (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act true)
212
                            ))
213
               ))
214
            (or (not (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.__temporal1_temporal1__POINTTemporal1_Temporal1_unless_1 true))
215
               (and (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act POINT__TO__TEMPORAL1_A_1)
216
                    (= temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act true)
217
                    ))
218
       )
219
       )
220
  (temporal1_temporal1__POINTTemporal1_Temporal1_unless temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_in temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_in temporal1_temporal1__POINTTemporal1_Temporal1_unless.idTemporal1_Temporal1_1 temporal1_temporal1__POINTTemporal1_Temporal1_unless.E temporal1_temporal1__POINTTemporal1_Temporal1_unless.after_E_2_output temporal1_temporal1__POINTTemporal1_Temporal1_unless.after_E_3_output temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__restart_act temporal1_temporal1__POINTTemporal1_Temporal1_unless.temporal1_temporal1__state_act)
221
))
222

    
223
; temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until
224
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_1 Int)
225
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_1 Int)
226
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__restart_in Bool)
227
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__type)
228
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_out Int)
229
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_out Int)
230
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_2 Int)
231
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_2 Int)
232
(declare-rel temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until (Int Int Bool temporal1_temporal1__type Int Int))
233
(rule (=> 
234
  (and (Temporal1_A_en temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_1
235
                       temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_1
236
                       false
237
                       temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_2
238
                       temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_2)
239
       (= temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_out temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_2)
240
       (= temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__state_in POINTTemporal1_Temporal1)
241
       (= temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__restart_in true)
242
       (= temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_2)
243
       )
244
  (temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_1 temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_1 temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__restart_in temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until.x_out)
245
))
246

    
247
; temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless
248
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_in Bool)
249
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_in temporal1_temporal1__type)
250
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_act Bool)
251
(declare-var temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_act temporal1_temporal1__type)
252
(declare-rel temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless (Bool temporal1_temporal1__type Bool temporal1_temporal1__type))
253
(rule (=> 
254
  (and (= temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_act temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_in)
255
       (= temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_act temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_in)
256
       )
257
  (temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_in temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_in temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_act temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_act)
258
))
259

    
260
; temporal1_temporal1__TEMPORAL1_A_IDL_handler_until
261
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.idTemporal1_Temporal1_1 Int)
262
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.x_1 Int)
263
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.temporal1_temporal1__restart_in Bool)
264
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.temporal1_temporal1__state_in temporal1_temporal1__type)
265
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.idTemporal1_Temporal1_out Int)
266
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.x_out Int)
267
(declare-rel temporal1_temporal1__TEMPORAL1_A_IDL_handler_until (Int Int Bool temporal1_temporal1__type Int Int))
268
(rule (=> 
269
  (and (= temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.x_out temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.x_1)
270
       (= temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.temporal1_temporal1__state_in POINTTemporal1_Temporal1)
271
       (= temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.temporal1_temporal1__restart_in true)
272
       (= temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.idTemporal1_Temporal1_1)
273
       )
274
  (temporal1_temporal1__TEMPORAL1_A_IDL_handler_until temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.idTemporal1_Temporal1_1 temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.x_1 temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_A_IDL_handler_until.x_out)
275
))
276

    
277
; temporal1_temporal1__TEMPORAL1_A_IDL_unless
278
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__restart_in Bool)
279
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__state_in temporal1_temporal1__type)
280
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__restart_act Bool)
281
(declare-var temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__state_act temporal1_temporal1__type)
282
(declare-rel temporal1_temporal1__TEMPORAL1_A_IDL_unless (Bool temporal1_temporal1__type Bool temporal1_temporal1__type))
283
(rule (=> 
284
  (and (= temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__state_act temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__state_in)
285
       (= temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__restart_in)
286
       )
287
  (temporal1_temporal1__TEMPORAL1_A_IDL_unless temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_A_IDL_unless.temporal1_temporal1__state_act)
288
))
289

    
290
; temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until
291
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_1 Int)
292
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_1 Int)
293
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.temporal1_temporal1__restart_in Bool)
294
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__type)
295
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_out Int)
296
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_out Int)
297
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_2 Int)
298
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_3 Int)
299
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_2 Int)
300
(declare-rel temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until (Int Int Bool temporal1_temporal1__type Int Int))
301
(rule (=> 
302
  (and (Temporal1_A_ex temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_1
303
                       false
304
                       temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_2)
305
       (Temporal1_B_en temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_2
306
                       temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_1
307
                       false
308
                       temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_3
309
                       temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_2)
310
       (= temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_out temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_2)
311
       (= temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.temporal1_temporal1__state_in POINTTemporal1_Temporal1)
312
       (= temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.temporal1_temporal1__restart_in true)
313
       (= temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_3)
314
       )
315
  (temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_1 temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_1 temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until.x_out)
316
))
317

    
318
; temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless
319
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__restart_in Bool)
320
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__state_in temporal1_temporal1__type)
321
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__restart_act Bool)
322
(declare-var temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__state_act temporal1_temporal1__type)
323
(declare-rel temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless (Bool temporal1_temporal1__type Bool temporal1_temporal1__type))
324
(rule (=> 
325
  (and (= temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__state_act temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__state_in)
326
       (= temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__restart_in)
327
       )
328
  (temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless.temporal1_temporal1__state_act)
329
))
330

    
331
; temporal1_temporal1__TEMPORAL1_B_IDL_handler_until
332
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.idTemporal1_Temporal1_1 Int)
333
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.x_1 Int)
334
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.temporal1_temporal1__restart_in Bool)
335
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.temporal1_temporal1__state_in temporal1_temporal1__type)
336
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.idTemporal1_Temporal1_out Int)
337
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.x_out Int)
338
(declare-rel temporal1_temporal1__TEMPORAL1_B_IDL_handler_until (Int Int Bool temporal1_temporal1__type Int Int))
339
(rule (=> 
340
  (and (= temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.x_out temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.x_1)
341
       (= temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.temporal1_temporal1__state_in POINTTemporal1_Temporal1)
342
       (= temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.temporal1_temporal1__restart_in true)
343
       (= temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.idTemporal1_Temporal1_1)
344
       )
345
  (temporal1_temporal1__TEMPORAL1_B_IDL_handler_until temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.idTemporal1_Temporal1_1 temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.x_1 temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_B_IDL_handler_until.x_out)
346
))
347

    
348
; temporal1_temporal1__TEMPORAL1_B_IDL_unless
349
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__restart_in Bool)
350
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__state_in temporal1_temporal1__type)
351
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__restart_act Bool)
352
(declare-var temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__state_act temporal1_temporal1__type)
353
(declare-rel temporal1_temporal1__TEMPORAL1_B_IDL_unless (Bool temporal1_temporal1__type Bool temporal1_temporal1__type))
354
(rule (=> 
355
  (and (= temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__state_act temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__state_in)
356
       (= temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__restart_in)
357
       )
358
  (temporal1_temporal1__TEMPORAL1_B_IDL_unless temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_B_IDL_unless.temporal1_temporal1__state_act)
359
))
360

    
361
; temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until
362
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_1 Int)
363
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_1 Int)
364
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__restart_in Bool)
365
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__type)
366
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_out Int)
367
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_out Int)
368
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_2 Int)
369
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_3 Int)
370
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_2 Int)
371
(declare-rel temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until (Int Int Bool temporal1_temporal1__type Int Int))
372
(rule (=> 
373
  (and (Temporal1_B_ex temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_1
374
                       false
375
                       temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_2)
376
       (Temporal1_A_en temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_2
377
                       temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_1
378
                       false
379
                       temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_3
380
                       temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_2)
381
       (= temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_out temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_2)
382
       (= temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__state_in POINTTemporal1_Temporal1)
383
       (= temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__restart_in true)
384
       (= temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_3)
385
       )
386
  (temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_1 temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_1 temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.idTemporal1_Temporal1_out temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until.x_out)
387
))
388

    
389
; temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless
390
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_in Bool)
391
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_in temporal1_temporal1__type)
392
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_act Bool)
393
(declare-var temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_act temporal1_temporal1__type)
394
(declare-rel temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless (Bool temporal1_temporal1__type Bool temporal1_temporal1__type))
395
(rule (=> 
396
  (and (= temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_act temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_in)
397
       (= temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_in)
398
       )
399
  (temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_in temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_in temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__restart_act temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless.temporal1_temporal1__state_act)
400
))
401

    
402
; Temporal1_Temporal1_node
403
(declare-var Temporal1_Temporal1_node.idTemporal1_Temporal1_1 Int)
404
(declare-var Temporal1_Temporal1_node.x_1 Int)
405
(declare-var Temporal1_Temporal1_node.E Bool)
406
(declare-var Temporal1_Temporal1_node.idTemporal1_Temporal1 Int)
407
(declare-var Temporal1_Temporal1_node.x Int)
408
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c Bool)
409
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c temporal1_temporal1__type)
410
(declare-var Temporal1_Temporal1_node.ni_4.after.__after_2_c Int)
411
(declare-var Temporal1_Temporal1_node.ni_4.after.__after_4_c Int)
412
(declare-var Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c Bool)
413
(declare-var Temporal1_Temporal1_node.ni_5.after.__after_2_c Int)
414
(declare-var Temporal1_Temporal1_node.ni_5.after.__after_4_c Int)
415
(declare-var Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c Bool)
416
(declare-var Temporal1_Temporal1_node.ni_6._arrow._first_c Bool)
417
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m Bool)
418
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m temporal1_temporal1__type)
419
(declare-var Temporal1_Temporal1_node.ni_4.after.__after_2_m Int)
420
(declare-var Temporal1_Temporal1_node.ni_4.after.__after_4_m Int)
421
(declare-var Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m Bool)
422
(declare-var Temporal1_Temporal1_node.ni_5.after.__after_2_m Int)
423
(declare-var Temporal1_Temporal1_node.ni_5.after.__after_4_m Int)
424
(declare-var Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m Bool)
425
(declare-var Temporal1_Temporal1_node.ni_6._arrow._first_m Bool)
426
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x Bool)
427
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x temporal1_temporal1__type)
428
(declare-var Temporal1_Temporal1_node.ni_4.after.__after_2_x Int)
429
(declare-var Temporal1_Temporal1_node.ni_4.after.__after_4_x Int)
430
(declare-var Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x Bool)
431
(declare-var Temporal1_Temporal1_node.ni_5.after.__after_2_x Int)
432
(declare-var Temporal1_Temporal1_node.ni_5.after.__after_4_x Int)
433
(declare-var Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x Bool)
434
(declare-var Temporal1_Temporal1_node.ni_6._arrow._first_x Bool)
435
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_1 Bool)
436
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_10 temporal1_temporal1__type)
437
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_11 Bool)
438
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_12 temporal1_temporal1__type)
439
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_13 Bool)
440
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_14 temporal1_temporal1__type)
441
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_15 Int)
442
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_16 Int)
443
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_17 Bool)
444
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_18 temporal1_temporal1__type)
445
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_19 Int)
446
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_2 temporal1_temporal1__type)
447
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_20 Int)
448
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_21 Bool)
449
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_22 temporal1_temporal1__type)
450
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_23 Int)
451
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_24 Int)
452
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_25 Bool)
453
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_26 temporal1_temporal1__type)
454
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_27 Int)
455
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_28 Int)
456
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_29 Bool)
457
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_3 Bool)
458
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_30 temporal1_temporal1__type)
459
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_31 Int)
460
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_32 Int)
461
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_33 Bool)
462
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_34 temporal1_temporal1__type)
463
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_35 Int)
464
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_36 Int)
465
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_37 Bool)
466
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_4 temporal1_temporal1__type)
467
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_5 Bool)
468
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_6 temporal1_temporal1__type)
469
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_7 Bool)
470
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_8 temporal1_temporal1__type)
471
(declare-var Temporal1_Temporal1_node.__Temporal1_Temporal1_node_9 Bool)
472
(declare-var Temporal1_Temporal1_node.after_E_2_output Bool)
473
(declare-var Temporal1_Temporal1_node.after_E_3_output Bool)
474
(declare-var Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in Bool)
475
(declare-var Temporal1_Temporal1_node.temporal1_temporal1__next_state_in temporal1_temporal1__type)
476
(declare-var Temporal1_Temporal1_node.temporal1_temporal1__restart_act Bool)
477
(declare-var Temporal1_Temporal1_node.temporal1_temporal1__restart_in Bool)
478
(declare-var Temporal1_Temporal1_node.temporal1_temporal1__state_act temporal1_temporal1__type)
479
(declare-var Temporal1_Temporal1_node.temporal1_temporal1__state_in temporal1_temporal1__type)
480
(declare-rel Temporal1_Temporal1_node_reset (Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool))
481
(declare-rel Temporal1_Temporal1_node_step (Int Int Bool Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool))
482

    
483
(rule (=> 
484
  (and 
485
       (= Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c)
486
       (= Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c)
487
       (= Temporal1_Temporal1_node.ni_6._arrow._first_m true)
488
       (after_reset Temporal1_Temporal1_node.ni_5.after.__after_2_c
489
                    Temporal1_Temporal1_node.ni_5.after.__after_4_c
490
                    Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
491
                    Temporal1_Temporal1_node.ni_5.after.__after_2_m
492
                    Temporal1_Temporal1_node.ni_5.after.__after_4_m
493
                    Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m)
494
       (after_reset Temporal1_Temporal1_node.ni_4.after.__after_2_c
495
                    Temporal1_Temporal1_node.ni_4.after.__after_4_c
496
                    Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
497
                    Temporal1_Temporal1_node.ni_4.after.__after_2_m
498
                    Temporal1_Temporal1_node.ni_4.after.__after_4_m
499
                    Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m)
500
  )
501
  (Temporal1_Temporal1_node_reset Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
502
                                  Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
503
                                  Temporal1_Temporal1_node.ni_4.after.__after_2_c
504
                                  Temporal1_Temporal1_node.ni_4.after.__after_4_c
505
                                  Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
506
                                  Temporal1_Temporal1_node.ni_5.after.__after_2_c
507
                                  Temporal1_Temporal1_node.ni_5.after.__after_4_c
508
                                  Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
509
                                  Temporal1_Temporal1_node.ni_6._arrow._first_c
510
                                  Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m
511
                                  Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m
512
                                  Temporal1_Temporal1_node.ni_4.after.__after_2_m
513
                                  Temporal1_Temporal1_node.ni_4.after.__after_4_m
514
                                  Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
515
                                  Temporal1_Temporal1_node.ni_5.after.__after_2_m
516
                                  Temporal1_Temporal1_node.ni_5.after.__after_4_m
517
                                  Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
518
                                  Temporal1_Temporal1_node.ni_6._arrow._first_m)
519
))
520

    
521
(rule (=> 
522
  (and (= Temporal1_Temporal1_node.ni_6._arrow._first_m Temporal1_Temporal1_node.ni_6._arrow._first_c)
523
       (and (= Temporal1_Temporal1_node.__Temporal1_Temporal1_node_37 (ite Temporal1_Temporal1_node.ni_6._arrow._first_m true false))
524
            (= Temporal1_Temporal1_node.ni_6._arrow._first_x false))
525
       (and (or (not (= Temporal1_Temporal1_node.__Temporal1_Temporal1_node_37 false))
526
               (and (= Temporal1_Temporal1_node.temporal1_temporal1__state_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c)
527
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c)
528
                    ))
529
            (or (not (= Temporal1_Temporal1_node.__Temporal1_Temporal1_node_37 true))
530
               (and (= Temporal1_Temporal1_node.temporal1_temporal1__state_in POINTTemporal1_Temporal1)
531
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_in false)
532
                    ))
533
       )
534
       (and (= Temporal1_Temporal1_node.ni_5.after.__after_2_m Temporal1_Temporal1_node.ni_5.after.__after_2_c)
535
            (= Temporal1_Temporal1_node.ni_5.after.__after_4_m Temporal1_Temporal1_node.ni_5.after.__after_4_c)
536
            (= Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c)
537
            )
538
       (after_step 3
539
                   Temporal1_Temporal1_node.E
540
                   Temporal1_Temporal1_node.idTemporal1_Temporal1_1
541
                   Temporal1_Temporal1_node.after_E_3_output
542
                   Temporal1_Temporal1_node.ni_5.after.__after_2_m
543
                   Temporal1_Temporal1_node.ni_5.after.__after_4_m
544
                   Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
545
                   Temporal1_Temporal1_node.ni_5.after.__after_2_x
546
                   Temporal1_Temporal1_node.ni_5.after.__after_4_x
547
                   Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x)
548
       (and (= Temporal1_Temporal1_node.ni_4.after.__after_2_m Temporal1_Temporal1_node.ni_4.after.__after_2_c)
549
            (= Temporal1_Temporal1_node.ni_4.after.__after_4_m Temporal1_Temporal1_node.ni_4.after.__after_4_c)
550
            (= Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c)
551
            )
552
       (after_step 2
553
                   Temporal1_Temporal1_node.E
554
                   Temporal1_Temporal1_node.idTemporal1_Temporal1_1
555
                   Temporal1_Temporal1_node.after_E_2_output
556
                   Temporal1_Temporal1_node.ni_4.after.__after_2_m
557
                   Temporal1_Temporal1_node.ni_4.after.__after_4_m
558
                   Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
559
                   Temporal1_Temporal1_node.ni_4.after.__after_2_x
560
                   Temporal1_Temporal1_node.ni_4.after.__after_4_x
561
                   Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x)
562
       (and (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_in POINTTemporal1_Temporal1))
563
               (and (temporal1_temporal1__POINTTemporal1_Temporal1_unless 
564
                    Temporal1_Temporal1_node.temporal1_temporal1__restart_in
565
                    Temporal1_Temporal1_node.temporal1_temporal1__state_in
566
                    Temporal1_Temporal1_node.idTemporal1_Temporal1_1
567
                    Temporal1_Temporal1_node.E
568
                    Temporal1_Temporal1_node.after_E_2_output
569
                    Temporal1_Temporal1_node.after_E_3_output
570
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_11
571
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_12)
572
                    (= Temporal1_Temporal1_node.temporal1_temporal1__state_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_12)
573
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_11)
574
                    ))
575
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_in POINT__TO__TEMPORAL1_A_1))
576
               (and (temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_unless 
577
                    Temporal1_Temporal1_node.temporal1_temporal1__restart_in
578
                    Temporal1_Temporal1_node.temporal1_temporal1__state_in
579
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_9
580
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_10)
581
                    (= Temporal1_Temporal1_node.temporal1_temporal1__state_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_10)
582
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_9)
583
                    ))
584
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_in TEMPORAL1_A_IDL))
585
               (and (temporal1_temporal1__TEMPORAL1_A_IDL_unless Temporal1_Temporal1_node.temporal1_temporal1__restart_in
586
                                                                 Temporal1_Temporal1_node.temporal1_temporal1__state_in
587
                                                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_3
588
                                                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_4)
589
                    (= Temporal1_Temporal1_node.temporal1_temporal1__state_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_4)
590
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_3)
591
                    ))
592
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_in TEMPORAL1_A__TO__TEMPORAL1_B_1))
593
               (and (temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_unless 
594
                    Temporal1_Temporal1_node.temporal1_temporal1__restart_in
595
                    Temporal1_Temporal1_node.temporal1_temporal1__state_in
596
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_7
597
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_8)
598
                    (= Temporal1_Temporal1_node.temporal1_temporal1__state_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_8)
599
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_7)
600
                    ))
601
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_in TEMPORAL1_B_IDL))
602
               (and (temporal1_temporal1__TEMPORAL1_B_IDL_unless Temporal1_Temporal1_node.temporal1_temporal1__restart_in
603
                                                                 Temporal1_Temporal1_node.temporal1_temporal1__state_in
604
                                                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_1
605
                                                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_2)
606
                    (= Temporal1_Temporal1_node.temporal1_temporal1__state_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_2)
607
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_1)
608
                    ))
609
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_in TEMPORAL1_B__TO__TEMPORAL1_A_1))
610
               (and (temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_unless 
611
                    Temporal1_Temporal1_node.temporal1_temporal1__restart_in
612
                    Temporal1_Temporal1_node.temporal1_temporal1__state_in
613
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_5
614
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_6)
615
                    (= Temporal1_Temporal1_node.temporal1_temporal1__state_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_6)
616
                    (= Temporal1_Temporal1_node.temporal1_temporal1__restart_act Temporal1_Temporal1_node.__Temporal1_Temporal1_node_5)
617
                    ))
618
       )
619
       (and (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_act POINTTemporal1_Temporal1))
620
               (and (temporal1_temporal1__POINTTemporal1_Temporal1_handler_until 
621
                    Temporal1_Temporal1_node.idTemporal1_Temporal1_1
622
                    Temporal1_Temporal1_node.x_1
623
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_33
624
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_34
625
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_35
626
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_36)
627
                    (= Temporal1_Temporal1_node.x Temporal1_Temporal1_node.__Temporal1_Temporal1_node_36)
628
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_state_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_34)
629
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_33)
630
                    (= Temporal1_Temporal1_node.idTemporal1_Temporal1 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_35)
631
                    ))
632
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_act POINT__TO__TEMPORAL1_A_1))
633
               (and (temporal1_temporal1__POINT__TO__TEMPORAL1_A_1_handler_until 
634
                    Temporal1_Temporal1_node.idTemporal1_Temporal1_1
635
                    Temporal1_Temporal1_node.x_1
636
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_29
637
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_30
638
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_31
639
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_32)
640
                    (= Temporal1_Temporal1_node.x Temporal1_Temporal1_node.__Temporal1_Temporal1_node_32)
641
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_state_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_30)
642
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_29)
643
                    (= Temporal1_Temporal1_node.idTemporal1_Temporal1 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_31)
644
                    ))
645
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_act TEMPORAL1_A_IDL))
646
               (and (temporal1_temporal1__TEMPORAL1_A_IDL_handler_until 
647
                    Temporal1_Temporal1_node.idTemporal1_Temporal1_1
648
                    Temporal1_Temporal1_node.x_1
649
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_17
650
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_18
651
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_19
652
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_20)
653
                    (= Temporal1_Temporal1_node.x Temporal1_Temporal1_node.__Temporal1_Temporal1_node_20)
654
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_state_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_18)
655
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_17)
656
                    (= Temporal1_Temporal1_node.idTemporal1_Temporal1 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_19)
657
                    ))
658
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_act TEMPORAL1_A__TO__TEMPORAL1_B_1))
659
               (and (temporal1_temporal1__TEMPORAL1_A__TO__TEMPORAL1_B_1_handler_until 
660
                    Temporal1_Temporal1_node.idTemporal1_Temporal1_1
661
                    Temporal1_Temporal1_node.x_1
662
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_25
663
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_26
664
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_27
665
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_28)
666
                    (= Temporal1_Temporal1_node.x Temporal1_Temporal1_node.__Temporal1_Temporal1_node_28)
667
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_state_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_26)
668
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_25)
669
                    (= Temporal1_Temporal1_node.idTemporal1_Temporal1 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_27)
670
                    ))
671
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_act TEMPORAL1_B_IDL))
672
               (and (temporal1_temporal1__TEMPORAL1_B_IDL_handler_until 
673
                    Temporal1_Temporal1_node.idTemporal1_Temporal1_1
674
                    Temporal1_Temporal1_node.x_1
675
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_13
676
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_14
677
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_15
678
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_16)
679
                    (= Temporal1_Temporal1_node.x Temporal1_Temporal1_node.__Temporal1_Temporal1_node_16)
680
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_state_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_14)
681
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_13)
682
                    (= Temporal1_Temporal1_node.idTemporal1_Temporal1 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_15)
683
                    ))
684
            (or (not (= Temporal1_Temporal1_node.temporal1_temporal1__state_act TEMPORAL1_B__TO__TEMPORAL1_A_1))
685
               (and (temporal1_temporal1__TEMPORAL1_B__TO__TEMPORAL1_A_1_handler_until 
686
                    Temporal1_Temporal1_node.idTemporal1_Temporal1_1
687
                    Temporal1_Temporal1_node.x_1
688
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_21
689
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_22
690
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_23
691
                    Temporal1_Temporal1_node.__Temporal1_Temporal1_node_24)
692
                    (= Temporal1_Temporal1_node.x Temporal1_Temporal1_node.__Temporal1_Temporal1_node_24)
693
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_state_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_22)
694
                    (= Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in Temporal1_Temporal1_node.__Temporal1_Temporal1_node_21)
695
                    (= Temporal1_Temporal1_node.idTemporal1_Temporal1 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_23)
696
                    ))
697
       )
698
       (= Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x Temporal1_Temporal1_node.temporal1_temporal1__next_state_in)
699
       (= Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x Temporal1_Temporal1_node.temporal1_temporal1__next_restart_in)
700
       )
701
  (Temporal1_Temporal1_node_step Temporal1_Temporal1_node.idTemporal1_Temporal1_1
702
                                 Temporal1_Temporal1_node.x_1
703
                                 Temporal1_Temporal1_node.E
704
                                 Temporal1_Temporal1_node.idTemporal1_Temporal1
705
                                 Temporal1_Temporal1_node.x
706
                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
707
                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
708
                                 Temporal1_Temporal1_node.ni_4.after.__after_2_c
709
                                 Temporal1_Temporal1_node.ni_4.after.__after_4_c
710
                                 Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
711
                                 Temporal1_Temporal1_node.ni_5.after.__after_2_c
712
                                 Temporal1_Temporal1_node.ni_5.after.__after_4_c
713
                                 Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
714
                                 Temporal1_Temporal1_node.ni_6._arrow._first_c
715
                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x
716
                                 Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x
717
                                 Temporal1_Temporal1_node.ni_4.after.__after_2_x
718
                                 Temporal1_Temporal1_node.ni_4.after.__after_4_x
719
                                 Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x
720
                                 Temporal1_Temporal1_node.ni_5.after.__after_2_x
721
                                 Temporal1_Temporal1_node.ni_5.after.__after_4_x
722
                                 Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x
723
                                 Temporal1_Temporal1_node.ni_6._arrow._first_x)
724
))
725

    
726
; Temporal1_Temporal1
727
(declare-var Temporal1_Temporal1.E Bool)
728
(declare-var Temporal1_Temporal1.x Int)
729
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_4_c Int)
730
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_5_c Int)
731
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c Bool)
732
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c temporal1_temporal1__type)
733
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c Int)
734
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c Int)
735
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c Bool)
736
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c Int)
737
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c Int)
738
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c Bool)
739
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c Bool)
740
(declare-var Temporal1_Temporal1.ni_3._arrow._first_c Bool)
741
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_4_m Int)
742
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_5_m Int)
743
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m Bool)
744
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m temporal1_temporal1__type)
745
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m Int)
746
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m Int)
747
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m Bool)
748
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m Int)
749
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m Int)
750
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m Bool)
751
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m Bool)
752
(declare-var Temporal1_Temporal1.ni_3._arrow._first_m Bool)
753
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_4_x Int)
754
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_5_x Int)
755
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x Bool)
756
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x temporal1_temporal1__type)
757
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_x Int)
758
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_x Int)
759
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x Bool)
760
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_x Int)
761
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_x Int)
762
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x Bool)
763
(declare-var Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_x Bool)
764
(declare-var Temporal1_Temporal1.ni_3._arrow._first_x Bool)
765
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_1 Int)
766
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_2 Int)
767
(declare-var Temporal1_Temporal1.__Temporal1_Temporal1_3 Bool)
768
(declare-var Temporal1_Temporal1.idTemporal1_Temporal1 Int)
769
(declare-var Temporal1_Temporal1.idTemporal1_Temporal1_1 Int)
770
(declare-var Temporal1_Temporal1.x_1 Int)
771
(declare-rel Temporal1_Temporal1_reset (Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool))
772
(declare-rel Temporal1_Temporal1_step (Bool Int Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool))
773

    
774
(rule (=> 
775
  (and 
776
       (= Temporal1_Temporal1.__Temporal1_Temporal1_4_m Temporal1_Temporal1.__Temporal1_Temporal1_4_c)
777
       (= Temporal1_Temporal1.__Temporal1_Temporal1_5_m Temporal1_Temporal1.__Temporal1_Temporal1_5_c)
778
       (= Temporal1_Temporal1.ni_3._arrow._first_m true)
779
       (Temporal1_Temporal1_node_reset Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
780
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
781
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c
782
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c
783
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
784
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c
785
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c
786
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
787
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c
788
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m
789
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m
790
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m
791
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m
792
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
793
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m
794
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m
795
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
796
                                       Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m)
797
  )
798
  (Temporal1_Temporal1_reset Temporal1_Temporal1.__Temporal1_Temporal1_4_c
799
                             Temporal1_Temporal1.__Temporal1_Temporal1_5_c
800
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
801
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
802
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c
803
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c
804
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
805
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c
806
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c
807
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
808
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c
809
                             Temporal1_Temporal1.ni_3._arrow._first_c
810
                             Temporal1_Temporal1.__Temporal1_Temporal1_4_m
811
                             Temporal1_Temporal1.__Temporal1_Temporal1_5_m
812
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m
813
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m
814
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m
815
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m
816
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
817
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m
818
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m
819
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
820
                             Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m
821
                             Temporal1_Temporal1.ni_3._arrow._first_m)
822
))
823

    
824
(rule (=> 
825
  (and (= Temporal1_Temporal1.ni_3._arrow._first_m Temporal1_Temporal1.ni_3._arrow._first_c)
826
       (and (= Temporal1_Temporal1.__Temporal1_Temporal1_3 (ite Temporal1_Temporal1.ni_3._arrow._first_m true false))
827
            (= Temporal1_Temporal1.ni_3._arrow._first_x false))
828
       (and (or (not (= Temporal1_Temporal1.__Temporal1_Temporal1_3 false))
829
               (and (= Temporal1_Temporal1.x_1 Temporal1_Temporal1.__Temporal1_Temporal1_5_c)
830
                    (= Temporal1_Temporal1.idTemporal1_Temporal1_1 Temporal1_Temporal1.__Temporal1_Temporal1_4_c)
831
                    ))
832
            (or (not (= Temporal1_Temporal1.__Temporal1_Temporal1_3 true))
833
               (and (= Temporal1_Temporal1.x_1 0)
834
                    (= Temporal1_Temporal1.idTemporal1_Temporal1_1 0)
835
                    ))
836
       )
837
       (and (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c)
838
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c)
839
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c)
840
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c)
841
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c)
842
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c)
843
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c)
844
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c)
845
            (= Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c)
846
            )
847
       (Temporal1_Temporal1_node_step Temporal1_Temporal1.idTemporal1_Temporal1_1
848
                                      Temporal1_Temporal1.x_1
849
                                      Temporal1_Temporal1.E
850
                                      Temporal1_Temporal1.__Temporal1_Temporal1_1
851
                                      Temporal1_Temporal1.__Temporal1_Temporal1_2
852
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m
853
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m
854
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m
855
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m
856
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
857
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m
858
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m
859
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
860
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m
861
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x
862
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x
863
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_x
864
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_x
865
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x
866
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_x
867
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_x
868
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x
869
                                      Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_x)
870
       (and (or (not (= Temporal1_Temporal1.E false))
871
               (and (= Temporal1_Temporal1.x Temporal1_Temporal1.x_1)
872
                    (= Temporal1_Temporal1.idTemporal1_Temporal1 Temporal1_Temporal1.idTemporal1_Temporal1_1)
873
                    ))
874
            (or (not (= Temporal1_Temporal1.E true))
875
               (and (= Temporal1_Temporal1.x Temporal1_Temporal1.__Temporal1_Temporal1_2)
876
                    (= Temporal1_Temporal1.idTemporal1_Temporal1 Temporal1_Temporal1.__Temporal1_Temporal1_1)
877
                    ))
878
       )
879
       (= Temporal1_Temporal1.__Temporal1_Temporal1_5_x Temporal1_Temporal1.x)
880
       (= Temporal1_Temporal1.__Temporal1_Temporal1_4_x Temporal1_Temporal1.idTemporal1_Temporal1)
881
       )
882
  (Temporal1_Temporal1_step Temporal1_Temporal1.E
883
                            Temporal1_Temporal1.x
884
                            Temporal1_Temporal1.__Temporal1_Temporal1_4_c
885
                            Temporal1_Temporal1.__Temporal1_Temporal1_5_c
886
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
887
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
888
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c
889
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c
890
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
891
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c
892
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c
893
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
894
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c
895
                            Temporal1_Temporal1.ni_3._arrow._first_c
896
                            Temporal1_Temporal1.__Temporal1_Temporal1_4_x
897
                            Temporal1_Temporal1.__Temporal1_Temporal1_5_x
898
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x
899
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x
900
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_x
901
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_x
902
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x
903
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_x
904
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_x
905
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x
906
                            Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_x
907
                            Temporal1_Temporal1.ni_3._arrow._first_x)
908
))
909

    
910
; Temporal1
911
(declare-var Temporal1.E_1_1 Real)
912
(declare-var Temporal1.x_1_1 Int)
913
(declare-var Temporal1.__Temporal1_2_c Real)
914
(declare-var Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_c Int)
915
(declare-var Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_c Int)
916
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c Bool)
917
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c temporal1_temporal1__type)
918
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c Int)
919
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c Int)
920
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c Bool)
921
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c Int)
922
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c Int)
923
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c Bool)
924
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c Bool)
925
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_c Bool)
926
(declare-var Temporal1.ni_1._arrow._first_c Bool)
927
(declare-var Temporal1.__Temporal1_2_m Real)
928
(declare-var Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_m Int)
929
(declare-var Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_m Int)
930
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m Bool)
931
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m temporal1_temporal1__type)
932
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m Int)
933
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m Int)
934
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m Bool)
935
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m Int)
936
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m Int)
937
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m Bool)
938
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m Bool)
939
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_m Bool)
940
(declare-var Temporal1.ni_1._arrow._first_m Bool)
941
(declare-var Temporal1.__Temporal1_2_x Real)
942
(declare-var Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_x Int)
943
(declare-var Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_x Int)
944
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x Bool)
945
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x temporal1_temporal1__type)
946
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_x Int)
947
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_x Int)
948
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x Bool)
949
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_x Int)
950
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_x Int)
951
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x Bool)
952
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_x Bool)
953
(declare-var Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_x Bool)
954
(declare-var Temporal1.ni_1._arrow._first_x Bool)
955
(declare-var Temporal1.Temporal1E_1_1_event Bool)
956
(declare-var Temporal1.Temporal1_1_1 Int)
957
(declare-var Temporal1.__Temporal1_1 Bool)
958
(declare-var Temporal1.i_virtual_local Real)
959
(declare-rel Temporal1_reset (Real Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool Bool Real Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool Bool))
960
(declare-rel Temporal1_step (Real Int Real Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool Bool Real Int Int Bool temporal1_temporal1__type Int Int Bool Int Int Bool Bool Bool Bool))
961

    
962
(rule (=> 
963
  (and 
964
       (= Temporal1.__Temporal1_2_m Temporal1.__Temporal1_2_c)
965
       (= Temporal1.ni_1._arrow._first_m true)
966
       (Temporal1_Temporal1_reset Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_c
967
                                  Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_c
968
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
969
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
970
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c
971
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c
972
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
973
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c
974
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c
975
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
976
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c
977
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_c
978
                                  Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_m
979
                                  Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_m
980
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m
981
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m
982
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m
983
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m
984
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
985
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m
986
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m
987
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
988
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m
989
                                  Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_m)
990
  )
991
  (Temporal1_reset Temporal1.__Temporal1_2_c
992
                   Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_c
993
                   Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_c
994
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
995
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
996
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c
997
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c
998
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
999
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c
1000
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c
1001
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
1002
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c
1003
                   Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_c
1004
                   Temporal1.ni_1._arrow._first_c
1005
                   Temporal1.__Temporal1_2_m
1006
                   Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_m
1007
                   Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_m
1008
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m
1009
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m
1010
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m
1011
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m
1012
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
1013
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m
1014
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m
1015
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
1016
                   Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m
1017
                   Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_m
1018
                   Temporal1.ni_1._arrow._first_m)
1019
))
1020

    
1021
(rule (=> 
1022
  (and (= Temporal1.ni_1._arrow._first_m Temporal1.ni_1._arrow._first_c)
1023
       (and (= Temporal1.__Temporal1_1 (ite Temporal1.ni_1._arrow._first_m true false))
1024
            (= Temporal1.ni_1._arrow._first_x false))
1025
       (and (or (not (= Temporal1.__Temporal1_1 true))
1026
               (= Temporal1.Temporal1E_1_1_event false))
1027
            (or (not (= Temporal1.__Temporal1_1 false))
1028
               (= Temporal1.Temporal1E_1_1_event (and (<= Temporal1.__Temporal1_2_c 0.) (> Temporal1.E_1_1 0.))))
1029
       )
1030
       (and (= Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_m Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_c)
1031
            (= Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_m Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_c)
1032
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c)
1033
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c)
1034
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c)
1035
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c)
1036
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c)
1037
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c)
1038
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c)
1039
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c)
1040
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c)
1041
            (= Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_m Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_c)
1042
            )
1043
       (Temporal1_Temporal1_step Temporal1.Temporal1E_1_1_event
1044
                                 Temporal1.Temporal1_1_1
1045
                                 Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_m
1046
                                 Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_m
1047
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_m
1048
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_m
1049
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_m
1050
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_m
1051
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_m
1052
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_m
1053
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_m
1054
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_m
1055
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_m
1056
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_m
1057
                                 Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_x
1058
                                 Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_x
1059
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x
1060
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x
1061
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_x
1062
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_x
1063
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x
1064
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_x
1065
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_x
1066
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x
1067
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_x
1068
                                 Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_x)
1069
       (= Temporal1.x_1_1 Temporal1.Temporal1_1_1)
1070
       (and (or (not (= Temporal1.__Temporal1_1 true))
1071
               (= Temporal1.i_virtual_local 0.))
1072
            (or (not (= Temporal1.__Temporal1_1 false))
1073
               (= Temporal1.i_virtual_local 1.))
1074
       )
1075
       (= Temporal1.__Temporal1_2_x Temporal1.E_1_1)
1076
       )
1077
  (Temporal1_step Temporal1.E_1_1
1078
                  Temporal1.x_1_1
1079
                  Temporal1.__Temporal1_2_c
1080
                  Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_c
1081
                  Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_c
1082
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_c
1083
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_c
1084
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_c
1085
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_c
1086
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_c
1087
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_c
1088
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_c
1089
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_c
1090
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_c
1091
                  Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_c
1092
                  Temporal1.ni_1._arrow._first_c
1093
                  Temporal1.__Temporal1_2_x
1094
                  Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_4_x
1095
                  Temporal1.ni_0.Temporal1_Temporal1.__Temporal1_Temporal1_5_x
1096
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_38_x
1097
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.__Temporal1_Temporal1_node_39_x
1098
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_2_x
1099
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.__after_4_x
1100
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_4.after.ni_7._arrow._first_x
1101
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_2_x
1102
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.__after_4_x
1103
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_5.after.ni_7._arrow._first_x
1104
                  Temporal1.ni_0.Temporal1_Temporal1.ni_2.Temporal1_Temporal1_node.ni_6._arrow._first_x
1105
                  Temporal1.ni_0.Temporal1_Temporal1.ni_3._arrow._first_x
1106
                  Temporal1.ni_1._arrow._first_x)
1107
))
1108