Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions3 / Junctions3.smt2 @ eb639349

History | View | Annotate | Download (82.7 KB)

1 eb639349 bourbouh
(declare-datatypes () ((junctions3_junctions3__type POINTJunctions3_Junctions3 POINT__TO__JUNCTIONS3_A_1 JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1 JUNCTIONS3_A_IDL JUNCTIONS3_B_IDL)));
2
3
; Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action
4
(declare-var Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action.y_1 Int)
5
(declare-var Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action.y Int)
6
(declare-rel Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action (Int Int))
7
(rule (=> 
8
  (= Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action.y 0)
9
  (Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action.y_1 Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action.y)
10
))
11
12
; Junctions3_A_ex
13
(declare-var Junctions3_A_ex.idJunctions3_Junctions3_1 Int)
14
(declare-var Junctions3_A_ex.isInner Bool)
15
(declare-var Junctions3_A_ex.idJunctions3_Junctions3 Int)
16
(declare-var Junctions3_A_ex.idJunctions3_Junctions3_2 Int)
17
(declare-rel Junctions3_A_ex (Int Bool Int))
18
(rule (=> 
19
  (and (and (or (not (= (not Junctions3_A_ex.isInner) true))
20
               (= Junctions3_A_ex.idJunctions3_Junctions3_2 0))
21
            (or (not (= (not Junctions3_A_ex.isInner) false))
22
               (= Junctions3_A_ex.idJunctions3_Junctions3_2 Junctions3_A_ex.idJunctions3_Junctions3_1))
23
       )
24
       (= Junctions3_A_ex.idJunctions3_Junctions3 Junctions3_A_ex.idJunctions3_Junctions3_1)
25
       )
26
  (Junctions3_A_ex Junctions3_A_ex.idJunctions3_Junctions3_1 Junctions3_A_ex.isInner Junctions3_A_ex.idJunctions3_Junctions3)
27
))
28
29
; Junctions3_B_en
30
(declare-var Junctions3_B_en.idJunctions3_Junctions3_1 Int)
31
(declare-var Junctions3_B_en.isInner Bool)
32
(declare-var Junctions3_B_en.idJunctions3_Junctions3 Int)
33
(declare-rel Junctions3_B_en (Int Bool Int))
34
(rule (=> 
35
  (= Junctions3_B_en.idJunctions3_Junctions3 1225)
36
  (Junctions3_B_en Junctions3_B_en.idJunctions3_Junctions3_1 Junctions3_B_en.isInner Junctions3_B_en.idJunctions3_Junctions3)
37
))
38
39
; Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action
40
(declare-var Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action.y_1 Int)
41
(declare-var Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action.y Int)
42
(declare-rel Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action (Int Int))
43
(rule (=> 
44
  (= Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action.y (+ Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action.y_1 1))
45
  (Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action.y_1 Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action.y)
46
))
47
48
; Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action
49
(declare-var Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action.y_1 Int)
50
(declare-var Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action.y Int)
51
(declare-rel Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action (Int Int))
52
(rule (=> 
53
  (= Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action.y (+ Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action.y_1 1))
54
  (Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action.y_1 Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action.y)
55
))
56
57
; Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action
58
(declare-var Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action.y_1 Int)
59
(declare-var Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action.y Int)
60
(declare-rel Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action (Int Int))
61
(rule (=> 
62
  (= Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action.y (+ Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action.y_1 1))
63
  (Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action.y_1 Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action.y)
64
))
65
66
; Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action
67
(declare-var Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action.y_1 Int)
68
(declare-var Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action.y Int)
69
(declare-rel Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action (Int Int))
70
(rule (=> 
71
  (= Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action.y (+ Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action.y_1 1))
72
  (Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action.y_1 Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action.y)
73
))
74
75
; Junctions3_A_en
76
(declare-var Junctions3_A_en.idJunctions3_Junctions3_1 Int)
77
(declare-var Junctions3_A_en.isInner Bool)
78
(declare-var Junctions3_A_en.idJunctions3_Junctions3 Int)
79
(declare-rel Junctions3_A_en (Int Bool Int))
80
(rule (=> 
81
  (= Junctions3_A_en.idJunctions3_Junctions3 1224)
82
  (Junctions3_A_en Junctions3_A_en.idJunctions3_Junctions3_1 Junctions3_A_en.isInner Junctions3_A_en.idJunctions3_Junctions3)
83
))
84
85
; junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until
86
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.idJunctions3_Junctions3_1 Int)
87
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.y_1 Int)
88
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.junctions3_junctions3__restart_in Bool)
89
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.junctions3_junctions3__state_in junctions3_junctions3__type)
90
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.idJunctions3_Junctions3_out Int)
91
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.y_out Int)
92
(declare-rel junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until (Int Int Bool junctions3_junctions3__type Int Int))
93
(rule (=> 
94
  (and (= junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.y_out junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.y_1)
95
       (= junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.junctions3_junctions3__state_in POINTJunctions3_Junctions3)
96
       (= junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.junctions3_junctions3__restart_in true)
97
       (= junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.idJunctions3_Junctions3_1)
98
       )
99
  (junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.idJunctions3_Junctions3_1 junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.y_1 junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.junctions3_junctions3__restart_in junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.junctions3_junctions3__state_in junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until.y_out)
100
))
101
102
; junctions3_junctions3__JUNCTIONS3_A_IDL_unless
103
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__restart_in Bool)
104
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__state_in junctions3_junctions3__type)
105
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__restart_act Bool)
106
(declare-var junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__state_act junctions3_junctions3__type)
107
(declare-rel junctions3_junctions3__JUNCTIONS3_A_IDL_unless (Bool junctions3_junctions3__type Bool junctions3_junctions3__type))
108
(rule (=> 
109
  (and (= junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__state_act junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__state_in)
110
       (= junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__restart_act junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__restart_in)
111
       )
112
  (junctions3_junctions3__JUNCTIONS3_A_IDL_unless junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__restart_in junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__state_in junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__restart_act junctions3_junctions3__JUNCTIONS3_A_IDL_unless.junctions3_junctions3__state_act)
113
))
114
115
; junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until
116
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1 Int)
117
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_1 Int)
118
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.junctions3_junctions3__restart_in Bool)
119
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.junctions3_junctions3__state_in junctions3_junctions3__type)
120
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_out Int)
121
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_out Int)
122
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 Bool)
123
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 Bool)
124
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 Bool)
125
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_4 Int)
126
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_5 Int)
127
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_6 Int)
128
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_7 Int)
129
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_8 Int)
130
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_9 Int)
131
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3 Int)
132
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_2 Int)
133
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_3 Int)
134
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y Int)
135
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2 Int)
136
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3 Int)
137
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_4 Int)
138
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_5 Int)
139
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_6 Int)
140
(declare-rel junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until (Int Int Bool junctions3_junctions3__type Int Int))
141
(rule (=> 
142
  (and (Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action 
143
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_1
144
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2)
145
       (Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action 
146
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2
147
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_9)
148
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2 0))
149
       (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 true))
150
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_9))
151
            (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 false))
152
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2))
153
       )
154
       (Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action 
155
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3
156
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_8)
157
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 (and (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2 0) (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3 1)))
158
       (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 true))
159
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_4 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_8))
160
            (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 false))
161
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_4 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3))
162
       )
163
       (Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action 
164
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_4
165
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_7)
166
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 (and (and (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2 0) (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3 1)) (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_4 2)))
167
       (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 true))
168
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_5 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_7))
169
            (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 false))
170
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_5 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_4))
171
       )
172
       (Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action 
173
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_5
174
       junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_6)
175
       (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 false))
176
               (and (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_6 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_5)
177
                    (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 true))
178
                            (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_5))
179
                         (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 false))
180
                            (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 true))
181
                                    (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_4))
182
                                 (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 false))
183
                                    (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 true))
184
                                            (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_3))
185
                                         (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 false))
186
                                            (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_2))
187
                                    ))
188
                            ))
189
                    )
190
                    ))
191
            (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 true))
192
               (and (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_6 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_6)
193
                    (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_6)
194
                    ))
195
       )
196
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_out junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y)
197
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.junctions3_junctions3__state_in POINTJunctions3_Junctions3)
198
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.junctions3_junctions3__restart_in true)
199
       (Junctions3_A_ex junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1
200
                        false
201
                        junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_5)
202
       (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 true))
203
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_2 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_5))
204
            (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 false))
205
               (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_2 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1))
206
       )
207
       (Junctions3_B_en junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_2
208
                        false
209
                        junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_4)
210
       (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 false))
211
               (and (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_2)
212
                    (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 true))
213
                            (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1))
214
                         (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 false))
215
                            (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 true))
216
                                    (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1))
217
                                 (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_2 false))
218
                                    (and (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 true))
219
                                            (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1))
220
                                         (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_3 false))
221
                                            (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1))
222
                                    ))
223
                            ))
224
                    )
225
                    ))
226
            (or (not (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_1 true))
227
               (and (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.__junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until_4)
228
                    (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_3)
229
                    ))
230
       )
231
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3)
232
       )
233
  (junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_1 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_1 junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.junctions3_junctions3__restart_in junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.junctions3_junctions3__state_in junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until.y_out)
234
))
235
236
; junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless
237
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__restart_in Bool)
238
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__state_in junctions3_junctions3__type)
239
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__restart_act Bool)
240
(declare-var junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__state_act junctions3_junctions3__type)
241
(declare-rel junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless (Bool junctions3_junctions3__type Bool junctions3_junctions3__type))
242
(rule (=> 
243
  (and (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__state_act junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__state_in)
244
       (= junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__restart_act junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__restart_in)
245
       )
246
  (junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__restart_in junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__state_in junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__restart_act junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless.junctions3_junctions3__state_act)
247
))
248
249
; junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until
250
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.idJunctions3_Junctions3_1 Int)
251
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.y_1 Int)
252
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.junctions3_junctions3__restart_in Bool)
253
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.junctions3_junctions3__state_in junctions3_junctions3__type)
254
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.idJunctions3_Junctions3_out Int)
255
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.y_out Int)
256
(declare-rel junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until (Int Int Bool junctions3_junctions3__type Int Int))
257
(rule (=> 
258
  (and (= junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.y_out junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.y_1)
259
       (= junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.junctions3_junctions3__state_in POINTJunctions3_Junctions3)
260
       (= junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.junctions3_junctions3__restart_in true)
261
       (= junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.idJunctions3_Junctions3_1)
262
       )
263
  (junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.idJunctions3_Junctions3_1 junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.y_1 junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.junctions3_junctions3__restart_in junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.junctions3_junctions3__state_in junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until.y_out)
264
))
265
266
; junctions3_junctions3__JUNCTIONS3_B_IDL_unless
267
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__restart_in Bool)
268
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__state_in junctions3_junctions3__type)
269
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__restart_act Bool)
270
(declare-var junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__state_act junctions3_junctions3__type)
271
(declare-rel junctions3_junctions3__JUNCTIONS3_B_IDL_unless (Bool junctions3_junctions3__type Bool junctions3_junctions3__type))
272
(rule (=> 
273
  (and (= junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__state_act junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__state_in)
274
       (= junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__restart_act junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__restart_in)
275
       )
276
  (junctions3_junctions3__JUNCTIONS3_B_IDL_unless junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__restart_in junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__state_in junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__restart_act junctions3_junctions3__JUNCTIONS3_B_IDL_unless.junctions3_junctions3__state_act)
277
))
278
279
; junctions3_junctions3__POINTJunctions3_Junctions3_handler_until
280
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.idJunctions3_Junctions3_1 Int)
281
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.y_1 Int)
282
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.junctions3_junctions3__restart_in Bool)
283
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.junctions3_junctions3__state_in junctions3_junctions3__type)
284
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.idJunctions3_Junctions3_out Int)
285
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.y_out Int)
286
(declare-rel junctions3_junctions3__POINTJunctions3_Junctions3_handler_until (Int Int Bool junctions3_junctions3__type Int Int))
287
(rule (=> 
288
  (and (= junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.y_out junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.y_1)
289
       (= junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.junctions3_junctions3__state_in POINTJunctions3_Junctions3)
290
       (= junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.junctions3_junctions3__restart_in false)
291
       (= junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.idJunctions3_Junctions3_1)
292
       )
293
  (junctions3_junctions3__POINTJunctions3_Junctions3_handler_until junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.idJunctions3_Junctions3_1 junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.y_1 junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.junctions3_junctions3__restart_in junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.junctions3_junctions3__state_in junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__POINTJunctions3_Junctions3_handler_until.y_out)
294
))
295
296
; junctions3_junctions3__POINTJunctions3_Junctions3_unless
297
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_in Bool)
298
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_in junctions3_junctions3__type)
299
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.idJunctions3_Junctions3_1 Int)
300
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.x Int)
301
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_act Bool)
302
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_act junctions3_junctions3__type)
303
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_1 Bool)
304
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_2 Bool)
305
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_3 Bool)
306
(declare-var junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_4 Bool)
307
(declare-rel junctions3_junctions3__POINTJunctions3_Junctions3_unless (Bool junctions3_junctions3__type Int Int Bool junctions3_junctions3__type))
308
(rule (=> 
309
  (and (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_4 (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.idJunctions3_Junctions3_1 1225))
310
       (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_3 (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.idJunctions3_Junctions3_1 1224))
311
       (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_2 (and (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.idJunctions3_Junctions3_1 1224) (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.x 0)))
312
       (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_1 (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.idJunctions3_Junctions3_1 0))
313
       (and (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_1 false))
314
               (and (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_2 false))
315
                       (and (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_3 false))
316
                               (and (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_4 false))
317
                                       (and (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_act junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_in)
318
                                            (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_act junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_in)
319
                                            ))
320
                                    (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_4 true))
321
                                       (and (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_act JUNCTIONS3_B_IDL)
322
                                            (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_act true)
323
                                            ))
324
                               ))
325
                            (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_3 true))
326
                               (and (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_act JUNCTIONS3_A_IDL)
327
                                    (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_act true)
328
                                    ))
329
                       ))
330
                    (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_2 true))
331
                       (and (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_act JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1)
332
                            (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_act true)
333
                            ))
334
               ))
335
            (or (not (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.__junctions3_junctions3__POINTJunctions3_Junctions3_unless_1 true))
336
               (and (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_act POINT__TO__JUNCTIONS3_A_1)
337
                    (= junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_act true)
338
                    ))
339
       )
340
       )
341
  (junctions3_junctions3__POINTJunctions3_Junctions3_unless junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_in junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_in junctions3_junctions3__POINTJunctions3_Junctions3_unless.idJunctions3_Junctions3_1 junctions3_junctions3__POINTJunctions3_Junctions3_unless.x junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__restart_act junctions3_junctions3__POINTJunctions3_Junctions3_unless.junctions3_junctions3__state_act)
342
))
343
344
; junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until
345
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_1 Int)
346
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.y_1 Int)
347
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.junctions3_junctions3__restart_in Bool)
348
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.junctions3_junctions3__state_in junctions3_junctions3__type)
349
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_out Int)
350
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.y_out Int)
351
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_2 Int)
352
(declare-rel junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until (Int Int Bool junctions3_junctions3__type Int Int))
353
(rule (=> 
354
  (and (= junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.y_out junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.y_1)
355
       (= junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.junctions3_junctions3__state_in POINTJunctions3_Junctions3)
356
       (= junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.junctions3_junctions3__restart_in true)
357
       (Junctions3_A_en junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_1
358
                        false
359
                        junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_2)
360
       (= junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_2)
361
       )
362
  (junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_1 junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.y_1 junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.junctions3_junctions3__restart_in junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.junctions3_junctions3__state_in junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.idJunctions3_Junctions3_out junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until.y_out)
363
))
364
365
; junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless
366
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__restart_in Bool)
367
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__state_in junctions3_junctions3__type)
368
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__restart_act Bool)
369
(declare-var junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__state_act junctions3_junctions3__type)
370
(declare-rel junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless (Bool junctions3_junctions3__type Bool junctions3_junctions3__type))
371
(rule (=> 
372
  (and (= junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__state_act junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__state_in)
373
       (= junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__restart_act junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__restart_in)
374
       )
375
  (junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__restart_in junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__state_in junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__restart_act junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless.junctions3_junctions3__state_act)
376
))
377
378
; Junctions3_Junctions3_node
379
(declare-var Junctions3_Junctions3_node.idJunctions3_Junctions3_1 Int)
380
(declare-var Junctions3_Junctions3_node.x Int)
381
(declare-var Junctions3_Junctions3_node.y_1 Int)
382
(declare-var Junctions3_Junctions3_node.idJunctions3_Junctions3 Int)
383
(declare-var Junctions3_Junctions3_node.y Int)
384
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c Bool)
385
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c junctions3_junctions3__type)
386
(declare-var Junctions3_Junctions3_node.ni_4._arrow._first_c Bool)
387
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m Bool)
388
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m junctions3_junctions3__type)
389
(declare-var Junctions3_Junctions3_node.ni_4._arrow._first_m Bool)
390
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x Bool)
391
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x junctions3_junctions3__type)
392
(declare-var Junctions3_Junctions3_node.ni_4._arrow._first_x Bool)
393
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_1 Bool)
394
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_10 junctions3_junctions3__type)
395
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_11 Bool)
396
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_12 junctions3_junctions3__type)
397
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_13 Int)
398
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_14 Int)
399
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_15 Bool)
400
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_16 junctions3_junctions3__type)
401
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_17 Int)
402
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_18 Int)
403
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_19 Bool)
404
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_2 junctions3_junctions3__type)
405
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_20 junctions3_junctions3__type)
406
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_21 Int)
407
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_22 Int)
408
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_23 Bool)
409
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_24 junctions3_junctions3__type)
410
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_25 Int)
411
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_26 Int)
412
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_27 Bool)
413
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_28 junctions3_junctions3__type)
414
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_29 Int)
415
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_3 Bool)
416
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_30 Int)
417
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_31 Bool)
418
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_4 junctions3_junctions3__type)
419
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_5 Bool)
420
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_6 junctions3_junctions3__type)
421
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_7 Bool)
422
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_8 junctions3_junctions3__type)
423
(declare-var Junctions3_Junctions3_node.__Junctions3_Junctions3_node_9 Bool)
424
(declare-var Junctions3_Junctions3_node.junctions3_junctions3__next_restart_in Bool)
425
(declare-var Junctions3_Junctions3_node.junctions3_junctions3__next_state_in junctions3_junctions3__type)
426
(declare-var Junctions3_Junctions3_node.junctions3_junctions3__restart_act Bool)
427
(declare-var Junctions3_Junctions3_node.junctions3_junctions3__restart_in Bool)
428
(declare-var Junctions3_Junctions3_node.junctions3_junctions3__state_act junctions3_junctions3__type)
429
(declare-var Junctions3_Junctions3_node.junctions3_junctions3__state_in junctions3_junctions3__type)
430
(declare-rel Junctions3_Junctions3_node_reset (Bool junctions3_junctions3__type Bool Bool junctions3_junctions3__type Bool))
431
(declare-rel Junctions3_Junctions3_node_step (Int Int Int Int Int Bool junctions3_junctions3__type Bool Bool junctions3_junctions3__type Bool))
432
433
(rule (=> 
434
  (and 
435
       (= Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c)
436
       (= Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c)
437
       (= Junctions3_Junctions3_node.ni_4._arrow._first_m true)
438
  )
439
  (Junctions3_Junctions3_node_reset Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
440
                                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
441
                                    Junctions3_Junctions3_node.ni_4._arrow._first_c
442
                                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m
443
                                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m
444
                                    Junctions3_Junctions3_node.ni_4._arrow._first_m)
445
))
446
447
(rule (=> 
448
  (and (= Junctions3_Junctions3_node.ni_4._arrow._first_m Junctions3_Junctions3_node.ni_4._arrow._first_c)
449
       (and (= Junctions3_Junctions3_node.__Junctions3_Junctions3_node_31 (ite Junctions3_Junctions3_node.ni_4._arrow._first_m true false))
450
            (= Junctions3_Junctions3_node.ni_4._arrow._first_x false))
451
       (and (or (not (= Junctions3_Junctions3_node.__Junctions3_Junctions3_node_31 false))
452
               (and (= Junctions3_Junctions3_node.junctions3_junctions3__state_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c)
453
                    (= Junctions3_Junctions3_node.junctions3_junctions3__restart_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c)
454
                    ))
455
            (or (not (= Junctions3_Junctions3_node.__Junctions3_Junctions3_node_31 true))
456
               (and (= Junctions3_Junctions3_node.junctions3_junctions3__state_in POINTJunctions3_Junctions3)
457
                    (= Junctions3_Junctions3_node.junctions3_junctions3__restart_in false)
458
                    ))
459
       )
460
       (and (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_in JUNCTIONS3_A_IDL))
461
               (and (junctions3_junctions3__JUNCTIONS3_A_IDL_unless Junctions3_Junctions3_node.junctions3_junctions3__restart_in
462
                                                                    Junctions3_Junctions3_node.junctions3_junctions3__state_in
463
                                                                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_3
464
                                                                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_4)
465
                    (= Junctions3_Junctions3_node.junctions3_junctions3__state_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_4)
466
                    (= Junctions3_Junctions3_node.junctions3_junctions3__restart_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_3)
467
                    ))
468
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_in JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1))
469
               (and (junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_unless 
470
                    Junctions3_Junctions3_node.junctions3_junctions3__restart_in
471
                    Junctions3_Junctions3_node.junctions3_junctions3__state_in
472
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_5
473
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_6)
474
                    (= Junctions3_Junctions3_node.junctions3_junctions3__state_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_6)
475
                    (= Junctions3_Junctions3_node.junctions3_junctions3__restart_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_5)
476
                    ))
477
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_in JUNCTIONS3_B_IDL))
478
               (and (junctions3_junctions3__JUNCTIONS3_B_IDL_unless Junctions3_Junctions3_node.junctions3_junctions3__restart_in
479
                                                                    Junctions3_Junctions3_node.junctions3_junctions3__state_in
480
                                                                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_1
481
                                                                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_2)
482
                    (= Junctions3_Junctions3_node.junctions3_junctions3__state_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_2)
483
                    (= Junctions3_Junctions3_node.junctions3_junctions3__restart_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_1)
484
                    ))
485
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_in POINTJunctions3_Junctions3))
486
               (and (junctions3_junctions3__POINTJunctions3_Junctions3_unless 
487
                    Junctions3_Junctions3_node.junctions3_junctions3__restart_in
488
                    Junctions3_Junctions3_node.junctions3_junctions3__state_in
489
                    Junctions3_Junctions3_node.idJunctions3_Junctions3_1
490
                    Junctions3_Junctions3_node.x
491
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_9
492
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_10)
493
                    (= Junctions3_Junctions3_node.junctions3_junctions3__state_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_10)
494
                    (= Junctions3_Junctions3_node.junctions3_junctions3__restart_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_9)
495
                    ))
496
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_in POINT__TO__JUNCTIONS3_A_1))
497
               (and (junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_unless 
498
                    Junctions3_Junctions3_node.junctions3_junctions3__restart_in
499
                    Junctions3_Junctions3_node.junctions3_junctions3__state_in
500
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_7
501
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_8)
502
                    (= Junctions3_Junctions3_node.junctions3_junctions3__state_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_8)
503
                    (= Junctions3_Junctions3_node.junctions3_junctions3__restart_act Junctions3_Junctions3_node.__Junctions3_Junctions3_node_7)
504
                    ))
505
       )
506
       (and (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_act JUNCTIONS3_A_IDL))
507
               (and (junctions3_junctions3__JUNCTIONS3_A_IDL_handler_until 
508
                    Junctions3_Junctions3_node.idJunctions3_Junctions3_1
509
                    Junctions3_Junctions3_node.y_1
510
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_15
511
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_16
512
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_17
513
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_18)
514
                    (= Junctions3_Junctions3_node.y Junctions3_Junctions3_node.__Junctions3_Junctions3_node_18)
515
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_state_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_16)
516
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_restart_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_15)
517
                    (= Junctions3_Junctions3_node.idJunctions3_Junctions3 Junctions3_Junctions3_node.__Junctions3_Junctions3_node_17)
518
                    ))
519
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_act JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1))
520
               (and (junctions3_junctions3__JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1_handler_until 
521
                    Junctions3_Junctions3_node.idJunctions3_Junctions3_1
522
                    Junctions3_Junctions3_node.y_1
523
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_19
524
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_20
525
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_21
526
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_22)
527
                    (= Junctions3_Junctions3_node.y Junctions3_Junctions3_node.__Junctions3_Junctions3_node_22)
528
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_state_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_20)
529
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_restart_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_19)
530
                    (= Junctions3_Junctions3_node.idJunctions3_Junctions3 Junctions3_Junctions3_node.__Junctions3_Junctions3_node_21)
531
                    ))
532
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_act JUNCTIONS3_B_IDL))
533
               (and (junctions3_junctions3__JUNCTIONS3_B_IDL_handler_until 
534
                    Junctions3_Junctions3_node.idJunctions3_Junctions3_1
535
                    Junctions3_Junctions3_node.y_1
536
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_11
537
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_12
538
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_13
539
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_14)
540
                    (= Junctions3_Junctions3_node.y Junctions3_Junctions3_node.__Junctions3_Junctions3_node_14)
541
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_state_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_12)
542
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_restart_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_11)
543
                    (= Junctions3_Junctions3_node.idJunctions3_Junctions3 Junctions3_Junctions3_node.__Junctions3_Junctions3_node_13)
544
                    ))
545
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_act POINTJunctions3_Junctions3))
546
               (and (junctions3_junctions3__POINTJunctions3_Junctions3_handler_until 
547
                    Junctions3_Junctions3_node.idJunctions3_Junctions3_1
548
                    Junctions3_Junctions3_node.y_1
549
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_27
550
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_28
551
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_29
552
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_30)
553
                    (= Junctions3_Junctions3_node.y Junctions3_Junctions3_node.__Junctions3_Junctions3_node_30)
554
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_state_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_28)
555
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_restart_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_27)
556
                    (= Junctions3_Junctions3_node.idJunctions3_Junctions3 Junctions3_Junctions3_node.__Junctions3_Junctions3_node_29)
557
                    ))
558
            (or (not (= Junctions3_Junctions3_node.junctions3_junctions3__state_act POINT__TO__JUNCTIONS3_A_1))
559
               (and (junctions3_junctions3__POINT__TO__JUNCTIONS3_A_1_handler_until 
560
                    Junctions3_Junctions3_node.idJunctions3_Junctions3_1
561
                    Junctions3_Junctions3_node.y_1
562
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_23
563
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_24
564
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_25
565
                    Junctions3_Junctions3_node.__Junctions3_Junctions3_node_26)
566
                    (= Junctions3_Junctions3_node.y Junctions3_Junctions3_node.__Junctions3_Junctions3_node_26)
567
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_state_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_24)
568
                    (= Junctions3_Junctions3_node.junctions3_junctions3__next_restart_in Junctions3_Junctions3_node.__Junctions3_Junctions3_node_23)
569
                    (= Junctions3_Junctions3_node.idJunctions3_Junctions3 Junctions3_Junctions3_node.__Junctions3_Junctions3_node_25)
570
                    ))
571
       )
572
       (= Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x Junctions3_Junctions3_node.junctions3_junctions3__next_state_in)
573
       (= Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x Junctions3_Junctions3_node.junctions3_junctions3__next_restart_in)
574
       )
575
  (Junctions3_Junctions3_node_step Junctions3_Junctions3_node.idJunctions3_Junctions3_1
576
                                   Junctions3_Junctions3_node.x
577
                                   Junctions3_Junctions3_node.y_1
578
                                   Junctions3_Junctions3_node.idJunctions3_Junctions3
579
                                   Junctions3_Junctions3_node.y
580
                                   Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
581
                                   Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
582
                                   Junctions3_Junctions3_node.ni_4._arrow._first_c
583
                                   Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x
584
                                   Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x
585
                                   Junctions3_Junctions3_node.ni_4._arrow._first_x)
586
))
587
588
; Junctions3_Junctions3
589
(declare-var Junctions3_Junctions3.x Int)
590
(declare-var Junctions3_Junctions3.y Int)
591
(declare-var Junctions3_Junctions3.__Junctions3_Junctions3_2_c Int)
592
(declare-var Junctions3_Junctions3.__Junctions3_Junctions3_3_c Int)
593
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c Bool)
594
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c junctions3_junctions3__type)
595
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c Bool)
596
(declare-var Junctions3_Junctions3.ni_3._arrow._first_c Bool)
597
(declare-var Junctions3_Junctions3.__Junctions3_Junctions3_2_m Int)
598
(declare-var Junctions3_Junctions3.__Junctions3_Junctions3_3_m Int)
599
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m Bool)
600
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m junctions3_junctions3__type)
601
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m Bool)
602
(declare-var Junctions3_Junctions3.ni_3._arrow._first_m Bool)
603
(declare-var Junctions3_Junctions3.__Junctions3_Junctions3_2_x Int)
604
(declare-var Junctions3_Junctions3.__Junctions3_Junctions3_3_x Int)
605
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x Bool)
606
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x junctions3_junctions3__type)
607
(declare-var Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_x Bool)
608
(declare-var Junctions3_Junctions3.ni_3._arrow._first_x Bool)
609
(declare-var Junctions3_Junctions3.__Junctions3_Junctions3_1 Bool)
610
(declare-var Junctions3_Junctions3.idJunctions3_Junctions3 Int)
611
(declare-var Junctions3_Junctions3.idJunctions3_Junctions3_1 Int)
612
(declare-var Junctions3_Junctions3.y_1 Int)
613
(declare-rel Junctions3_Junctions3_reset (Int Int Bool junctions3_junctions3__type Bool Bool Int Int Bool junctions3_junctions3__type Bool Bool))
614
(declare-rel Junctions3_Junctions3_step (Int Int Int Int Bool junctions3_junctions3__type Bool Bool Int Int Bool junctions3_junctions3__type Bool Bool))
615
616
(rule (=> 
617
  (and 
618
       (= Junctions3_Junctions3.__Junctions3_Junctions3_2_m Junctions3_Junctions3.__Junctions3_Junctions3_2_c)
619
       (= Junctions3_Junctions3.__Junctions3_Junctions3_3_m Junctions3_Junctions3.__Junctions3_Junctions3_3_c)
620
       (= Junctions3_Junctions3.ni_3._arrow._first_m true)
621
       (Junctions3_Junctions3_node_reset Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
622
                                         Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
623
                                         Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c
624
                                         Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m
625
                                         Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m
626
                                         Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m)
627
  )
628
  (Junctions3_Junctions3_reset Junctions3_Junctions3.__Junctions3_Junctions3_2_c
629
                               Junctions3_Junctions3.__Junctions3_Junctions3_3_c
630
                               Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
631
                               Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
632
                               Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c
633
                               Junctions3_Junctions3.ni_3._arrow._first_c
634
                               Junctions3_Junctions3.__Junctions3_Junctions3_2_m
635
                               Junctions3_Junctions3.__Junctions3_Junctions3_3_m
636
                               Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m
637
                               Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m
638
                               Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m
639
                               Junctions3_Junctions3.ni_3._arrow._first_m)
640
))
641
642
(rule (=> 
643
  (and (= Junctions3_Junctions3.ni_3._arrow._first_m Junctions3_Junctions3.ni_3._arrow._first_c)
644
       (and (= Junctions3_Junctions3.__Junctions3_Junctions3_1 (ite Junctions3_Junctions3.ni_3._arrow._first_m true false))
645
            (= Junctions3_Junctions3.ni_3._arrow._first_x false))
646
       (and (or (not (= Junctions3_Junctions3.__Junctions3_Junctions3_1 false))
647
               (and (= Junctions3_Junctions3.y_1 Junctions3_Junctions3.__Junctions3_Junctions3_3_c)
648
                    (= Junctions3_Junctions3.idJunctions3_Junctions3_1 Junctions3_Junctions3.__Junctions3_Junctions3_2_c)
649
                    ))
650
            (or (not (= Junctions3_Junctions3.__Junctions3_Junctions3_1 true))
651
               (and (= Junctions3_Junctions3.y_1 111111)
652
                    (= Junctions3_Junctions3.idJunctions3_Junctions3_1 0)
653
                    ))
654
       )
655
       (and (= Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c)
656
            (= Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c)
657
            (= Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c)
658
            )
659
       (Junctions3_Junctions3_node_step Junctions3_Junctions3.idJunctions3_Junctions3_1
660
                                        Junctions3_Junctions3.x
661
                                        Junctions3_Junctions3.y_1
662
                                        Junctions3_Junctions3.idJunctions3_Junctions3
663
                                        Junctions3_Junctions3.y
664
                                        Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m
665
                                        Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m
666
                                        Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m
667
                                        Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x
668
                                        Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x
669
                                        Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_x)
670
       (= Junctions3_Junctions3.__Junctions3_Junctions3_3_x Junctions3_Junctions3.y)
671
       (= Junctions3_Junctions3.__Junctions3_Junctions3_2_x Junctions3_Junctions3.idJunctions3_Junctions3)
672
       )
673
  (Junctions3_Junctions3_step Junctions3_Junctions3.x
674
                              Junctions3_Junctions3.y
675
                              Junctions3_Junctions3.__Junctions3_Junctions3_2_c
676
                              Junctions3_Junctions3.__Junctions3_Junctions3_3_c
677
                              Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
678
                              Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
679
                              Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c
680
                              Junctions3_Junctions3.ni_3._arrow._first_c
681
                              Junctions3_Junctions3.__Junctions3_Junctions3_2_x
682
                              Junctions3_Junctions3.__Junctions3_Junctions3_3_x
683
                              Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x
684
                              Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x
685
                              Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_x
686
                              Junctions3_Junctions3.ni_3._arrow._first_x)
687
))
688
689
; Junctions3
690
(declare-var Junctions3.x_1_1 Int)
691
(declare-var Junctions3.y_1_1 Int)
692
(declare-var Junctions3.ni_0._arrow._first_c Bool)
693
(declare-var Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_c Int)
694
(declare-var Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_c Int)
695
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c Bool)
696
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c junctions3_junctions3__type)
697
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c Bool)
698
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_c Bool)
699
(declare-var Junctions3.ni_0._arrow._first_m Bool)
700
(declare-var Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_m Int)
701
(declare-var Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_m Int)
702
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m Bool)
703
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m junctions3_junctions3__type)
704
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m Bool)
705
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_m Bool)
706
(declare-var Junctions3.ni_0._arrow._first_x Bool)
707
(declare-var Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_x Int)
708
(declare-var Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_x Int)
709
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x Bool)
710
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x junctions3_junctions3__type)
711
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_x Bool)
712
(declare-var Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_x Bool)
713
(declare-var Junctions3.Junctions3_1_1 Int)
714
(declare-var Junctions3.__Junctions3_1 Bool)
715
(declare-var Junctions3.i_virtual_local Real)
716
(declare-rel Junctions3_reset (Bool Int Int Bool junctions3_junctions3__type Bool Bool Bool Int Int Bool junctions3_junctions3__type Bool Bool))
717
(declare-rel Junctions3_step (Int Int Bool Int Int Bool junctions3_junctions3__type Bool Bool Bool Int Int Bool junctions3_junctions3__type Bool Bool))
718
719
(rule (=> 
720
  (and 
721
       
722
       (Junctions3_Junctions3_reset Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_c
723
                                    Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_c
724
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
725
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
726
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c
727
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_c
728
                                    Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_m
729
                                    Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_m
730
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m
731
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m
732
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m
733
                                    Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_m)
734
       (= Junctions3.ni_0._arrow._first_m true)
735
  )
736
  (Junctions3_reset Junctions3.ni_0._arrow._first_c
737
                    Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_c
738
                    Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_c
739
                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
740
                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
741
                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c
742
                    Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_c
743
                    Junctions3.ni_0._arrow._first_m
744
                    Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_m
745
                    Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_m
746
                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m
747
                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m
748
                    Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m
749
                    Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_m)
750
))
751
752
(rule (=> 
753
  (and (and (= Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_m Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_c)
754
            (= Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_m Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_c)
755
            (= Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c)
756
            (= Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c)
757
            (= Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c)
758
            (= Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_m Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_c)
759
            )
760
       (Junctions3_Junctions3_step Junctions3.x_1_1
761
                                   Junctions3.Junctions3_1_1
762
                                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_m
763
                                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_m
764
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_m
765
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_m
766
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_m
767
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_m
768
                                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_x
769
                                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_x
770
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x
771
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x
772
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_x
773
                                   Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_x)
774
       (= Junctions3.y_1_1 Junctions3.Junctions3_1_1)
775
       (= Junctions3.ni_0._arrow._first_m Junctions3.ni_0._arrow._first_c)
776
       (and (= Junctions3.__Junctions3_1 (ite Junctions3.ni_0._arrow._first_m true false))
777
            (= Junctions3.ni_0._arrow._first_x false))
778
       (and (or (not (= Junctions3.__Junctions3_1 true))
779
               (= Junctions3.i_virtual_local 0.))
780
            (or (not (= Junctions3.__Junctions3_1 false))
781
               (= Junctions3.i_virtual_local 1.))
782
       )
783
       )
784
  (Junctions3_step Junctions3.x_1_1
785
                   Junctions3.y_1_1
786
                   Junctions3.ni_0._arrow._first_c
787
                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_c
788
                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_c
789
                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_c
790
                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_c
791
                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_c
792
                   Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_c
793
                   Junctions3.ni_0._arrow._first_x
794
                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_2_x
795
                   Junctions3.ni_1.Junctions3_Junctions3.__Junctions3_Junctions3_3_x
796
                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_32_x
797
                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.__Junctions3_Junctions3_node_33_x
798
                   Junctions3.ni_1.Junctions3_Junctions3.ni_2.Junctions3_Junctions3_node.ni_4._arrow._first_x
799
                   Junctions3.ni_1.Junctions3_Junctions3.ni_3._arrow._first_x)
800
))
801
802
; Junctions3_B_ex
803
(declare-var Junctions3_B_ex.idJunctions3_Junctions3_1 Int)
804
(declare-var Junctions3_B_ex.isInner Bool)
805
(declare-var Junctions3_B_ex.idJunctions3_Junctions3 Int)
806
(declare-var Junctions3_B_ex.idJunctions3_Junctions3_2 Int)
807
(declare-rel Junctions3_B_ex (Int Bool Int))
808
(rule (=> 
809
  (and (and (or (not (= (not Junctions3_B_ex.isInner) true))
810
               (= Junctions3_B_ex.idJunctions3_Junctions3_2 0))
811
            (or (not (= (not Junctions3_B_ex.isInner) false))
812
               (= Junctions3_B_ex.idJunctions3_Junctions3_2 Junctions3_B_ex.idJunctions3_Junctions3_1))
813
       )
814
       (= Junctions3_B_ex.idJunctions3_Junctions3 Junctions3_B_ex.idJunctions3_Junctions3_1)
815
       )
816
  (Junctions3_B_ex Junctions3_B_ex.idJunctions3_Junctions3_1 Junctions3_B_ex.isInner Junctions3_B_ex.idJunctions3_Junctions3)
817
))