Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions7 / Junctions7.smt2 @ eb639349

History | View | Annotate | Download (82.8 KB)

1
(declare-datatypes () ((junctions7_junctions7__type POINTJunctions7_Junctions7 POINT__TO__JUNCTIONS7_A_1 JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1 JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2 JUNCTIONS7_A_IDL JUNCTIONS7_B_IDL)));
2

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

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

    
29
; Junctions7_B_en
30
(declare-var Junctions7_B_en.idJunctions7_Junctions7_1 Int)
31
(declare-var Junctions7_B_en.isInner Bool)
32
(declare-var Junctions7_B_en.idJunctions7_Junctions7 Int)
33
(declare-rel Junctions7_B_en (Int Bool Int))
34
(rule (=> 
35
  (= Junctions7_B_en.idJunctions7_Junctions7 1319)
36
  (Junctions7_B_en Junctions7_B_en.idJunctions7_Junctions7_1 Junctions7_B_en.isInner Junctions7_B_en.idJunctions7_Junctions7)
37
))
38

    
39
; Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action
40
(declare-var Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action.y_1 Int)
41
(declare-var Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action.y Int)
42
(declare-rel Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action (Int Int))
43
(rule (=> 
44
  (= Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action.y (- Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action.y_1 1))
45
  (Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action.y_1 Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action.y)
46
))
47

    
48
; Junctions7_A_en
49
(declare-var Junctions7_A_en.idJunctions7_Junctions7_1 Int)
50
(declare-var Junctions7_A_en.isInner Bool)
51
(declare-var Junctions7_A_en.idJunctions7_Junctions7 Int)
52
(declare-rel Junctions7_A_en (Int Bool Int))
53
(rule (=> 
54
  (= Junctions7_A_en.idJunctions7_Junctions7 1318)
55
  (Junctions7_A_en Junctions7_A_en.idJunctions7_Junctions7_1 Junctions7_A_en.isInner Junctions7_A_en.idJunctions7_Junctions7)
56
))
57

    
58
; junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until
59
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.idJunctions7_Junctions7_1 Int)
60
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.y_1 Int)
61
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.junctions7_junctions7__restart_in Bool)
62
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.junctions7_junctions7__state_in junctions7_junctions7__type)
63
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.idJunctions7_Junctions7_out Int)
64
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.y_out Int)
65
(declare-rel junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until (Int Int Bool junctions7_junctions7__type Int Int))
66
(rule (=> 
67
  (and (= junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.y_out junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.y_1)
68
       (= junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.junctions7_junctions7__state_in POINTJunctions7_Junctions7)
69
       (= junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.junctions7_junctions7__restart_in true)
70
       (= junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.idJunctions7_Junctions7_1)
71
       )
72
  (junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.idJunctions7_Junctions7_1 junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.y_1 junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until.y_out)
73
))
74

    
75
; junctions7_junctions7__JUNCTIONS7_A_IDL_unless
76
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__restart_in Bool)
77
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__state_in junctions7_junctions7__type)
78
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__restart_act Bool)
79
(declare-var junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__state_act junctions7_junctions7__type)
80
(declare-rel junctions7_junctions7__JUNCTIONS7_A_IDL_unless (Bool junctions7_junctions7__type Bool junctions7_junctions7__type))
81
(rule (=> 
82
  (and (= junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__state_act junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__state_in)
83
       (= junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__restart_in)
84
       )
85
  (junctions7_junctions7__JUNCTIONS7_A_IDL_unless junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_A_IDL_unless.junctions7_junctions7__state_act)
86
))
87

    
88
; junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until
89
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_1 Int)
90
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.x Int)
91
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_1 Int)
92
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.junctions7_junctions7__restart_in Bool)
93
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.junctions7_junctions7__state_in junctions7_junctions7__type)
94
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_out Int)
95
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_out Int)
96
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 Bool)
97
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_2 Int)
98
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_3 Int)
99
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7 Int)
100
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_2 Int)
101
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_3 Int)
102
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y Int)
103
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_2 Int)
104
(declare-rel junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until (Int Int Int Bool junctions7_junctions7__type Int Int))
105
(rule (=> 
106
  (and (Junctions7_A__To__Junctions7_Junctions7Junction1322_1_Condition_Action 
107
       junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_1
108
       junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_2)
109
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 (< junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.x 2))
110
       (and (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 true))
111
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_2))
112
            (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 false))
113
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_2))
114
       )
115
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_out junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y)
116
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.junctions7_junctions7__state_in POINTJunctions7_Junctions7)
117
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.junctions7_junctions7__restart_in true)
118
       (Junctions7_A_ex junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_1
119
                        false
120
                        junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_3)
121
       (and (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 true))
122
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_2 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_3))
123
            (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 false))
124
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_2 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_1))
125
       )
126
       (Junctions7_B_en junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_2
127
                        false
128
                        junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_2)
129
       (and (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 false))
130
               (and (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_3 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_2)
131
                    (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_1)
132
                    ))
133
            (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_1 true))
134
               (and (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_3 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until_2)
135
                    (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_3)
136
                    ))
137
       )
138
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7)
139
       )
140
  (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_1 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.x junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_1 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until.y_out)
141
))
142

    
143
; junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless
144
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__restart_in Bool)
145
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__state_in junctions7_junctions7__type)
146
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__restart_act Bool)
147
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__state_act junctions7_junctions7__type)
148
(declare-rel junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless (Bool junctions7_junctions7__type Bool junctions7_junctions7__type))
149
(rule (=> 
150
  (and (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__state_act junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__state_in)
151
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__restart_in)
152
       )
153
  (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless.junctions7_junctions7__state_act)
154
))
155

    
156
; junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until
157
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_1 Int)
158
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.x Int)
159
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_1 Int)
160
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.junctions7_junctions7__restart_in Bool)
161
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.junctions7_junctions7__state_in junctions7_junctions7__type)
162
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_out Int)
163
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_out Int)
164
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 Bool)
165
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_2 Int)
166
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_3 Int)
167
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7 Int)
168
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_2 Int)
169
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_3 Int)
170
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y Int)
171
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_2 Int)
172
(declare-rel junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until (Int Int Int Bool junctions7_junctions7__type Int Int))
173
(rule (=> 
174
  (and (Junctions7_A__To__Junctions7_Junctions7Junction1322_2_Condition_Action 
175
       junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_1
176
       junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_2)
177
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 (< junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.x 2))
178
       (and (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 true))
179
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_2))
180
            (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 false))
181
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_2))
182
       )
183
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_out junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y)
184
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.junctions7_junctions7__state_in POINTJunctions7_Junctions7)
185
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.junctions7_junctions7__restart_in true)
186
       (Junctions7_A_ex junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_1
187
                        false
188
                        junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_3)
189
       (and (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 true))
190
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_2 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_3))
191
            (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 false))
192
               (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_2 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_1))
193
       )
194
       (Junctions7_B_en junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_2
195
                        false
196
                        junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_2)
197
       (and (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 false))
198
               (and (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_3 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_2)
199
                    (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_1)
200
                    ))
201
            (or (not (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_1 true))
202
               (and (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_3 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.__junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until_2)
203
                    (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_3)
204
                    ))
205
       )
206
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7)
207
       )
208
  (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_1 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.x junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_1 junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until.y_out)
209
))
210

    
211
; junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless
212
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__restart_in Bool)
213
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__state_in junctions7_junctions7__type)
214
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__restart_act Bool)
215
(declare-var junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__state_act junctions7_junctions7__type)
216
(declare-rel junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless (Bool junctions7_junctions7__type Bool junctions7_junctions7__type))
217
(rule (=> 
218
  (and (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__state_act junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__state_in)
219
       (= junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__restart_in)
220
       )
221
  (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless.junctions7_junctions7__state_act)
222
))
223

    
224
; junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until
225
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.idJunctions7_Junctions7_1 Int)
226
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.y_1 Int)
227
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.junctions7_junctions7__restart_in Bool)
228
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.junctions7_junctions7__state_in junctions7_junctions7__type)
229
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.idJunctions7_Junctions7_out Int)
230
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.y_out Int)
231
(declare-rel junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until (Int Int Bool junctions7_junctions7__type Int Int))
232
(rule (=> 
233
  (and (= junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.y_out junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.y_1)
234
       (= junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.junctions7_junctions7__state_in POINTJunctions7_Junctions7)
235
       (= junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.junctions7_junctions7__restart_in true)
236
       (= junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.idJunctions7_Junctions7_1)
237
       )
238
  (junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.idJunctions7_Junctions7_1 junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.y_1 junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until.y_out)
239
))
240

    
241
; junctions7_junctions7__JUNCTIONS7_B_IDL_unless
242
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__restart_in Bool)
243
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__state_in junctions7_junctions7__type)
244
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__restart_act Bool)
245
(declare-var junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__state_act junctions7_junctions7__type)
246
(declare-rel junctions7_junctions7__JUNCTIONS7_B_IDL_unless (Bool junctions7_junctions7__type Bool junctions7_junctions7__type))
247
(rule (=> 
248
  (and (= junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__state_act junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__state_in)
249
       (= junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__restart_in)
250
       )
251
  (junctions7_junctions7__JUNCTIONS7_B_IDL_unless junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__restart_in junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__state_in junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__restart_act junctions7_junctions7__JUNCTIONS7_B_IDL_unless.junctions7_junctions7__state_act)
252
))
253

    
254
; junctions7_junctions7__POINTJunctions7_Junctions7_handler_until
255
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.idJunctions7_Junctions7_1 Int)
256
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.y_1 Int)
257
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.junctions7_junctions7__restart_in Bool)
258
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.junctions7_junctions7__state_in junctions7_junctions7__type)
259
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.idJunctions7_Junctions7_out Int)
260
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.y_out Int)
261
(declare-rel junctions7_junctions7__POINTJunctions7_Junctions7_handler_until (Int Int Bool junctions7_junctions7__type Int Int))
262
(rule (=> 
263
  (and (= junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.y_out junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.y_1)
264
       (= junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.junctions7_junctions7__state_in POINTJunctions7_Junctions7)
265
       (= junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.junctions7_junctions7__restart_in false)
266
       (= junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.idJunctions7_Junctions7_1)
267
       )
268
  (junctions7_junctions7__POINTJunctions7_Junctions7_handler_until junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.idJunctions7_Junctions7_1 junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.y_1 junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.junctions7_junctions7__restart_in junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.junctions7_junctions7__state_in junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__POINTJunctions7_Junctions7_handler_until.y_out)
269
))
270

    
271
; junctions7_junctions7__POINTJunctions7_Junctions7_unless
272
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_in Bool)
273
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_in junctions7_junctions7__type)
274
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.idJunctions7_Junctions7_1 Int)
275
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.x Int)
276
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act Bool)
277
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act junctions7_junctions7__type)
278
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_1 Bool)
279
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_2 Bool)
280
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_3 Bool)
281
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_4 Bool)
282
(declare-var junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_5 Bool)
283
(declare-rel junctions7_junctions7__POINTJunctions7_Junctions7_unless (Bool junctions7_junctions7__type Int Int Bool junctions7_junctions7__type))
284
(rule (=> 
285
  (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_5 (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.idJunctions7_Junctions7_1 1319))
286
       (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_4 (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.idJunctions7_Junctions7_1 1318))
287
       (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_3 (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.idJunctions7_Junctions7_1 1318) (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.x 0)))
288
       (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_2 (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.idJunctions7_Junctions7_1 1318) (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.x 0))))
289
       (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_1 (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.idJunctions7_Junctions7_1 0))
290
       (and (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_1 false))
291
               (and (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_2 false))
292
                       (and (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_3 false))
293
                               (and (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_4 false))
294
                                       (and (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_5 false))
295
                                               (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_in)
296
                                                    (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_in)
297
                                                    ))
298
                                            (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_5 true))
299
                                               (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act JUNCTIONS7_B_IDL)
300
                                                    (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act true)
301
                                                    ))
302
                                       ))
303
                                    (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_4 true))
304
                                       (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act JUNCTIONS7_A_IDL)
305
                                            (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act true)
306
                                            ))
307
                               ))
308
                            (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_3 true))
309
                               (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2)
310
                                    (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act true)
311
                                    ))
312
                       ))
313
                    (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_2 true))
314
                       (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1)
315
                            (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act true)
316
                            ))
317
               ))
318
            (or (not (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.__junctions7_junctions7__POINTJunctions7_Junctions7_unless_1 true))
319
               (and (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act POINT__TO__JUNCTIONS7_A_1)
320
                    (= junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act true)
321
                    ))
322
       )
323
       )
324
  (junctions7_junctions7__POINTJunctions7_Junctions7_unless junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_in junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_in junctions7_junctions7__POINTJunctions7_Junctions7_unless.idJunctions7_Junctions7_1 junctions7_junctions7__POINTJunctions7_Junctions7_unless.x junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__restart_act junctions7_junctions7__POINTJunctions7_Junctions7_unless.junctions7_junctions7__state_act)
325
))
326

    
327
; junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until
328
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_1 Int)
329
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.y_1 Int)
330
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.junctions7_junctions7__restart_in Bool)
331
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.junctions7_junctions7__state_in junctions7_junctions7__type)
332
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_out Int)
333
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.y_out Int)
334
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_2 Int)
335
(declare-rel junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until (Int Int Bool junctions7_junctions7__type Int Int))
336
(rule (=> 
337
  (and (= junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.y_out junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.y_1)
338
       (= junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.junctions7_junctions7__state_in POINTJunctions7_Junctions7)
339
       (= junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.junctions7_junctions7__restart_in true)
340
       (Junctions7_A_en junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_1
341
                        false
342
                        junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_2)
343
       (= junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_2)
344
       )
345
  (junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_1 junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.y_1 junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.junctions7_junctions7__restart_in junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.junctions7_junctions7__state_in junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.idJunctions7_Junctions7_out junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until.y_out)
346
))
347

    
348
; junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless
349
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__restart_in Bool)
350
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__state_in junctions7_junctions7__type)
351
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__restart_act Bool)
352
(declare-var junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__state_act junctions7_junctions7__type)
353
(declare-rel junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless (Bool junctions7_junctions7__type Bool junctions7_junctions7__type))
354
(rule (=> 
355
  (and (= junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__state_act junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__state_in)
356
       (= junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__restart_act junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__restart_in)
357
       )
358
  (junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__restart_in junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__state_in junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__restart_act junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless.junctions7_junctions7__state_act)
359
))
360

    
361
; Junctions7_Junctions7_node
362
(declare-var Junctions7_Junctions7_node.idJunctions7_Junctions7_1 Int)
363
(declare-var Junctions7_Junctions7_node.x Int)
364
(declare-var Junctions7_Junctions7_node.y_1 Int)
365
(declare-var Junctions7_Junctions7_node.idJunctions7_Junctions7 Int)
366
(declare-var Junctions7_Junctions7_node.y Int)
367
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c Bool)
368
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c junctions7_junctions7__type)
369
(declare-var Junctions7_Junctions7_node.ni_4._arrow._first_c Bool)
370
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m Bool)
371
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m junctions7_junctions7__type)
372
(declare-var Junctions7_Junctions7_node.ni_4._arrow._first_m Bool)
373
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x Bool)
374
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x junctions7_junctions7__type)
375
(declare-var Junctions7_Junctions7_node.ni_4._arrow._first_x Bool)
376
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_1 Bool)
377
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_10 junctions7_junctions7__type)
378
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_11 Bool)
379
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_12 junctions7_junctions7__type)
380
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_13 Bool)
381
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_14 junctions7_junctions7__type)
382
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_15 Int)
383
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_16 Int)
384
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_17 Bool)
385
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_18 junctions7_junctions7__type)
386
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_19 Int)
387
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_2 junctions7_junctions7__type)
388
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_20 Int)
389
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_21 Bool)
390
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_22 junctions7_junctions7__type)
391
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_23 Int)
392
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_24 Int)
393
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_25 Bool)
394
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_26 junctions7_junctions7__type)
395
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_27 Int)
396
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_28 Int)
397
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_29 Bool)
398
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_3 Bool)
399
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_30 junctions7_junctions7__type)
400
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_31 Int)
401
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_32 Int)
402
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_33 Bool)
403
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_34 junctions7_junctions7__type)
404
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_35 Int)
405
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_36 Int)
406
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_37 Bool)
407
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_4 junctions7_junctions7__type)
408
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_5 Bool)
409
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_6 junctions7_junctions7__type)
410
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_7 Bool)
411
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_8 junctions7_junctions7__type)
412
(declare-var Junctions7_Junctions7_node.__Junctions7_Junctions7_node_9 Bool)
413
(declare-var Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in Bool)
414
(declare-var Junctions7_Junctions7_node.junctions7_junctions7__next_state_in junctions7_junctions7__type)
415
(declare-var Junctions7_Junctions7_node.junctions7_junctions7__restart_act Bool)
416
(declare-var Junctions7_Junctions7_node.junctions7_junctions7__restart_in Bool)
417
(declare-var Junctions7_Junctions7_node.junctions7_junctions7__state_act junctions7_junctions7__type)
418
(declare-var Junctions7_Junctions7_node.junctions7_junctions7__state_in junctions7_junctions7__type)
419
(declare-rel Junctions7_Junctions7_node_reset (Bool junctions7_junctions7__type Bool Bool junctions7_junctions7__type Bool))
420
(declare-rel Junctions7_Junctions7_node_step (Int Int Int Int Int Bool junctions7_junctions7__type Bool Bool junctions7_junctions7__type Bool))
421

    
422
(rule (=> 
423
  (and 
424
       (= Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c)
425
       (= Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c)
426
       (= Junctions7_Junctions7_node.ni_4._arrow._first_m true)
427
  )
428
  (Junctions7_Junctions7_node_reset Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
429
                                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
430
                                    Junctions7_Junctions7_node.ni_4._arrow._first_c
431
                                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m
432
                                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m
433
                                    Junctions7_Junctions7_node.ni_4._arrow._first_m)
434
))
435

    
436
(rule (=> 
437
  (and (= Junctions7_Junctions7_node.ni_4._arrow._first_m Junctions7_Junctions7_node.ni_4._arrow._first_c)
438
       (and (= Junctions7_Junctions7_node.__Junctions7_Junctions7_node_37 (ite Junctions7_Junctions7_node.ni_4._arrow._first_m true false))
439
            (= Junctions7_Junctions7_node.ni_4._arrow._first_x false))
440
       (and (or (not (= Junctions7_Junctions7_node.__Junctions7_Junctions7_node_37 false))
441
               (and (= Junctions7_Junctions7_node.junctions7_junctions7__state_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c)
442
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c)
443
                    ))
444
            (or (not (= Junctions7_Junctions7_node.__Junctions7_Junctions7_node_37 true))
445
               (and (= Junctions7_Junctions7_node.junctions7_junctions7__state_in POINTJunctions7_Junctions7)
446
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_in false)
447
                    ))
448
       )
449
       (and (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_in JUNCTIONS7_A_IDL))
450
               (and (junctions7_junctions7__JUNCTIONS7_A_IDL_unless Junctions7_Junctions7_node.junctions7_junctions7__restart_in
451
                                                                    Junctions7_Junctions7_node.junctions7_junctions7__state_in
452
                                                                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_3
453
                                                                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_4)
454
                    (= Junctions7_Junctions7_node.junctions7_junctions7__state_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_4)
455
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_3)
456
                    ))
457
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_in JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1))
458
               (and (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_unless 
459
                    Junctions7_Junctions7_node.junctions7_junctions7__restart_in
460
                    Junctions7_Junctions7_node.junctions7_junctions7__state_in
461
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_7
462
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_8)
463
                    (= Junctions7_Junctions7_node.junctions7_junctions7__state_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_8)
464
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_7)
465
                    ))
466
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_in JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2))
467
               (and (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_unless 
468
                    Junctions7_Junctions7_node.junctions7_junctions7__restart_in
469
                    Junctions7_Junctions7_node.junctions7_junctions7__state_in
470
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_5
471
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_6)
472
                    (= Junctions7_Junctions7_node.junctions7_junctions7__state_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_6)
473
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_5)
474
                    ))
475
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_in JUNCTIONS7_B_IDL))
476
               (and (junctions7_junctions7__JUNCTIONS7_B_IDL_unless Junctions7_Junctions7_node.junctions7_junctions7__restart_in
477
                                                                    Junctions7_Junctions7_node.junctions7_junctions7__state_in
478
                                                                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_1
479
                                                                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_2)
480
                    (= Junctions7_Junctions7_node.junctions7_junctions7__state_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_2)
481
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_1)
482
                    ))
483
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_in POINTJunctions7_Junctions7))
484
               (and (junctions7_junctions7__POINTJunctions7_Junctions7_unless 
485
                    Junctions7_Junctions7_node.junctions7_junctions7__restart_in
486
                    Junctions7_Junctions7_node.junctions7_junctions7__state_in
487
                    Junctions7_Junctions7_node.idJunctions7_Junctions7_1
488
                    Junctions7_Junctions7_node.x
489
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_11
490
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_12)
491
                    (= Junctions7_Junctions7_node.junctions7_junctions7__state_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_12)
492
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_11)
493
                    ))
494
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_in POINT__TO__JUNCTIONS7_A_1))
495
               (and (junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_unless 
496
                    Junctions7_Junctions7_node.junctions7_junctions7__restart_in
497
                    Junctions7_Junctions7_node.junctions7_junctions7__state_in
498
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_9
499
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_10)
500
                    (= Junctions7_Junctions7_node.junctions7_junctions7__state_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_10)
501
                    (= Junctions7_Junctions7_node.junctions7_junctions7__restart_act Junctions7_Junctions7_node.__Junctions7_Junctions7_node_9)
502
                    ))
503
       )
504
       (and (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_act JUNCTIONS7_A_IDL))
505
               (and (junctions7_junctions7__JUNCTIONS7_A_IDL_handler_until 
506
                    Junctions7_Junctions7_node.idJunctions7_Junctions7_1
507
                    Junctions7_Junctions7_node.y_1
508
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_17
509
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_18
510
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_19
511
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_20)
512
                    (= Junctions7_Junctions7_node.y Junctions7_Junctions7_node.__Junctions7_Junctions7_node_20)
513
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_state_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_18)
514
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_17)
515
                    (= Junctions7_Junctions7_node.idJunctions7_Junctions7 Junctions7_Junctions7_node.__Junctions7_Junctions7_node_19)
516
                    ))
517
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_act JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1))
518
               (and (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_1_handler_until 
519
                    Junctions7_Junctions7_node.idJunctions7_Junctions7_1
520
                    Junctions7_Junctions7_node.x
521
                    Junctions7_Junctions7_node.y_1
522
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_25
523
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_26
524
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_27
525
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_28)
526
                    (= Junctions7_Junctions7_node.y Junctions7_Junctions7_node.__Junctions7_Junctions7_node_28)
527
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_state_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_26)
528
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_25)
529
                    (= Junctions7_Junctions7_node.idJunctions7_Junctions7 Junctions7_Junctions7_node.__Junctions7_Junctions7_node_27)
530
                    ))
531
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_act JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2))
532
               (and (junctions7_junctions7__JUNCTIONS7_A__TO__JUNCTIONS7_JUNCTIONS7JUNCTION1322_2_handler_until 
533
                    Junctions7_Junctions7_node.idJunctions7_Junctions7_1
534
                    Junctions7_Junctions7_node.x
535
                    Junctions7_Junctions7_node.y_1
536
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_21
537
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_22
538
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_23
539
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_24)
540
                    (= Junctions7_Junctions7_node.y Junctions7_Junctions7_node.__Junctions7_Junctions7_node_24)
541
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_state_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_22)
542
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_21)
543
                    (= Junctions7_Junctions7_node.idJunctions7_Junctions7 Junctions7_Junctions7_node.__Junctions7_Junctions7_node_23)
544
                    ))
545
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_act JUNCTIONS7_B_IDL))
546
               (and (junctions7_junctions7__JUNCTIONS7_B_IDL_handler_until 
547
                    Junctions7_Junctions7_node.idJunctions7_Junctions7_1
548
                    Junctions7_Junctions7_node.y_1
549
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_13
550
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_14
551
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_15
552
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_16)
553
                    (= Junctions7_Junctions7_node.y Junctions7_Junctions7_node.__Junctions7_Junctions7_node_16)
554
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_state_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_14)
555
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_13)
556
                    (= Junctions7_Junctions7_node.idJunctions7_Junctions7 Junctions7_Junctions7_node.__Junctions7_Junctions7_node_15)
557
                    ))
558
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_act POINTJunctions7_Junctions7))
559
               (and (junctions7_junctions7__POINTJunctions7_Junctions7_handler_until 
560
                    Junctions7_Junctions7_node.idJunctions7_Junctions7_1
561
                    Junctions7_Junctions7_node.y_1
562
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_33
563
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_34
564
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_35
565
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_36)
566
                    (= Junctions7_Junctions7_node.y Junctions7_Junctions7_node.__Junctions7_Junctions7_node_36)
567
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_state_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_34)
568
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_33)
569
                    (= Junctions7_Junctions7_node.idJunctions7_Junctions7 Junctions7_Junctions7_node.__Junctions7_Junctions7_node_35)
570
                    ))
571
            (or (not (= Junctions7_Junctions7_node.junctions7_junctions7__state_act POINT__TO__JUNCTIONS7_A_1))
572
               (and (junctions7_junctions7__POINT__TO__JUNCTIONS7_A_1_handler_until 
573
                    Junctions7_Junctions7_node.idJunctions7_Junctions7_1
574
                    Junctions7_Junctions7_node.y_1
575
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_29
576
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_30
577
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_31
578
                    Junctions7_Junctions7_node.__Junctions7_Junctions7_node_32)
579
                    (= Junctions7_Junctions7_node.y Junctions7_Junctions7_node.__Junctions7_Junctions7_node_32)
580
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_state_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_30)
581
                    (= Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in Junctions7_Junctions7_node.__Junctions7_Junctions7_node_29)
582
                    (= Junctions7_Junctions7_node.idJunctions7_Junctions7 Junctions7_Junctions7_node.__Junctions7_Junctions7_node_31)
583
                    ))
584
       )
585
       (= Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x Junctions7_Junctions7_node.junctions7_junctions7__next_state_in)
586
       (= Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x Junctions7_Junctions7_node.junctions7_junctions7__next_restart_in)
587
       )
588
  (Junctions7_Junctions7_node_step Junctions7_Junctions7_node.idJunctions7_Junctions7_1
589
                                   Junctions7_Junctions7_node.x
590
                                   Junctions7_Junctions7_node.y_1
591
                                   Junctions7_Junctions7_node.idJunctions7_Junctions7
592
                                   Junctions7_Junctions7_node.y
593
                                   Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
594
                                   Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
595
                                   Junctions7_Junctions7_node.ni_4._arrow._first_c
596
                                   Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x
597
                                   Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x
598
                                   Junctions7_Junctions7_node.ni_4._arrow._first_x)
599
))
600

    
601
; Junctions7_Junctions7
602
(declare-var Junctions7_Junctions7.x Int)
603
(declare-var Junctions7_Junctions7.y Int)
604
(declare-var Junctions7_Junctions7.__Junctions7_Junctions7_2_c Int)
605
(declare-var Junctions7_Junctions7.__Junctions7_Junctions7_3_c Int)
606
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c Bool)
607
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c junctions7_junctions7__type)
608
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c Bool)
609
(declare-var Junctions7_Junctions7.ni_3._arrow._first_c Bool)
610
(declare-var Junctions7_Junctions7.__Junctions7_Junctions7_2_m Int)
611
(declare-var Junctions7_Junctions7.__Junctions7_Junctions7_3_m Int)
612
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m Bool)
613
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m junctions7_junctions7__type)
614
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m Bool)
615
(declare-var Junctions7_Junctions7.ni_3._arrow._first_m Bool)
616
(declare-var Junctions7_Junctions7.__Junctions7_Junctions7_2_x Int)
617
(declare-var Junctions7_Junctions7.__Junctions7_Junctions7_3_x Int)
618
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x Bool)
619
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x junctions7_junctions7__type)
620
(declare-var Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_x Bool)
621
(declare-var Junctions7_Junctions7.ni_3._arrow._first_x Bool)
622
(declare-var Junctions7_Junctions7.__Junctions7_Junctions7_1 Bool)
623
(declare-var Junctions7_Junctions7.idJunctions7_Junctions7 Int)
624
(declare-var Junctions7_Junctions7.idJunctions7_Junctions7_1 Int)
625
(declare-var Junctions7_Junctions7.y_1 Int)
626
(declare-rel Junctions7_Junctions7_reset (Int Int Bool junctions7_junctions7__type Bool Bool Int Int Bool junctions7_junctions7__type Bool Bool))
627
(declare-rel Junctions7_Junctions7_step (Int Int Int Int Bool junctions7_junctions7__type Bool Bool Int Int Bool junctions7_junctions7__type Bool Bool))
628

    
629
(rule (=> 
630
  (and 
631
       (= Junctions7_Junctions7.__Junctions7_Junctions7_2_m Junctions7_Junctions7.__Junctions7_Junctions7_2_c)
632
       (= Junctions7_Junctions7.__Junctions7_Junctions7_3_m Junctions7_Junctions7.__Junctions7_Junctions7_3_c)
633
       (= Junctions7_Junctions7.ni_3._arrow._first_m true)
634
       (Junctions7_Junctions7_node_reset Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
635
                                         Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
636
                                         Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c
637
                                         Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m
638
                                         Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m
639
                                         Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m)
640
  )
641
  (Junctions7_Junctions7_reset Junctions7_Junctions7.__Junctions7_Junctions7_2_c
642
                               Junctions7_Junctions7.__Junctions7_Junctions7_3_c
643
                               Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
644
                               Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
645
                               Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c
646
                               Junctions7_Junctions7.ni_3._arrow._first_c
647
                               Junctions7_Junctions7.__Junctions7_Junctions7_2_m
648
                               Junctions7_Junctions7.__Junctions7_Junctions7_3_m
649
                               Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m
650
                               Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m
651
                               Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m
652
                               Junctions7_Junctions7.ni_3._arrow._first_m)
653
))
654

    
655
(rule (=> 
656
  (and (= Junctions7_Junctions7.ni_3._arrow._first_m Junctions7_Junctions7.ni_3._arrow._first_c)
657
       (and (= Junctions7_Junctions7.__Junctions7_Junctions7_1 (ite Junctions7_Junctions7.ni_3._arrow._first_m true false))
658
            (= Junctions7_Junctions7.ni_3._arrow._first_x false))
659
       (and (or (not (= Junctions7_Junctions7.__Junctions7_Junctions7_1 false))
660
               (and (= Junctions7_Junctions7.y_1 Junctions7_Junctions7.__Junctions7_Junctions7_3_c)
661
                    (= Junctions7_Junctions7.idJunctions7_Junctions7_1 Junctions7_Junctions7.__Junctions7_Junctions7_2_c)
662
                    ))
663
            (or (not (= Junctions7_Junctions7.__Junctions7_Junctions7_1 true))
664
               (and (= Junctions7_Junctions7.y_1 0)
665
                    (= Junctions7_Junctions7.idJunctions7_Junctions7_1 0)
666
                    ))
667
       )
668
       (and (= Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c)
669
            (= Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c)
670
            (= Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c)
671
            )
672
       (Junctions7_Junctions7_node_step Junctions7_Junctions7.idJunctions7_Junctions7_1
673
                                        Junctions7_Junctions7.x
674
                                        Junctions7_Junctions7.y_1
675
                                        Junctions7_Junctions7.idJunctions7_Junctions7
676
                                        Junctions7_Junctions7.y
677
                                        Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m
678
                                        Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m
679
                                        Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m
680
                                        Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x
681
                                        Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x
682
                                        Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_x)
683
       (= Junctions7_Junctions7.__Junctions7_Junctions7_3_x Junctions7_Junctions7.y)
684
       (= Junctions7_Junctions7.__Junctions7_Junctions7_2_x Junctions7_Junctions7.idJunctions7_Junctions7)
685
       )
686
  (Junctions7_Junctions7_step Junctions7_Junctions7.x
687
                              Junctions7_Junctions7.y
688
                              Junctions7_Junctions7.__Junctions7_Junctions7_2_c
689
                              Junctions7_Junctions7.__Junctions7_Junctions7_3_c
690
                              Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
691
                              Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
692
                              Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c
693
                              Junctions7_Junctions7.ni_3._arrow._first_c
694
                              Junctions7_Junctions7.__Junctions7_Junctions7_2_x
695
                              Junctions7_Junctions7.__Junctions7_Junctions7_3_x
696
                              Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x
697
                              Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x
698
                              Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_x
699
                              Junctions7_Junctions7.ni_3._arrow._first_x)
700
))
701

    
702
; Junctions7
703
(declare-var Junctions7.x_1_1 Int)
704
(declare-var Junctions7.y_1_1 Int)
705
(declare-var Junctions7.ni_0._arrow._first_c Bool)
706
(declare-var Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_c Int)
707
(declare-var Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_c Int)
708
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c Bool)
709
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c junctions7_junctions7__type)
710
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c Bool)
711
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_c Bool)
712
(declare-var Junctions7.ni_0._arrow._first_m Bool)
713
(declare-var Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_m Int)
714
(declare-var Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_m Int)
715
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m Bool)
716
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m junctions7_junctions7__type)
717
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m Bool)
718
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_m Bool)
719
(declare-var Junctions7.ni_0._arrow._first_x Bool)
720
(declare-var Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_x Int)
721
(declare-var Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_x Int)
722
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x Bool)
723
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x junctions7_junctions7__type)
724
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_x Bool)
725
(declare-var Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_x Bool)
726
(declare-var Junctions7.Junctions7_1_1 Int)
727
(declare-var Junctions7.__Junctions7_1 Bool)
728
(declare-var Junctions7.i_virtual_local Real)
729
(declare-rel Junctions7_reset (Bool Int Int Bool junctions7_junctions7__type Bool Bool Bool Int Int Bool junctions7_junctions7__type Bool Bool))
730
(declare-rel Junctions7_step (Int Int Bool Int Int Bool junctions7_junctions7__type Bool Bool Bool Int Int Bool junctions7_junctions7__type Bool Bool))
731

    
732
(rule (=> 
733
  (and 
734
       
735
       (Junctions7_Junctions7_reset Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_c
736
                                    Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_c
737
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
738
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
739
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c
740
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_c
741
                                    Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_m
742
                                    Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_m
743
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m
744
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m
745
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m
746
                                    Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_m)
747
       (= Junctions7.ni_0._arrow._first_m true)
748
  )
749
  (Junctions7_reset Junctions7.ni_0._arrow._first_c
750
                    Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_c
751
                    Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_c
752
                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
753
                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
754
                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c
755
                    Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_c
756
                    Junctions7.ni_0._arrow._first_m
757
                    Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_m
758
                    Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_m
759
                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m
760
                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m
761
                    Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m
762
                    Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_m)
763
))
764

    
765
(rule (=> 
766
  (and (and (= Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_m Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_c)
767
            (= Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_m Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_c)
768
            (= Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c)
769
            (= Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c)
770
            (= Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c)
771
            (= Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_m Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_c)
772
            )
773
       (Junctions7_Junctions7_step Junctions7.x_1_1
774
                                   Junctions7.Junctions7_1_1
775
                                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_m
776
                                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_m
777
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_m
778
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_m
779
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_m
780
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_m
781
                                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_x
782
                                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_x
783
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x
784
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x
785
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_x
786
                                   Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_x)
787
       (= Junctions7.y_1_1 Junctions7.Junctions7_1_1)
788
       (= Junctions7.ni_0._arrow._first_m Junctions7.ni_0._arrow._first_c)
789
       (and (= Junctions7.__Junctions7_1 (ite Junctions7.ni_0._arrow._first_m true false))
790
            (= Junctions7.ni_0._arrow._first_x false))
791
       (and (or (not (= Junctions7.__Junctions7_1 true))
792
               (= Junctions7.i_virtual_local 0.))
793
            (or (not (= Junctions7.__Junctions7_1 false))
794
               (= Junctions7.i_virtual_local 1.))
795
       )
796
       )
797
  (Junctions7_step Junctions7.x_1_1
798
                   Junctions7.y_1_1
799
                   Junctions7.ni_0._arrow._first_c
800
                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_c
801
                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_c
802
                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_c
803
                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_c
804
                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_c
805
                   Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_c
806
                   Junctions7.ni_0._arrow._first_x
807
                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_2_x
808
                   Junctions7.ni_1.Junctions7_Junctions7.__Junctions7_Junctions7_3_x
809
                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_38_x
810
                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.__Junctions7_Junctions7_node_39_x
811
                   Junctions7.ni_1.Junctions7_Junctions7.ni_2.Junctions7_Junctions7_node.ni_4._arrow._first_x
812
                   Junctions7.ni_1.Junctions7_Junctions7.ni_3._arrow._first_x)
813
))
814

    
815
; Junctions7_B_ex
816
(declare-var Junctions7_B_ex.idJunctions7_Junctions7_1 Int)
817
(declare-var Junctions7_B_ex.isInner Bool)
818
(declare-var Junctions7_B_ex.idJunctions7_Junctions7 Int)
819
(declare-var Junctions7_B_ex.idJunctions7_Junctions7_2 Int)
820
(declare-rel Junctions7_B_ex (Int Bool Int))
821
(rule (=> 
822
  (and (and (or (not (= (not Junctions7_B_ex.isInner) true))
823
               (= Junctions7_B_ex.idJunctions7_Junctions7_2 0))
824
            (or (not (= (not Junctions7_B_ex.isInner) false))
825
               (= Junctions7_B_ex.idJunctions7_Junctions7_2 Junctions7_B_ex.idJunctions7_Junctions7_1))
826
       )
827
       (= Junctions7_B_ex.idJunctions7_Junctions7 Junctions7_B_ex.idJunctions7_Junctions7_1)
828
       )
829
  (Junctions7_B_ex Junctions7_B_ex.idJunctions7_Junctions7_1 Junctions7_B_ex.isInner Junctions7_B_ex.idJunctions7_Junctions7)
830
))
831