Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions5 / Junctions5.smt2 @ eb639349

History | View | Annotate | Download (98.5 KB)

1
(declare-datatypes () ((junctions5_junctions5__type POINTJunctions5_Junctions5 POINT__TO__JUNCTIONS5_A_1 JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1 JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2 JUNCTIONS5_A_IDL JUNCTIONS5_B_IDL)));
2

    
3
; Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action
4
(declare-var Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action.a_1 Real)
5
(declare-var Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action.a Real)
6
(declare-rel Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action (Real Real))
7
(rule (=> 
8
  (= Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action.a (+ Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action.a_1 10.))
9
  (Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action.a_1 Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action.a)
10
))
11

    
12
; Junctions5_A_ex
13
(declare-var Junctions5_A_ex.a_1 Real)
14
(declare-var Junctions5_A_ex.idJunctions5_Junctions5_1 Int)
15
(declare-var Junctions5_A_ex.isInner Bool)
16
(declare-var Junctions5_A_ex.a Real)
17
(declare-var Junctions5_A_ex.idJunctions5_Junctions5 Int)
18
(declare-var Junctions5_A_ex.__Junctions5_A_ex_1 Bool)
19
(declare-var Junctions5_A_ex.a_2 Real)
20
(declare-var Junctions5_A_ex.idJunctions5_Junctions5_2 Int)
21
(declare-rel Junctions5_A_ex (Real Int Bool Real Int))
22
(rule (=> 
23
  (and (= Junctions5_A_ex.__Junctions5_A_ex_1 (not Junctions5_A_ex.isInner))
24
       (and (or (not (= Junctions5_A_ex.__Junctions5_A_ex_1 false))
25
               (and (= Junctions5_A_ex.idJunctions5_Junctions5_2 Junctions5_A_ex.idJunctions5_Junctions5_1)
26
                    (= Junctions5_A_ex.a_2 Junctions5_A_ex.a_1)
27
                    ))
28
            (or (not (= Junctions5_A_ex.__Junctions5_A_ex_1 true))
29
               (and (= Junctions5_A_ex.idJunctions5_Junctions5_2 0)
30
                    (= Junctions5_A_ex.a_2 (+ Junctions5_A_ex.a_1 10000.))
31
                    ))
32
       )
33
       (= Junctions5_A_ex.idJunctions5_Junctions5 Junctions5_A_ex.idJunctions5_Junctions5_1)
34
       (= Junctions5_A_ex.a Junctions5_A_ex.a_2)
35
       )
36
  (Junctions5_A_ex Junctions5_A_ex.a_1 Junctions5_A_ex.idJunctions5_Junctions5_1 Junctions5_A_ex.isInner Junctions5_A_ex.a Junctions5_A_ex.idJunctions5_Junctions5)
37
))
38

    
39
; Junctions5_B_en
40
(declare-var Junctions5_B_en.idJunctions5_Junctions5_1 Int)
41
(declare-var Junctions5_B_en.isInner Bool)
42
(declare-var Junctions5_B_en.idJunctions5_Junctions5 Int)
43
(declare-rel Junctions5_B_en (Int Bool Int))
44
(rule (=> 
45
  (= Junctions5_B_en.idJunctions5_Junctions5 1283)
46
  (Junctions5_B_en Junctions5_B_en.idJunctions5_Junctions5_1 Junctions5_B_en.isInner Junctions5_B_en.idJunctions5_Junctions5)
47
))
48

    
49
; Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action
50
(declare-var Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action.a_1 Real)
51
(declare-var Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action.a Real)
52
(declare-rel Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action (Real Real))
53
(rule (=> 
54
  (= Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action.a (+ Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action.a_1 100.))
55
  (Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action.a_1 Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action.a)
56
))
57

    
58
; Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action
59
(declare-var Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action.a_1 Real)
60
(declare-var Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action.a Real)
61
(declare-rel Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action (Real Real))
62
(rule (=> 
63
  (= Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action.a (+ Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action.a_1 1000.))
64
  (Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action.a_1 Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action.a)
65
))
66

    
67
; Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action
68
(declare-var Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action.a_1 Real)
69
(declare-var Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action.a Real)
70
(declare-rel Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action (Real Real))
71
(rule (=> 
72
  (= Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action.a (+ Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action.a_1 1.))
73
  (Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action.a_1 Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action.a)
74
))
75

    
76
; Junctions5_A_en
77
(declare-var Junctions5_A_en.idJunctions5_Junctions5_1 Int)
78
(declare-var Junctions5_A_en.isInner Bool)
79
(declare-var Junctions5_A_en.idJunctions5_Junctions5 Int)
80
(declare-rel Junctions5_A_en (Int Bool Int))
81
(rule (=> 
82
  (= Junctions5_A_en.idJunctions5_Junctions5 1282)
83
  (Junctions5_A_en Junctions5_A_en.idJunctions5_Junctions5_1 Junctions5_A_en.isInner Junctions5_A_en.idJunctions5_Junctions5)
84
))
85

    
86
; junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until
87
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.idJunctions5_Junctions5_1 Int)
88
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.a_1 Real)
89
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.junctions5_junctions5__restart_in Bool)
90
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.junctions5_junctions5__state_in junctions5_junctions5__type)
91
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.a_out Real)
92
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.idJunctions5_Junctions5_out Int)
93
(declare-rel junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until (Int Real Bool junctions5_junctions5__type Real Int))
94
(rule (=> 
95
  (and (= junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.junctions5_junctions5__state_in POINTJunctions5_Junctions5)
96
       (= junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.junctions5_junctions5__restart_in true)
97
       (= junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.idJunctions5_Junctions5_out junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.idJunctions5_Junctions5_1)
98
       (= junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.a_out junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.a_1)
99
       )
100
  (junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.idJunctions5_Junctions5_1 junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.a_1 junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.a_out junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until.idJunctions5_Junctions5_out)
101
))
102

    
103
; junctions5_junctions5__JUNCTIONS5_A_IDL_unless
104
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__restart_in Bool)
105
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__state_in junctions5_junctions5__type)
106
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__restart_act Bool)
107
(declare-var junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__state_act junctions5_junctions5__type)
108
(declare-rel junctions5_junctions5__JUNCTIONS5_A_IDL_unless (Bool junctions5_junctions5__type Bool junctions5_junctions5__type))
109
(rule (=> 
110
  (and (= junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__state_act junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__state_in)
111
       (= junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__restart_in)
112
       )
113
  (junctions5_junctions5__JUNCTIONS5_A_IDL_unless junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_A_IDL_unless.junctions5_junctions5__state_act)
114
))
115

    
116
; junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until
117
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_1 Int)
118
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.x Int)
119
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_1 Real)
120
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.junctions5_junctions5__restart_in Bool)
121
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.junctions5_junctions5__state_in junctions5_junctions5__type)
122
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_out Real)
123
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_out Int)
124
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 Bool)
125
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 Bool)
126
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_3 Int)
127
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_4 Real)
128
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_5 Int)
129
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_6 Real)
130
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_7 Real)
131
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a Real)
132
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_2 Real)
133
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_3 Real)
134
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_4 Real)
135
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_5 Real)
136
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5 Int)
137
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_2 Int)
138
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_3 Int)
139
(declare-rel junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until (Int Int Real Bool junctions5_junctions5__type Real Int))
140
(rule (=> 
141
  (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.junctions5_junctions5__state_in POINTJunctions5_Junctions5)
142
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.junctions5_junctions5__restart_in true)
143
       (Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action 
144
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_1
145
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_2)
146
       (Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action 
147
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_2
148
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_7)
149
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 (>= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.x 2))
150
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 true))
151
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_7))
152
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 false))
153
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_2))
154
       )
155
       (Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action 
156
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_3
157
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_6)
158
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 (and (>= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.x 2) (>= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.x 4)))
159
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 true))
160
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_4 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_6))
161
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 false))
162
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_4 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_3))
163
       )
164
       (Junctions5_A_ex junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_4
165
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_1
166
                        false
167
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_4
168
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_5)
169
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 true))
170
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_2 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_5))
171
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 false))
172
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_2 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_1))
173
       )
174
       (Junctions5_B_en junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_2
175
                        false
176
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_3)
177
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 false))
178
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_2)
179
                    (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 true))
180
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_1))
181
                         (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 false))
182
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_1))
183
                    )
184
                    ))
185
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 true))
186
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_3)
187
                    (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_3)
188
                    ))
189
       )
190
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_out junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5)
191
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 false))
192
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_4)
193
                    (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 true))
194
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_3))
195
                         (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_2 false))
196
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_2))
197
                    )
198
                    ))
199
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_1 true))
200
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until_4)
201
                    (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_5)
202
                    ))
203
       )
204
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_out junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a)
205
       )
206
  (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_1 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.x junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_1 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.a_out junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until.idJunctions5_Junctions5_out)
207
))
208

    
209
; junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless
210
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__restart_in Bool)
211
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__state_in junctions5_junctions5__type)
212
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__restart_act Bool)
213
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__state_act junctions5_junctions5__type)
214
(declare-rel junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless (Bool junctions5_junctions5__type Bool junctions5_junctions5__type))
215
(rule (=> 
216
  (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__state_act junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__state_in)
217
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__restart_in)
218
       )
219
  (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless.junctions5_junctions5__state_act)
220
))
221

    
222
; junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until
223
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_1 Int)
224
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.x Int)
225
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_1 Real)
226
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.junctions5_junctions5__restart_in Bool)
227
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.junctions5_junctions5__state_in junctions5_junctions5__type)
228
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_out Real)
229
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_out Int)
230
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 Bool)
231
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 Bool)
232
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_3 Int)
233
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_4 Real)
234
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_5 Int)
235
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_6 Real)
236
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_7 Real)
237
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a Real)
238
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_2 Real)
239
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_3 Real)
240
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_4 Real)
241
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_5 Real)
242
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5 Int)
243
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_2 Int)
244
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_3 Int)
245
(declare-rel junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until (Int Int Real Bool junctions5_junctions5__type Real Int))
246
(rule (=> 
247
  (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.junctions5_junctions5__state_in POINTJunctions5_Junctions5)
248
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.junctions5_junctions5__restart_in true)
249
       (Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action 
250
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_1
251
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_2)
252
       (Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action 
253
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_2
254
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_7)
255
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 (>= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.x 2))
256
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 true))
257
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_7))
258
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 false))
259
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_2))
260
       )
261
       (Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action 
262
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_3
263
       junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_6)
264
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 (and (>= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.x 2) (>= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.x 4)))
265
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 true))
266
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_4 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_6))
267
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 false))
268
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_4 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_3))
269
       )
270
       (Junctions5_A_ex junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_4
271
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_1
272
                        false
273
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_4
274
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_5)
275
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 true))
276
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_2 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_5))
277
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 false))
278
               (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_2 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_1))
279
       )
280
       (Junctions5_B_en junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_2
281
                        false
282
                        junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_3)
283
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 false))
284
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_2)
285
                    (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 true))
286
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_1))
287
                         (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 false))
288
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_1))
289
                    )
290
                    ))
291
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 true))
292
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_3 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_3)
293
                    (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_3)
294
                    ))
295
       )
296
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_out junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5)
297
       (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 false))
298
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_4)
299
                    (and (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 true))
300
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_3))
301
                         (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_2 false))
302
                            (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_2))
303
                    )
304
                    ))
305
            (or (not (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_1 true))
306
               (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_5 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.__junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until_4)
307
                    (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_5)
308
                    ))
309
       )
310
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_out junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a)
311
       )
312
  (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_1 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.x junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_1 junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.a_out junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until.idJunctions5_Junctions5_out)
313
))
314

    
315
; junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless
316
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__restart_in Bool)
317
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__state_in junctions5_junctions5__type)
318
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__restart_act Bool)
319
(declare-var junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__state_act junctions5_junctions5__type)
320
(declare-rel junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless (Bool junctions5_junctions5__type Bool junctions5_junctions5__type))
321
(rule (=> 
322
  (and (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__state_act junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__state_in)
323
       (= junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__restart_in)
324
       )
325
  (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless.junctions5_junctions5__state_act)
326
))
327

    
328
; junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until
329
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.idJunctions5_Junctions5_1 Int)
330
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.a_1 Real)
331
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.junctions5_junctions5__restart_in Bool)
332
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.junctions5_junctions5__state_in junctions5_junctions5__type)
333
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.a_out Real)
334
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.idJunctions5_Junctions5_out Int)
335
(declare-rel junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until (Int Real Bool junctions5_junctions5__type Real Int))
336
(rule (=> 
337
  (and (= junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.junctions5_junctions5__state_in POINTJunctions5_Junctions5)
338
       (= junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.junctions5_junctions5__restart_in true)
339
       (= junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.idJunctions5_Junctions5_out junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.idJunctions5_Junctions5_1)
340
       (= junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.a_out junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.a_1)
341
       )
342
  (junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.idJunctions5_Junctions5_1 junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.a_1 junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.a_out junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until.idJunctions5_Junctions5_out)
343
))
344

    
345
; junctions5_junctions5__JUNCTIONS5_B_IDL_unless
346
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__restart_in Bool)
347
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__state_in junctions5_junctions5__type)
348
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__restart_act Bool)
349
(declare-var junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__state_act junctions5_junctions5__type)
350
(declare-rel junctions5_junctions5__JUNCTIONS5_B_IDL_unless (Bool junctions5_junctions5__type Bool junctions5_junctions5__type))
351
(rule (=> 
352
  (and (= junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__state_act junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__state_in)
353
       (= junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__restart_in)
354
       )
355
  (junctions5_junctions5__JUNCTIONS5_B_IDL_unless junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__restart_in junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__state_in junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__restart_act junctions5_junctions5__JUNCTIONS5_B_IDL_unless.junctions5_junctions5__state_act)
356
))
357

    
358
; junctions5_junctions5__POINTJunctions5_Junctions5_handler_until
359
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.idJunctions5_Junctions5_1 Int)
360
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.a_1 Real)
361
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.junctions5_junctions5__restart_in Bool)
362
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.junctions5_junctions5__state_in junctions5_junctions5__type)
363
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.a_out Real)
364
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.idJunctions5_Junctions5_out Int)
365
(declare-rel junctions5_junctions5__POINTJunctions5_Junctions5_handler_until (Int Real Bool junctions5_junctions5__type Real Int))
366
(rule (=> 
367
  (and (= junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.junctions5_junctions5__state_in POINTJunctions5_Junctions5)
368
       (= junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.junctions5_junctions5__restart_in false)
369
       (= junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.idJunctions5_Junctions5_out junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.idJunctions5_Junctions5_1)
370
       (= junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.a_out junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.a_1)
371
       )
372
  (junctions5_junctions5__POINTJunctions5_Junctions5_handler_until junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.idJunctions5_Junctions5_1 junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.a_1 junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.junctions5_junctions5__restart_in junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.junctions5_junctions5__state_in junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.a_out junctions5_junctions5__POINTJunctions5_Junctions5_handler_until.idJunctions5_Junctions5_out)
373
))
374

    
375
; junctions5_junctions5__POINTJunctions5_Junctions5_unless
376
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_in Bool)
377
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_in junctions5_junctions5__type)
378
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.idJunctions5_Junctions5_1 Int)
379
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.x Int)
380
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act Bool)
381
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act junctions5_junctions5__type)
382
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_1 Bool)
383
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_2 Bool)
384
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_3 Bool)
385
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_4 Bool)
386
(declare-var junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_5 Bool)
387
(declare-rel junctions5_junctions5__POINTJunctions5_Junctions5_unless (Bool junctions5_junctions5__type Int Int Bool junctions5_junctions5__type))
388
(rule (=> 
389
  (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_5 (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.idJunctions5_Junctions5_1 1283))
390
       (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_4 (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.idJunctions5_Junctions5_1 1282))
391
       (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_3 (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.idJunctions5_Junctions5_1 1282) (= (mod junctions5_junctions5__POINTJunctions5_Junctions5_unless.x 3) 0)))
392
       (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_2 (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.idJunctions5_Junctions5_1 1282) (= (mod junctions5_junctions5__POINTJunctions5_Junctions5_unless.x 3) 1)))
393
       (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_1 (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.idJunctions5_Junctions5_1 0))
394
       (and (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_1 false))
395
               (and (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_2 false))
396
                       (and (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_3 false))
397
                               (and (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_4 false))
398
                                       (and (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_5 false))
399
                                               (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_in)
400
                                                    (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_in)
401
                                                    ))
402
                                            (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_5 true))
403
                                               (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act JUNCTIONS5_B_IDL)
404
                                                    (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act true)
405
                                                    ))
406
                                       ))
407
                                    (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_4 true))
408
                                       (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act JUNCTIONS5_A_IDL)
409
                                            (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act true)
410
                                            ))
411
                               ))
412
                            (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_3 true))
413
                               (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2)
414
                                    (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act true)
415
                                    ))
416
                       ))
417
                    (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_2 true))
418
                       (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1)
419
                            (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act true)
420
                            ))
421
               ))
422
            (or (not (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.__junctions5_junctions5__POINTJunctions5_Junctions5_unless_1 true))
423
               (and (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act POINT__TO__JUNCTIONS5_A_1)
424
                    (= junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act true)
425
                    ))
426
       )
427
       )
428
  (junctions5_junctions5__POINTJunctions5_Junctions5_unless junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_in junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_in junctions5_junctions5__POINTJunctions5_Junctions5_unless.idJunctions5_Junctions5_1 junctions5_junctions5__POINTJunctions5_Junctions5_unless.x junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__restart_act junctions5_junctions5__POINTJunctions5_Junctions5_unless.junctions5_junctions5__state_act)
429
))
430

    
431
; junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until
432
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_1 Int)
433
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.a_1 Real)
434
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.junctions5_junctions5__restart_in Bool)
435
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.junctions5_junctions5__state_in junctions5_junctions5__type)
436
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.a_out Real)
437
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_out Int)
438
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_2 Int)
439
(declare-rel junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until (Int Real Bool junctions5_junctions5__type Real Int))
440
(rule (=> 
441
  (and (= junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.junctions5_junctions5__state_in POINTJunctions5_Junctions5)
442
       (= junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.junctions5_junctions5__restart_in true)
443
       (Junctions5_A_en junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_1
444
                        false
445
                        junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_2)
446
       (= junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_out junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_2)
447
       (= junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.a_out junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.a_1)
448
       )
449
  (junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_1 junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.a_1 junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.junctions5_junctions5__restart_in junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.junctions5_junctions5__state_in junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.a_out junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until.idJunctions5_Junctions5_out)
450
))
451

    
452
; junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless
453
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__restart_in Bool)
454
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__state_in junctions5_junctions5__type)
455
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__restart_act Bool)
456
(declare-var junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__state_act junctions5_junctions5__type)
457
(declare-rel junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless (Bool junctions5_junctions5__type Bool junctions5_junctions5__type))
458
(rule (=> 
459
  (and (= junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__state_act junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__state_in)
460
       (= junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__restart_act junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__restart_in)
461
       )
462
  (junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__restart_in junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__state_in junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__restart_act junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless.junctions5_junctions5__state_act)
463
))
464

    
465
; Junctions5_Junctions5_node
466
(declare-var Junctions5_Junctions5_node.idJunctions5_Junctions5_1 Int)
467
(declare-var Junctions5_Junctions5_node.x Int)
468
(declare-var Junctions5_Junctions5_node.a_1 Real)
469
(declare-var Junctions5_Junctions5_node.idJunctions5_Junctions5 Int)
470
(declare-var Junctions5_Junctions5_node.a Real)
471
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c Bool)
472
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c junctions5_junctions5__type)
473
(declare-var Junctions5_Junctions5_node.ni_4._arrow._first_c Bool)
474
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m Bool)
475
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m junctions5_junctions5__type)
476
(declare-var Junctions5_Junctions5_node.ni_4._arrow._first_m Bool)
477
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x Bool)
478
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x junctions5_junctions5__type)
479
(declare-var Junctions5_Junctions5_node.ni_4._arrow._first_x Bool)
480
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_1 Bool)
481
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_10 junctions5_junctions5__type)
482
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_11 Bool)
483
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_12 junctions5_junctions5__type)
484
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_13 Bool)
485
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_14 junctions5_junctions5__type)
486
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_15 Real)
487
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_16 Int)
488
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_17 Bool)
489
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_18 junctions5_junctions5__type)
490
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_19 Real)
491
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_2 junctions5_junctions5__type)
492
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_20 Int)
493
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_21 Bool)
494
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_22 junctions5_junctions5__type)
495
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_23 Real)
496
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_24 Int)
497
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_25 Bool)
498
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_26 junctions5_junctions5__type)
499
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_27 Real)
500
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_28 Int)
501
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_29 Bool)
502
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_3 Bool)
503
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_30 junctions5_junctions5__type)
504
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_31 Real)
505
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_32 Int)
506
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_33 Bool)
507
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_34 junctions5_junctions5__type)
508
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_35 Real)
509
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_36 Int)
510
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_37 Bool)
511
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_4 junctions5_junctions5__type)
512
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_5 Bool)
513
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_6 junctions5_junctions5__type)
514
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_7 Bool)
515
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_8 junctions5_junctions5__type)
516
(declare-var Junctions5_Junctions5_node.__Junctions5_Junctions5_node_9 Bool)
517
(declare-var Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in Bool)
518
(declare-var Junctions5_Junctions5_node.junctions5_junctions5__next_state_in junctions5_junctions5__type)
519
(declare-var Junctions5_Junctions5_node.junctions5_junctions5__restart_act Bool)
520
(declare-var Junctions5_Junctions5_node.junctions5_junctions5__restart_in Bool)
521
(declare-var Junctions5_Junctions5_node.junctions5_junctions5__state_act junctions5_junctions5__type)
522
(declare-var Junctions5_Junctions5_node.junctions5_junctions5__state_in junctions5_junctions5__type)
523
(declare-rel Junctions5_Junctions5_node_reset (Bool junctions5_junctions5__type Bool Bool junctions5_junctions5__type Bool))
524
(declare-rel Junctions5_Junctions5_node_step (Int Int Real Int Real Bool junctions5_junctions5__type Bool Bool junctions5_junctions5__type Bool))
525

    
526
(rule (=> 
527
  (and 
528
       (= Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c)
529
       (= Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c)
530
       (= Junctions5_Junctions5_node.ni_4._arrow._first_m true)
531
  )
532
  (Junctions5_Junctions5_node_reset Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
533
                                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
534
                                    Junctions5_Junctions5_node.ni_4._arrow._first_c
535
                                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m
536
                                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m
537
                                    Junctions5_Junctions5_node.ni_4._arrow._first_m)
538
))
539

    
540
(rule (=> 
541
  (and (= Junctions5_Junctions5_node.ni_4._arrow._first_m Junctions5_Junctions5_node.ni_4._arrow._first_c)
542
       (and (= Junctions5_Junctions5_node.__Junctions5_Junctions5_node_37 (ite Junctions5_Junctions5_node.ni_4._arrow._first_m true false))
543
            (= Junctions5_Junctions5_node.ni_4._arrow._first_x false))
544
       (and (or (not (= Junctions5_Junctions5_node.__Junctions5_Junctions5_node_37 false))
545
               (and (= Junctions5_Junctions5_node.junctions5_junctions5__state_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c)
546
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c)
547
                    ))
548
            (or (not (= Junctions5_Junctions5_node.__Junctions5_Junctions5_node_37 true))
549
               (and (= Junctions5_Junctions5_node.junctions5_junctions5__state_in POINTJunctions5_Junctions5)
550
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_in false)
551
                    ))
552
       )
553
       (and (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_in JUNCTIONS5_A_IDL))
554
               (and (junctions5_junctions5__JUNCTIONS5_A_IDL_unless Junctions5_Junctions5_node.junctions5_junctions5__restart_in
555
                                                                    Junctions5_Junctions5_node.junctions5_junctions5__state_in
556
                                                                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_3
557
                                                                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_4)
558
                    (= Junctions5_Junctions5_node.junctions5_junctions5__state_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_4)
559
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_3)
560
                    ))
561
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_in JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1))
562
               (and (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_unless 
563
                    Junctions5_Junctions5_node.junctions5_junctions5__restart_in
564
                    Junctions5_Junctions5_node.junctions5_junctions5__state_in
565
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_7
566
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_8)
567
                    (= Junctions5_Junctions5_node.junctions5_junctions5__state_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_8)
568
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_7)
569
                    ))
570
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_in JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2))
571
               (and (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_unless 
572
                    Junctions5_Junctions5_node.junctions5_junctions5__restart_in
573
                    Junctions5_Junctions5_node.junctions5_junctions5__state_in
574
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_5
575
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_6)
576
                    (= Junctions5_Junctions5_node.junctions5_junctions5__state_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_6)
577
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_5)
578
                    ))
579
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_in JUNCTIONS5_B_IDL))
580
               (and (junctions5_junctions5__JUNCTIONS5_B_IDL_unless Junctions5_Junctions5_node.junctions5_junctions5__restart_in
581
                                                                    Junctions5_Junctions5_node.junctions5_junctions5__state_in
582
                                                                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_1
583
                                                                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_2)
584
                    (= Junctions5_Junctions5_node.junctions5_junctions5__state_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_2)
585
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_1)
586
                    ))
587
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_in POINTJunctions5_Junctions5))
588
               (and (junctions5_junctions5__POINTJunctions5_Junctions5_unless 
589
                    Junctions5_Junctions5_node.junctions5_junctions5__restart_in
590
                    Junctions5_Junctions5_node.junctions5_junctions5__state_in
591
                    Junctions5_Junctions5_node.idJunctions5_Junctions5_1
592
                    Junctions5_Junctions5_node.x
593
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_11
594
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_12)
595
                    (= Junctions5_Junctions5_node.junctions5_junctions5__state_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_12)
596
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_11)
597
                    ))
598
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_in POINT__TO__JUNCTIONS5_A_1))
599
               (and (junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_unless 
600
                    Junctions5_Junctions5_node.junctions5_junctions5__restart_in
601
                    Junctions5_Junctions5_node.junctions5_junctions5__state_in
602
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_9
603
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_10)
604
                    (= Junctions5_Junctions5_node.junctions5_junctions5__state_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_10)
605
                    (= Junctions5_Junctions5_node.junctions5_junctions5__restart_act Junctions5_Junctions5_node.__Junctions5_Junctions5_node_9)
606
                    ))
607
       )
608
       (and (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_act JUNCTIONS5_A_IDL))
609
               (and (junctions5_junctions5__JUNCTIONS5_A_IDL_handler_until 
610
                    Junctions5_Junctions5_node.idJunctions5_Junctions5_1
611
                    Junctions5_Junctions5_node.a_1
612
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_17
613
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_18
614
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_19
615
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_20)
616
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_state_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_18)
617
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_17)
618
                    (= Junctions5_Junctions5_node.idJunctions5_Junctions5 Junctions5_Junctions5_node.__Junctions5_Junctions5_node_20)
619
                    (= Junctions5_Junctions5_node.a Junctions5_Junctions5_node.__Junctions5_Junctions5_node_19)
620
                    ))
621
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_act JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1))
622
               (and (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1_handler_until 
623
                    Junctions5_Junctions5_node.idJunctions5_Junctions5_1
624
                    Junctions5_Junctions5_node.x
625
                    Junctions5_Junctions5_node.a_1
626
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_25
627
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_26
628
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_27
629
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_28)
630
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_state_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_26)
631
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_25)
632
                    (= Junctions5_Junctions5_node.idJunctions5_Junctions5 Junctions5_Junctions5_node.__Junctions5_Junctions5_node_28)
633
                    (= Junctions5_Junctions5_node.a Junctions5_Junctions5_node.__Junctions5_Junctions5_node_27)
634
                    ))
635
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_act JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2))
636
               (and (junctions5_junctions5__JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2_handler_until 
637
                    Junctions5_Junctions5_node.idJunctions5_Junctions5_1
638
                    Junctions5_Junctions5_node.x
639
                    Junctions5_Junctions5_node.a_1
640
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_21
641
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_22
642
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_23
643
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_24)
644
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_state_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_22)
645
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_21)
646
                    (= Junctions5_Junctions5_node.idJunctions5_Junctions5 Junctions5_Junctions5_node.__Junctions5_Junctions5_node_24)
647
                    (= Junctions5_Junctions5_node.a Junctions5_Junctions5_node.__Junctions5_Junctions5_node_23)
648
                    ))
649
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_act JUNCTIONS5_B_IDL))
650
               (and (junctions5_junctions5__JUNCTIONS5_B_IDL_handler_until 
651
                    Junctions5_Junctions5_node.idJunctions5_Junctions5_1
652
                    Junctions5_Junctions5_node.a_1
653
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_13
654
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_14
655
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_15
656
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_16)
657
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_state_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_14)
658
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_13)
659
                    (= Junctions5_Junctions5_node.idJunctions5_Junctions5 Junctions5_Junctions5_node.__Junctions5_Junctions5_node_16)
660
                    (= Junctions5_Junctions5_node.a Junctions5_Junctions5_node.__Junctions5_Junctions5_node_15)
661
                    ))
662
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_act POINTJunctions5_Junctions5))
663
               (and (junctions5_junctions5__POINTJunctions5_Junctions5_handler_until 
664
                    Junctions5_Junctions5_node.idJunctions5_Junctions5_1
665
                    Junctions5_Junctions5_node.a_1
666
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_33
667
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_34
668
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_35
669
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_36)
670
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_state_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_34)
671
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_33)
672
                    (= Junctions5_Junctions5_node.idJunctions5_Junctions5 Junctions5_Junctions5_node.__Junctions5_Junctions5_node_36)
673
                    (= Junctions5_Junctions5_node.a Junctions5_Junctions5_node.__Junctions5_Junctions5_node_35)
674
                    ))
675
            (or (not (= Junctions5_Junctions5_node.junctions5_junctions5__state_act POINT__TO__JUNCTIONS5_A_1))
676
               (and (junctions5_junctions5__POINT__TO__JUNCTIONS5_A_1_handler_until 
677
                    Junctions5_Junctions5_node.idJunctions5_Junctions5_1
678
                    Junctions5_Junctions5_node.a_1
679
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_29
680
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_30
681
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_31
682
                    Junctions5_Junctions5_node.__Junctions5_Junctions5_node_32)
683
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_state_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_30)
684
                    (= Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in Junctions5_Junctions5_node.__Junctions5_Junctions5_node_29)
685
                    (= Junctions5_Junctions5_node.idJunctions5_Junctions5 Junctions5_Junctions5_node.__Junctions5_Junctions5_node_32)
686
                    (= Junctions5_Junctions5_node.a Junctions5_Junctions5_node.__Junctions5_Junctions5_node_31)
687
                    ))
688
       )
689
       (= Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x Junctions5_Junctions5_node.junctions5_junctions5__next_state_in)
690
       (= Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x Junctions5_Junctions5_node.junctions5_junctions5__next_restart_in)
691
       )
692
  (Junctions5_Junctions5_node_step Junctions5_Junctions5_node.idJunctions5_Junctions5_1
693
                                   Junctions5_Junctions5_node.x
694
                                   Junctions5_Junctions5_node.a_1
695
                                   Junctions5_Junctions5_node.idJunctions5_Junctions5
696
                                   Junctions5_Junctions5_node.a
697
                                   Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
698
                                   Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
699
                                   Junctions5_Junctions5_node.ni_4._arrow._first_c
700
                                   Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x
701
                                   Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x
702
                                   Junctions5_Junctions5_node.ni_4._arrow._first_x)
703
))
704

    
705
; Junctions5_Junctions5
706
(declare-var Junctions5_Junctions5.x Int)
707
(declare-var Junctions5_Junctions5.a Real)
708
(declare-var Junctions5_Junctions5.__Junctions5_Junctions5_2_c Int)
709
(declare-var Junctions5_Junctions5.__Junctions5_Junctions5_3_c Real)
710
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c Bool)
711
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c junctions5_junctions5__type)
712
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c Bool)
713
(declare-var Junctions5_Junctions5.ni_3._arrow._first_c Bool)
714
(declare-var Junctions5_Junctions5.__Junctions5_Junctions5_2_m Int)
715
(declare-var Junctions5_Junctions5.__Junctions5_Junctions5_3_m Real)
716
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m Bool)
717
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m junctions5_junctions5__type)
718
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m Bool)
719
(declare-var Junctions5_Junctions5.ni_3._arrow._first_m Bool)
720
(declare-var Junctions5_Junctions5.__Junctions5_Junctions5_2_x Int)
721
(declare-var Junctions5_Junctions5.__Junctions5_Junctions5_3_x Real)
722
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x Bool)
723
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x junctions5_junctions5__type)
724
(declare-var Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_x Bool)
725
(declare-var Junctions5_Junctions5.ni_3._arrow._first_x Bool)
726
(declare-var Junctions5_Junctions5.__Junctions5_Junctions5_1 Bool)
727
(declare-var Junctions5_Junctions5.a_1 Real)
728
(declare-var Junctions5_Junctions5.idJunctions5_Junctions5 Int)
729
(declare-var Junctions5_Junctions5.idJunctions5_Junctions5_1 Int)
730
(declare-rel Junctions5_Junctions5_reset (Int Real Bool junctions5_junctions5__type Bool Bool Int Real Bool junctions5_junctions5__type Bool Bool))
731
(declare-rel Junctions5_Junctions5_step (Int Real Int Real Bool junctions5_junctions5__type Bool Bool Int Real Bool junctions5_junctions5__type Bool Bool))
732

    
733
(rule (=> 
734
  (and 
735
       (= Junctions5_Junctions5.__Junctions5_Junctions5_2_m Junctions5_Junctions5.__Junctions5_Junctions5_2_c)
736
       (= Junctions5_Junctions5.__Junctions5_Junctions5_3_m Junctions5_Junctions5.__Junctions5_Junctions5_3_c)
737
       (= Junctions5_Junctions5.ni_3._arrow._first_m true)
738
       (Junctions5_Junctions5_node_reset Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
739
                                         Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
740
                                         Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c
741
                                         Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m
742
                                         Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m
743
                                         Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m)
744
  )
745
  (Junctions5_Junctions5_reset Junctions5_Junctions5.__Junctions5_Junctions5_2_c
746
                               Junctions5_Junctions5.__Junctions5_Junctions5_3_c
747
                               Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
748
                               Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
749
                               Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c
750
                               Junctions5_Junctions5.ni_3._arrow._first_c
751
                               Junctions5_Junctions5.__Junctions5_Junctions5_2_m
752
                               Junctions5_Junctions5.__Junctions5_Junctions5_3_m
753
                               Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m
754
                               Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m
755
                               Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m
756
                               Junctions5_Junctions5.ni_3._arrow._first_m)
757
))
758

    
759
(rule (=> 
760
  (and (= Junctions5_Junctions5.ni_3._arrow._first_m Junctions5_Junctions5.ni_3._arrow._first_c)
761
       (and (= Junctions5_Junctions5.__Junctions5_Junctions5_1 (ite Junctions5_Junctions5.ni_3._arrow._first_m true false))
762
            (= Junctions5_Junctions5.ni_3._arrow._first_x false))
763
       (and (or (not (= Junctions5_Junctions5.__Junctions5_Junctions5_1 false))
764
               (and (= Junctions5_Junctions5.idJunctions5_Junctions5_1 Junctions5_Junctions5.__Junctions5_Junctions5_2_c)
765
                    (= Junctions5_Junctions5.a_1 Junctions5_Junctions5.__Junctions5_Junctions5_3_c)
766
                    ))
767
            (or (not (= Junctions5_Junctions5.__Junctions5_Junctions5_1 true))
768
               (and (= Junctions5_Junctions5.idJunctions5_Junctions5_1 0)
769
                    (= Junctions5_Junctions5.a_1 0.)
770
                    ))
771
       )
772
       (and (= Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c)
773
            (= Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c)
774
            (= Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c)
775
            )
776
       (Junctions5_Junctions5_node_step Junctions5_Junctions5.idJunctions5_Junctions5_1
777
                                        Junctions5_Junctions5.x
778
                                        Junctions5_Junctions5.a_1
779
                                        Junctions5_Junctions5.idJunctions5_Junctions5
780
                                        Junctions5_Junctions5.a
781
                                        Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m
782
                                        Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m
783
                                        Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m
784
                                        Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x
785
                                        Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x
786
                                        Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_x)
787
       (= Junctions5_Junctions5.__Junctions5_Junctions5_3_x Junctions5_Junctions5.a)
788
       (= Junctions5_Junctions5.__Junctions5_Junctions5_2_x Junctions5_Junctions5.idJunctions5_Junctions5)
789
       )
790
  (Junctions5_Junctions5_step Junctions5_Junctions5.x
791
                              Junctions5_Junctions5.a
792
                              Junctions5_Junctions5.__Junctions5_Junctions5_2_c
793
                              Junctions5_Junctions5.__Junctions5_Junctions5_3_c
794
                              Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
795
                              Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
796
                              Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c
797
                              Junctions5_Junctions5.ni_3._arrow._first_c
798
                              Junctions5_Junctions5.__Junctions5_Junctions5_2_x
799
                              Junctions5_Junctions5.__Junctions5_Junctions5_3_x
800
                              Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x
801
                              Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x
802
                              Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_x
803
                              Junctions5_Junctions5.ni_3._arrow._first_x)
804
))
805

    
806
; Junctions5
807
(declare-var Junctions5.x_1_1 Int)
808
(declare-var Junctions5.a_1_1 Real)
809
(declare-var Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_c Int)
810
(declare-var Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_c Real)
811
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c Bool)
812
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c junctions5_junctions5__type)
813
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c Bool)
814
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_c Bool)
815
(declare-var Junctions5.ni_1._arrow._first_c Bool)
816
(declare-var Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_m Int)
817
(declare-var Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_m Real)
818
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m Bool)
819
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m junctions5_junctions5__type)
820
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m Bool)
821
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_m Bool)
822
(declare-var Junctions5.ni_1._arrow._first_m Bool)
823
(declare-var Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_x Int)
824
(declare-var Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_x Real)
825
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x Bool)
826
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x junctions5_junctions5__type)
827
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_x Bool)
828
(declare-var Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_x Bool)
829
(declare-var Junctions5.ni_1._arrow._first_x Bool)
830
(declare-var Junctions5.Junctions5_1_1 Real)
831
(declare-var Junctions5.__Junctions5_1 Bool)
832
(declare-var Junctions5.i_virtual_local Real)
833
(declare-rel Junctions5_reset (Int Real Bool junctions5_junctions5__type Bool Bool Bool Int Real Bool junctions5_junctions5__type Bool Bool Bool))
834
(declare-rel Junctions5_step (Int Real Int Real Bool junctions5_junctions5__type Bool Bool Bool Int Real Bool junctions5_junctions5__type Bool Bool Bool))
835

    
836
(rule (=> 
837
  (and 
838
       
839
       (= Junctions5.ni_1._arrow._first_m true)
840
       (Junctions5_Junctions5_reset Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_c
841
                                    Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_c
842
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
843
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
844
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c
845
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_c
846
                                    Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_m
847
                                    Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_m
848
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m
849
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m
850
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m
851
                                    Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_m)
852
  )
853
  (Junctions5_reset Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_c
854
                    Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_c
855
                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
856
                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
857
                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c
858
                    Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_c
859
                    Junctions5.ni_1._arrow._first_c
860
                    Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_m
861
                    Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_m
862
                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m
863
                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m
864
                    Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m
865
                    Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_m
866
                    Junctions5.ni_1._arrow._first_m)
867
))
868

    
869
(rule (=> 
870
  (and (= Junctions5.ni_1._arrow._first_m Junctions5.ni_1._arrow._first_c)
871
       (and (= Junctions5.__Junctions5_1 (ite Junctions5.ni_1._arrow._first_m true false))
872
            (= Junctions5.ni_1._arrow._first_x false))
873
       (and (or (not (= Junctions5.__Junctions5_1 true))
874
               (= Junctions5.i_virtual_local 0.))
875
            (or (not (= Junctions5.__Junctions5_1 false))
876
               (= Junctions5.i_virtual_local 1.))
877
       )
878
       (and (= Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_m Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_c)
879
            (= Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_m Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_c)
880
            (= Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c)
881
            (= Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c)
882
            (= Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c)
883
            (= Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_m Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_c)
884
            )
885
       (Junctions5_Junctions5_step Junctions5.x_1_1
886
                                   Junctions5.Junctions5_1_1
887
                                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_m
888
                                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_m
889
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_m
890
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_m
891
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_m
892
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_m
893
                                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_x
894
                                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_x
895
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x
896
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x
897
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_x
898
                                   Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_x)
899
       (= Junctions5.a_1_1 Junctions5.Junctions5_1_1)
900
       )
901
  (Junctions5_step Junctions5.x_1_1
902
                   Junctions5.a_1_1
903
                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_c
904
                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_c
905
                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_c
906
                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_c
907
                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_c
908
                   Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_c
909
                   Junctions5.ni_1._arrow._first_c
910
                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_2_x
911
                   Junctions5.ni_0.Junctions5_Junctions5.__Junctions5_Junctions5_3_x
912
                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_38_x
913
                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.__Junctions5_Junctions5_node_39_x
914
                   Junctions5.ni_0.Junctions5_Junctions5.ni_2.Junctions5_Junctions5_node.ni_4._arrow._first_x
915
                   Junctions5.ni_0.Junctions5_Junctions5.ni_3._arrow._first_x
916
                   Junctions5.ni_1._arrow._first_x)
917
))
918

    
919
; Junctions5_B_ex
920
(declare-var Junctions5_B_ex.a_1 Real)
921
(declare-var Junctions5_B_ex.idJunctions5_Junctions5_1 Int)
922
(declare-var Junctions5_B_ex.isInner Bool)
923
(declare-var Junctions5_B_ex.a Real)
924
(declare-var Junctions5_B_ex.idJunctions5_Junctions5 Int)
925
(declare-var Junctions5_B_ex.__Junctions5_B_ex_1 Bool)
926
(declare-var Junctions5_B_ex.a_2 Real)
927
(declare-var Junctions5_B_ex.idJunctions5_Junctions5_2 Int)
928
(declare-rel Junctions5_B_ex (Real Int Bool Real Int))
929
(rule (=> 
930
  (and (= Junctions5_B_ex.__Junctions5_B_ex_1 (not Junctions5_B_ex.isInner))
931
       (and (or (not (= Junctions5_B_ex.__Junctions5_B_ex_1 false))
932
               (and (= Junctions5_B_ex.idJunctions5_Junctions5_2 Junctions5_B_ex.idJunctions5_Junctions5_1)
933
                    (= Junctions5_B_ex.a_2 Junctions5_B_ex.a_1)
934
                    ))
935
            (or (not (= Junctions5_B_ex.__Junctions5_B_ex_1 true))
936
               (and (= Junctions5_B_ex.idJunctions5_Junctions5_2 0)
937
                    (= Junctions5_B_ex.a_2 0.)
938
                    ))
939
       )
940
       (= Junctions5_B_ex.idJunctions5_Junctions5 Junctions5_B_ex.idJunctions5_Junctions5_1)
941
       (= Junctions5_B_ex.a Junctions5_B_ex.a_2)
942
       )
943
  (Junctions5_B_ex Junctions5_B_ex.a_1 Junctions5_B_ex.idJunctions5_Junctions5_1 Junctions5_B_ex.isInner Junctions5_B_ex.a Junctions5_B_ex.idJunctions5_Junctions5)
944
))
945