Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions6 / Junctions6.smt2 @ eb639349

History | View | Annotate | Download (211 KB)

1
(declare-datatypes () ((junctions6_junctions6__type POINTJunctions6_Junctions6 POINT__TO__JUNCTIONS6_TOP_1 JUNCTIONS6_TOP_IDL)));
2

    
3
(declare-datatypes () ((junctions6_top__type POINTJunctions6_TOP POINT__TO__TOP_A_1 POINT__TO__TOP_B_2 TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1 TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1 TOP_C__TO__JUNCTIONS6_TOP_1 TOP_D__TO__TOP_C_1 TOP_A_IDL TOP_B_IDL TOP_C_IDL TOP_D_IDL)));
4

    
5
; POINT__To__TOP_A_1_Condition_Action
6
(declare-var POINT__To__TOP_A_1_Condition_Action.y_1 Int)
7
(declare-var POINT__To__TOP_A_1_Condition_Action.y Int)
8
(declare-rel POINT__To__TOP_A_1_Condition_Action (Int Int))
9
(rule (=> 
10
  (= POINT__To__TOP_A_1_Condition_Action.y (+ POINT__To__TOP_A_1_Condition_Action.y_1 1))
11
  (POINT__To__TOP_A_1_Condition_Action POINT__To__TOP_A_1_Condition_Action.y_1 POINT__To__TOP_A_1_Condition_Action.y)
12
))
13

    
14
; POINT__To__TOP_B_2_Condition_Action
15
(declare-var POINT__To__TOP_B_2_Condition_Action.y_1 Int)
16
(declare-var POINT__To__TOP_B_2_Condition_Action.y Int)
17
(declare-rel POINT__To__TOP_B_2_Condition_Action (Int Int))
18
(rule (=> 
19
  (= POINT__To__TOP_B_2_Condition_Action.y (+ POINT__To__TOP_B_2_Condition_Action.y_1 10))
20
  (POINT__To__TOP_B_2_Condition_Action POINT__To__TOP_B_2_Condition_Action.y_1 POINT__To__TOP_B_2_Condition_Action.y)
21
))
22

    
23
; TOP_A_en
24
(declare-var TOP_A_en.idJunctions6_TOP_1 Int)
25
(declare-var TOP_A_en.isInner Bool)
26
(declare-var TOP_A_en.idJunctions6_TOP Int)
27
(declare-rel TOP_A_en (Int Bool Int))
28
(rule (=> 
29
  (= TOP_A_en.idJunctions6_TOP 1297)
30
  (TOP_A_en TOP_A_en.idJunctions6_TOP_1 TOP_A_en.isInner TOP_A_en.idJunctions6_TOP)
31
))
32

    
33
; TOP_B_en
34
(declare-var TOP_B_en.idJunctions6_TOP_1 Int)
35
(declare-var TOP_B_en.isInner Bool)
36
(declare-var TOP_B_en.idJunctions6_TOP Int)
37
(declare-rel TOP_B_en (Int Bool Int))
38
(rule (=> 
39
  (= TOP_B_en.idJunctions6_TOP 1298)
40
  (TOP_B_en TOP_B_en.idJunctions6_TOP_1 TOP_B_en.isInner TOP_B_en.idJunctions6_TOP)
41
))
42

    
43
; TOP_C_en
44
(declare-var TOP_C_en.idJunctions6_TOP_1 Int)
45
(declare-var TOP_C_en.isInner Bool)
46
(declare-var TOP_C_en.idJunctions6_TOP Int)
47
(declare-rel TOP_C_en (Int Bool Int))
48
(rule (=> 
49
  (= TOP_C_en.idJunctions6_TOP 1299)
50
  (TOP_C_en TOP_C_en.idJunctions6_TOP_1 TOP_C_en.isInner TOP_C_en.idJunctions6_TOP)
51
))
52

    
53
; TOP_D_en
54
(declare-var TOP_D_en.idJunctions6_TOP_1 Int)
55
(declare-var TOP_D_en.isInner Bool)
56
(declare-var TOP_D_en.idJunctions6_TOP Int)
57
(declare-rel TOP_D_en (Int Bool Int))
58
(rule (=> 
59
  (= TOP_D_en.idJunctions6_TOP 1300)
60
  (TOP_D_en TOP_D_en.idJunctions6_TOP_1 TOP_D_en.isInner TOP_D_en.idJunctions6_TOP)
61
))
62

    
63
; Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action
64
(declare-var Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action.y_1 Int)
65
(declare-var Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action.y Int)
66
(declare-rel Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action (Int Int))
67
(rule (=> 
68
  (= Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action.y (+ Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action.y_1 10000))
69
  (Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action.y_1 Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action.y)
70
))
71

    
72
; Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action
73
(declare-var Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action.y_1 Int)
74
(declare-var Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action.y Int)
75
(declare-rel Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action (Int Int))
76
(rule (=> 
77
  (= Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action.y (+ Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action.y_1 100000))
78
  (Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action.y_1 Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action.y)
79
))
80

    
81
; TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action
82
(declare-var TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y_1 Int)
83
(declare-var TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y Int)
84
(declare-rel TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action (Int Int))
85
(rule (=> 
86
  (= TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y (+ TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y_1 100))
87
  (TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y_1 TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y)
88
))
89

    
90
; TOP_A_ex
91
(declare-var TOP_A_ex.idJunctions6_TOP_1 Int)
92
(declare-var TOP_A_ex.isInner Bool)
93
(declare-var TOP_A_ex.idJunctions6_TOP Int)
94
(declare-var TOP_A_ex.idJunctions6_TOP_2 Int)
95
(declare-rel TOP_A_ex (Int Bool Int))
96
(rule (=> 
97
  (and (and (or (not (= (not TOP_A_ex.isInner) true))
98
               (= TOP_A_ex.idJunctions6_TOP_2 0))
99
            (or (not (= (not TOP_A_ex.isInner) false))
100
               (= TOP_A_ex.idJunctions6_TOP_2 TOP_A_ex.idJunctions6_TOP_1))
101
       )
102
       (= TOP_A_ex.idJunctions6_TOP TOP_A_ex.idJunctions6_TOP_1)
103
       )
104
  (TOP_A_ex TOP_A_ex.idJunctions6_TOP_1 TOP_A_ex.isInner TOP_A_ex.idJunctions6_TOP)
105
))
106

    
107
; TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action
108
(declare-var TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y_1 Int)
109
(declare-var TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y Int)
110
(declare-rel TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action (Int Int))
111
(rule (=> 
112
  (= TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y (+ TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y_1 1000))
113
  (TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y_1 TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action.y)
114
))
115

    
116
; TOP_B_ex
117
(declare-var TOP_B_ex.idJunctions6_TOP_1 Int)
118
(declare-var TOP_B_ex.isInner Bool)
119
(declare-var TOP_B_ex.idJunctions6_TOP Int)
120
(declare-var TOP_B_ex.idJunctions6_TOP_2 Int)
121
(declare-rel TOP_B_ex (Int Bool Int))
122
(rule (=> 
123
  (and (and (or (not (= (not TOP_B_ex.isInner) true))
124
               (= TOP_B_ex.idJunctions6_TOP_2 0))
125
            (or (not (= (not TOP_B_ex.isInner) false))
126
               (= TOP_B_ex.idJunctions6_TOP_2 TOP_B_ex.idJunctions6_TOP_1))
127
       )
128
       (= TOP_B_ex.idJunctions6_TOP TOP_B_ex.idJunctions6_TOP_1)
129
       )
130
  (TOP_B_ex TOP_B_ex.idJunctions6_TOP_1 TOP_B_ex.isInner TOP_B_ex.idJunctions6_TOP)
131
))
132

    
133
; Junctions6_TOP_en
134
(declare-var Junctions6_TOP_en.idJunctions6_TOP_1 Int)
135
(declare-var Junctions6_TOP_en.idJunctions6_Junctions6_1 Int)
136
(declare-var Junctions6_TOP_en.x Int)
137
(declare-var Junctions6_TOP_en.y_1 Int)
138
(declare-var Junctions6_TOP_en.isInner Bool)
139
(declare-var Junctions6_TOP_en.idJunctions6_TOP Int)
140
(declare-var Junctions6_TOP_en.idJunctions6_Junctions6 Int)
141
(declare-var Junctions6_TOP_en.y Int)
142
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_1 Bool)
143
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_10 Bool)
144
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_11 Bool)
145
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_12 Int)
146
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_13 Int)
147
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_2 Bool)
148
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_3 Bool)
149
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_4 Bool)
150
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_5 Bool)
151
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_6 Int)
152
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_7 Int)
153
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_8 Int)
154
(declare-var Junctions6_TOP_en.__Junctions6_TOP_en_9 Int)
155
(declare-var Junctions6_TOP_en.idJunctions6_Junctions6_3 Int)
156
(declare-var Junctions6_TOP_en.idJunctions6_Junctions6_4 Int)
157
(declare-var Junctions6_TOP_en.idJunctions6_TOP_2 Int)
158
(declare-var Junctions6_TOP_en.idJunctions6_TOP_3 Int)
159
(declare-var Junctions6_TOP_en.idJunctions6_TOP_4 Int)
160
(declare-var Junctions6_TOP_en.idJunctions6_TOP_5 Int)
161
(declare-var Junctions6_TOP_en.idJunctions6_TOP_6 Int)
162
(declare-var Junctions6_TOP_en.idJunctions6_TOP_7 Int)
163
(declare-var Junctions6_TOP_en.idJunctions6_TOP_8 Int)
164
(declare-var Junctions6_TOP_en.idJunctions6_TOP_9 Int)
165
(declare-var Junctions6_TOP_en.y_2 Int)
166
(declare-var Junctions6_TOP_en.y_3 Int)
167
(declare-var Junctions6_TOP_en.y_4 Int)
168
(declare-var Junctions6_TOP_en.y_5 Int)
169
(declare-rel Junctions6_TOP_en (Int Int Int Int Bool Int Int Int))
170
(rule (=> 
171
  (and (POINT__To__TOP_B_2_Condition_Action Junctions6_TOP_en.y_1
172
                                            Junctions6_TOP_en.__Junctions6_TOP_en_12)
173
       (= Junctions6_TOP_en.__Junctions6_TOP_en_11 (>= Junctions6_TOP_en.x 4))
174
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_11 true))
175
               (= Junctions6_TOP_en.y_3 Junctions6_TOP_en.__Junctions6_TOP_en_12))
176
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_11 false))
177
               (= Junctions6_TOP_en.y_3 Junctions6_TOP_en.y_1))
178
       )
179
       (POINT__To__TOP_A_1_Condition_Action Junctions6_TOP_en.y_1
180
                                            Junctions6_TOP_en.__Junctions6_TOP_en_13)
181
       (= Junctions6_TOP_en.__Junctions6_TOP_en_10 (< Junctions6_TOP_en.x 4))
182
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_10 true))
183
               (= Junctions6_TOP_en.y_2 Junctions6_TOP_en.__Junctions6_TOP_en_13))
184
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_10 false))
185
               (= Junctions6_TOP_en.y_2 Junctions6_TOP_en.y_1))
186
       )
187
       (TOP_D_en Junctions6_TOP_en.idJunctions6_TOP_1
188
                 false
189
                 Junctions6_TOP_en.__Junctions6_TOP_en_6)
190
       (= Junctions6_TOP_en.__Junctions6_TOP_en_5 (= Junctions6_TOP_en.idJunctions6_TOP_1 1300))
191
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_5 true))
192
               (= Junctions6_TOP_en.idJunctions6_TOP_8 Junctions6_TOP_en.__Junctions6_TOP_en_6))
193
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_5 false))
194
               (= Junctions6_TOP_en.idJunctions6_TOP_8 Junctions6_TOP_en.idJunctions6_TOP_1))
195
       )
196
       (TOP_C_en Junctions6_TOP_en.idJunctions6_TOP_1
197
                 false
198
                 Junctions6_TOP_en.__Junctions6_TOP_en_7)
199
       (= Junctions6_TOP_en.__Junctions6_TOP_en_4 (= Junctions6_TOP_en.idJunctions6_TOP_1 1299))
200
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_4 true))
201
               (= Junctions6_TOP_en.idJunctions6_TOP_7 Junctions6_TOP_en.__Junctions6_TOP_en_7))
202
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_4 false))
203
               (= Junctions6_TOP_en.idJunctions6_TOP_7 Junctions6_TOP_en.idJunctions6_TOP_1))
204
       )
205
       (TOP_B_en Junctions6_TOP_en.idJunctions6_TOP_1
206
                 false
207
                 Junctions6_TOP_en.__Junctions6_TOP_en_8)
208
       (= Junctions6_TOP_en.__Junctions6_TOP_en_3 (= Junctions6_TOP_en.idJunctions6_TOP_1 1298))
209
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_3 true))
210
               (= Junctions6_TOP_en.idJunctions6_TOP_6 Junctions6_TOP_en.__Junctions6_TOP_en_8))
211
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_3 false))
212
               (= Junctions6_TOP_en.idJunctions6_TOP_6 Junctions6_TOP_en.idJunctions6_TOP_1))
213
       )
214
       (TOP_A_en Junctions6_TOP_en.idJunctions6_TOP_1
215
                 false
216
                 Junctions6_TOP_en.__Junctions6_TOP_en_9)
217
       (= Junctions6_TOP_en.__Junctions6_TOP_en_2 (= Junctions6_TOP_en.idJunctions6_TOP_1 1297))
218
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_2 true))
219
               (= Junctions6_TOP_en.idJunctions6_TOP_5 Junctions6_TOP_en.__Junctions6_TOP_en_9))
220
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_2 false))
221
               (= Junctions6_TOP_en.idJunctions6_TOP_5 Junctions6_TOP_en.idJunctions6_TOP_1))
222
       )
223
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_11 true))
224
               (= Junctions6_TOP_en.idJunctions6_TOP_3 Junctions6_TOP_en.__Junctions6_TOP_en_8))
225
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_11 false))
226
               (= Junctions6_TOP_en.idJunctions6_TOP_3 Junctions6_TOP_en.idJunctions6_TOP_1))
227
       )
228
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_10 true))
229
               (= Junctions6_TOP_en.idJunctions6_TOP_2 Junctions6_TOP_en.__Junctions6_TOP_en_9))
230
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_10 false))
231
               (= Junctions6_TOP_en.idJunctions6_TOP_2 Junctions6_TOP_en.idJunctions6_TOP_1))
232
       )
233
       (= Junctions6_TOP_en.__Junctions6_TOP_en_1 (= Junctions6_TOP_en.idJunctions6_TOP_1 0))
234
       (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_1 false))
235
               (and (= Junctions6_TOP_en.y_4 Junctions6_TOP_en.y_1)
236
                    (= Junctions6_TOP_en.idJunctions6_TOP_4 Junctions6_TOP_en.idJunctions6_TOP_1)
237
                    (= Junctions6_TOP_en.idJunctions6_Junctions6_3 1301)
238
                    (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_2 false))
239
                            (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_3 false))
240
                                    (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_4 false))
241
                                            (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_5 false))
242
                                                    (and (= Junctions6_TOP_en.y_5 Junctions6_TOP_en.y_1)
243
                                                         (= Junctions6_TOP_en.idJunctions6_TOP_9 Junctions6_TOP_en.idJunctions6_TOP_1)
244
                                                         (= Junctions6_TOP_en.idJunctions6_Junctions6_4 1301)
245
                                                         ))
246
                                                 (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_5 true))
247
                                                    (and (= Junctions6_TOP_en.y_5 Junctions6_TOP_en.y_1)
248
                                                         (= Junctions6_TOP_en.idJunctions6_TOP_9 Junctions6_TOP_en.idJunctions6_TOP_8)
249
                                                         (= Junctions6_TOP_en.idJunctions6_Junctions6_4 Junctions6_TOP_en.idJunctions6_Junctions6_3)
250
                                                         ))
251
                                            ))
252
                                         (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_4 true))
253
                                            (and (= Junctions6_TOP_en.y_5 Junctions6_TOP_en.y_1)
254
                                                 (= Junctions6_TOP_en.idJunctions6_TOP_9 Junctions6_TOP_en.idJunctions6_TOP_7)
255
                                                 (= Junctions6_TOP_en.idJunctions6_Junctions6_4 Junctions6_TOP_en.idJunctions6_Junctions6_3)
256
                                                 ))
257
                                    ))
258
                                 (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_3 true))
259
                                    (and (= Junctions6_TOP_en.y_5 Junctions6_TOP_en.y_1)
260
                                         (= Junctions6_TOP_en.idJunctions6_TOP_9 Junctions6_TOP_en.idJunctions6_TOP_6)
261
                                         (= Junctions6_TOP_en.idJunctions6_Junctions6_4 Junctions6_TOP_en.idJunctions6_Junctions6_3)
262
                                         ))
263
                            ))
264
                         (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_2 true))
265
                            (and (= Junctions6_TOP_en.y_5 Junctions6_TOP_en.y_1)
266
                                 (= Junctions6_TOP_en.idJunctions6_TOP_9 Junctions6_TOP_en.idJunctions6_TOP_5)
267
                                 (= Junctions6_TOP_en.idJunctions6_Junctions6_4 Junctions6_TOP_en.idJunctions6_Junctions6_3)
268
                                 ))
269
                    )
270
                    ))
271
            (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_1 true))
272
               (and (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_10 false))
273
                            (and (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_11 false))
274
                                    (and (= Junctions6_TOP_en.y_4 Junctions6_TOP_en.y_1)
275
                                         (= Junctions6_TOP_en.idJunctions6_TOP_4 Junctions6_TOP_en.idJunctions6_TOP_1)
276
                                         (= Junctions6_TOP_en.idJunctions6_Junctions6_3 1301)
277
                                         ))
278
                                 (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_11 true))
279
                                    (and (= Junctions6_TOP_en.y_4 Junctions6_TOP_en.y_3)
280
                                         (= Junctions6_TOP_en.idJunctions6_TOP_4 Junctions6_TOP_en.idJunctions6_TOP_3)
281
                                         (= Junctions6_TOP_en.idJunctions6_Junctions6_3 1301)
282
                                         ))
283
                            ))
284
                         (or (not (= Junctions6_TOP_en.__Junctions6_TOP_en_10 true))
285
                            (and (= Junctions6_TOP_en.y_4 Junctions6_TOP_en.y_2)
286
                                 (= Junctions6_TOP_en.idJunctions6_TOP_4 Junctions6_TOP_en.idJunctions6_TOP_2)
287
                                 (= Junctions6_TOP_en.idJunctions6_Junctions6_3 1301)
288
                                 ))
289
                    )
290
                    (= Junctions6_TOP_en.y_5 Junctions6_TOP_en.y_4)
291
                    (= Junctions6_TOP_en.idJunctions6_TOP_9 Junctions6_TOP_en.idJunctions6_TOP_4)
292
                    (= Junctions6_TOP_en.idJunctions6_Junctions6_4 Junctions6_TOP_en.idJunctions6_Junctions6_3)
293
                    ))
294
       )
295
       (= Junctions6_TOP_en.y Junctions6_TOP_en.y_5)
296
       (= Junctions6_TOP_en.idJunctions6_TOP Junctions6_TOP_en.idJunctions6_TOP_9)
297
       (= Junctions6_TOP_en.idJunctions6_Junctions6 Junctions6_TOP_en.idJunctions6_Junctions6_4)
298
       )
299
  (Junctions6_TOP_en Junctions6_TOP_en.idJunctions6_TOP_1 Junctions6_TOP_en.idJunctions6_Junctions6_1 Junctions6_TOP_en.x Junctions6_TOP_en.y_1 Junctions6_TOP_en.isInner Junctions6_TOP_en.idJunctions6_TOP Junctions6_TOP_en.idJunctions6_Junctions6 Junctions6_TOP_en.y)
300
))
301

    
302
; TOP_C_ex
303
(declare-var TOP_C_ex.idJunctions6_TOP_1 Int)
304
(declare-var TOP_C_ex.isInner Bool)
305
(declare-var TOP_C_ex.idJunctions6_TOP Int)
306
(declare-var TOP_C_ex.idJunctions6_TOP_2 Int)
307
(declare-rel TOP_C_ex (Int Bool Int))
308
(rule (=> 
309
  (and (and (or (not (= (not TOP_C_ex.isInner) true))
310
               (= TOP_C_ex.idJunctions6_TOP_2 0))
311
            (or (not (= (not TOP_C_ex.isInner) false))
312
               (= TOP_C_ex.idJunctions6_TOP_2 TOP_C_ex.idJunctions6_TOP_1))
313
       )
314
       (= TOP_C_ex.idJunctions6_TOP TOP_C_ex.idJunctions6_TOP_1)
315
       )
316
  (TOP_C_ex TOP_C_ex.idJunctions6_TOP_1 TOP_C_ex.isInner TOP_C_ex.idJunctions6_TOP)
317
))
318

    
319
; TOP_D_ex
320
(declare-var TOP_D_ex.idJunctions6_TOP_1 Int)
321
(declare-var TOP_D_ex.isInner Bool)
322
(declare-var TOP_D_ex.idJunctions6_TOP Int)
323
(declare-var TOP_D_ex.idJunctions6_TOP_2 Int)
324
(declare-rel TOP_D_ex (Int Bool Int))
325
(rule (=> 
326
  (and (and (or (not (= (not TOP_D_ex.isInner) true))
327
               (= TOP_D_ex.idJunctions6_TOP_2 0))
328
            (or (not (= (not TOP_D_ex.isInner) false))
329
               (= TOP_D_ex.idJunctions6_TOP_2 TOP_D_ex.idJunctions6_TOP_1))
330
       )
331
       (= TOP_D_ex.idJunctions6_TOP TOP_D_ex.idJunctions6_TOP_1)
332
       )
333
  (TOP_D_ex TOP_D_ex.idJunctions6_TOP_1 TOP_D_ex.isInner TOP_D_ex.idJunctions6_TOP)
334
))
335

    
336
; junctions6_top__POINTJunctions6_TOP_handler_until
337
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_TOP_1 Int)
338
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.y_1 Int)
339
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_Junctions6_1 Int)
340
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.junctions6_top__restart_in Bool)
341
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.junctions6_top__state_in junctions6_top__type)
342
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_Junctions6_out Int)
343
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_TOP_out Int)
344
(declare-var junctions6_top__POINTJunctions6_TOP_handler_until.y_out Int)
345
(declare-rel junctions6_top__POINTJunctions6_TOP_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
346
(rule (=> 
347
  (and (= junctions6_top__POINTJunctions6_TOP_handler_until.y_out junctions6_top__POINTJunctions6_TOP_handler_until.y_1)
348
       (= junctions6_top__POINTJunctions6_TOP_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
349
       (= junctions6_top__POINTJunctions6_TOP_handler_until.junctions6_top__restart_in false)
350
       (= junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_TOP_out junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_TOP_1)
351
       (= junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_Junctions6_out junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_Junctions6_1)
352
       )
353
  (junctions6_top__POINTJunctions6_TOP_handler_until junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_TOP_1 junctions6_top__POINTJunctions6_TOP_handler_until.y_1 junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_Junctions6_1 junctions6_top__POINTJunctions6_TOP_handler_until.junctions6_top__restart_in junctions6_top__POINTJunctions6_TOP_handler_until.junctions6_top__state_in junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_Junctions6_out junctions6_top__POINTJunctions6_TOP_handler_until.idJunctions6_TOP_out junctions6_top__POINTJunctions6_TOP_handler_until.y_out)
354
))
355

    
356
; junctions6_top__POINTJunctions6_TOP_unless
357
(declare-var junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_in Bool)
358
(declare-var junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_in junctions6_top__type)
359
(declare-var junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 Int)
360
(declare-var junctions6_top__POINTJunctions6_TOP_unless.x Int)
361
(declare-var junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act Bool)
362
(declare-var junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act junctions6_top__type)
363
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_1 Bool)
364
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_2 Bool)
365
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_3 Bool)
366
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_4 Bool)
367
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_5 Bool)
368
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_6 Bool)
369
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_7 Bool)
370
(declare-var junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_8 Bool)
371
(declare-rel junctions6_top__POINTJunctions6_TOP_unless (Bool junctions6_top__type Int Int Bool junctions6_top__type))
372
(rule (=> 
373
  (and (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_8 (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 1298))
374
       (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_7 (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 1297))
375
       (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_6 (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 1300))
376
       (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_5 (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 1299))
377
       (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_4 (and (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 1298) (>= junctions6_top__POINTJunctions6_TOP_unless.x 6)))
378
       (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_3 (and (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 1297) (<= junctions6_top__POINTJunctions6_TOP_unless.x 2)))
379
       (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_2 (and (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 0) (>= junctions6_top__POINTJunctions6_TOP_unless.x 4)))
380
       (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_1 (and (= junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 0) (< junctions6_top__POINTJunctions6_TOP_unless.x 4)))
381
       (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_1 false))
382
               (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_2 false))
383
                       (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_3 false))
384
                               (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_4 false))
385
                                       (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_5 false))
386
                                               (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_6 false))
387
                                                       (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_7 false))
388
                                                               (and (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_8 false))
389
                                                                    (and 
390
                                                                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_5 false))
391
                                                                    (and 
392
                                                                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_6 false))
393
                                                                    (and 
394
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_in)
395
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_in)
396
                                                                    ))
397
                                                                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_6 true))
398
                                                                    (and 
399
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_D_IDL)
400
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
401
                                                                    ))
402
                                                                    ))
403
                                                                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_5 true))
404
                                                                    (and 
405
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_C_IDL)
406
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
407
                                                                    ))
408
                                                                    ))
409
                                                                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_8 true))
410
                                                                    (and 
411
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_B_IDL)
412
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
413
                                                                    ))
414
                                                               ))
415
                                                            (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_7 true))
416
                                                               (and (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_A_IDL)
417
                                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
418
                                                                    ))
419
                                                       ))
420
                                                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_6 true))
421
                                                       (and (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_D__TO__TOP_C_1)
422
                                                            (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
423
                                                            ))
424
                                               ))
425
                                            (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_5 true))
426
                                               (and (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_C__TO__JUNCTIONS6_TOP_1)
427
                                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
428
                                                    ))
429
                                       ))
430
                                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_4 true))
431
                                       (and (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1)
432
                                            (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
433
                                            ))
434
                               ))
435
                            (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_3 true))
436
                               (and (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1)
437
                                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
438
                                    ))
439
                       ))
440
                    (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_2 true))
441
                       (and (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act POINT__TO__TOP_B_2)
442
                            (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
443
                            ))
444
               ))
445
            (or (not (= junctions6_top__POINTJunctions6_TOP_unless.__junctions6_top__POINTJunctions6_TOP_unless_1 true))
446
               (and (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act POINT__TO__TOP_A_1)
447
                    (= junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act true)
448
                    ))
449
       )
450
       )
451
  (junctions6_top__POINTJunctions6_TOP_unless junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_in junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_in junctions6_top__POINTJunctions6_TOP_unless.idJunctions6_TOP_1 junctions6_top__POINTJunctions6_TOP_unless.x junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__restart_act junctions6_top__POINTJunctions6_TOP_unless.junctions6_top__state_act)
452
))
453

    
454
; junctions6_top__POINT__TO__TOP_A_1_handler_until
455
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_1 Int)
456
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.y_1 Int)
457
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_Junctions6_1 Int)
458
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.junctions6_top__restart_in Bool)
459
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.junctions6_top__state_in junctions6_top__type)
460
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_Junctions6_out Int)
461
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_out Int)
462
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.y_out Int)
463
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_2 Int)
464
(declare-var junctions6_top__POINT__TO__TOP_A_1_handler_until.y_2 Int)
465
(declare-rel junctions6_top__POINT__TO__TOP_A_1_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
466
(rule (=> 
467
  (and (POINT__To__TOP_A_1_Condition_Action junctions6_top__POINT__TO__TOP_A_1_handler_until.y_1
468
                                            junctions6_top__POINT__TO__TOP_A_1_handler_until.y_2)
469
       (= junctions6_top__POINT__TO__TOP_A_1_handler_until.y_out junctions6_top__POINT__TO__TOP_A_1_handler_until.y_2)
470
       (= junctions6_top__POINT__TO__TOP_A_1_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
471
       (= junctions6_top__POINT__TO__TOP_A_1_handler_until.junctions6_top__restart_in true)
472
       (TOP_A_en junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_1
473
                 false
474
                 junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_2)
475
       (= junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_out junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_2)
476
       (= junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_Junctions6_out junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_Junctions6_1)
477
       )
478
  (junctions6_top__POINT__TO__TOP_A_1_handler_until junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_1 junctions6_top__POINT__TO__TOP_A_1_handler_until.y_1 junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_Junctions6_1 junctions6_top__POINT__TO__TOP_A_1_handler_until.junctions6_top__restart_in junctions6_top__POINT__TO__TOP_A_1_handler_until.junctions6_top__state_in junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_Junctions6_out junctions6_top__POINT__TO__TOP_A_1_handler_until.idJunctions6_TOP_out junctions6_top__POINT__TO__TOP_A_1_handler_until.y_out)
479
))
480

    
481
; junctions6_top__POINT__TO__TOP_A_1_unless
482
(declare-var junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__restart_in Bool)
483
(declare-var junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__state_in junctions6_top__type)
484
(declare-var junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__restart_act Bool)
485
(declare-var junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__state_act junctions6_top__type)
486
(declare-rel junctions6_top__POINT__TO__TOP_A_1_unless (Bool junctions6_top__type Bool junctions6_top__type))
487
(rule (=> 
488
  (and (= junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__state_act junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__state_in)
489
       (= junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__restart_act junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__restart_in)
490
       )
491
  (junctions6_top__POINT__TO__TOP_A_1_unless junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__restart_in junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__state_in junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__restart_act junctions6_top__POINT__TO__TOP_A_1_unless.junctions6_top__state_act)
492
))
493

    
494
; junctions6_top__POINT__TO__TOP_B_2_handler_until
495
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_1 Int)
496
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.y_1 Int)
497
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_Junctions6_1 Int)
498
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.junctions6_top__restart_in Bool)
499
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.junctions6_top__state_in junctions6_top__type)
500
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_Junctions6_out Int)
501
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_out Int)
502
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.y_out Int)
503
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_2 Int)
504
(declare-var junctions6_top__POINT__TO__TOP_B_2_handler_until.y_2 Int)
505
(declare-rel junctions6_top__POINT__TO__TOP_B_2_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
506
(rule (=> 
507
  (and (POINT__To__TOP_B_2_Condition_Action junctions6_top__POINT__TO__TOP_B_2_handler_until.y_1
508
                                            junctions6_top__POINT__TO__TOP_B_2_handler_until.y_2)
509
       (= junctions6_top__POINT__TO__TOP_B_2_handler_until.y_out junctions6_top__POINT__TO__TOP_B_2_handler_until.y_2)
510
       (= junctions6_top__POINT__TO__TOP_B_2_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
511
       (= junctions6_top__POINT__TO__TOP_B_2_handler_until.junctions6_top__restart_in true)
512
       (TOP_B_en junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_1
513
                 false
514
                 junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_2)
515
       (= junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_out junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_2)
516
       (= junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_Junctions6_out junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_Junctions6_1)
517
       )
518
  (junctions6_top__POINT__TO__TOP_B_2_handler_until junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_1 junctions6_top__POINT__TO__TOP_B_2_handler_until.y_1 junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_Junctions6_1 junctions6_top__POINT__TO__TOP_B_2_handler_until.junctions6_top__restart_in junctions6_top__POINT__TO__TOP_B_2_handler_until.junctions6_top__state_in junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_Junctions6_out junctions6_top__POINT__TO__TOP_B_2_handler_until.idJunctions6_TOP_out junctions6_top__POINT__TO__TOP_B_2_handler_until.y_out)
519
))
520

    
521
; junctions6_top__POINT__TO__TOP_B_2_unless
522
(declare-var junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__restart_in Bool)
523
(declare-var junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__state_in junctions6_top__type)
524
(declare-var junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__restart_act Bool)
525
(declare-var junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__state_act junctions6_top__type)
526
(declare-rel junctions6_top__POINT__TO__TOP_B_2_unless (Bool junctions6_top__type Bool junctions6_top__type))
527
(rule (=> 
528
  (and (= junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__state_act junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__state_in)
529
       (= junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__restart_act junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__restart_in)
530
       )
531
  (junctions6_top__POINT__TO__TOP_B_2_unless junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__restart_in junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__state_in junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__restart_act junctions6_top__POINT__TO__TOP_B_2_unless.junctions6_top__state_act)
532
))
533

    
534
; junctions6_top__TOP_A_IDL_handler_until
535
(declare-var junctions6_top__TOP_A_IDL_handler_until.idJunctions6_TOP_1 Int)
536
(declare-var junctions6_top__TOP_A_IDL_handler_until.y_1 Int)
537
(declare-var junctions6_top__TOP_A_IDL_handler_until.idJunctions6_Junctions6_1 Int)
538
(declare-var junctions6_top__TOP_A_IDL_handler_until.junctions6_top__restart_in Bool)
539
(declare-var junctions6_top__TOP_A_IDL_handler_until.junctions6_top__state_in junctions6_top__type)
540
(declare-var junctions6_top__TOP_A_IDL_handler_until.idJunctions6_Junctions6_out Int)
541
(declare-var junctions6_top__TOP_A_IDL_handler_until.idJunctions6_TOP_out Int)
542
(declare-var junctions6_top__TOP_A_IDL_handler_until.y_out Int)
543
(declare-rel junctions6_top__TOP_A_IDL_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
544
(rule (=> 
545
  (and (= junctions6_top__TOP_A_IDL_handler_until.y_out junctions6_top__TOP_A_IDL_handler_until.y_1)
546
       (= junctions6_top__TOP_A_IDL_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
547
       (= junctions6_top__TOP_A_IDL_handler_until.junctions6_top__restart_in true)
548
       (= junctions6_top__TOP_A_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_A_IDL_handler_until.idJunctions6_TOP_1)
549
       (= junctions6_top__TOP_A_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_A_IDL_handler_until.idJunctions6_Junctions6_1)
550
       )
551
  (junctions6_top__TOP_A_IDL_handler_until junctions6_top__TOP_A_IDL_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_A_IDL_handler_until.y_1 junctions6_top__TOP_A_IDL_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_A_IDL_handler_until.junctions6_top__restart_in junctions6_top__TOP_A_IDL_handler_until.junctions6_top__state_in junctions6_top__TOP_A_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_A_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_A_IDL_handler_until.y_out)
552
))
553

    
554
; junctions6_top__TOP_A_IDL_unless
555
(declare-var junctions6_top__TOP_A_IDL_unless.junctions6_top__restart_in Bool)
556
(declare-var junctions6_top__TOP_A_IDL_unless.junctions6_top__state_in junctions6_top__type)
557
(declare-var junctions6_top__TOP_A_IDL_unless.junctions6_top__restart_act Bool)
558
(declare-var junctions6_top__TOP_A_IDL_unless.junctions6_top__state_act junctions6_top__type)
559
(declare-rel junctions6_top__TOP_A_IDL_unless (Bool junctions6_top__type Bool junctions6_top__type))
560
(rule (=> 
561
  (and (= junctions6_top__TOP_A_IDL_unless.junctions6_top__state_act junctions6_top__TOP_A_IDL_unless.junctions6_top__state_in)
562
       (= junctions6_top__TOP_A_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_A_IDL_unless.junctions6_top__restart_in)
563
       )
564
  (junctions6_top__TOP_A_IDL_unless junctions6_top__TOP_A_IDL_unless.junctions6_top__restart_in junctions6_top__TOP_A_IDL_unless.junctions6_top__state_in junctions6_top__TOP_A_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_A_IDL_unless.junctions6_top__state_act)
565
))
566

    
567
; junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until
568
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1 Int)
569
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x Int)
570
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1 Int)
571
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_1 Int)
572
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__restart_in Bool)
573
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__state_in junctions6_top__type)
574
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_out Int)
575
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_out Int)
576
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_out Int)
577
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 Bool)
578
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 Bool)
579
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_3 Int)
580
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4 Int)
581
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_5 Int)
582
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_6 Int)
583
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_7 Int)
584
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP Int)
585
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2 Int)
586
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3 Int)
587
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4 Int)
588
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5 Int)
589
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y Int)
590
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2 Int)
591
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3 Int)
592
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4 Int)
593
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5 Int)
594
(declare-rel junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until (Int Int Int Int Bool junctions6_top__type Int Int Int))
595
(rule (=> 
596
  (and (TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action 
597
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1
598
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4)
599
       (Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action 
600
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4
601
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_5)
602
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 (= (mod junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x 3) 1))
603
       (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
604
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_5))
605
            (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
606
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4))
607
       )
608
       (TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action 
609
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1
610
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2)
611
       (Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action 
612
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2
613
       junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_7)
614
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 (= (mod junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x 3) 0))
615
       (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 false))
616
               (and (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2)
617
                    (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
618
                            (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5))
619
                         (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
620
                            (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4))
621
                    )
622
                    ))
623
            (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 true))
624
               (and (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_7)
625
                    (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3)
626
                    ))
627
       )
628
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_out junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y)
629
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
630
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__restart_in true)
631
       (TOP_A_ex junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1
632
                 false
633
                 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4)
634
       (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
635
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4))
636
            (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
637
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1))
638
       )
639
       (TOP_C_en junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4
640
                 false
641
                 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_3)
642
       (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
643
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_3))
644
            (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
645
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4))
646
       )
647
       (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 true))
648
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4))
649
            (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 false))
650
               (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1))
651
       )
652
       (TOP_D_en junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2
653
                 false
654
                 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_6)
655
       (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 false))
656
               (and (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2)
657
                    (and (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
658
                            (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5))
659
                         (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
660
                            (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1))
661
                    )
662
                    ))
663
            (or (not (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 true))
664
               (and (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_6)
665
                    (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3)
666
                    ))
667
       )
668
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP)
669
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_1)
670
       )
671
  (junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__restart_in junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__state_in junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_out)
672
))
673

    
674
; junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless
675
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_in Bool)
676
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_in junctions6_top__type)
677
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_act Bool)
678
(declare-var junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_act junctions6_top__type)
679
(declare-rel junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless (Bool junctions6_top__type Bool junctions6_top__type))
680
(rule (=> 
681
  (and (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_act junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_in)
682
       (= junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_act junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_in)
683
       )
684
  (junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_in junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_in junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_act junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_act)
685
))
686

    
687
; junctions6_top__TOP_B_IDL_handler_until
688
(declare-var junctions6_top__TOP_B_IDL_handler_until.idJunctions6_TOP_1 Int)
689
(declare-var junctions6_top__TOP_B_IDL_handler_until.y_1 Int)
690
(declare-var junctions6_top__TOP_B_IDL_handler_until.idJunctions6_Junctions6_1 Int)
691
(declare-var junctions6_top__TOP_B_IDL_handler_until.junctions6_top__restart_in Bool)
692
(declare-var junctions6_top__TOP_B_IDL_handler_until.junctions6_top__state_in junctions6_top__type)
693
(declare-var junctions6_top__TOP_B_IDL_handler_until.idJunctions6_Junctions6_out Int)
694
(declare-var junctions6_top__TOP_B_IDL_handler_until.idJunctions6_TOP_out Int)
695
(declare-var junctions6_top__TOP_B_IDL_handler_until.y_out Int)
696
(declare-rel junctions6_top__TOP_B_IDL_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
697
(rule (=> 
698
  (and (= junctions6_top__TOP_B_IDL_handler_until.y_out junctions6_top__TOP_B_IDL_handler_until.y_1)
699
       (= junctions6_top__TOP_B_IDL_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
700
       (= junctions6_top__TOP_B_IDL_handler_until.junctions6_top__restart_in true)
701
       (= junctions6_top__TOP_B_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_B_IDL_handler_until.idJunctions6_TOP_1)
702
       (= junctions6_top__TOP_B_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_B_IDL_handler_until.idJunctions6_Junctions6_1)
703
       )
704
  (junctions6_top__TOP_B_IDL_handler_until junctions6_top__TOP_B_IDL_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_B_IDL_handler_until.y_1 junctions6_top__TOP_B_IDL_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_B_IDL_handler_until.junctions6_top__restart_in junctions6_top__TOP_B_IDL_handler_until.junctions6_top__state_in junctions6_top__TOP_B_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_B_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_B_IDL_handler_until.y_out)
705
))
706

    
707
; junctions6_top__TOP_B_IDL_unless
708
(declare-var junctions6_top__TOP_B_IDL_unless.junctions6_top__restart_in Bool)
709
(declare-var junctions6_top__TOP_B_IDL_unless.junctions6_top__state_in junctions6_top__type)
710
(declare-var junctions6_top__TOP_B_IDL_unless.junctions6_top__restart_act Bool)
711
(declare-var junctions6_top__TOP_B_IDL_unless.junctions6_top__state_act junctions6_top__type)
712
(declare-rel junctions6_top__TOP_B_IDL_unless (Bool junctions6_top__type Bool junctions6_top__type))
713
(rule (=> 
714
  (and (= junctions6_top__TOP_B_IDL_unless.junctions6_top__state_act junctions6_top__TOP_B_IDL_unless.junctions6_top__state_in)
715
       (= junctions6_top__TOP_B_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_B_IDL_unless.junctions6_top__restart_in)
716
       )
717
  (junctions6_top__TOP_B_IDL_unless junctions6_top__TOP_B_IDL_unless.junctions6_top__restart_in junctions6_top__TOP_B_IDL_unless.junctions6_top__state_in junctions6_top__TOP_B_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_B_IDL_unless.junctions6_top__state_act)
718
))
719

    
720
; junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until
721
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1 Int)
722
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x Int)
723
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1 Int)
724
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_1 Int)
725
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__restart_in Bool)
726
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__state_in junctions6_top__type)
727
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_out Int)
728
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_out Int)
729
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_out Int)
730
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 Bool)
731
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 Bool)
732
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_3 Int)
733
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4 Int)
734
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_5 Int)
735
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_6 Int)
736
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_7 Int)
737
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP Int)
738
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2 Int)
739
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3 Int)
740
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4 Int)
741
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5 Int)
742
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y Int)
743
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2 Int)
744
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3 Int)
745
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4 Int)
746
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5 Int)
747
(declare-rel junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until (Int Int Int Int Bool junctions6_top__type Int Int Int))
748
(rule (=> 
749
  (and (TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action 
750
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1
751
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4)
752
       (Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action 
753
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4
754
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_5)
755
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 (= (mod junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x 3) 1))
756
       (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
757
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_5))
758
            (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
759
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4))
760
       )
761
       (TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action 
762
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1
763
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2)
764
       (Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action 
765
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2
766
       junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_7)
767
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 (= (mod junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x 3) 0))
768
       (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 false))
769
               (and (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_2)
770
                    (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
771
                            (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_5))
772
                         (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
773
                            (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_4))
774
                    )
775
                    ))
776
            (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 true))
777
               (and (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_7)
778
                    (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_3)
779
                    ))
780
       )
781
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_out junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y)
782
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
783
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__restart_in true)
784
       (TOP_B_ex junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1
785
                 false
786
                 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4)
787
       (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
788
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4))
789
            (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
790
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1))
791
       )
792
       (TOP_C_en junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4
793
                 false
794
                 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_3)
795
       (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
796
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_3))
797
            (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
798
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_4))
799
       )
800
       (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 true))
801
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_4))
802
            (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 false))
803
               (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1))
804
       )
805
       (TOP_D_en junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2
806
                 false
807
                 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_6)
808
       (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 false))
809
               (and (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_2)
810
                    (and (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 true))
811
                            (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_5))
812
                         (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_2 false))
813
                            (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1))
814
                    )
815
                    ))
816
            (or (not (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_1 true))
817
               (and (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.__junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until_6)
818
                    (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_3)
819
                    ))
820
       )
821
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP)
822
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_1)
823
       )
824
  (junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.x junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_1 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__restart_in junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.junctions6_top__state_in junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until.y_out)
825
))
826

    
827
; junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless
828
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_in Bool)
829
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_in junctions6_top__type)
830
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_act Bool)
831
(declare-var junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_act junctions6_top__type)
832
(declare-rel junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless (Bool junctions6_top__type Bool junctions6_top__type))
833
(rule (=> 
834
  (and (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_act junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_in)
835
       (= junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_act junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_in)
836
       )
837
  (junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_in junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_in junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__restart_act junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless.junctions6_top__state_act)
838
))
839

    
840
; junctions6_top__TOP_C_IDL_handler_until
841
(declare-var junctions6_top__TOP_C_IDL_handler_until.idJunctions6_TOP_1 Int)
842
(declare-var junctions6_top__TOP_C_IDL_handler_until.y_1 Int)
843
(declare-var junctions6_top__TOP_C_IDL_handler_until.idJunctions6_Junctions6_1 Int)
844
(declare-var junctions6_top__TOP_C_IDL_handler_until.junctions6_top__restart_in Bool)
845
(declare-var junctions6_top__TOP_C_IDL_handler_until.junctions6_top__state_in junctions6_top__type)
846
(declare-var junctions6_top__TOP_C_IDL_handler_until.idJunctions6_Junctions6_out Int)
847
(declare-var junctions6_top__TOP_C_IDL_handler_until.idJunctions6_TOP_out Int)
848
(declare-var junctions6_top__TOP_C_IDL_handler_until.y_out Int)
849
(declare-rel junctions6_top__TOP_C_IDL_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
850
(rule (=> 
851
  (and (= junctions6_top__TOP_C_IDL_handler_until.y_out junctions6_top__TOP_C_IDL_handler_until.y_1)
852
       (= junctions6_top__TOP_C_IDL_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
853
       (= junctions6_top__TOP_C_IDL_handler_until.junctions6_top__restart_in true)
854
       (= junctions6_top__TOP_C_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_C_IDL_handler_until.idJunctions6_TOP_1)
855
       (= junctions6_top__TOP_C_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_C_IDL_handler_until.idJunctions6_Junctions6_1)
856
       )
857
  (junctions6_top__TOP_C_IDL_handler_until junctions6_top__TOP_C_IDL_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_C_IDL_handler_until.y_1 junctions6_top__TOP_C_IDL_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_C_IDL_handler_until.junctions6_top__restart_in junctions6_top__TOP_C_IDL_handler_until.junctions6_top__state_in junctions6_top__TOP_C_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_C_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_C_IDL_handler_until.y_out)
858
))
859

    
860
; junctions6_top__TOP_C_IDL_unless
861
(declare-var junctions6_top__TOP_C_IDL_unless.junctions6_top__restart_in Bool)
862
(declare-var junctions6_top__TOP_C_IDL_unless.junctions6_top__state_in junctions6_top__type)
863
(declare-var junctions6_top__TOP_C_IDL_unless.junctions6_top__restart_act Bool)
864
(declare-var junctions6_top__TOP_C_IDL_unless.junctions6_top__state_act junctions6_top__type)
865
(declare-rel junctions6_top__TOP_C_IDL_unless (Bool junctions6_top__type Bool junctions6_top__type))
866
(rule (=> 
867
  (and (= junctions6_top__TOP_C_IDL_unless.junctions6_top__state_act junctions6_top__TOP_C_IDL_unless.junctions6_top__state_in)
868
       (= junctions6_top__TOP_C_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_C_IDL_unless.junctions6_top__restart_in)
869
       )
870
  (junctions6_top__TOP_C_IDL_unless junctions6_top__TOP_C_IDL_unless.junctions6_top__restart_in junctions6_top__TOP_C_IDL_unless.junctions6_top__state_in junctions6_top__TOP_C_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_C_IDL_unless.junctions6_top__state_act)
871
))
872

    
873
; junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until
874
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_1 Int)
875
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.x Int)
876
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_1 Int)
877
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_1 Int)
878
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_top__restart_in Bool)
879
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_top__state_in junctions6_top__type)
880
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_out Int)
881
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_out Int)
882
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_out Int)
883
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_2 Int)
884
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_2 Int)
885
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_4 Int)
886
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_2 Int)
887
(declare-rel junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until (Int Int Int Int Bool junctions6_top__type Int Int Int))
888
(rule (=> 
889
  (and (Junctions6_TOP_en 0
890
                          junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_1
891
                          junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.x
892
                          junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_1
893
                          true
894
                          junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_4
895
                          junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_2
896
                          junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_2)
897
       (= junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_out junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_2)
898
       (= junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
899
       (= junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_top__restart_in true)
900
       (= junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_4)
901
       (TOP_C_ex junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_1
902
                 false
903
                 junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_2)
904
       (= junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_2)
905
       )
906
  (junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.x junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_1 junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_top__restart_in junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_top__state_in junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until.y_out)
907
))
908

    
909
; junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless
910
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__restart_in Bool)
911
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__state_in junctions6_top__type)
912
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__restart_act Bool)
913
(declare-var junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__state_act junctions6_top__type)
914
(declare-rel junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless (Bool junctions6_top__type Bool junctions6_top__type))
915
(rule (=> 
916
  (and (= junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__state_act junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__state_in)
917
       (= junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__restart_act junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__restart_in)
918
       )
919
  (junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__restart_in junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__state_in junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__restart_act junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless.junctions6_top__state_act)
920
))
921

    
922
; junctions6_top__TOP_D_IDL_handler_until
923
(declare-var junctions6_top__TOP_D_IDL_handler_until.idJunctions6_TOP_1 Int)
924
(declare-var junctions6_top__TOP_D_IDL_handler_until.y_1 Int)
925
(declare-var junctions6_top__TOP_D_IDL_handler_until.idJunctions6_Junctions6_1 Int)
926
(declare-var junctions6_top__TOP_D_IDL_handler_until.junctions6_top__restart_in Bool)
927
(declare-var junctions6_top__TOP_D_IDL_handler_until.junctions6_top__state_in junctions6_top__type)
928
(declare-var junctions6_top__TOP_D_IDL_handler_until.idJunctions6_Junctions6_out Int)
929
(declare-var junctions6_top__TOP_D_IDL_handler_until.idJunctions6_TOP_out Int)
930
(declare-var junctions6_top__TOP_D_IDL_handler_until.y_out Int)
931
(declare-rel junctions6_top__TOP_D_IDL_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
932
(rule (=> 
933
  (and (= junctions6_top__TOP_D_IDL_handler_until.y_out junctions6_top__TOP_D_IDL_handler_until.y_1)
934
       (= junctions6_top__TOP_D_IDL_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
935
       (= junctions6_top__TOP_D_IDL_handler_until.junctions6_top__restart_in true)
936
       (= junctions6_top__TOP_D_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_D_IDL_handler_until.idJunctions6_TOP_1)
937
       (= junctions6_top__TOP_D_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_D_IDL_handler_until.idJunctions6_Junctions6_1)
938
       )
939
  (junctions6_top__TOP_D_IDL_handler_until junctions6_top__TOP_D_IDL_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_D_IDL_handler_until.y_1 junctions6_top__TOP_D_IDL_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_D_IDL_handler_until.junctions6_top__restart_in junctions6_top__TOP_D_IDL_handler_until.junctions6_top__state_in junctions6_top__TOP_D_IDL_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_D_IDL_handler_until.idJunctions6_TOP_out junctions6_top__TOP_D_IDL_handler_until.y_out)
940
))
941

    
942
; junctions6_top__TOP_D_IDL_unless
943
(declare-var junctions6_top__TOP_D_IDL_unless.junctions6_top__restart_in Bool)
944
(declare-var junctions6_top__TOP_D_IDL_unless.junctions6_top__state_in junctions6_top__type)
945
(declare-var junctions6_top__TOP_D_IDL_unless.junctions6_top__restart_act Bool)
946
(declare-var junctions6_top__TOP_D_IDL_unless.junctions6_top__state_act junctions6_top__type)
947
(declare-rel junctions6_top__TOP_D_IDL_unless (Bool junctions6_top__type Bool junctions6_top__type))
948
(rule (=> 
949
  (and (= junctions6_top__TOP_D_IDL_unless.junctions6_top__state_act junctions6_top__TOP_D_IDL_unless.junctions6_top__state_in)
950
       (= junctions6_top__TOP_D_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_D_IDL_unless.junctions6_top__restart_in)
951
       )
952
  (junctions6_top__TOP_D_IDL_unless junctions6_top__TOP_D_IDL_unless.junctions6_top__restart_in junctions6_top__TOP_D_IDL_unless.junctions6_top__state_in junctions6_top__TOP_D_IDL_unless.junctions6_top__restart_act junctions6_top__TOP_D_IDL_unless.junctions6_top__state_act)
953
))
954

    
955
; junctions6_top__TOP_D__TO__TOP_C_1_handler_until
956
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_1 Int)
957
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.y_1 Int)
958
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_Junctions6_1 Int)
959
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.junctions6_top__restart_in Bool)
960
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.junctions6_top__state_in junctions6_top__type)
961
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_Junctions6_out Int)
962
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_out Int)
963
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.y_out Int)
964
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_2 Int)
965
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_3 Int)
966
(declare-rel junctions6_top__TOP_D__TO__TOP_C_1_handler_until (Int Int Int Bool junctions6_top__type Int Int Int))
967
(rule (=> 
968
  (and (= junctions6_top__TOP_D__TO__TOP_C_1_handler_until.y_out junctions6_top__TOP_D__TO__TOP_C_1_handler_until.y_1)
969
       (= junctions6_top__TOP_D__TO__TOP_C_1_handler_until.junctions6_top__state_in POINTJunctions6_TOP)
970
       (= junctions6_top__TOP_D__TO__TOP_C_1_handler_until.junctions6_top__restart_in true)
971
       (TOP_D_ex junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_1
972
                 false
973
                 junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_2)
974
       (TOP_C_en junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_2
975
                 false
976
                 junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_3)
977
       (= junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_3)
978
       (= junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_Junctions6_1)
979
       )
980
  (junctions6_top__TOP_D__TO__TOP_C_1_handler_until junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_1 junctions6_top__TOP_D__TO__TOP_C_1_handler_until.y_1 junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_Junctions6_1 junctions6_top__TOP_D__TO__TOP_C_1_handler_until.junctions6_top__restart_in junctions6_top__TOP_D__TO__TOP_C_1_handler_until.junctions6_top__state_in junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_Junctions6_out junctions6_top__TOP_D__TO__TOP_C_1_handler_until.idJunctions6_TOP_out junctions6_top__TOP_D__TO__TOP_C_1_handler_until.y_out)
981
))
982

    
983
; junctions6_top__TOP_D__TO__TOP_C_1_unless
984
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__restart_in Bool)
985
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__state_in junctions6_top__type)
986
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__restart_act Bool)
987
(declare-var junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__state_act junctions6_top__type)
988
(declare-rel junctions6_top__TOP_D__TO__TOP_C_1_unless (Bool junctions6_top__type Bool junctions6_top__type))
989
(rule (=> 
990
  (and (= junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__state_act junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__state_in)
991
       (= junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__restart_act junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__restart_in)
992
       )
993
  (junctions6_top__TOP_D__TO__TOP_C_1_unless junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__restart_in junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__state_in junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__restart_act junctions6_top__TOP_D__TO__TOP_C_1_unless.junctions6_top__state_act)
994
))
995

    
996
; Junctions6_TOP_node
997
(declare-var Junctions6_TOP_node.idJunctions6_TOP_1 Int)
998
(declare-var Junctions6_TOP_node.x Int)
999
(declare-var Junctions6_TOP_node.y_1 Int)
1000
(declare-var Junctions6_TOP_node.idJunctions6_Junctions6_1 Int)
1001
(declare-var Junctions6_TOP_node.idJunctions6_TOP Int)
1002
(declare-var Junctions6_TOP_node.y Int)
1003
(declare-var Junctions6_TOP_node.idJunctions6_Junctions6 Int)
1004
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_79_c Bool)
1005
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_80_c junctions6_top__type)
1006
(declare-var Junctions6_TOP_node.ni_7._arrow._first_c Bool)
1007
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_79_m Bool)
1008
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_80_m junctions6_top__type)
1009
(declare-var Junctions6_TOP_node.ni_7._arrow._first_m Bool)
1010
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_79_x Bool)
1011
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_80_x junctions6_top__type)
1012
(declare-var Junctions6_TOP_node.ni_7._arrow._first_x Bool)
1013
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_1 Bool)
1014
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_10 junctions6_top__type)
1015
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_11 Bool)
1016
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_12 junctions6_top__type)
1017
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_13 Bool)
1018
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_14 junctions6_top__type)
1019
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_15 Bool)
1020
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_16 junctions6_top__type)
1021
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_17 Bool)
1022
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_18 junctions6_top__type)
1023
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_19 Bool)
1024
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_2 junctions6_top__type)
1025
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_20 junctions6_top__type)
1026
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_21 Bool)
1027
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_22 junctions6_top__type)
1028
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_23 Bool)
1029
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_24 junctions6_top__type)
1030
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_25 Int)
1031
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_26 Int)
1032
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_27 Int)
1033
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_28 Bool)
1034
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_29 junctions6_top__type)
1035
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_3 Bool)
1036
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_30 Int)
1037
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_31 Int)
1038
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_32 Int)
1039
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_33 Bool)
1040
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_34 junctions6_top__type)
1041
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_35 Int)
1042
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_36 Int)
1043
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_37 Int)
1044
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_38 Bool)
1045
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_39 junctions6_top__type)
1046
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_4 junctions6_top__type)
1047
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_40 Int)
1048
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_41 Int)
1049
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_42 Int)
1050
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_43 Bool)
1051
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_44 junctions6_top__type)
1052
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_45 Int)
1053
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_46 Int)
1054
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_47 Int)
1055
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_48 Bool)
1056
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_49 junctions6_top__type)
1057
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_5 Bool)
1058
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_50 Int)
1059
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_51 Int)
1060
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_52 Int)
1061
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_53 Bool)
1062
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_54 junctions6_top__type)
1063
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_55 Int)
1064
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_56 Int)
1065
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_57 Int)
1066
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_58 Bool)
1067
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_59 junctions6_top__type)
1068
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_6 junctions6_top__type)
1069
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_60 Int)
1070
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_61 Int)
1071
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_62 Int)
1072
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_63 Bool)
1073
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_64 junctions6_top__type)
1074
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_65 Int)
1075
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_66 Int)
1076
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_67 Int)
1077
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_68 Bool)
1078
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_69 junctions6_top__type)
1079
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_7 Bool)
1080
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_70 Int)
1081
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_71 Int)
1082
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_72 Int)
1083
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_73 Bool)
1084
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_74 junctions6_top__type)
1085
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_75 Int)
1086
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_76 Int)
1087
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_77 Int)
1088
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_78 Bool)
1089
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_8 junctions6_top__type)
1090
(declare-var Junctions6_TOP_node.__Junctions6_TOP_node_9 Bool)
1091
(declare-var Junctions6_TOP_node.junctions6_top__next_restart_in Bool)
1092
(declare-var Junctions6_TOP_node.junctions6_top__next_state_in junctions6_top__type)
1093
(declare-var Junctions6_TOP_node.junctions6_top__restart_act Bool)
1094
(declare-var Junctions6_TOP_node.junctions6_top__restart_in Bool)
1095
(declare-var Junctions6_TOP_node.junctions6_top__state_act junctions6_top__type)
1096
(declare-var Junctions6_TOP_node.junctions6_top__state_in junctions6_top__type)
1097
(declare-rel Junctions6_TOP_node_reset (Bool junctions6_top__type Bool Bool junctions6_top__type Bool))
1098
(declare-rel Junctions6_TOP_node_step (Int Int Int Int Int Int Int Bool junctions6_top__type Bool Bool junctions6_top__type Bool))
1099

    
1100
(rule (=> 
1101
  (and 
1102
       (= Junctions6_TOP_node.__Junctions6_TOP_node_79_m Junctions6_TOP_node.__Junctions6_TOP_node_79_c)
1103
       (= Junctions6_TOP_node.__Junctions6_TOP_node_80_m Junctions6_TOP_node.__Junctions6_TOP_node_80_c)
1104
       (= Junctions6_TOP_node.ni_7._arrow._first_m true)
1105
  )
1106
  (Junctions6_TOP_node_reset Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1107
                             Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1108
                             Junctions6_TOP_node.ni_7._arrow._first_c
1109
                             Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1110
                             Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1111
                             Junctions6_TOP_node.ni_7._arrow._first_m)
1112
))
1113

    
1114
(rule (=> 
1115
  (and (= Junctions6_TOP_node.ni_7._arrow._first_m Junctions6_TOP_node.ni_7._arrow._first_c)
1116
       (and (= Junctions6_TOP_node.__Junctions6_TOP_node_78 (ite Junctions6_TOP_node.ni_7._arrow._first_m true false))
1117
            (= Junctions6_TOP_node.ni_7._arrow._first_x false))
1118
       (and (or (not (= Junctions6_TOP_node.__Junctions6_TOP_node_78 false))
1119
               (and (= Junctions6_TOP_node.junctions6_top__state_in Junctions6_TOP_node.__Junctions6_TOP_node_80_c)
1120
                    (= Junctions6_TOP_node.junctions6_top__restart_in Junctions6_TOP_node.__Junctions6_TOP_node_79_c)
1121
                    ))
1122
            (or (not (= Junctions6_TOP_node.__Junctions6_TOP_node_78 true))
1123
               (and (= Junctions6_TOP_node.junctions6_top__state_in POINTJunctions6_TOP)
1124
                    (= Junctions6_TOP_node.junctions6_top__restart_in false)
1125
                    ))
1126
       )
1127
       (and (or (not (= Junctions6_TOP_node.junctions6_top__state_in POINTJunctions6_TOP))
1128
               (and (junctions6_top__POINTJunctions6_TOP_unless Junctions6_TOP_node.junctions6_top__restart_in
1129
                                                                Junctions6_TOP_node.junctions6_top__state_in
1130
                                                                Junctions6_TOP_node.idJunctions6_TOP_1
1131
                                                                Junctions6_TOP_node.x
1132
                                                                Junctions6_TOP_node.__Junctions6_TOP_node_21
1133
                                                                Junctions6_TOP_node.__Junctions6_TOP_node_22)
1134
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_22)
1135
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_21)
1136
                    ))
1137
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in POINT__TO__TOP_A_1))
1138
               (and (junctions6_top__POINT__TO__TOP_A_1_unless Junctions6_TOP_node.junctions6_top__restart_in
1139
                                                               Junctions6_TOP_node.junctions6_top__state_in
1140
                                                               Junctions6_TOP_node.__Junctions6_TOP_node_19
1141
                                                               Junctions6_TOP_node.__Junctions6_TOP_node_20)
1142
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_20)
1143
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_19)
1144
                    ))
1145
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in POINT__TO__TOP_B_2))
1146
               (and (junctions6_top__POINT__TO__TOP_B_2_unless Junctions6_TOP_node.junctions6_top__restart_in
1147
                                                               Junctions6_TOP_node.junctions6_top__state_in
1148
                                                               Junctions6_TOP_node.__Junctions6_TOP_node_17
1149
                                                               Junctions6_TOP_node.__Junctions6_TOP_node_18)
1150
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_18)
1151
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_17)
1152
                    ))
1153
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_A_IDL))
1154
               (and (junctions6_top__TOP_A_IDL_unless Junctions6_TOP_node.junctions6_top__restart_in
1155
                                                      Junctions6_TOP_node.junctions6_top__state_in
1156
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_7
1157
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_8)
1158
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_8)
1159
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_7)
1160
                    ))
1161
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1))
1162
               (and (junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless 
1163
                    Junctions6_TOP_node.junctions6_top__restart_in
1164
                    Junctions6_TOP_node.junctions6_top__state_in
1165
                    Junctions6_TOP_node.__Junctions6_TOP_node_15
1166
                    Junctions6_TOP_node.__Junctions6_TOP_node_16)
1167
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_16)
1168
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_15)
1169
                    ))
1170
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_B_IDL))
1171
               (and (junctions6_top__TOP_B_IDL_unless Junctions6_TOP_node.junctions6_top__restart_in
1172
                                                      Junctions6_TOP_node.junctions6_top__state_in
1173
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_5
1174
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_6)
1175
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_6)
1176
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_5)
1177
                    ))
1178
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1))
1179
               (and (junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_unless 
1180
                    Junctions6_TOP_node.junctions6_top__restart_in
1181
                    Junctions6_TOP_node.junctions6_top__state_in
1182
                    Junctions6_TOP_node.__Junctions6_TOP_node_13
1183
                    Junctions6_TOP_node.__Junctions6_TOP_node_14)
1184
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_14)
1185
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_13)
1186
                    ))
1187
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_C_IDL))
1188
               (and (junctions6_top__TOP_C_IDL_unless Junctions6_TOP_node.junctions6_top__restart_in
1189
                                                      Junctions6_TOP_node.junctions6_top__state_in
1190
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_3
1191
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_4)
1192
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_4)
1193
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_3)
1194
                    ))
1195
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_C__TO__JUNCTIONS6_TOP_1))
1196
               (and (junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_unless 
1197
                    Junctions6_TOP_node.junctions6_top__restart_in
1198
                    Junctions6_TOP_node.junctions6_top__state_in
1199
                    Junctions6_TOP_node.__Junctions6_TOP_node_11
1200
                    Junctions6_TOP_node.__Junctions6_TOP_node_12)
1201
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_12)
1202
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_11)
1203
                    ))
1204
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_D_IDL))
1205
               (and (junctions6_top__TOP_D_IDL_unless Junctions6_TOP_node.junctions6_top__restart_in
1206
                                                      Junctions6_TOP_node.junctions6_top__state_in
1207
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_1
1208
                                                      Junctions6_TOP_node.__Junctions6_TOP_node_2)
1209
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_2)
1210
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_1)
1211
                    ))
1212
            (or (not (= Junctions6_TOP_node.junctions6_top__state_in TOP_D__TO__TOP_C_1))
1213
               (and (junctions6_top__TOP_D__TO__TOP_C_1_unless Junctions6_TOP_node.junctions6_top__restart_in
1214
                                                               Junctions6_TOP_node.junctions6_top__state_in
1215
                                                               Junctions6_TOP_node.__Junctions6_TOP_node_9
1216
                                                               Junctions6_TOP_node.__Junctions6_TOP_node_10)
1217
                    (= Junctions6_TOP_node.junctions6_top__state_act Junctions6_TOP_node.__Junctions6_TOP_node_10)
1218
                    (= Junctions6_TOP_node.junctions6_top__restart_act Junctions6_TOP_node.__Junctions6_TOP_node_9)
1219
                    ))
1220
       )
1221
       (and (or (not (= Junctions6_TOP_node.junctions6_top__state_act POINTJunctions6_TOP))
1222
               (and (junctions6_top__POINTJunctions6_TOP_handler_until 
1223
                    Junctions6_TOP_node.idJunctions6_TOP_1
1224
                    Junctions6_TOP_node.y_1
1225
                    Junctions6_TOP_node.idJunctions6_Junctions6_1
1226
                    Junctions6_TOP_node.__Junctions6_TOP_node_73
1227
                    Junctions6_TOP_node.__Junctions6_TOP_node_74
1228
                    Junctions6_TOP_node.__Junctions6_TOP_node_75
1229
                    Junctions6_TOP_node.__Junctions6_TOP_node_76
1230
                    Junctions6_TOP_node.__Junctions6_TOP_node_77)
1231
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_77)
1232
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_74)
1233
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_73)
1234
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_76)
1235
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_75)
1236
                    ))
1237
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act POINT__TO__TOP_A_1))
1238
               (and (junctions6_top__POINT__TO__TOP_A_1_handler_until 
1239
                    Junctions6_TOP_node.idJunctions6_TOP_1
1240
                    Junctions6_TOP_node.y_1
1241
                    Junctions6_TOP_node.idJunctions6_Junctions6_1
1242
                    Junctions6_TOP_node.__Junctions6_TOP_node_68
1243
                    Junctions6_TOP_node.__Junctions6_TOP_node_69
1244
                    Junctions6_TOP_node.__Junctions6_TOP_node_70
1245
                    Junctions6_TOP_node.__Junctions6_TOP_node_71
1246
                    Junctions6_TOP_node.__Junctions6_TOP_node_72)
1247
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_72)
1248
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_69)
1249
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_68)
1250
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_71)
1251
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_70)
1252
                    ))
1253
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act POINT__TO__TOP_B_2))
1254
               (and (junctions6_top__POINT__TO__TOP_B_2_handler_until 
1255
                    Junctions6_TOP_node.idJunctions6_TOP_1
1256
                    Junctions6_TOP_node.y_1
1257
                    Junctions6_TOP_node.idJunctions6_Junctions6_1
1258
                    Junctions6_TOP_node.__Junctions6_TOP_node_63
1259
                    Junctions6_TOP_node.__Junctions6_TOP_node_64
1260
                    Junctions6_TOP_node.__Junctions6_TOP_node_65
1261
                    Junctions6_TOP_node.__Junctions6_TOP_node_66
1262
                    Junctions6_TOP_node.__Junctions6_TOP_node_67)
1263
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_67)
1264
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_64)
1265
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_63)
1266
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_66)
1267
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_65)
1268
                    ))
1269
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_A_IDL))
1270
               (and (junctions6_top__TOP_A_IDL_handler_until Junctions6_TOP_node.idJunctions6_TOP_1
1271
                                                             Junctions6_TOP_node.y_1
1272
                                                             Junctions6_TOP_node.idJunctions6_Junctions6_1
1273
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_38
1274
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_39
1275
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_40
1276
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_41
1277
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_42)
1278
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_42)
1279
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_39)
1280
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_38)
1281
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_41)
1282
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_40)
1283
                    ))
1284
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1))
1285
               (and (junctions6_top__TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until 
1286
                    Junctions6_TOP_node.idJunctions6_TOP_1
1287
                    Junctions6_TOP_node.x
1288
                    Junctions6_TOP_node.y_1
1289
                    Junctions6_TOP_node.idJunctions6_Junctions6_1
1290
                    Junctions6_TOP_node.__Junctions6_TOP_node_58
1291
                    Junctions6_TOP_node.__Junctions6_TOP_node_59
1292
                    Junctions6_TOP_node.__Junctions6_TOP_node_60
1293
                    Junctions6_TOP_node.__Junctions6_TOP_node_61
1294
                    Junctions6_TOP_node.__Junctions6_TOP_node_62)
1295
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_62)
1296
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_59)
1297
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_58)
1298
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_61)
1299
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_60)
1300
                    ))
1301
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_B_IDL))
1302
               (and (junctions6_top__TOP_B_IDL_handler_until Junctions6_TOP_node.idJunctions6_TOP_1
1303
                                                             Junctions6_TOP_node.y_1
1304
                                                             Junctions6_TOP_node.idJunctions6_Junctions6_1
1305
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_33
1306
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_34
1307
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_35
1308
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_36
1309
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_37)
1310
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_37)
1311
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_34)
1312
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_33)
1313
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_36)
1314
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_35)
1315
                    ))
1316
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1))
1317
               (and (junctions6_top__TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1_handler_until 
1318
                    Junctions6_TOP_node.idJunctions6_TOP_1
1319
                    Junctions6_TOP_node.x
1320
                    Junctions6_TOP_node.y_1
1321
                    Junctions6_TOP_node.idJunctions6_Junctions6_1
1322
                    Junctions6_TOP_node.__Junctions6_TOP_node_53
1323
                    Junctions6_TOP_node.__Junctions6_TOP_node_54
1324
                    Junctions6_TOP_node.__Junctions6_TOP_node_55
1325
                    Junctions6_TOP_node.__Junctions6_TOP_node_56
1326
                    Junctions6_TOP_node.__Junctions6_TOP_node_57)
1327
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_57)
1328
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_54)
1329
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_53)
1330
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_56)
1331
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_55)
1332
                    ))
1333
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_C_IDL))
1334
               (and (junctions6_top__TOP_C_IDL_handler_until Junctions6_TOP_node.idJunctions6_TOP_1
1335
                                                             Junctions6_TOP_node.y_1
1336
                                                             Junctions6_TOP_node.idJunctions6_Junctions6_1
1337
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_28
1338
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_29
1339
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_30
1340
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_31
1341
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_32)
1342
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_32)
1343
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_29)
1344
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_28)
1345
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_31)
1346
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_30)
1347
                    ))
1348
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_C__TO__JUNCTIONS6_TOP_1))
1349
               (and (junctions6_top__TOP_C__TO__JUNCTIONS6_TOP_1_handler_until 
1350
                    Junctions6_TOP_node.idJunctions6_TOP_1
1351
                    Junctions6_TOP_node.x
1352
                    Junctions6_TOP_node.y_1
1353
                    Junctions6_TOP_node.idJunctions6_Junctions6_1
1354
                    Junctions6_TOP_node.__Junctions6_TOP_node_48
1355
                    Junctions6_TOP_node.__Junctions6_TOP_node_49
1356
                    Junctions6_TOP_node.__Junctions6_TOP_node_50
1357
                    Junctions6_TOP_node.__Junctions6_TOP_node_51
1358
                    Junctions6_TOP_node.__Junctions6_TOP_node_52)
1359
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_52)
1360
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_49)
1361
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_48)
1362
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_51)
1363
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_50)
1364
                    ))
1365
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_D_IDL))
1366
               (and (junctions6_top__TOP_D_IDL_handler_until Junctions6_TOP_node.idJunctions6_TOP_1
1367
                                                             Junctions6_TOP_node.y_1
1368
                                                             Junctions6_TOP_node.idJunctions6_Junctions6_1
1369
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_23
1370
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_24
1371
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_25
1372
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_26
1373
                                                             Junctions6_TOP_node.__Junctions6_TOP_node_27)
1374
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_27)
1375
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_24)
1376
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_23)
1377
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_26)
1378
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_25)
1379
                    ))
1380
            (or (not (= Junctions6_TOP_node.junctions6_top__state_act TOP_D__TO__TOP_C_1))
1381
               (and (junctions6_top__TOP_D__TO__TOP_C_1_handler_until 
1382
                    Junctions6_TOP_node.idJunctions6_TOP_1
1383
                    Junctions6_TOP_node.y_1
1384
                    Junctions6_TOP_node.idJunctions6_Junctions6_1
1385
                    Junctions6_TOP_node.__Junctions6_TOP_node_43
1386
                    Junctions6_TOP_node.__Junctions6_TOP_node_44
1387
                    Junctions6_TOP_node.__Junctions6_TOP_node_45
1388
                    Junctions6_TOP_node.__Junctions6_TOP_node_46
1389
                    Junctions6_TOP_node.__Junctions6_TOP_node_47)
1390
                    (= Junctions6_TOP_node.y Junctions6_TOP_node.__Junctions6_TOP_node_47)
1391
                    (= Junctions6_TOP_node.junctions6_top__next_state_in Junctions6_TOP_node.__Junctions6_TOP_node_44)
1392
                    (= Junctions6_TOP_node.junctions6_top__next_restart_in Junctions6_TOP_node.__Junctions6_TOP_node_43)
1393
                    (= Junctions6_TOP_node.idJunctions6_TOP Junctions6_TOP_node.__Junctions6_TOP_node_46)
1394
                    (= Junctions6_TOP_node.idJunctions6_Junctions6 Junctions6_TOP_node.__Junctions6_TOP_node_45)
1395
                    ))
1396
       )
1397
       (= Junctions6_TOP_node.__Junctions6_TOP_node_80_x Junctions6_TOP_node.junctions6_top__next_state_in)
1398
       (= Junctions6_TOP_node.__Junctions6_TOP_node_79_x Junctions6_TOP_node.junctions6_top__next_restart_in)
1399
       )
1400
  (Junctions6_TOP_node_step Junctions6_TOP_node.idJunctions6_TOP_1
1401
                            Junctions6_TOP_node.x
1402
                            Junctions6_TOP_node.y_1
1403
                            Junctions6_TOP_node.idJunctions6_Junctions6_1
1404
                            Junctions6_TOP_node.idJunctions6_TOP
1405
                            Junctions6_TOP_node.y
1406
                            Junctions6_TOP_node.idJunctions6_Junctions6
1407
                            Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1408
                            Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1409
                            Junctions6_TOP_node.ni_7._arrow._first_c
1410
                            Junctions6_TOP_node.__Junctions6_TOP_node_79_x
1411
                            Junctions6_TOP_node.__Junctions6_TOP_node_80_x
1412
                            Junctions6_TOP_node.ni_7._arrow._first_x)
1413
))
1414

    
1415
; junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until
1416
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_1 Int)
1417
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_1 Int)
1418
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.x Int)
1419
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_1 Int)
1420
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.junctions6_junctions6__restart_in Bool)
1421
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.junctions6_junctions6__state_in junctions6_junctions6__type)
1422
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_out Int)
1423
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_out Int)
1424
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_out Int)
1425
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c Bool)
1426
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c junctions6_top__type)
1427
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c Bool)
1428
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Bool)
1429
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m junctions6_top__type)
1430
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Bool)
1431
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x Bool)
1432
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x junctions6_top__type)
1433
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x Bool)
1434
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_2 Int)
1435
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_2 Int)
1436
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_2 Int)
1437
(declare-rel junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until_reset (Bool junctions6_top__type Bool Bool junctions6_top__type Bool))
1438
(declare-rel junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until_step (Int Int Int Int Bool junctions6_junctions6__type Int Int Int Bool junctions6_top__type Bool Bool junctions6_top__type Bool))
1439

    
1440
(rule (=> 
1441
  (and 
1442
       
1443
       (Junctions6_TOP_node_reset junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1444
                                  junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1445
                                  junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1446
                                  junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1447
                                  junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1448
                                  junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m)
1449
  )
1450
  (junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until_reset junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1451
                                                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1452
                                                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1453
                                                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1454
                                                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1455
                                                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m)
1456
))
1457

    
1458
(rule (=> 
1459
  (and (and (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c)
1460
            (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c)
1461
            (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c)
1462
            )
1463
       (Junctions6_TOP_node_step junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_1
1464
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.x
1465
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_1
1466
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_1
1467
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_2
1468
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_2
1469
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_2
1470
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1471
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1472
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
1473
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
1474
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
1475
                                 junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x)
1476
       (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_out junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_2)
1477
       (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.junctions6_junctions6__state_in POINTJunctions6_Junctions6)
1478
       (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.junctions6_junctions6__restart_in true)
1479
       (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_out junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_2)
1480
       (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_out junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_2)
1481
       )
1482
  (junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until_step junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_1
1483
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_1
1484
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.x
1485
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_1
1486
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.junctions6_junctions6__restart_in
1487
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.junctions6_junctions6__state_in
1488
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_Junctions6_out
1489
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.idJunctions6_TOP_out
1490
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.y_out
1491
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1492
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1493
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1494
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
1495
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
1496
                                                                junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x)
1497
))
1498

    
1499
; junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless
1500
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__restart_in Bool)
1501
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__state_in junctions6_junctions6__type)
1502
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__restart_act Bool)
1503
(declare-var junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__state_act junctions6_junctions6__type)
1504
(declare-rel junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless (Bool junctions6_junctions6__type Bool junctions6_junctions6__type))
1505
(rule (=> 
1506
  (and (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__state_act junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__state_in)
1507
       (= junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__restart_act junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__restart_in)
1508
       )
1509
  (junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__restart_in junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__state_in junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__restart_act junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless.junctions6_junctions6__state_act)
1510
))
1511

    
1512
; junctions6_junctions6__POINTJunctions6_Junctions6_handler_until
1513
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_Junctions6_1 Int)
1514
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_TOP_1 Int)
1515
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.y_1 Int)
1516
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.junctions6_junctions6__restart_in Bool)
1517
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.junctions6_junctions6__state_in junctions6_junctions6__type)
1518
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_Junctions6_out Int)
1519
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_TOP_out Int)
1520
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.y_out Int)
1521
(declare-rel junctions6_junctions6__POINTJunctions6_Junctions6_handler_until (Int Int Int Bool junctions6_junctions6__type Int Int Int))
1522
(rule (=> 
1523
  (and (= junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.y_out junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.y_1)
1524
       (= junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.junctions6_junctions6__state_in POINTJunctions6_Junctions6)
1525
       (= junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.junctions6_junctions6__restart_in false)
1526
       (= junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_TOP_out junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_TOP_1)
1527
       (= junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_Junctions6_out junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_Junctions6_1)
1528
       )
1529
  (junctions6_junctions6__POINTJunctions6_Junctions6_handler_until junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_Junctions6_1 junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_TOP_1 junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.y_1 junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.junctions6_junctions6__restart_in junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.junctions6_junctions6__state_in junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_Junctions6_out junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.idJunctions6_TOP_out junctions6_junctions6__POINTJunctions6_Junctions6_handler_until.y_out)
1530
))
1531

    
1532
; junctions6_junctions6__POINTJunctions6_Junctions6_unless
1533
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_in Bool)
1534
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_in junctions6_junctions6__type)
1535
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_unless.idJunctions6_Junctions6_1 Int)
1536
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_act Bool)
1537
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_act junctions6_junctions6__type)
1538
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_1 Bool)
1539
(declare-var junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_2 Bool)
1540
(declare-rel junctions6_junctions6__POINTJunctions6_Junctions6_unless (Bool junctions6_junctions6__type Int Bool junctions6_junctions6__type))
1541
(rule (=> 
1542
  (and (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_2 (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.idJunctions6_Junctions6_1 1301))
1543
       (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_1 (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.idJunctions6_Junctions6_1 0))
1544
       (and (or (not (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_1 false))
1545
               (and (or (not (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_2 false))
1546
                       (and (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_act junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_in)
1547
                            (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_act junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_in)
1548
                            ))
1549
                    (or (not (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_2 true))
1550
                       (and (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_act JUNCTIONS6_TOP_IDL)
1551
                            (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_act true)
1552
                            ))
1553
               ))
1554
            (or (not (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.__junctions6_junctions6__POINTJunctions6_Junctions6_unless_1 true))
1555
               (and (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_act POINT__TO__JUNCTIONS6_TOP_1)
1556
                    (= junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_act true)
1557
                    ))
1558
       )
1559
       )
1560
  (junctions6_junctions6__POINTJunctions6_Junctions6_unless junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_in junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_in junctions6_junctions6__POINTJunctions6_Junctions6_unless.idJunctions6_Junctions6_1 junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__restart_act junctions6_junctions6__POINTJunctions6_Junctions6_unless.junctions6_junctions6__state_act)
1561
))
1562

    
1563
; junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until
1564
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_1 Int)
1565
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_1 Int)
1566
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.x Int)
1567
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_1 Int)
1568
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_junctions6__restart_in Bool)
1569
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_junctions6__state_in junctions6_junctions6__type)
1570
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_out Int)
1571
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_out Int)
1572
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_out Int)
1573
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_2 Int)
1574
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_2 Int)
1575
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_2 Int)
1576
(declare-rel junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until (Int Int Int Int Bool junctions6_junctions6__type Int Int Int))
1577
(rule (=> 
1578
  (and (Junctions6_TOP_en junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_1
1579
                          junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_1
1580
                          junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.x
1581
                          junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_1
1582
                          false
1583
                          junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_2
1584
                          junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_2
1585
                          junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_2)
1586
       (= junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_out junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_2)
1587
       (= junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_junctions6__state_in POINTJunctions6_Junctions6)
1588
       (= junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_junctions6__restart_in true)
1589
       (= junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_out junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_2)
1590
       (= junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_out junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_2)
1591
       )
1592
  (junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_1 junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_1 junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.x junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_1 junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_junctions6__restart_in junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.junctions6_junctions6__state_in junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_Junctions6_out junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.idJunctions6_TOP_out junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until.y_out)
1593
))
1594

    
1595
; junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless
1596
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__restart_in Bool)
1597
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__state_in junctions6_junctions6__type)
1598
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__restart_act Bool)
1599
(declare-var junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__state_act junctions6_junctions6__type)
1600
(declare-rel junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless (Bool junctions6_junctions6__type Bool junctions6_junctions6__type))
1601
(rule (=> 
1602
  (and (= junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__state_act junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__state_in)
1603
       (= junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__restart_act junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__restart_in)
1604
       )
1605
  (junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__restart_in junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__state_in junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__restart_act junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless.junctions6_junctions6__state_act)
1606
))
1607

    
1608
; Junctions6_Junctions6_node
1609
(declare-var Junctions6_Junctions6_node.idJunctions6_Junctions6_1 Int)
1610
(declare-var Junctions6_Junctions6_node.idJunctions6_TOP_1 Int)
1611
(declare-var Junctions6_Junctions6_node.x Int)
1612
(declare-var Junctions6_Junctions6_node.y_1 Int)
1613
(declare-var Junctions6_Junctions6_node.idJunctions6_Junctions6 Int)
1614
(declare-var Junctions6_Junctions6_node.idJunctions6_TOP Int)
1615
(declare-var Junctions6_Junctions6_node.y Int)
1616
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c Bool)
1617
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c junctions6_junctions6__type)
1618
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c Bool)
1619
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c junctions6_top__type)
1620
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c Bool)
1621
(declare-var Junctions6_Junctions6_node.ni_5._arrow._first_c Bool)
1622
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m Bool)
1623
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m junctions6_junctions6__type)
1624
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Bool)
1625
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m junctions6_top__type)
1626
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Bool)
1627
(declare-var Junctions6_Junctions6_node.ni_5._arrow._first_m Bool)
1628
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x Bool)
1629
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x junctions6_junctions6__type)
1630
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x Bool)
1631
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x junctions6_top__type)
1632
(declare-var Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x Bool)
1633
(declare-var Junctions6_Junctions6_node.ni_5._arrow._first_x Bool)
1634
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_1 Bool)
1635
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_10 Int)
1636
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_11 Int)
1637
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_12 Bool)
1638
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_13 junctions6_junctions6__type)
1639
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_14 Int)
1640
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_15 Int)
1641
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_16 Int)
1642
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_17 Bool)
1643
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_18 junctions6_junctions6__type)
1644
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_19 Int)
1645
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_2 junctions6_junctions6__type)
1646
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_20 Int)
1647
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_21 Int)
1648
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_22 Bool)
1649
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_3 Bool)
1650
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_4 junctions6_junctions6__type)
1651
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_5 Bool)
1652
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_6 junctions6_junctions6__type)
1653
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_7 Bool)
1654
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_8 junctions6_junctions6__type)
1655
(declare-var Junctions6_Junctions6_node.__Junctions6_Junctions6_node_9 Int)
1656
(declare-var Junctions6_Junctions6_node.junctions6_junctions6__next_restart_in Bool)
1657
(declare-var Junctions6_Junctions6_node.junctions6_junctions6__next_state_in junctions6_junctions6__type)
1658
(declare-var Junctions6_Junctions6_node.junctions6_junctions6__restart_act Bool)
1659
(declare-var Junctions6_Junctions6_node.junctions6_junctions6__restart_in Bool)
1660
(declare-var Junctions6_Junctions6_node.junctions6_junctions6__state_act junctions6_junctions6__type)
1661
(declare-var Junctions6_Junctions6_node.junctions6_junctions6__state_in junctions6_junctions6__type)
1662
(declare-rel Junctions6_Junctions6_node_reset (Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool))
1663
(declare-rel Junctions6_Junctions6_node_step (Int Int Int Int Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool))
1664

    
1665
(rule (=> 
1666
  (and 
1667
       (= Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c)
1668
       (= Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c)
1669
       (= Junctions6_Junctions6_node.ni_5._arrow._first_m true)
1670
       (junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until_reset 
1671
       Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1672
       Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1673
       Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1674
       Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1675
       Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1676
       Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m)
1677
  )
1678
  (Junctions6_Junctions6_node_reset Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
1679
                                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
1680
                                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1681
                                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1682
                                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1683
                                    Junctions6_Junctions6_node.ni_5._arrow._first_c
1684
                                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m
1685
                                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m
1686
                                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1687
                                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1688
                                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
1689
                                    Junctions6_Junctions6_node.ni_5._arrow._first_m)
1690
))
1691

    
1692
(rule (=> 
1693
  (and (= Junctions6_Junctions6_node.ni_5._arrow._first_m Junctions6_Junctions6_node.ni_5._arrow._first_c)
1694
       (and (= Junctions6_Junctions6_node.__Junctions6_Junctions6_node_22 (ite Junctions6_Junctions6_node.ni_5._arrow._first_m true false))
1695
            (= Junctions6_Junctions6_node.ni_5._arrow._first_x false))
1696
       (and (or (not (= Junctions6_Junctions6_node.__Junctions6_Junctions6_node_22 false))
1697
               (and (= Junctions6_Junctions6_node.junctions6_junctions6__state_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c)
1698
                    (= Junctions6_Junctions6_node.junctions6_junctions6__restart_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c)
1699
                    ))
1700
            (or (not (= Junctions6_Junctions6_node.__Junctions6_Junctions6_node_22 true))
1701
               (and (= Junctions6_Junctions6_node.junctions6_junctions6__state_in POINTJunctions6_Junctions6)
1702
                    (= Junctions6_Junctions6_node.junctions6_junctions6__restart_in false)
1703
                    ))
1704
       )
1705
       (and (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__state_in JUNCTIONS6_TOP_IDL))
1706
               (and (junctions6_junctions6__JUNCTIONS6_TOP_IDL_unless 
1707
                    Junctions6_Junctions6_node.junctions6_junctions6__restart_in
1708
                    Junctions6_Junctions6_node.junctions6_junctions6__state_in
1709
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_1
1710
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_2)
1711
                    (= Junctions6_Junctions6_node.junctions6_junctions6__state_act Junctions6_Junctions6_node.__Junctions6_Junctions6_node_2)
1712
                    (= Junctions6_Junctions6_node.junctions6_junctions6__restart_act Junctions6_Junctions6_node.__Junctions6_Junctions6_node_1)
1713
                    ))
1714
            (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__state_in POINTJunctions6_Junctions6))
1715
               (and (junctions6_junctions6__POINTJunctions6_Junctions6_unless 
1716
                    Junctions6_Junctions6_node.junctions6_junctions6__restart_in
1717
                    Junctions6_Junctions6_node.junctions6_junctions6__state_in
1718
                    Junctions6_Junctions6_node.idJunctions6_Junctions6_1
1719
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_5
1720
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_6)
1721
                    (= Junctions6_Junctions6_node.junctions6_junctions6__state_act Junctions6_Junctions6_node.__Junctions6_Junctions6_node_6)
1722
                    (= Junctions6_Junctions6_node.junctions6_junctions6__restart_act Junctions6_Junctions6_node.__Junctions6_Junctions6_node_5)
1723
                    ))
1724
            (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__state_in POINT__TO__JUNCTIONS6_TOP_1))
1725
               (and (junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_unless 
1726
                    Junctions6_Junctions6_node.junctions6_junctions6__restart_in
1727
                    Junctions6_Junctions6_node.junctions6_junctions6__state_in
1728
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_3
1729
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_4)
1730
                    (= Junctions6_Junctions6_node.junctions6_junctions6__state_act Junctions6_Junctions6_node.__Junctions6_Junctions6_node_4)
1731
                    (= Junctions6_Junctions6_node.junctions6_junctions6__restart_act Junctions6_Junctions6_node.__Junctions6_Junctions6_node_3)
1732
                    ))
1733
       )
1734
       (and (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__state_act JUNCTIONS6_TOP_IDL))
1735
               (and (and (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__restart_act true))
1736
                            (junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until_reset 
1737
                            Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1738
                            Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1739
                            Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1740
                            Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1741
                            Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1742
                            Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m))
1743
                         (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__restart_act false))
1744
                            (and (= Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c)
1745
                                 (= Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c)
1746
                                 (= Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c)
1747
                                 )
1748
                            )
1749
                    )
1750
                    (and (= Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c)
1751
                         (= Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c)
1752
                         (= Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c)
1753
                         )
1754
                    (junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until_step 
1755
                    Junctions6_Junctions6_node.idJunctions6_Junctions6_1
1756
                    Junctions6_Junctions6_node.idJunctions6_TOP_1
1757
                    Junctions6_Junctions6_node.x
1758
                    Junctions6_Junctions6_node.y_1
1759
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_7
1760
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_8
1761
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_9
1762
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_10
1763
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_11
1764
                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1765
                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1766
                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
1767
                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
1768
                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
1769
                    Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x)
1770
                    (= Junctions6_Junctions6_node.y Junctions6_Junctions6_node.__Junctions6_Junctions6_node_11)
1771
                    (= Junctions6_Junctions6_node.junctions6_junctions6__next_state_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_8)
1772
                    (= Junctions6_Junctions6_node.junctions6_junctions6__next_restart_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_7)
1773
                    (= Junctions6_Junctions6_node.idJunctions6_TOP Junctions6_Junctions6_node.__Junctions6_Junctions6_node_10)
1774
                    (= Junctions6_Junctions6_node.idJunctions6_Junctions6 Junctions6_Junctions6_node.__Junctions6_Junctions6_node_9)
1775
                    ))
1776
            (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__state_act POINTJunctions6_Junctions6))
1777
               (and (junctions6_junctions6__POINTJunctions6_Junctions6_handler_until 
1778
                    Junctions6_Junctions6_node.idJunctions6_Junctions6_1
1779
                    Junctions6_Junctions6_node.idJunctions6_TOP_1
1780
                    Junctions6_Junctions6_node.y_1
1781
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_17
1782
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_18
1783
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_19
1784
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_20
1785
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_21)
1786
                    (= Junctions6_Junctions6_node.y Junctions6_Junctions6_node.__Junctions6_Junctions6_node_21)
1787
                    (= Junctions6_Junctions6_node.junctions6_junctions6__next_state_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_18)
1788
                    (= Junctions6_Junctions6_node.junctions6_junctions6__next_restart_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_17)
1789
                    (= Junctions6_Junctions6_node.idJunctions6_TOP Junctions6_Junctions6_node.__Junctions6_Junctions6_node_20)
1790
                    (= Junctions6_Junctions6_node.idJunctions6_Junctions6 Junctions6_Junctions6_node.__Junctions6_Junctions6_node_19)
1791
                    ))
1792
            (or (not (= Junctions6_Junctions6_node.junctions6_junctions6__state_act POINT__TO__JUNCTIONS6_TOP_1))
1793
               (and (junctions6_junctions6__POINT__TO__JUNCTIONS6_TOP_1_handler_until 
1794
                    Junctions6_Junctions6_node.idJunctions6_Junctions6_1
1795
                    Junctions6_Junctions6_node.idJunctions6_TOP_1
1796
                    Junctions6_Junctions6_node.x
1797
                    Junctions6_Junctions6_node.y_1
1798
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_12
1799
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_13
1800
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_14
1801
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_15
1802
                    Junctions6_Junctions6_node.__Junctions6_Junctions6_node_16)
1803
                    (= Junctions6_Junctions6_node.y Junctions6_Junctions6_node.__Junctions6_Junctions6_node_16)
1804
                    (= Junctions6_Junctions6_node.junctions6_junctions6__next_state_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_13)
1805
                    (= Junctions6_Junctions6_node.junctions6_junctions6__next_restart_in Junctions6_Junctions6_node.__Junctions6_Junctions6_node_12)
1806
                    (= Junctions6_Junctions6_node.idJunctions6_TOP Junctions6_Junctions6_node.__Junctions6_Junctions6_node_15)
1807
                    (= Junctions6_Junctions6_node.idJunctions6_Junctions6 Junctions6_Junctions6_node.__Junctions6_Junctions6_node_14)
1808
                    ))
1809
       )
1810
       (= Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x Junctions6_Junctions6_node.junctions6_junctions6__next_state_in)
1811
       (= Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x Junctions6_Junctions6_node.junctions6_junctions6__next_restart_in)
1812
       )
1813
  (Junctions6_Junctions6_node_step Junctions6_Junctions6_node.idJunctions6_Junctions6_1
1814
                                   Junctions6_Junctions6_node.idJunctions6_TOP_1
1815
                                   Junctions6_Junctions6_node.x
1816
                                   Junctions6_Junctions6_node.y_1
1817
                                   Junctions6_Junctions6_node.idJunctions6_Junctions6
1818
                                   Junctions6_Junctions6_node.idJunctions6_TOP
1819
                                   Junctions6_Junctions6_node.y
1820
                                   Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
1821
                                   Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
1822
                                   Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1823
                                   Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1824
                                   Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1825
                                   Junctions6_Junctions6_node.ni_5._arrow._first_c
1826
                                   Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x
1827
                                   Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x
1828
                                   Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
1829
                                   Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
1830
                                   Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x
1831
                                   Junctions6_Junctions6_node.ni_5._arrow._first_x)
1832
))
1833

    
1834
; Junctions6_Junctions6
1835
(declare-var Junctions6_Junctions6.x Int)
1836
(declare-var Junctions6_Junctions6.y Int)
1837
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_2_c Int)
1838
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_3_c Int)
1839
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_4_c Int)
1840
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c Bool)
1841
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c junctions6_junctions6__type)
1842
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c Bool)
1843
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c junctions6_top__type)
1844
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c Bool)
1845
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c Bool)
1846
(declare-var Junctions6_Junctions6.ni_3._arrow._first_c Bool)
1847
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_2_m Int)
1848
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_3_m Int)
1849
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_4_m Int)
1850
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m Bool)
1851
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m junctions6_junctions6__type)
1852
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Bool)
1853
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m junctions6_top__type)
1854
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Bool)
1855
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m Bool)
1856
(declare-var Junctions6_Junctions6.ni_3._arrow._first_m Bool)
1857
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_2_x Int)
1858
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_3_x Int)
1859
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_4_x Int)
1860
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x Bool)
1861
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x junctions6_junctions6__type)
1862
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x Bool)
1863
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x junctions6_top__type)
1864
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x Bool)
1865
(declare-var Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_x Bool)
1866
(declare-var Junctions6_Junctions6.ni_3._arrow._first_x Bool)
1867
(declare-var Junctions6_Junctions6.__Junctions6_Junctions6_1 Bool)
1868
(declare-var Junctions6_Junctions6.idJunctions6_Junctions6 Int)
1869
(declare-var Junctions6_Junctions6.idJunctions6_Junctions6_1 Int)
1870
(declare-var Junctions6_Junctions6.idJunctions6_TOP Int)
1871
(declare-var Junctions6_Junctions6.idJunctions6_TOP_1 Int)
1872
(declare-var Junctions6_Junctions6.y_1 Int)
1873
(declare-rel Junctions6_Junctions6_reset (Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool))
1874
(declare-rel Junctions6_Junctions6_step (Int Int Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool))
1875

    
1876
(rule (=> 
1877
  (and 
1878
       (= Junctions6_Junctions6.__Junctions6_Junctions6_2_m Junctions6_Junctions6.__Junctions6_Junctions6_2_c)
1879
       (= Junctions6_Junctions6.__Junctions6_Junctions6_3_m Junctions6_Junctions6.__Junctions6_Junctions6_3_c)
1880
       (= Junctions6_Junctions6.__Junctions6_Junctions6_4_m Junctions6_Junctions6.__Junctions6_Junctions6_4_c)
1881
       (= Junctions6_Junctions6.ni_3._arrow._first_m true)
1882
       (Junctions6_Junctions6_node_reset Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
1883
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
1884
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1885
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1886
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1887
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c
1888
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m
1889
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m
1890
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1891
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1892
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
1893
                                         Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m)
1894
  )
1895
  (Junctions6_Junctions6_reset Junctions6_Junctions6.__Junctions6_Junctions6_2_c
1896
                               Junctions6_Junctions6.__Junctions6_Junctions6_3_c
1897
                               Junctions6_Junctions6.__Junctions6_Junctions6_4_c
1898
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
1899
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
1900
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1901
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1902
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1903
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c
1904
                               Junctions6_Junctions6.ni_3._arrow._first_c
1905
                               Junctions6_Junctions6.__Junctions6_Junctions6_2_m
1906
                               Junctions6_Junctions6.__Junctions6_Junctions6_3_m
1907
                               Junctions6_Junctions6.__Junctions6_Junctions6_4_m
1908
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m
1909
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m
1910
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1911
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1912
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
1913
                               Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m
1914
                               Junctions6_Junctions6.ni_3._arrow._first_m)
1915
))
1916

    
1917
(rule (=> 
1918
  (and (= Junctions6_Junctions6.ni_3._arrow._first_m Junctions6_Junctions6.ni_3._arrow._first_c)
1919
       (and (= Junctions6_Junctions6.__Junctions6_Junctions6_1 (ite Junctions6_Junctions6.ni_3._arrow._first_m true false))
1920
            (= Junctions6_Junctions6.ni_3._arrow._first_x false))
1921
       (and (or (not (= Junctions6_Junctions6.__Junctions6_Junctions6_1 false))
1922
               (and (= Junctions6_Junctions6.y_1 Junctions6_Junctions6.__Junctions6_Junctions6_4_c)
1923
                    (= Junctions6_Junctions6.idJunctions6_TOP_1 Junctions6_Junctions6.__Junctions6_Junctions6_2_c)
1924
                    (= Junctions6_Junctions6.idJunctions6_Junctions6_1 Junctions6_Junctions6.__Junctions6_Junctions6_3_c)
1925
                    ))
1926
            (or (not (= Junctions6_Junctions6.__Junctions6_Junctions6_1 true))
1927
               (and (= Junctions6_Junctions6.y_1 111111)
1928
                    (= Junctions6_Junctions6.idJunctions6_TOP_1 0)
1929
                    (= Junctions6_Junctions6.idJunctions6_Junctions6_1 0)
1930
                    ))
1931
       )
1932
       (and (= Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c)
1933
            (= Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c)
1934
            (= Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c)
1935
            (= Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c)
1936
            (= Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c)
1937
            (= Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c)
1938
            )
1939
       (Junctions6_Junctions6_node_step Junctions6_Junctions6.idJunctions6_Junctions6_1
1940
                                        Junctions6_Junctions6.idJunctions6_TOP_1
1941
                                        Junctions6_Junctions6.x
1942
                                        Junctions6_Junctions6.y_1
1943
                                        Junctions6_Junctions6.idJunctions6_Junctions6
1944
                                        Junctions6_Junctions6.idJunctions6_TOP
1945
                                        Junctions6_Junctions6.y
1946
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m
1947
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m
1948
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
1949
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
1950
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
1951
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m
1952
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x
1953
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x
1954
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
1955
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
1956
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x
1957
                                        Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_x)
1958
       (= Junctions6_Junctions6.__Junctions6_Junctions6_4_x Junctions6_Junctions6.y)
1959
       (= Junctions6_Junctions6.__Junctions6_Junctions6_3_x Junctions6_Junctions6.idJunctions6_Junctions6)
1960
       (= Junctions6_Junctions6.__Junctions6_Junctions6_2_x Junctions6_Junctions6.idJunctions6_TOP)
1961
       )
1962
  (Junctions6_Junctions6_step Junctions6_Junctions6.x
1963
                              Junctions6_Junctions6.y
1964
                              Junctions6_Junctions6.__Junctions6_Junctions6_2_c
1965
                              Junctions6_Junctions6.__Junctions6_Junctions6_3_c
1966
                              Junctions6_Junctions6.__Junctions6_Junctions6_4_c
1967
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
1968
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
1969
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
1970
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
1971
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
1972
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c
1973
                              Junctions6_Junctions6.ni_3._arrow._first_c
1974
                              Junctions6_Junctions6.__Junctions6_Junctions6_2_x
1975
                              Junctions6_Junctions6.__Junctions6_Junctions6_3_x
1976
                              Junctions6_Junctions6.__Junctions6_Junctions6_4_x
1977
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x
1978
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x
1979
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
1980
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
1981
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x
1982
                              Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_x
1983
                              Junctions6_Junctions6.ni_3._arrow._first_x)
1984
))
1985

    
1986
; Junctions6_TOP_ex
1987
(declare-var Junctions6_TOP_ex.idJunctions6_TOP_1 Int)
1988
(declare-var Junctions6_TOP_ex.idJunctions6_Junctions6_1 Int)
1989
(declare-var Junctions6_TOP_ex.isInner Bool)
1990
(declare-var Junctions6_TOP_ex.idJunctions6_TOP Int)
1991
(declare-var Junctions6_TOP_ex.idJunctions6_Junctions6 Int)
1992
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_2 Bool)
1993
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_3 Bool)
1994
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_4 Bool)
1995
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_5 Bool)
1996
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_6 Int)
1997
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_7 Int)
1998
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_8 Int)
1999
(declare-var Junctions6_TOP_ex.__Junctions6_TOP_ex_9 Int)
2000
(declare-var Junctions6_TOP_ex.idJunctions6_Junctions6_2 Int)
2001
(declare-var Junctions6_TOP_ex.idJunctions6_TOP_2 Int)
2002
(declare-var Junctions6_TOP_ex.idJunctions6_TOP_3 Int)
2003
(declare-var Junctions6_TOP_ex.idJunctions6_TOP_4 Int)
2004
(declare-var Junctions6_TOP_ex.idJunctions6_TOP_5 Int)
2005
(declare-var Junctions6_TOP_ex.idJunctions6_TOP_6 Int)
2006
(declare-rel Junctions6_TOP_ex (Int Int Bool Int Int))
2007
(rule (=> 
2008
  (and (TOP_D_ex Junctions6_TOP_ex.idJunctions6_TOP_1
2009
                 false
2010
                 Junctions6_TOP_ex.__Junctions6_TOP_ex_6)
2011
       (= Junctions6_TOP_ex.__Junctions6_TOP_ex_5 (= Junctions6_TOP_ex.idJunctions6_TOP_1 1300))
2012
       (and (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_5 true))
2013
               (= Junctions6_TOP_ex.idJunctions6_TOP_5 Junctions6_TOP_ex.__Junctions6_TOP_ex_6))
2014
            (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_5 false))
2015
               (= Junctions6_TOP_ex.idJunctions6_TOP_5 Junctions6_TOP_ex.idJunctions6_TOP_1))
2016
       )
2017
       (TOP_C_ex Junctions6_TOP_ex.idJunctions6_TOP_1
2018
                 false
2019
                 Junctions6_TOP_ex.__Junctions6_TOP_ex_7)
2020
       (= Junctions6_TOP_ex.__Junctions6_TOP_ex_4 (= Junctions6_TOP_ex.idJunctions6_TOP_1 1299))
2021
       (and (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_4 true))
2022
               (= Junctions6_TOP_ex.idJunctions6_TOP_4 Junctions6_TOP_ex.__Junctions6_TOP_ex_7))
2023
            (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_4 false))
2024
               (= Junctions6_TOP_ex.idJunctions6_TOP_4 Junctions6_TOP_ex.idJunctions6_TOP_1))
2025
       )
2026
       (TOP_B_ex Junctions6_TOP_ex.idJunctions6_TOP_1
2027
                 false
2028
                 Junctions6_TOP_ex.__Junctions6_TOP_ex_8)
2029
       (= Junctions6_TOP_ex.__Junctions6_TOP_ex_3 (= Junctions6_TOP_ex.idJunctions6_TOP_1 1298))
2030
       (and (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_3 true))
2031
               (= Junctions6_TOP_ex.idJunctions6_TOP_3 Junctions6_TOP_ex.__Junctions6_TOP_ex_8))
2032
            (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_3 false))
2033
               (= Junctions6_TOP_ex.idJunctions6_TOP_3 Junctions6_TOP_ex.idJunctions6_TOP_1))
2034
       )
2035
       (TOP_A_ex Junctions6_TOP_ex.idJunctions6_TOP_1
2036
                 false
2037
                 Junctions6_TOP_ex.__Junctions6_TOP_ex_9)
2038
       (= Junctions6_TOP_ex.__Junctions6_TOP_ex_2 (= Junctions6_TOP_ex.idJunctions6_TOP_1 1297))
2039
       (and (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_2 false))
2040
               (and (= Junctions6_TOP_ex.idJunctions6_TOP_2 Junctions6_TOP_ex.idJunctions6_TOP_1)
2041
                    (and (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_3 true))
2042
                            (= Junctions6_TOP_ex.idJunctions6_TOP_6 Junctions6_TOP_ex.idJunctions6_TOP_3))
2043
                         (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_3 false))
2044
                            (and (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_4 true))
2045
                                    (= Junctions6_TOP_ex.idJunctions6_TOP_6 Junctions6_TOP_ex.idJunctions6_TOP_4))
2046
                                 (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_4 false))
2047
                                    (and (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_5 true))
2048
                                            (= Junctions6_TOP_ex.idJunctions6_TOP_6 Junctions6_TOP_ex.idJunctions6_TOP_5))
2049
                                         (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_5 false))
2050
                                            (= Junctions6_TOP_ex.idJunctions6_TOP_6 Junctions6_TOP_ex.idJunctions6_TOP_1))
2051
                                    ))
2052
                            ))
2053
                    )
2054
                    ))
2055
            (or (not (= Junctions6_TOP_ex.__Junctions6_TOP_ex_2 true))
2056
               (and (= Junctions6_TOP_ex.idJunctions6_TOP_2 Junctions6_TOP_ex.__Junctions6_TOP_ex_9)
2057
                    (= Junctions6_TOP_ex.idJunctions6_TOP_6 Junctions6_TOP_ex.idJunctions6_TOP_2)
2058
                    ))
2059
       )
2060
       (and (or (not (= (not Junctions6_TOP_ex.isInner) true))
2061
               (= Junctions6_TOP_ex.idJunctions6_Junctions6_2 0))
2062
            (or (not (= (not Junctions6_TOP_ex.isInner) false))
2063
               (= Junctions6_TOP_ex.idJunctions6_Junctions6_2 Junctions6_TOP_ex.idJunctions6_Junctions6_1))
2064
       )
2065
       (= Junctions6_TOP_ex.idJunctions6_TOP 0)
2066
       (= Junctions6_TOP_ex.idJunctions6_Junctions6 Junctions6_TOP_ex.idJunctions6_Junctions6_1)
2067
       )
2068
  (Junctions6_TOP_ex Junctions6_TOP_ex.idJunctions6_TOP_1 Junctions6_TOP_ex.idJunctions6_Junctions6_1 Junctions6_TOP_ex.isInner Junctions6_TOP_ex.idJunctions6_TOP Junctions6_TOP_ex.idJunctions6_Junctions6)
2069
))
2070

    
2071
; Junctions6
2072
(declare-var Junctions6.x_1_1 Int)
2073
(declare-var Junctions6.y_1_1 Int)
2074
(declare-var Junctions6.ni_0._arrow._first_c Bool)
2075
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_c Int)
2076
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_c Int)
2077
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_c Int)
2078
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c Bool)
2079
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c junctions6_junctions6__type)
2080
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c Bool)
2081
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c junctions6_top__type)
2082
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c Bool)
2083
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c Bool)
2084
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_c Bool)
2085
(declare-var Junctions6.ni_0._arrow._first_m Bool)
2086
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_m Int)
2087
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_m Int)
2088
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_m Int)
2089
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m Bool)
2090
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m junctions6_junctions6__type)
2091
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Bool)
2092
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m junctions6_top__type)
2093
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Bool)
2094
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m Bool)
2095
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_m Bool)
2096
(declare-var Junctions6.ni_0._arrow._first_x Bool)
2097
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_x Int)
2098
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_x Int)
2099
(declare-var Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_x Int)
2100
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x Bool)
2101
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x junctions6_junctions6__type)
2102
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x Bool)
2103
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x junctions6_top__type)
2104
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x Bool)
2105
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_x Bool)
2106
(declare-var Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_x Bool)
2107
(declare-var Junctions6.Junctions6_1_1 Int)
2108
(declare-var Junctions6.__Junctions6_1 Bool)
2109
(declare-var Junctions6.i_virtual_local Real)
2110
(declare-rel Junctions6_reset (Bool Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool Bool Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool))
2111
(declare-rel Junctions6_step (Int Int Bool Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool Bool Int Int Int Bool junctions6_junctions6__type Bool junctions6_top__type Bool Bool Bool))
2112

    
2113
(rule (=> 
2114
  (and 
2115
       
2116
       (Junctions6_Junctions6_reset Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_c
2117
                                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_c
2118
                                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_c
2119
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
2120
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
2121
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
2122
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
2123
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
2124
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c
2125
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_c
2126
                                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_m
2127
                                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_m
2128
                                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_m
2129
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m
2130
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m
2131
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
2132
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
2133
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
2134
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m
2135
                                    Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_m)
2136
       (= Junctions6.ni_0._arrow._first_m true)
2137
  )
2138
  (Junctions6_reset Junctions6.ni_0._arrow._first_c
2139
                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_c
2140
                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_c
2141
                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_c
2142
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
2143
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
2144
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
2145
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
2146
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
2147
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c
2148
                    Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_c
2149
                    Junctions6.ni_0._arrow._first_m
2150
                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_m
2151
                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_m
2152
                    Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_m
2153
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m
2154
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m
2155
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
2156
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
2157
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
2158
                    Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m
2159
                    Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_m)
2160
))
2161

    
2162
(rule (=> 
2163
  (and (and (= Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_m Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_c)
2164
            (= Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_m Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_c)
2165
            (= Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_m Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_c)
2166
            (= Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c)
2167
            (= Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c)
2168
            (= Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c)
2169
            (= Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c)
2170
            (= Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c)
2171
            (= Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c)
2172
            (= Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_m Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_c)
2173
            )
2174
       (Junctions6_Junctions6_step Junctions6.x_1_1
2175
                                   Junctions6.Junctions6_1_1
2176
                                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_m
2177
                                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_m
2178
                                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_m
2179
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_m
2180
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_m
2181
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_m
2182
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_m
2183
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_m
2184
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_m
2185
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_m
2186
                                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_x
2187
                                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_x
2188
                                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_x
2189
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x
2190
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x
2191
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
2192
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
2193
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x
2194
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_x
2195
                                   Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_x)
2196
       (= Junctions6.y_1_1 Junctions6.Junctions6_1_1)
2197
       (= Junctions6.ni_0._arrow._first_m Junctions6.ni_0._arrow._first_c)
2198
       (and (= Junctions6.__Junctions6_1 (ite Junctions6.ni_0._arrow._first_m true false))
2199
            (= Junctions6.ni_0._arrow._first_x false))
2200
       (and (or (not (= Junctions6.__Junctions6_1 true))
2201
               (= Junctions6.i_virtual_local 0.))
2202
            (or (not (= Junctions6.__Junctions6_1 false))
2203
               (= Junctions6.i_virtual_local 1.))
2204
       )
2205
       )
2206
  (Junctions6_step Junctions6.x_1_1
2207
                   Junctions6.y_1_1
2208
                   Junctions6.ni_0._arrow._first_c
2209
                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_c
2210
                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_c
2211
                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_c
2212
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_c
2213
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_c
2214
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_c
2215
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_c
2216
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_c
2217
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_c
2218
                   Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_c
2219
                   Junctions6.ni_0._arrow._first_x
2220
                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_2_x
2221
                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_3_x
2222
                   Junctions6.ni_1.Junctions6_Junctions6.__Junctions6_Junctions6_4_x
2223
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_23_x
2224
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.__Junctions6_Junctions6_node_24_x
2225
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_79_x
2226
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.__Junctions6_TOP_node_80_x
2227
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_4.junctions6_junctions6__JUNCTIONS6_TOP_IDL_handler_until.ni_6.Junctions6_TOP_node.ni_7._arrow._first_x
2228
                   Junctions6.ni_1.Junctions6_Junctions6.ni_2.Junctions6_Junctions6_node.ni_5._arrow._first_x
2229
                   Junctions6.ni_1.Junctions6_Junctions6.ni_3._arrow._first_x)
2230
))
2231