Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions2 / Junctions2.smt2 @ eb639349

History | View | Annotate | Download (132 KB)

1
(declare-datatypes () ((junctions2_junctions2__type POINTJunctions2_Junctions2 POINT__TO__JUNCTIONS2_A_1 JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1 JUNCTIONS2_B__TO__JUNCTIONS2_C_1 JUNCTIONS2_C__TO__JUNCTIONS2_D_1 JUNCTIONS2_D__TO__JUNCTIONS2_A_1 JUNCTIONS2_A_IDL JUNCTIONS2_B_IDL JUNCTIONS2_C_IDL JUNCTIONS2_D_IDL)));
2

    
3
; Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action
4
(declare-var Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action.y_1 Int)
5
(declare-var Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action.y Int)
6
(declare-rel Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action (Int Int))
7
(rule (=> 
8
  (= Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action.y (+ Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action.y_1 1))
9
  (Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action.y_1 Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action.y)
10
))
11

    
12
; Junctions2_A_ex
13
(declare-var Junctions2_A_ex.idJunctions2_Junctions2_1 Int)
14
(declare-var Junctions2_A_ex.isInner Bool)
15
(declare-var Junctions2_A_ex.idJunctions2_Junctions2 Int)
16
(declare-var Junctions2_A_ex.idJunctions2_Junctions2_2 Int)
17
(declare-rel Junctions2_A_ex (Int Bool Int))
18
(rule (=> 
19
  (and (and (or (not (= (not Junctions2_A_ex.isInner) true))
20
               (= Junctions2_A_ex.idJunctions2_Junctions2_2 0))
21
            (or (not (= (not Junctions2_A_ex.isInner) false))
22
               (= Junctions2_A_ex.idJunctions2_Junctions2_2 Junctions2_A_ex.idJunctions2_Junctions2_1))
23
       )
24
       (= Junctions2_A_ex.idJunctions2_Junctions2 Junctions2_A_ex.idJunctions2_Junctions2_1)
25
       )
26
  (Junctions2_A_ex Junctions2_A_ex.idJunctions2_Junctions2_1 Junctions2_A_ex.isInner Junctions2_A_ex.idJunctions2_Junctions2)
27
))
28

    
29
; Junctions2_B_en
30
(declare-var Junctions2_B_en.idJunctions2_Junctions2_1 Int)
31
(declare-var Junctions2_B_en.isInner Bool)
32
(declare-var Junctions2_B_en.idJunctions2_Junctions2 Int)
33
(declare-rel Junctions2_B_en (Int Bool Int))
34
(rule (=> 
35
  (= Junctions2_B_en.idJunctions2_Junctions2 1204)
36
  (Junctions2_B_en Junctions2_B_en.idJunctions2_Junctions2_1 Junctions2_B_en.isInner Junctions2_B_en.idJunctions2_Junctions2)
37
))
38

    
39
; Junctions2_C_en
40
(declare-var Junctions2_C_en.idJunctions2_Junctions2_1 Int)
41
(declare-var Junctions2_C_en.isInner Bool)
42
(declare-var Junctions2_C_en.idJunctions2_Junctions2 Int)
43
(declare-rel Junctions2_C_en (Int Bool Int))
44
(rule (=> 
45
  (= Junctions2_C_en.idJunctions2_Junctions2 1205)
46
  (Junctions2_C_en Junctions2_C_en.idJunctions2_Junctions2_1 Junctions2_C_en.isInner Junctions2_C_en.idJunctions2_Junctions2)
47
))
48

    
49
; Junctions2_D_en
50
(declare-var Junctions2_D_en.idJunctions2_Junctions2_1 Int)
51
(declare-var Junctions2_D_en.isInner Bool)
52
(declare-var Junctions2_D_en.idJunctions2_Junctions2 Int)
53
(declare-rel Junctions2_D_en (Int Bool Int))
54
(rule (=> 
55
  (= Junctions2_D_en.idJunctions2_Junctions2 1206)
56
  (Junctions2_D_en Junctions2_D_en.idJunctions2_Junctions2_1 Junctions2_D_en.isInner Junctions2_D_en.idJunctions2_Junctions2)
57
))
58

    
59
; Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action
60
(declare-var Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action.y_1 Int)
61
(declare-var Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action.y Int)
62
(declare-rel Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action (Int Int))
63
(rule (=> 
64
  (= Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action.y (+ Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action.y_1 10))
65
  (Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action.y_1 Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action.y)
66
))
67

    
68
; Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action
69
(declare-var Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action.y_1 Int)
70
(declare-var Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action.y Int)
71
(declare-rel Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action (Int Int))
72
(rule (=> 
73
  (= Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action.y (+ Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action.y_1 100))
74
  (Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action.y_1 Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action.y)
75
))
76

    
77
; Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action
78
(declare-var Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action.y_1 Int)
79
(declare-var Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action.y Int)
80
(declare-rel Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action (Int Int))
81
(rule (=> 
82
  (= Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action.y (+ Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action.y_1 1000))
83
  (Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action.y_1 Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action.y)
84
))
85

    
86
; Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action
87
(declare-var Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action.y_1 Int)
88
(declare-var Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action.y Int)
89
(declare-rel Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action (Int Int))
90
(rule (=> 
91
  (= Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action.y (+ Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action.y_1 10000))
92
  (Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action.y_1 Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action.y)
93
))
94

    
95
; Junctions2_B_ex
96
(declare-var Junctions2_B_ex.idJunctions2_Junctions2_1 Int)
97
(declare-var Junctions2_B_ex.isInner Bool)
98
(declare-var Junctions2_B_ex.idJunctions2_Junctions2 Int)
99
(declare-var Junctions2_B_ex.idJunctions2_Junctions2_2 Int)
100
(declare-rel Junctions2_B_ex (Int Bool Int))
101
(rule (=> 
102
  (and (and (or (not (= (not Junctions2_B_ex.isInner) true))
103
               (= Junctions2_B_ex.idJunctions2_Junctions2_2 0))
104
            (or (not (= (not Junctions2_B_ex.isInner) false))
105
               (= Junctions2_B_ex.idJunctions2_Junctions2_2 Junctions2_B_ex.idJunctions2_Junctions2_1))
106
       )
107
       (= Junctions2_B_ex.idJunctions2_Junctions2 Junctions2_B_ex.idJunctions2_Junctions2_1)
108
       )
109
  (Junctions2_B_ex Junctions2_B_ex.idJunctions2_Junctions2_1 Junctions2_B_ex.isInner Junctions2_B_ex.idJunctions2_Junctions2)
110
))
111

    
112
; Junctions2_C_ex
113
(declare-var Junctions2_C_ex.idJunctions2_Junctions2_1 Int)
114
(declare-var Junctions2_C_ex.isInner Bool)
115
(declare-var Junctions2_C_ex.idJunctions2_Junctions2 Int)
116
(declare-var Junctions2_C_ex.idJunctions2_Junctions2_2 Int)
117
(declare-rel Junctions2_C_ex (Int Bool Int))
118
(rule (=> 
119
  (and (and (or (not (= (not Junctions2_C_ex.isInner) true))
120
               (= Junctions2_C_ex.idJunctions2_Junctions2_2 0))
121
            (or (not (= (not Junctions2_C_ex.isInner) false))
122
               (= Junctions2_C_ex.idJunctions2_Junctions2_2 Junctions2_C_ex.idJunctions2_Junctions2_1))
123
       )
124
       (= Junctions2_C_ex.idJunctions2_Junctions2 Junctions2_C_ex.idJunctions2_Junctions2_1)
125
       )
126
  (Junctions2_C_ex Junctions2_C_ex.idJunctions2_Junctions2_1 Junctions2_C_ex.isInner Junctions2_C_ex.idJunctions2_Junctions2)
127
))
128

    
129
; Junctions2_A_en
130
(declare-var Junctions2_A_en.idJunctions2_Junctions2_1 Int)
131
(declare-var Junctions2_A_en.isInner Bool)
132
(declare-var Junctions2_A_en.idJunctions2_Junctions2 Int)
133
(declare-rel Junctions2_A_en (Int Bool Int))
134
(rule (=> 
135
  (= Junctions2_A_en.idJunctions2_Junctions2 1203)
136
  (Junctions2_A_en Junctions2_A_en.idJunctions2_Junctions2_1 Junctions2_A_en.isInner Junctions2_A_en.idJunctions2_Junctions2)
137
))
138

    
139
; Junctions2_D_ex
140
(declare-var Junctions2_D_ex.idJunctions2_Junctions2_1 Int)
141
(declare-var Junctions2_D_ex.isInner Bool)
142
(declare-var Junctions2_D_ex.idJunctions2_Junctions2 Int)
143
(declare-var Junctions2_D_ex.idJunctions2_Junctions2_2 Int)
144
(declare-rel Junctions2_D_ex (Int Bool Int))
145
(rule (=> 
146
  (and (and (or (not (= (not Junctions2_D_ex.isInner) true))
147
               (= Junctions2_D_ex.idJunctions2_Junctions2_2 0))
148
            (or (not (= (not Junctions2_D_ex.isInner) false))
149
               (= Junctions2_D_ex.idJunctions2_Junctions2_2 Junctions2_D_ex.idJunctions2_Junctions2_1))
150
       )
151
       (= Junctions2_D_ex.idJunctions2_Junctions2 Junctions2_D_ex.idJunctions2_Junctions2_1)
152
       )
153
  (Junctions2_D_ex Junctions2_D_ex.idJunctions2_Junctions2_1 Junctions2_D_ex.isInner Junctions2_D_ex.idJunctions2_Junctions2)
154
))
155

    
156
; junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until
157
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.idJunctions2_Junctions2_1 Int)
158
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.y_1 Int)
159
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.junctions2_junctions2__restart_in Bool)
160
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
161
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.idJunctions2_Junctions2_out Int)
162
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.y_out Int)
163
(declare-rel junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
164
(rule (=> 
165
  (and (= junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.y_out junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.y_1)
166
       (= junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
167
       (= junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.junctions2_junctions2__restart_in true)
168
       (= junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.idJunctions2_Junctions2_1)
169
       )
170
  (junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until.y_out)
171
))
172

    
173
; junctions2_junctions2__JUNCTIONS2_A_IDL_unless
174
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__restart_in Bool)
175
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
176
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__restart_act Bool)
177
(declare-var junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
178
(declare-rel junctions2_junctions2__JUNCTIONS2_A_IDL_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
179
(rule (=> 
180
  (and (= junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__state_in)
181
       (= junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__restart_in)
182
       )
183
  (junctions2_junctions2__JUNCTIONS2_A_IDL_unless junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_A_IDL_unless.junctions2_junctions2__state_act)
184
))
185

    
186
; junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until
187
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1 Int)
188
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x Int)
189
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_1 Int)
190
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.junctions2_junctions2__restart_in Bool)
191
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
192
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_out Int)
193
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_out Int)
194
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 Bool)
195
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_10 Int)
196
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_11 Int)
197
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_12 Int)
198
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_13 Int)
199
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 Bool)
200
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 Bool)
201
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 Bool)
202
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_5 Int)
203
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_6 Int)
204
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_7 Int)
205
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_8 Int)
206
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_9 Int)
207
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2 Int)
208
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_2 Int)
209
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_3 Int)
210
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_4 Int)
211
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_5 Int)
212
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_6 Int)
213
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_7 Int)
214
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y Int)
215
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_2 Int)
216
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_3 Int)
217
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_4 Int)
218
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_5 Int)
219
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_6 Int)
220
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_7 Int)
221
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_8 Int)
222
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_9 Int)
223
(declare-rel junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until (Int Int Int Bool junctions2_junctions2__type Int Int))
224
(rule (=> 
225
  (and (Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action 
226
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_1
227
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_8)
228
       (Junctions2_Junctions2Junction1209__To__Junctions2_B_2_Condition_Action 
229
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_8
230
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_7)
231
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 (< junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x 2))
232
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 true))
233
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_9 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_7))
234
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 false))
235
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_9 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_8))
236
       )
237
       (Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action 
238
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_1
239
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_5)
240
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 (>= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x 2))
241
       (Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action 
242
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_5
243
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_10)
244
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 true))
245
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_6 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_10))
246
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 false))
247
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_6 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_5))
248
       )
249
       (Junctions2_Junctions2Junction1210__To__Junctions2_C_2_Condition_Action 
250
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_6
251
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_9)
252
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 (and (>= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x 2) (< junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x 4)))
253
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 true))
254
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_7 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_9))
255
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 false))
256
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_7 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_6))
257
       )
258
       (Junctions2_A__To__Junctions2_Junctions2Junction1209_1_Condition_Action 
259
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_1
260
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_2)
261
       (Junctions2_Junctions2Junction1209__To__Junctions2_Junctions2Junction1210_1_Condition_Action 
262
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_2
263
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_13)
264
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 true))
265
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_3 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_13))
266
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 false))
267
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_3 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_2))
268
       )
269
       (Junctions2_Junctions2Junction1210__To__Junctions2_D_1_Condition_Action 
270
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_3
271
       junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_12)
272
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 (and (>= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x 2) (>= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x 4)))
273
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 false))
274
               (and (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_4 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_3)
275
                    (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 true))
276
                            (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_7))
277
                         (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 false))
278
                            (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 true))
279
                                    (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_6))
280
                                 (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 false))
281
                                    (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 true))
282
                                            (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_9))
283
                                         (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 false))
284
                                            (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_8))
285
                                    ))
286
                            ))
287
                    )
288
                    ))
289
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 true))
290
               (and (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_4 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_12)
291
                    (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_4)
292
                    ))
293
       )
294
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_out junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y)
295
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
296
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.junctions2_junctions2__restart_in true)
297
       (Junctions2_A_ex junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1
298
                        false
299
                        junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_6)
300
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 true))
301
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_6 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_6))
302
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 false))
303
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_6 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1))
304
       )
305
       (Junctions2_B_en junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_6
306
                        false
307
                        junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_5)
308
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 true))
309
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_7 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_5))
310
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 false))
311
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_7 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_6))
312
       )
313
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 true))
314
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_4 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_6))
315
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 false))
316
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_4 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1))
317
       )
318
       (Junctions2_C_en junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_4
319
                        false
320
                        junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_8)
321
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 true))
322
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_5 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_8))
323
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 false))
324
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_5 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_4))
325
       )
326
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 true))
327
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_2 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_6))
328
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 false))
329
               (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_2 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1))
330
       )
331
       (Junctions2_D_en junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_2
332
                        false
333
                        junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_11)
334
       (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 false))
335
               (and (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_3 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_2)
336
                    (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 true))
337
                            (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_5))
338
                         (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_2 false))
339
                            (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 true))
340
                                    (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1))
341
                                 (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_3 false))
342
                                    (and (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 true))
343
                                            (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_7))
344
                                         (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_4 false))
345
                                            (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1))
346
                                    ))
347
                            ))
348
                    )
349
                    ))
350
            (or (not (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_1 true))
351
               (and (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_3 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.__junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until_11)
352
                    (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_3)
353
                    ))
354
       )
355
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2)
356
       )
357
  (junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.x junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until.y_out)
358
))
359

    
360
; junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless
361
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__restart_in Bool)
362
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
363
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__restart_act Bool)
364
(declare-var junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
365
(declare-rel junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
366
(rule (=> 
367
  (and (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__state_in)
368
       (= junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__restart_in)
369
       )
370
  (junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless.junctions2_junctions2__state_act)
371
))
372

    
373
; junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until
374
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.idJunctions2_Junctions2_1 Int)
375
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.y_1 Int)
376
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.junctions2_junctions2__restart_in Bool)
377
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
378
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.idJunctions2_Junctions2_out Int)
379
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.y_out Int)
380
(declare-rel junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
381
(rule (=> 
382
  (and (= junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.y_out junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.y_1)
383
       (= junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
384
       (= junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.junctions2_junctions2__restart_in true)
385
       (= junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.idJunctions2_Junctions2_1)
386
       )
387
  (junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until.y_out)
388
))
389

    
390
; junctions2_junctions2__JUNCTIONS2_B_IDL_unless
391
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__restart_in Bool)
392
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
393
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__restart_act Bool)
394
(declare-var junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
395
(declare-rel junctions2_junctions2__JUNCTIONS2_B_IDL_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
396
(rule (=> 
397
  (and (= junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__state_in)
398
       (= junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__restart_in)
399
       )
400
  (junctions2_junctions2__JUNCTIONS2_B_IDL_unless junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_B_IDL_unless.junctions2_junctions2__state_act)
401
))
402

    
403
; junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until
404
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_1 Int)
405
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.y_1 Int)
406
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.junctions2_junctions2__restart_in Bool)
407
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
408
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_out Int)
409
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.y_out Int)
410
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_2 Int)
411
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_3 Int)
412
(declare-rel junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
413
(rule (=> 
414
  (and (= junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.y_out junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.y_1)
415
       (= junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
416
       (= junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.junctions2_junctions2__restart_in true)
417
       (Junctions2_B_ex junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_1
418
                        false
419
                        junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_2)
420
       (Junctions2_C_en junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_2
421
                        false
422
                        junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_3)
423
       (= junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_3)
424
       )
425
  (junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until.y_out)
426
))
427

    
428
; junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless
429
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__restart_in Bool)
430
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
431
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__restart_act Bool)
432
(declare-var junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
433
(declare-rel junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
434
(rule (=> 
435
  (and (= junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__state_in)
436
       (= junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__restart_in)
437
       )
438
  (junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless.junctions2_junctions2__state_act)
439
))
440

    
441
; junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until
442
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.idJunctions2_Junctions2_1 Int)
443
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.y_1 Int)
444
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.junctions2_junctions2__restart_in Bool)
445
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
446
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.idJunctions2_Junctions2_out Int)
447
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.y_out Int)
448
(declare-rel junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
449
(rule (=> 
450
  (and (= junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.y_out junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.y_1)
451
       (= junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
452
       (= junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.junctions2_junctions2__restart_in true)
453
       (= junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.idJunctions2_Junctions2_1)
454
       )
455
  (junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until.y_out)
456
))
457

    
458
; junctions2_junctions2__JUNCTIONS2_C_IDL_unless
459
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__restart_in Bool)
460
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
461
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__restart_act Bool)
462
(declare-var junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
463
(declare-rel junctions2_junctions2__JUNCTIONS2_C_IDL_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
464
(rule (=> 
465
  (and (= junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__state_in)
466
       (= junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__restart_in)
467
       )
468
  (junctions2_junctions2__JUNCTIONS2_C_IDL_unless junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_C_IDL_unless.junctions2_junctions2__state_act)
469
))
470

    
471
; junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until
472
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_1 Int)
473
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.y_1 Int)
474
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.junctions2_junctions2__restart_in Bool)
475
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
476
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_out Int)
477
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.y_out Int)
478
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_2 Int)
479
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_3 Int)
480
(declare-rel junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
481
(rule (=> 
482
  (and (= junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.y_out junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.y_1)
483
       (= junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
484
       (= junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.junctions2_junctions2__restart_in true)
485
       (Junctions2_C_ex junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_1
486
                        false
487
                        junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_2)
488
       (Junctions2_D_en junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_2
489
                        false
490
                        junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_3)
491
       (= junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_3)
492
       )
493
  (junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until.y_out)
494
))
495

    
496
; junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless
497
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__restart_in Bool)
498
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
499
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__restart_act Bool)
500
(declare-var junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
501
(declare-rel junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
502
(rule (=> 
503
  (and (= junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__state_in)
504
       (= junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__restart_in)
505
       )
506
  (junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless.junctions2_junctions2__state_act)
507
))
508

    
509
; junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until
510
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.idJunctions2_Junctions2_1 Int)
511
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.y_1 Int)
512
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.junctions2_junctions2__restart_in Bool)
513
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
514
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.idJunctions2_Junctions2_out Int)
515
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.y_out Int)
516
(declare-rel junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
517
(rule (=> 
518
  (and (= junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.y_out junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.y_1)
519
       (= junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
520
       (= junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.junctions2_junctions2__restart_in true)
521
       (= junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.idJunctions2_Junctions2_1)
522
       )
523
  (junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until.y_out)
524
))
525

    
526
; junctions2_junctions2__JUNCTIONS2_D_IDL_unless
527
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__restart_in Bool)
528
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
529
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__restart_act Bool)
530
(declare-var junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
531
(declare-rel junctions2_junctions2__JUNCTIONS2_D_IDL_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
532
(rule (=> 
533
  (and (= junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__state_in)
534
       (= junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__restart_in)
535
       )
536
  (junctions2_junctions2__JUNCTIONS2_D_IDL_unless junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_D_IDL_unless.junctions2_junctions2__state_act)
537
))
538

    
539
; junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until
540
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_1 Int)
541
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.y_1 Int)
542
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__restart_in Bool)
543
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
544
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_out Int)
545
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.y_out Int)
546
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_2 Int)
547
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_3 Int)
548
(declare-rel junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
549
(rule (=> 
550
  (and (= junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.y_out junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.y_1)
551
       (= junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
552
       (= junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__restart_in true)
553
       (Junctions2_D_ex junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_1
554
                        false
555
                        junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_2)
556
       (Junctions2_A_en junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_2
557
                        false
558
                        junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_3)
559
       (= junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_3)
560
       )
561
  (junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.y_1 junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until.y_out)
562
))
563

    
564
; junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless
565
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_in Bool)
566
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
567
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_act Bool)
568
(declare-var junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
569
(declare-rel junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
570
(rule (=> 
571
  (and (= junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_act junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_in)
572
       (= junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_in)
573
       )
574
  (junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_in junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_in junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_act)
575
))
576

    
577
; junctions2_junctions2__POINTJunctions2_Junctions2_handler_until
578
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.idJunctions2_Junctions2_1 Int)
579
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.y_1 Int)
580
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.junctions2_junctions2__restart_in Bool)
581
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
582
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.idJunctions2_Junctions2_out Int)
583
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.y_out Int)
584
(declare-rel junctions2_junctions2__POINTJunctions2_Junctions2_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
585
(rule (=> 
586
  (and (= junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.y_out junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.y_1)
587
       (= junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
588
       (= junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.junctions2_junctions2__restart_in false)
589
       (= junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.idJunctions2_Junctions2_1)
590
       )
591
  (junctions2_junctions2__POINTJunctions2_Junctions2_handler_until junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.y_1 junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.junctions2_junctions2__state_in junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__POINTJunctions2_Junctions2_handler_until.y_out)
592
))
593

    
594
; junctions2_junctions2__POINTJunctions2_Junctions2_unless
595
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_in Bool)
596
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
597
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 Int)
598
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.x Int)
599
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act Bool)
600
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
601
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_1 Bool)
602
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_2 Bool)
603
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_3 Bool)
604
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_4 Bool)
605
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_5 Bool)
606
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_6 Bool)
607
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_7 Bool)
608
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_8 Bool)
609
(declare-var junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_9 Bool)
610
(declare-rel junctions2_junctions2__POINTJunctions2_Junctions2_unless (Bool junctions2_junctions2__type Int Int Bool junctions2_junctions2__type))
611
(rule (=> 
612
  (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_9 (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1206))
613
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_8 (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1205))
614
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_7 (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1204))
615
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_6 (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1203))
616
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_5 (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1206) (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.x 0)))
617
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_4 (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1205) (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.x 0)))
618
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_3 (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1204) (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.x 0)))
619
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_2 (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 1203) (> junctions2_junctions2__POINTJunctions2_Junctions2_unless.x 0)))
620
       (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_1 (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 0))
621
       (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_1 false))
622
               (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_2 false))
623
                       (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_3 false))
624
                               (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_4 false))
625
                                       (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_5 false))
626
                                               (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_6 false))
627
                                                       (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_7 false))
628
                                                               (and (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_8 false))
629
                                                                    (and 
630
                                                                    (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_9 false))
631
                                                                    (and 
632
                                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_in)
633
                                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_in)
634
                                                                    ))
635
                                                                    (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_9 true))
636
                                                                    (and 
637
                                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_D_IDL)
638
                                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
639
                                                                    ))
640
                                                                    ))
641
                                                                    (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_8 true))
642
                                                                    (and 
643
                                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_C_IDL)
644
                                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
645
                                                                    ))
646
                                                               ))
647
                                                            (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_7 true))
648
                                                               (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_B_IDL)
649
                                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
650
                                                                    ))
651
                                                       ))
652
                                                    (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_6 true))
653
                                                       (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_A_IDL)
654
                                                            (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
655
                                                            ))
656
                                               ))
657
                                            (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_5 true))
658
                                               (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_D__TO__JUNCTIONS2_A_1)
659
                                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
660
                                                    ))
661
                                       ))
662
                                    (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_4 true))
663
                                       (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_C__TO__JUNCTIONS2_D_1)
664
                                            (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
665
                                            ))
666
                               ))
667
                            (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_3 true))
668
                               (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_B__TO__JUNCTIONS2_C_1)
669
                                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
670
                                    ))
671
                       ))
672
                    (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_2 true))
673
                       (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1)
674
                            (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
675
                            ))
676
               ))
677
            (or (not (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.__junctions2_junctions2__POINTJunctions2_Junctions2_unless_1 true))
678
               (and (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act POINT__TO__JUNCTIONS2_A_1)
679
                    (= junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act true)
680
                    ))
681
       )
682
       )
683
  (junctions2_junctions2__POINTJunctions2_Junctions2_unless junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_in junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_in junctions2_junctions2__POINTJunctions2_Junctions2_unless.idJunctions2_Junctions2_1 junctions2_junctions2__POINTJunctions2_Junctions2_unless.x junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__restart_act junctions2_junctions2__POINTJunctions2_Junctions2_unless.junctions2_junctions2__state_act)
684
))
685

    
686
; junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until
687
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_1 Int)
688
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.y_1 Int)
689
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__restart_in Bool)
690
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__type)
691
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_out Int)
692
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.y_out Int)
693
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_2 Int)
694
(declare-rel junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until (Int Int Bool junctions2_junctions2__type Int Int))
695
(rule (=> 
696
  (and (= junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.y_out junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.y_1)
697
       (= junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
698
       (= junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__restart_in true)
699
       (Junctions2_A_en junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_1
700
                        false
701
                        junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_2)
702
       (= junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_2)
703
       )
704
  (junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_1 junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.y_1 junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__restart_in junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.junctions2_junctions2__state_in junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.idJunctions2_Junctions2_out junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until.y_out)
705
))
706

    
707
; junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless
708
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_in Bool)
709
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_in junctions2_junctions2__type)
710
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_act Bool)
711
(declare-var junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_act junctions2_junctions2__type)
712
(declare-rel junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless (Bool junctions2_junctions2__type Bool junctions2_junctions2__type))
713
(rule (=> 
714
  (and (= junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_act junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_in)
715
       (= junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_in)
716
       )
717
  (junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_in junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_in junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__restart_act junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless.junctions2_junctions2__state_act)
718
))
719

    
720
; Junctions2_Junctions2_node
721
(declare-var Junctions2_Junctions2_node.idJunctions2_Junctions2_1 Int)
722
(declare-var Junctions2_Junctions2_node.x Int)
723
(declare-var Junctions2_Junctions2_node.y_1 Int)
724
(declare-var Junctions2_Junctions2_node.idJunctions2_Junctions2 Int)
725
(declare-var Junctions2_Junctions2_node.y Int)
726
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c Bool)
727
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c junctions2_junctions2__type)
728
(declare-var Junctions2_Junctions2_node.ni_4._arrow._first_c Bool)
729
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m Bool)
730
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m junctions2_junctions2__type)
731
(declare-var Junctions2_Junctions2_node.ni_4._arrow._first_m Bool)
732
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x Bool)
733
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x junctions2_junctions2__type)
734
(declare-var Junctions2_Junctions2_node.ni_4._arrow._first_x Bool)
735
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_1 Bool)
736
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_10 junctions2_junctions2__type)
737
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_11 Bool)
738
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_12 junctions2_junctions2__type)
739
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_13 Bool)
740
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_14 junctions2_junctions2__type)
741
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_15 Bool)
742
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_16 junctions2_junctions2__type)
743
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_17 Bool)
744
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_18 junctions2_junctions2__type)
745
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_19 Bool)
746
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_2 junctions2_junctions2__type)
747
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_20 junctions2_junctions2__type)
748
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_21 Bool)
749
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_22 junctions2_junctions2__type)
750
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_23 Int)
751
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_24 Int)
752
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_25 Bool)
753
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_26 junctions2_junctions2__type)
754
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_27 Int)
755
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_28 Int)
756
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_29 Bool)
757
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_3 Bool)
758
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_30 junctions2_junctions2__type)
759
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_31 Int)
760
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_32 Int)
761
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_33 Bool)
762
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_34 junctions2_junctions2__type)
763
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_35 Int)
764
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_36 Int)
765
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_37 Bool)
766
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_38 junctions2_junctions2__type)
767
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_39 Int)
768
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_4 junctions2_junctions2__type)
769
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_40 Int)
770
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_41 Bool)
771
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_42 junctions2_junctions2__type)
772
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_43 Int)
773
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_44 Int)
774
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_45 Bool)
775
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_46 junctions2_junctions2__type)
776
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_47 Int)
777
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_48 Int)
778
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_49 Bool)
779
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_5 Bool)
780
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_50 junctions2_junctions2__type)
781
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_51 Int)
782
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_52 Int)
783
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_53 Bool)
784
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_54 junctions2_junctions2__type)
785
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_55 Int)
786
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_56 Int)
787
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_57 Bool)
788
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_58 junctions2_junctions2__type)
789
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_59 Int)
790
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_6 junctions2_junctions2__type)
791
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_60 Int)
792
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_61 Bool)
793
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_7 Bool)
794
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_8 junctions2_junctions2__type)
795
(declare-var Junctions2_Junctions2_node.__Junctions2_Junctions2_node_9 Bool)
796
(declare-var Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Bool)
797
(declare-var Junctions2_Junctions2_node.junctions2_junctions2__next_state_in junctions2_junctions2__type)
798
(declare-var Junctions2_Junctions2_node.junctions2_junctions2__restart_act Bool)
799
(declare-var Junctions2_Junctions2_node.junctions2_junctions2__restart_in Bool)
800
(declare-var Junctions2_Junctions2_node.junctions2_junctions2__state_act junctions2_junctions2__type)
801
(declare-var Junctions2_Junctions2_node.junctions2_junctions2__state_in junctions2_junctions2__type)
802
(declare-rel Junctions2_Junctions2_node_reset (Bool junctions2_junctions2__type Bool Bool junctions2_junctions2__type Bool))
803
(declare-rel Junctions2_Junctions2_node_step (Int Int Int Int Int Bool junctions2_junctions2__type Bool Bool junctions2_junctions2__type Bool))
804

    
805
(rule (=> 
806
  (and 
807
       (= Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c)
808
       (= Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c)
809
       (= Junctions2_Junctions2_node.ni_4._arrow._first_m true)
810
  )
811
  (Junctions2_Junctions2_node_reset Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
812
                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
813
                                    Junctions2_Junctions2_node.ni_4._arrow._first_c
814
                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m
815
                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m
816
                                    Junctions2_Junctions2_node.ni_4._arrow._first_m)
817
))
818

    
819
(rule (=> 
820
  (and (= Junctions2_Junctions2_node.ni_4._arrow._first_m Junctions2_Junctions2_node.ni_4._arrow._first_c)
821
       (and (= Junctions2_Junctions2_node.__Junctions2_Junctions2_node_61 (ite Junctions2_Junctions2_node.ni_4._arrow._first_m true false))
822
            (= Junctions2_Junctions2_node.ni_4._arrow._first_x false))
823
       (and (or (not (= Junctions2_Junctions2_node.__Junctions2_Junctions2_node_61 false))
824
               (and (= Junctions2_Junctions2_node.junctions2_junctions2__state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c)
825
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c)
826
                    ))
827
            (or (not (= Junctions2_Junctions2_node.__Junctions2_Junctions2_node_61 true))
828
               (and (= Junctions2_Junctions2_node.junctions2_junctions2__state_in POINTJunctions2_Junctions2)
829
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_in false)
830
                    ))
831
       )
832
       (and (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_A_IDL))
833
               (and (junctions2_junctions2__JUNCTIONS2_A_IDL_unless Junctions2_Junctions2_node.junctions2_junctions2__restart_in
834
                                                                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
835
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_7
836
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_8)
837
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_8)
838
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_7)
839
                    ))
840
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1))
841
               (and (junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_unless 
842
                    Junctions2_Junctions2_node.junctions2_junctions2__restart_in
843
                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
844
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_15
845
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_16)
846
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_16)
847
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_15)
848
                    ))
849
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_B_IDL))
850
               (and (junctions2_junctions2__JUNCTIONS2_B_IDL_unless Junctions2_Junctions2_node.junctions2_junctions2__restart_in
851
                                                                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
852
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_5
853
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_6)
854
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_6)
855
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_5)
856
                    ))
857
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_B__TO__JUNCTIONS2_C_1))
858
               (and (junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_unless 
859
                    Junctions2_Junctions2_node.junctions2_junctions2__restart_in
860
                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
861
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_13
862
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_14)
863
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_14)
864
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_13)
865
                    ))
866
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_C_IDL))
867
               (and (junctions2_junctions2__JUNCTIONS2_C_IDL_unless Junctions2_Junctions2_node.junctions2_junctions2__restart_in
868
                                                                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
869
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_3
870
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_4)
871
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_4)
872
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_3)
873
                    ))
874
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_C__TO__JUNCTIONS2_D_1))
875
               (and (junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_unless 
876
                    Junctions2_Junctions2_node.junctions2_junctions2__restart_in
877
                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
878
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_11
879
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_12)
880
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_12)
881
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_11)
882
                    ))
883
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_D_IDL))
884
               (and (junctions2_junctions2__JUNCTIONS2_D_IDL_unless Junctions2_Junctions2_node.junctions2_junctions2__restart_in
885
                                                                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
886
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_1
887
                                                                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_2)
888
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_2)
889
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_1)
890
                    ))
891
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in JUNCTIONS2_D__TO__JUNCTIONS2_A_1))
892
               (and (junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_unless 
893
                    Junctions2_Junctions2_node.junctions2_junctions2__restart_in
894
                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
895
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_9
896
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_10)
897
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_10)
898
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_9)
899
                    ))
900
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in POINTJunctions2_Junctions2))
901
               (and (junctions2_junctions2__POINTJunctions2_Junctions2_unless 
902
                    Junctions2_Junctions2_node.junctions2_junctions2__restart_in
903
                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
904
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
905
                    Junctions2_Junctions2_node.x
906
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_19
907
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_20)
908
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_20)
909
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_19)
910
                    ))
911
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_in POINT__TO__JUNCTIONS2_A_1))
912
               (and (junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_unless 
913
                    Junctions2_Junctions2_node.junctions2_junctions2__restart_in
914
                    Junctions2_Junctions2_node.junctions2_junctions2__state_in
915
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_17
916
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_18)
917
                    (= Junctions2_Junctions2_node.junctions2_junctions2__state_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_18)
918
                    (= Junctions2_Junctions2_node.junctions2_junctions2__restart_act Junctions2_Junctions2_node.__Junctions2_Junctions2_node_17)
919
                    ))
920
       )
921
       (and (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_A_IDL))
922
               (and (junctions2_junctions2__JUNCTIONS2_A_IDL_handler_until 
923
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
924
                    Junctions2_Junctions2_node.y_1
925
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_33
926
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_34
927
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_35
928
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_36)
929
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_36)
930
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_34)
931
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_33)
932
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_35)
933
                    ))
934
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1))
935
               (and (junctions2_junctions2__JUNCTIONS2_A__TO__JUNCTIONS2_JUNCTIONS2JUNCTION1209_1_handler_until 
936
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
937
                    Junctions2_Junctions2_node.x
938
                    Junctions2_Junctions2_node.y_1
939
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_49
940
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_50
941
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_51
942
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_52)
943
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_52)
944
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_50)
945
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_49)
946
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_51)
947
                    ))
948
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_B_IDL))
949
               (and (junctions2_junctions2__JUNCTIONS2_B_IDL_handler_until 
950
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
951
                    Junctions2_Junctions2_node.y_1
952
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_29
953
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_30
954
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_31
955
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_32)
956
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_32)
957
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_30)
958
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_29)
959
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_31)
960
                    ))
961
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_B__TO__JUNCTIONS2_C_1))
962
               (and (junctions2_junctions2__JUNCTIONS2_B__TO__JUNCTIONS2_C_1_handler_until 
963
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
964
                    Junctions2_Junctions2_node.y_1
965
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_45
966
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_46
967
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_47
968
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_48)
969
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_48)
970
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_46)
971
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_45)
972
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_47)
973
                    ))
974
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_C_IDL))
975
               (and (junctions2_junctions2__JUNCTIONS2_C_IDL_handler_until 
976
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
977
                    Junctions2_Junctions2_node.y_1
978
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_25
979
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_26
980
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_27
981
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_28)
982
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_28)
983
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_26)
984
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_25)
985
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_27)
986
                    ))
987
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_C__TO__JUNCTIONS2_D_1))
988
               (and (junctions2_junctions2__JUNCTIONS2_C__TO__JUNCTIONS2_D_1_handler_until 
989
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
990
                    Junctions2_Junctions2_node.y_1
991
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_41
992
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_42
993
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_43
994
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_44)
995
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_44)
996
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_42)
997
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_41)
998
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_43)
999
                    ))
1000
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_D_IDL))
1001
               (and (junctions2_junctions2__JUNCTIONS2_D_IDL_handler_until 
1002
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
1003
                    Junctions2_Junctions2_node.y_1
1004
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_21
1005
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_22
1006
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_23
1007
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_24)
1008
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_24)
1009
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_22)
1010
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_21)
1011
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_23)
1012
                    ))
1013
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act JUNCTIONS2_D__TO__JUNCTIONS2_A_1))
1014
               (and (junctions2_junctions2__JUNCTIONS2_D__TO__JUNCTIONS2_A_1_handler_until 
1015
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
1016
                    Junctions2_Junctions2_node.y_1
1017
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_37
1018
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_38
1019
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_39
1020
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_40)
1021
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_40)
1022
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_38)
1023
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_37)
1024
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_39)
1025
                    ))
1026
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act POINTJunctions2_Junctions2))
1027
               (and (junctions2_junctions2__POINTJunctions2_Junctions2_handler_until 
1028
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
1029
                    Junctions2_Junctions2_node.y_1
1030
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_57
1031
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_58
1032
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_59
1033
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_60)
1034
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_60)
1035
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_58)
1036
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_57)
1037
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_59)
1038
                    ))
1039
            (or (not (= Junctions2_Junctions2_node.junctions2_junctions2__state_act POINT__TO__JUNCTIONS2_A_1))
1040
               (and (junctions2_junctions2__POINT__TO__JUNCTIONS2_A_1_handler_until 
1041
                    Junctions2_Junctions2_node.idJunctions2_Junctions2_1
1042
                    Junctions2_Junctions2_node.y_1
1043
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_53
1044
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_54
1045
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_55
1046
                    Junctions2_Junctions2_node.__Junctions2_Junctions2_node_56)
1047
                    (= Junctions2_Junctions2_node.y Junctions2_Junctions2_node.__Junctions2_Junctions2_node_56)
1048
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_state_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_54)
1049
                    (= Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in Junctions2_Junctions2_node.__Junctions2_Junctions2_node_53)
1050
                    (= Junctions2_Junctions2_node.idJunctions2_Junctions2 Junctions2_Junctions2_node.__Junctions2_Junctions2_node_55)
1051
                    ))
1052
       )
1053
       (= Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x Junctions2_Junctions2_node.junctions2_junctions2__next_state_in)
1054
       (= Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x Junctions2_Junctions2_node.junctions2_junctions2__next_restart_in)
1055
       )
1056
  (Junctions2_Junctions2_node_step Junctions2_Junctions2_node.idJunctions2_Junctions2_1
1057
                                   Junctions2_Junctions2_node.x
1058
                                   Junctions2_Junctions2_node.y_1
1059
                                   Junctions2_Junctions2_node.idJunctions2_Junctions2
1060
                                   Junctions2_Junctions2_node.y
1061
                                   Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
1062
                                   Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
1063
                                   Junctions2_Junctions2_node.ni_4._arrow._first_c
1064
                                   Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x
1065
                                   Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x
1066
                                   Junctions2_Junctions2_node.ni_4._arrow._first_x)
1067
))
1068

    
1069
; Junctions2_Junctions2
1070
(declare-var Junctions2_Junctions2.x Int)
1071
(declare-var Junctions2_Junctions2.y Int)
1072
(declare-var Junctions2_Junctions2.__Junctions2_Junctions2_2_c Int)
1073
(declare-var Junctions2_Junctions2.__Junctions2_Junctions2_3_c Int)
1074
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c Bool)
1075
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c junctions2_junctions2__type)
1076
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c Bool)
1077
(declare-var Junctions2_Junctions2.ni_3._arrow._first_c Bool)
1078
(declare-var Junctions2_Junctions2.__Junctions2_Junctions2_2_m Int)
1079
(declare-var Junctions2_Junctions2.__Junctions2_Junctions2_3_m Int)
1080
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m Bool)
1081
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m junctions2_junctions2__type)
1082
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m Bool)
1083
(declare-var Junctions2_Junctions2.ni_3._arrow._first_m Bool)
1084
(declare-var Junctions2_Junctions2.__Junctions2_Junctions2_2_x Int)
1085
(declare-var Junctions2_Junctions2.__Junctions2_Junctions2_3_x Int)
1086
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x Bool)
1087
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x junctions2_junctions2__type)
1088
(declare-var Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_x Bool)
1089
(declare-var Junctions2_Junctions2.ni_3._arrow._first_x Bool)
1090
(declare-var Junctions2_Junctions2.__Junctions2_Junctions2_1 Bool)
1091
(declare-var Junctions2_Junctions2.idJunctions2_Junctions2 Int)
1092
(declare-var Junctions2_Junctions2.idJunctions2_Junctions2_1 Int)
1093
(declare-var Junctions2_Junctions2.y_1 Int)
1094
(declare-rel Junctions2_Junctions2_reset (Int Int Bool junctions2_junctions2__type Bool Bool Int Int Bool junctions2_junctions2__type Bool Bool))
1095
(declare-rel Junctions2_Junctions2_step (Int Int Int Int Bool junctions2_junctions2__type Bool Bool Int Int Bool junctions2_junctions2__type Bool Bool))
1096

    
1097
(rule (=> 
1098
  (and 
1099
       (= Junctions2_Junctions2.__Junctions2_Junctions2_2_m Junctions2_Junctions2.__Junctions2_Junctions2_2_c)
1100
       (= Junctions2_Junctions2.__Junctions2_Junctions2_3_m Junctions2_Junctions2.__Junctions2_Junctions2_3_c)
1101
       (= Junctions2_Junctions2.ni_3._arrow._first_m true)
1102
       (Junctions2_Junctions2_node_reset Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
1103
                                         Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
1104
                                         Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c
1105
                                         Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m
1106
                                         Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m
1107
                                         Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m)
1108
  )
1109
  (Junctions2_Junctions2_reset Junctions2_Junctions2.__Junctions2_Junctions2_2_c
1110
                               Junctions2_Junctions2.__Junctions2_Junctions2_3_c
1111
                               Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
1112
                               Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
1113
                               Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c
1114
                               Junctions2_Junctions2.ni_3._arrow._first_c
1115
                               Junctions2_Junctions2.__Junctions2_Junctions2_2_m
1116
                               Junctions2_Junctions2.__Junctions2_Junctions2_3_m
1117
                               Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m
1118
                               Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m
1119
                               Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m
1120
                               Junctions2_Junctions2.ni_3._arrow._first_m)
1121
))
1122

    
1123
(rule (=> 
1124
  (and (= Junctions2_Junctions2.ni_3._arrow._first_m Junctions2_Junctions2.ni_3._arrow._first_c)
1125
       (and (= Junctions2_Junctions2.__Junctions2_Junctions2_1 (ite Junctions2_Junctions2.ni_3._arrow._first_m true false))
1126
            (= Junctions2_Junctions2.ni_3._arrow._first_x false))
1127
       (and (or (not (= Junctions2_Junctions2.__Junctions2_Junctions2_1 false))
1128
               (and (= Junctions2_Junctions2.y_1 Junctions2_Junctions2.__Junctions2_Junctions2_3_c)
1129
                    (= Junctions2_Junctions2.idJunctions2_Junctions2_1 Junctions2_Junctions2.__Junctions2_Junctions2_2_c)
1130
                    ))
1131
            (or (not (= Junctions2_Junctions2.__Junctions2_Junctions2_1 true))
1132
               (and (= Junctions2_Junctions2.y_1 11111)
1133
                    (= Junctions2_Junctions2.idJunctions2_Junctions2_1 0)
1134
                    ))
1135
       )
1136
       (and (= Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c)
1137
            (= Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c)
1138
            (= Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c)
1139
            )
1140
       (Junctions2_Junctions2_node_step Junctions2_Junctions2.idJunctions2_Junctions2_1
1141
                                        Junctions2_Junctions2.x
1142
                                        Junctions2_Junctions2.y_1
1143
                                        Junctions2_Junctions2.idJunctions2_Junctions2
1144
                                        Junctions2_Junctions2.y
1145
                                        Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m
1146
                                        Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m
1147
                                        Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m
1148
                                        Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x
1149
                                        Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x
1150
                                        Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_x)
1151
       (= Junctions2_Junctions2.__Junctions2_Junctions2_3_x Junctions2_Junctions2.y)
1152
       (= Junctions2_Junctions2.__Junctions2_Junctions2_2_x Junctions2_Junctions2.idJunctions2_Junctions2)
1153
       )
1154
  (Junctions2_Junctions2_step Junctions2_Junctions2.x
1155
                              Junctions2_Junctions2.y
1156
                              Junctions2_Junctions2.__Junctions2_Junctions2_2_c
1157
                              Junctions2_Junctions2.__Junctions2_Junctions2_3_c
1158
                              Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
1159
                              Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
1160
                              Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c
1161
                              Junctions2_Junctions2.ni_3._arrow._first_c
1162
                              Junctions2_Junctions2.__Junctions2_Junctions2_2_x
1163
                              Junctions2_Junctions2.__Junctions2_Junctions2_3_x
1164
                              Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x
1165
                              Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x
1166
                              Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_x
1167
                              Junctions2_Junctions2.ni_3._arrow._first_x)
1168
))
1169

    
1170
; Junctions2
1171
(declare-var Junctions2.In1_1_1 Int)
1172
(declare-var Junctions2.y_1_1 Int)
1173
(declare-var Junctions2.ni_0._arrow._first_c Bool)
1174
(declare-var Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_c Int)
1175
(declare-var Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_c Int)
1176
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c Bool)
1177
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c junctions2_junctions2__type)
1178
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c Bool)
1179
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_c Bool)
1180
(declare-var Junctions2.ni_0._arrow._first_m Bool)
1181
(declare-var Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_m Int)
1182
(declare-var Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_m Int)
1183
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m Bool)
1184
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m junctions2_junctions2__type)
1185
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m Bool)
1186
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_m Bool)
1187
(declare-var Junctions2.ni_0._arrow._first_x Bool)
1188
(declare-var Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_x Int)
1189
(declare-var Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_x Int)
1190
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x Bool)
1191
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x junctions2_junctions2__type)
1192
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_x Bool)
1193
(declare-var Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_x Bool)
1194
(declare-var Junctions2.Junctions2_1_1 Int)
1195
(declare-var Junctions2.__Junctions2_1 Bool)
1196
(declare-var Junctions2.i_virtual_local Real)
1197
(declare-rel Junctions2_reset (Bool Int Int Bool junctions2_junctions2__type Bool Bool Bool Int Int Bool junctions2_junctions2__type Bool Bool))
1198
(declare-rel Junctions2_step (Int Int Bool Int Int Bool junctions2_junctions2__type Bool Bool Bool Int Int Bool junctions2_junctions2__type Bool Bool))
1199

    
1200
(rule (=> 
1201
  (and 
1202
       
1203
       (Junctions2_Junctions2_reset Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_c
1204
                                    Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_c
1205
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
1206
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
1207
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c
1208
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_c
1209
                                    Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_m
1210
                                    Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_m
1211
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m
1212
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m
1213
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m
1214
                                    Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_m)
1215
       (= Junctions2.ni_0._arrow._first_m true)
1216
  )
1217
  (Junctions2_reset Junctions2.ni_0._arrow._first_c
1218
                    Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_c
1219
                    Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_c
1220
                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
1221
                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
1222
                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c
1223
                    Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_c
1224
                    Junctions2.ni_0._arrow._first_m
1225
                    Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_m
1226
                    Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_m
1227
                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m
1228
                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m
1229
                    Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m
1230
                    Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_m)
1231
))
1232

    
1233
(rule (=> 
1234
  (and (and (= Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_m Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_c)
1235
            (= Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_m Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_c)
1236
            (= Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c)
1237
            (= Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c)
1238
            (= Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c)
1239
            (= Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_m Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_c)
1240
            )
1241
       (Junctions2_Junctions2_step Junctions2.In1_1_1
1242
                                   Junctions2.Junctions2_1_1
1243
                                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_m
1244
                                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_m
1245
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_m
1246
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_m
1247
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_m
1248
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_m
1249
                                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_x
1250
                                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_x
1251
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x
1252
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x
1253
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_x
1254
                                   Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_x)
1255
       (= Junctions2.y_1_1 Junctions2.Junctions2_1_1)
1256
       (= Junctions2.ni_0._arrow._first_m Junctions2.ni_0._arrow._first_c)
1257
       (and (= Junctions2.__Junctions2_1 (ite Junctions2.ni_0._arrow._first_m true false))
1258
            (= Junctions2.ni_0._arrow._first_x false))
1259
       (and (or (not (= Junctions2.__Junctions2_1 true))
1260
               (= Junctions2.i_virtual_local 0.))
1261
            (or (not (= Junctions2.__Junctions2_1 false))
1262
               (= Junctions2.i_virtual_local 1.))
1263
       )
1264
       )
1265
  (Junctions2_step Junctions2.In1_1_1
1266
                   Junctions2.y_1_1
1267
                   Junctions2.ni_0._arrow._first_c
1268
                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_c
1269
                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_c
1270
                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_c
1271
                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_c
1272
                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_c
1273
                   Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_c
1274
                   Junctions2.ni_0._arrow._first_x
1275
                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_2_x
1276
                   Junctions2.ni_1.Junctions2_Junctions2.__Junctions2_Junctions2_3_x
1277
                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_62_x
1278
                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.__Junctions2_Junctions2_node_63_x
1279
                   Junctions2.ni_1.Junctions2_Junctions2.ni_2.Junctions2_Junctions2_node.ni_4._arrow._first_x
1280
                   Junctions2.ni_1.Junctions2_Junctions2.ni_3._arrow._first_x)
1281
))
1282