Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions1 / Junctions1.smt2 @ eb639349

History | View | Annotate | Download (97.1 KB)

1 eb639349 bourbouh
(declare-datatypes () ((chart_chart__type POINTChart_Chart POINT__TO__CHART_A_1 CHART_A__TO__CHART_CHARTJUNCTION1149_1 CHART_C__TO__CHART_A_1 CHART_B__TO__CHART_A_1 CHART_A_IDL CHART_C_IDL CHART_B_IDL)));
2
3
; Chart_A__To__Chart_ChartJunction1149_1_Condition_Action
4
(declare-var Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.y_1 Int)
5
(declare-var Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.z_1 Int)
6
(declare-var Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.y Int)
7
(declare-var Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.z Int)
8
(declare-rel Chart_A__To__Chart_ChartJunction1149_1_Condition_Action (Int Int Int Int))
9
(rule (=> 
10
  (and (= Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.z (+ Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.z_1 2))
11
       (= Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.y (+ Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.y_1 1))
12
       )
13
  (Chart_A__To__Chart_ChartJunction1149_1_Condition_Action Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.y_1 Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.z_1 Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.y Chart_A__To__Chart_ChartJunction1149_1_Condition_Action.z)
14
))
15
16
; Chart_A_ex
17
(declare-var Chart_A_ex.y_1 Int)
18
(declare-var Chart_A_ex.idChart_Chart_1 Int)
19
(declare-var Chart_A_ex.isInner Bool)
20
(declare-var Chart_A_ex.y Int)
21
(declare-var Chart_A_ex.idChart_Chart Int)
22
(declare-var Chart_A_ex.__Chart_A_ex_1 Bool)
23
(declare-var Chart_A_ex.idChart_Chart_2 Int)
24
(declare-var Chart_A_ex.y_2 Int)
25
(declare-rel Chart_A_ex (Int Int Bool Int Int))
26
(rule (=> 
27
  (and (= Chart_A_ex.__Chart_A_ex_1 (not Chart_A_ex.isInner))
28
       (and (or (not (= Chart_A_ex.__Chart_A_ex_1 false))
29
               (and (= Chart_A_ex.y_2 Chart_A_ex.y_1)
30
                    (= Chart_A_ex.idChart_Chart_2 Chart_A_ex.idChart_Chart_1)
31
                    ))
32
            (or (not (= Chart_A_ex.__Chart_A_ex_1 true))
33
               (and (= Chart_A_ex.y_2 (* Chart_A_ex.y_1 2))
34
                    (= Chart_A_ex.idChart_Chart_2 0)
35
                    ))
36
       )
37
       (= Chart_A_ex.y Chart_A_ex.y_2)
38
       (= Chart_A_ex.idChart_Chart Chart_A_ex.idChart_Chart_1)
39
       )
40
  (Chart_A_ex Chart_A_ex.y_1 Chart_A_ex.idChart_Chart_1 Chart_A_ex.isInner Chart_A_ex.y Chart_A_ex.idChart_Chart)
41
))
42
43
; Chart_B_en
44
(declare-var Chart_B_en.idChart_Chart_1 Int)
45
(declare-var Chart_B_en.isInner Bool)
46
(declare-var Chart_B_en.idChart_Chart Int)
47
(declare-rel Chart_B_en (Int Bool Int))
48
(rule (=> 
49
  (= Chart_B_en.idChart_Chart 1144)
50
  (Chart_B_en Chart_B_en.idChart_Chart_1 Chart_B_en.isInner Chart_B_en.idChart_Chart)
51
))
52
53
; Chart_C_en
54
(declare-var Chart_C_en.idChart_Chart_1 Int)
55
(declare-var Chart_C_en.isInner Bool)
56
(declare-var Chart_C_en.idChart_Chart Int)
57
(declare-rel Chart_C_en (Int Bool Int))
58
(rule (=> 
59
  (= Chart_C_en.idChart_Chart 1143)
60
  (Chart_C_en Chart_C_en.idChart_Chart_1 Chart_C_en.isInner Chart_C_en.idChart_Chart)
61
))
62
63
; Chart_ChartJunction1149__To__Chart_B_1_Condition_Action
64
(declare-var Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.y_1 Int)
65
(declare-var Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.z_1 Int)
66
(declare-var Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.y Int)
67
(declare-var Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.z Int)
68
(declare-rel Chart_ChartJunction1149__To__Chart_B_1_Condition_Action (Int Int Int Int))
69
(rule (=> 
70
  (and (= Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.z (+ Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.z_1 1))
71
       (= Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.y (+ Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.y_1 2))
72
       )
73
  (Chart_ChartJunction1149__To__Chart_B_1_Condition_Action Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.y_1 Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.z_1 Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.y Chart_ChartJunction1149__To__Chart_B_1_Condition_Action.z)
74
))
75
76
; Chart_ChartJunction1149__To__Chart_C_2_Condition_Action
77
(declare-var Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.y_1 Int)
78
(declare-var Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.z_1 Int)
79
(declare-var Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.y Int)
80
(declare-var Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.z Int)
81
(declare-rel Chart_ChartJunction1149__To__Chart_C_2_Condition_Action (Int Int Int Int))
82
(rule (=> 
83
  (and (= Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.z (+ Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.z_1 1))
84
       (= Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.y (+ Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.y_1 1))
85
       )
86
  (Chart_ChartJunction1149__To__Chart_C_2_Condition_Action Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.y_1 Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.z_1 Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.y Chart_ChartJunction1149__To__Chart_C_2_Condition_Action.z)
87
))
88
89
; Chart_A_en
90
(declare-var Chart_A_en.idChart_Chart_1 Int)
91
(declare-var Chart_A_en.isInner Bool)
92
(declare-var Chart_A_en.idChart_Chart Int)
93
(declare-rel Chart_A_en (Int Bool Int))
94
(rule (=> 
95
  (= Chart_A_en.idChart_Chart 1142)
96
  (Chart_A_en Chart_A_en.idChart_Chart_1 Chart_A_en.isInner Chart_A_en.idChart_Chart)
97
))
98
99
; Chart_B_ex
100
(declare-var Chart_B_ex.idChart_Chart_1 Int)
101
(declare-var Chart_B_ex.isInner Bool)
102
(declare-var Chart_B_ex.idChart_Chart Int)
103
(declare-var Chart_B_ex.idChart_Chart_2 Int)
104
(declare-rel Chart_B_ex (Int Bool Int))
105
(rule (=> 
106
  (and (and (or (not (= (not Chart_B_ex.isInner) true))
107
               (= Chart_B_ex.idChart_Chart_2 0))
108
            (or (not (= (not Chart_B_ex.isInner) false))
109
               (= Chart_B_ex.idChart_Chart_2 Chart_B_ex.idChart_Chart_1))
110
       )
111
       (= Chart_B_ex.idChart_Chart Chart_B_ex.idChart_Chart_1)
112
       )
113
  (Chart_B_ex Chart_B_ex.idChart_Chart_1 Chart_B_ex.isInner Chart_B_ex.idChart_Chart)
114
))
115
116
; Chart_C_ex
117
(declare-var Chart_C_ex.idChart_Chart_1 Int)
118
(declare-var Chart_C_ex.isInner Bool)
119
(declare-var Chart_C_ex.idChart_Chart Int)
120
(declare-var Chart_C_ex.idChart_Chart_2 Int)
121
(declare-rel Chart_C_ex (Int Bool Int))
122
(rule (=> 
123
  (and (and (or (not (= (not Chart_C_ex.isInner) true))
124
               (= Chart_C_ex.idChart_Chart_2 0))
125
            (or (not (= (not Chart_C_ex.isInner) false))
126
               (= Chart_C_ex.idChart_Chart_2 Chart_C_ex.idChart_Chart_1))
127
       )
128
       (= Chart_C_ex.idChart_Chart Chart_C_ex.idChart_Chart_1)
129
       )
130
  (Chart_C_ex Chart_C_ex.idChart_Chart_1 Chart_C_ex.isInner Chart_C_ex.idChart_Chart)
131
))
132
133
; chart_chart__CHART_A_IDL_handler_until
134
(declare-var chart_chart__CHART_A_IDL_handler_until.idChart_Chart_1 Int)
135
(declare-var chart_chart__CHART_A_IDL_handler_until.y_1 Int)
136
(declare-var chart_chart__CHART_A_IDL_handler_until.z_1 Int)
137
(declare-var chart_chart__CHART_A_IDL_handler_until.chart_chart__restart_in Bool)
138
(declare-var chart_chart__CHART_A_IDL_handler_until.chart_chart__state_in chart_chart__type)
139
(declare-var chart_chart__CHART_A_IDL_handler_until.idChart_Chart_out Int)
140
(declare-var chart_chart__CHART_A_IDL_handler_until.y_out Int)
141
(declare-var chart_chart__CHART_A_IDL_handler_until.z_out Int)
142
(declare-rel chart_chart__CHART_A_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
143
(rule (=> 
144
  (and (= chart_chart__CHART_A_IDL_handler_until.z_out chart_chart__CHART_A_IDL_handler_until.z_1)
145
       (= chart_chart__CHART_A_IDL_handler_until.y_out chart_chart__CHART_A_IDL_handler_until.y_1)
146
       (= chart_chart__CHART_A_IDL_handler_until.idChart_Chart_out chart_chart__CHART_A_IDL_handler_until.idChart_Chart_1)
147
       (= chart_chart__CHART_A_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
148
       (= chart_chart__CHART_A_IDL_handler_until.chart_chart__restart_in true)
149
       )
150
  (chart_chart__CHART_A_IDL_handler_until chart_chart__CHART_A_IDL_handler_until.idChart_Chart_1 chart_chart__CHART_A_IDL_handler_until.y_1 chart_chart__CHART_A_IDL_handler_until.z_1 chart_chart__CHART_A_IDL_handler_until.chart_chart__restart_in chart_chart__CHART_A_IDL_handler_until.chart_chart__state_in chart_chart__CHART_A_IDL_handler_until.idChart_Chart_out chart_chart__CHART_A_IDL_handler_until.y_out chart_chart__CHART_A_IDL_handler_until.z_out)
151
))
152
153
; chart_chart__CHART_A_IDL_unless
154
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__restart_in Bool)
155
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__state_in chart_chart__type)
156
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__restart_act Bool)
157
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__state_act chart_chart__type)
158
(declare-rel chart_chart__CHART_A_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
159
(rule (=> 
160
  (and (= chart_chart__CHART_A_IDL_unless.chart_chart__state_act chart_chart__CHART_A_IDL_unless.chart_chart__state_in)
161
       (= chart_chart__CHART_A_IDL_unless.chart_chart__restart_act chart_chart__CHART_A_IDL_unless.chart_chart__restart_in)
162
       )
163
  (chart_chart__CHART_A_IDL_unless chart_chart__CHART_A_IDL_unless.chart_chart__restart_in chart_chart__CHART_A_IDL_unless.chart_chart__state_in chart_chart__CHART_A_IDL_unless.chart_chart__restart_act chart_chart__CHART_A_IDL_unless.chart_chart__state_act)
164
))
165
166
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until
167
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_1 Int)
168
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.x Int)
169
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_1 Int)
170
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_1 Int)
171
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.chart_chart__restart_in Bool)
172
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.chart_chart__state_in chart_chart__type)
173
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_out Int)
174
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_out Int)
175
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_out Int)
176
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 Bool)
177
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_10 Int)
178
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_11 Int)
179
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_12 Int)
180
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 Bool)
181
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_3 Int)
182
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_4 Int)
183
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_5 Int)
184
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_6 Int)
185
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_7 Int)
186
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_8 Int)
187
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_9 Int)
188
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart Int)
189
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_2 Int)
190
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_3 Int)
191
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_4 Int)
192
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_5 Int)
193
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y Int)
194
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_2 Int)
195
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_3 Int)
196
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_4 Int)
197
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_5 Int)
198
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_6 Int)
199
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_7 Int)
200
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z Int)
201
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_2 Int)
202
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_3 Int)
203
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_4 Int)
204
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_5 Int)
205
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until (Int Int Int Int Bool chart_chart__type Int Int Int))
206
(rule (=> 
207
  (and (Chart_A__To__Chart_ChartJunction1149_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_1
208
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_1
209
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_5
210
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_4)
211
       (Chart_ChartJunction1149__To__Chart_C_2_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_5
212
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_4
213
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_6
214
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_7)
215
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 (< chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.x 2))
216
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
217
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_7))
218
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
219
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_4))
220
       )
221
       (Chart_A__To__Chart_ChartJunction1149_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_1
222
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_1
223
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_2
224
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_2)
225
       (Chart_ChartJunction1149__To__Chart_B_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_2
226
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_2
227
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_11
228
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_12)
229
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 (>= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.x 2))
230
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 false))
231
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_2)
232
                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
233
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_5))
234
                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
235
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_4))
236
                    )
237
                    ))
238
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 true))
239
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_12)
240
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_3)
241
                    ))
242
       )
243
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z)
244
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
245
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_6))
246
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
247
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_5))
248
       )
249
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_6
250
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_1
251
                   false
252
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_4
253
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_5)
254
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
255
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_4))
256
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
257
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_6))
258
       )
259
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 true))
260
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_11))
261
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 false))
262
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_2))
263
       )
264
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_3
265
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_1
266
                   false
267
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_9
268
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_10)
269
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 false))
270
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_3)
271
                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
272
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_7))
273
                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
274
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_5))
275
                    )
276
                    ))
277
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 true))
278
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_9)
279
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_4)
280
                    ))
281
       )
282
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y)
283
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
284
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_5))
285
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
286
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_1))
287
       )
288
       (Chart_C_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_4
289
                   false
290
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_3)
291
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
292
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_3))
293
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
294
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_4))
295
       )
296
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 true))
297
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_10))
298
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 false))
299
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_1))
300
       )
301
       (Chart_B_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_2
302
                   false
303
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_8)
304
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 false))
305
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_2)
306
                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 true))
307
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_5))
308
                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_2 false))
309
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_1))
310
                    )
311
                    ))
312
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_1 true))
313
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until_8)
314
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_3)
315
                    ))
316
       )
317
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart)
318
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.chart_chart__state_in POINTChart_Chart)
319
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.chart_chart__restart_in true)
320
       )
321
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.x chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until.z_out)
322
))
323
324
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless
325
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__restart_in Bool)
326
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__state_in chart_chart__type)
327
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__restart_act Bool)
328
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__state_act chart_chart__type)
329
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless (Bool chart_chart__type Bool chart_chart__type))
330
(rule (=> 
331
  (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__state_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__state_in)
332
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__restart_in)
333
       )
334
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless.chart_chart__state_act)
335
))
336
337
; chart_chart__CHART_B_IDL_handler_until
338
(declare-var chart_chart__CHART_B_IDL_handler_until.idChart_Chart_1 Int)
339
(declare-var chart_chart__CHART_B_IDL_handler_until.y_1 Int)
340
(declare-var chart_chart__CHART_B_IDL_handler_until.z_1 Int)
341
(declare-var chart_chart__CHART_B_IDL_handler_until.chart_chart__restart_in Bool)
342
(declare-var chart_chart__CHART_B_IDL_handler_until.chart_chart__state_in chart_chart__type)
343
(declare-var chart_chart__CHART_B_IDL_handler_until.idChart_Chart_out Int)
344
(declare-var chart_chart__CHART_B_IDL_handler_until.y_out Int)
345
(declare-var chart_chart__CHART_B_IDL_handler_until.z_out Int)
346
(declare-rel chart_chart__CHART_B_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
347
(rule (=> 
348
  (and (= chart_chart__CHART_B_IDL_handler_until.z_out chart_chart__CHART_B_IDL_handler_until.z_1)
349
       (= chart_chart__CHART_B_IDL_handler_until.y_out chart_chart__CHART_B_IDL_handler_until.y_1)
350
       (= chart_chart__CHART_B_IDL_handler_until.idChart_Chart_out chart_chart__CHART_B_IDL_handler_until.idChart_Chart_1)
351
       (= chart_chart__CHART_B_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
352
       (= chart_chart__CHART_B_IDL_handler_until.chart_chart__restart_in true)
353
       )
354
  (chart_chart__CHART_B_IDL_handler_until chart_chart__CHART_B_IDL_handler_until.idChart_Chart_1 chart_chart__CHART_B_IDL_handler_until.y_1 chart_chart__CHART_B_IDL_handler_until.z_1 chart_chart__CHART_B_IDL_handler_until.chart_chart__restart_in chart_chart__CHART_B_IDL_handler_until.chart_chart__state_in chart_chart__CHART_B_IDL_handler_until.idChart_Chart_out chart_chart__CHART_B_IDL_handler_until.y_out chart_chart__CHART_B_IDL_handler_until.z_out)
355
))
356
357
; chart_chart__CHART_B_IDL_unless
358
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__restart_in Bool)
359
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__state_in chart_chart__type)
360
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__restart_act Bool)
361
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__state_act chart_chart__type)
362
(declare-rel chart_chart__CHART_B_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
363
(rule (=> 
364
  (and (= chart_chart__CHART_B_IDL_unless.chart_chart__state_act chart_chart__CHART_B_IDL_unless.chart_chart__state_in)
365
       (= chart_chart__CHART_B_IDL_unless.chart_chart__restart_act chart_chart__CHART_B_IDL_unless.chart_chart__restart_in)
366
       )
367
  (chart_chart__CHART_B_IDL_unless chart_chart__CHART_B_IDL_unless.chart_chart__restart_in chart_chart__CHART_B_IDL_unless.chart_chart__state_in chart_chart__CHART_B_IDL_unless.chart_chart__restart_act chart_chart__CHART_B_IDL_unless.chart_chart__state_act)
368
))
369
370
; chart_chart__CHART_B__TO__CHART_A_1_handler_until
371
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
372
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_1 Int)
373
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_1 Int)
374
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
375
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
376
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
377
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_out Int)
378
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_out Int)
379
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
380
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_3 Int)
381
(declare-rel chart_chart__CHART_B__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
382
(rule (=> 
383
  (and (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_out chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_1)
384
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_1)
385
       (Chart_B_ex chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_1
386
                   false
387
                   chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2)
388
       (Chart_A_en chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2
389
                   false
390
                   chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_3)
391
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_3)
392
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
393
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
394
       )
395
  (chart_chart__CHART_B__TO__CHART_A_1_handler_until chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_1 chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_1 chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_1 chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__restart_in chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_out)
396
))
397
398
; chart_chart__CHART_B__TO__CHART_A_1_unless
399
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
400
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
401
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
402
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
403
(declare-rel chart_chart__CHART_B__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
404
(rule (=> 
405
  (and (= chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_in)
406
       (= chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_in)
407
       )
408
  (chart_chart__CHART_B__TO__CHART_A_1_unless chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_in chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_act)
409
))
410
411
; chart_chart__CHART_C_IDL_handler_until
412
(declare-var chart_chart__CHART_C_IDL_handler_until.idChart_Chart_1 Int)
413
(declare-var chart_chart__CHART_C_IDL_handler_until.y_1 Int)
414
(declare-var chart_chart__CHART_C_IDL_handler_until.z_1 Int)
415
(declare-var chart_chart__CHART_C_IDL_handler_until.chart_chart__restart_in Bool)
416
(declare-var chart_chart__CHART_C_IDL_handler_until.chart_chart__state_in chart_chart__type)
417
(declare-var chart_chart__CHART_C_IDL_handler_until.idChart_Chart_out Int)
418
(declare-var chart_chart__CHART_C_IDL_handler_until.y_out Int)
419
(declare-var chart_chart__CHART_C_IDL_handler_until.z_out Int)
420
(declare-rel chart_chart__CHART_C_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
421
(rule (=> 
422
  (and (= chart_chart__CHART_C_IDL_handler_until.z_out chart_chart__CHART_C_IDL_handler_until.z_1)
423
       (= chart_chart__CHART_C_IDL_handler_until.y_out chart_chart__CHART_C_IDL_handler_until.y_1)
424
       (= chart_chart__CHART_C_IDL_handler_until.idChart_Chart_out chart_chart__CHART_C_IDL_handler_until.idChart_Chart_1)
425
       (= chart_chart__CHART_C_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
426
       (= chart_chart__CHART_C_IDL_handler_until.chart_chart__restart_in true)
427
       )
428
  (chart_chart__CHART_C_IDL_handler_until chart_chart__CHART_C_IDL_handler_until.idChart_Chart_1 chart_chart__CHART_C_IDL_handler_until.y_1 chart_chart__CHART_C_IDL_handler_until.z_1 chart_chart__CHART_C_IDL_handler_until.chart_chart__restart_in chart_chart__CHART_C_IDL_handler_until.chart_chart__state_in chart_chart__CHART_C_IDL_handler_until.idChart_Chart_out chart_chart__CHART_C_IDL_handler_until.y_out chart_chart__CHART_C_IDL_handler_until.z_out)
429
))
430
431
; chart_chart__CHART_C_IDL_unless
432
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__restart_in Bool)
433
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__state_in chart_chart__type)
434
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__restart_act Bool)
435
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__state_act chart_chart__type)
436
(declare-rel chart_chart__CHART_C_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
437
(rule (=> 
438
  (and (= chart_chart__CHART_C_IDL_unless.chart_chart__state_act chart_chart__CHART_C_IDL_unless.chart_chart__state_in)
439
       (= chart_chart__CHART_C_IDL_unless.chart_chart__restart_act chart_chart__CHART_C_IDL_unless.chart_chart__restart_in)
440
       )
441
  (chart_chart__CHART_C_IDL_unless chart_chart__CHART_C_IDL_unless.chart_chart__restart_in chart_chart__CHART_C_IDL_unless.chart_chart__state_in chart_chart__CHART_C_IDL_unless.chart_chart__restart_act chart_chart__CHART_C_IDL_unless.chart_chart__state_act)
442
))
443
444
; chart_chart__CHART_C__TO__CHART_A_1_handler_until
445
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
446
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_1 Int)
447
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_1 Int)
448
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
449
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
450
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
451
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_out Int)
452
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_out Int)
453
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
454
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_3 Int)
455
(declare-rel chart_chart__CHART_C__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
456
(rule (=> 
457
  (and (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_out chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_1)
458
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_1)
459
       (Chart_C_ex chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_1
460
                   false
461
                   chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2)
462
       (Chart_A_en chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2
463
                   false
464
                   chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_3)
465
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_3)
466
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
467
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
468
       )
469
  (chart_chart__CHART_C__TO__CHART_A_1_handler_until chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_1 chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_1 chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_1 chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__restart_in chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_out)
470
))
471
472
; chart_chart__CHART_C__TO__CHART_A_1_unless
473
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
474
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
475
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
476
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
477
(declare-rel chart_chart__CHART_C__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
478
(rule (=> 
479
  (and (= chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_in)
480
       (= chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_in)
481
       )
482
  (chart_chart__CHART_C__TO__CHART_A_1_unless chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_in chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_act)
483
))
484
485
; chart_chart__POINTChart_Chart_handler_until
486
(declare-var chart_chart__POINTChart_Chart_handler_until.idChart_Chart_1 Int)
487
(declare-var chart_chart__POINTChart_Chart_handler_until.y_1 Int)
488
(declare-var chart_chart__POINTChart_Chart_handler_until.z_1 Int)
489
(declare-var chart_chart__POINTChart_Chart_handler_until.chart_chart__restart_in Bool)
490
(declare-var chart_chart__POINTChart_Chart_handler_until.chart_chart__state_in chart_chart__type)
491
(declare-var chart_chart__POINTChart_Chart_handler_until.idChart_Chart_out Int)
492
(declare-var chart_chart__POINTChart_Chart_handler_until.y_out Int)
493
(declare-var chart_chart__POINTChart_Chart_handler_until.z_out Int)
494
(declare-rel chart_chart__POINTChart_Chart_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
495
(rule (=> 
496
  (and (= chart_chart__POINTChart_Chart_handler_until.z_out chart_chart__POINTChart_Chart_handler_until.z_1)
497
       (= chart_chart__POINTChart_Chart_handler_until.y_out chart_chart__POINTChart_Chart_handler_until.y_1)
498
       (= chart_chart__POINTChart_Chart_handler_until.idChart_Chart_out chart_chart__POINTChart_Chart_handler_until.idChart_Chart_1)
499
       (= chart_chart__POINTChart_Chart_handler_until.chart_chart__state_in POINTChart_Chart)
500
       (= chart_chart__POINTChart_Chart_handler_until.chart_chart__restart_in false)
501
       )
502
  (chart_chart__POINTChart_Chart_handler_until chart_chart__POINTChart_Chart_handler_until.idChart_Chart_1 chart_chart__POINTChart_Chart_handler_until.y_1 chart_chart__POINTChart_Chart_handler_until.z_1 chart_chart__POINTChart_Chart_handler_until.chart_chart__restart_in chart_chart__POINTChart_Chart_handler_until.chart_chart__state_in chart_chart__POINTChart_Chart_handler_until.idChart_Chart_out chart_chart__POINTChart_Chart_handler_until.y_out chart_chart__POINTChart_Chart_handler_until.z_out)
503
))
504
505
; chart_chart__POINTChart_Chart_unless
506
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__restart_in Bool)
507
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__state_in chart_chart__type)
508
(declare-var chart_chart__POINTChart_Chart_unless.idChart_Chart_1 Int)
509
(declare-var chart_chart__POINTChart_Chart_unless.E1 Bool)
510
(declare-var chart_chart__POINTChart_Chart_unless.x Int)
511
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__restart_act Bool)
512
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__state_act chart_chart__type)
513
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 Bool)
514
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 Bool)
515
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 Bool)
516
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 Bool)
517
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 Bool)
518
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 Bool)
519
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 Bool)
520
(declare-rel chart_chart__POINTChart_Chart_unless (Bool chart_chart__type Int Bool Int Bool chart_chart__type))
521
(rule (=> 
522
  (and (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1144))
523
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1143))
524
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1142))
525
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1144) (> chart_chart__POINTChart_Chart_unless.x 3)))
526
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1143) (> chart_chart__POINTChart_Chart_unless.x 3)))
527
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 (and (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1142) chart_chart__POINTChart_Chart_unless.E1) (> chart_chart__POINTChart_Chart_unless.x 0)))
528
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 0))
529
       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 false))
530
               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 false))
531
                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 false))
532
                               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 false))
533
                                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 false))
534
                                               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 false))
535
                                                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 false))
536
                                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act chart_chart__POINTChart_Chart_unless.chart_chart__state_in)
537
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act chart_chart__POINTChart_Chart_unless.chart_chart__restart_in)
538
                                                                    ))
539
                                                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 true))
540
                                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_B_IDL)
541
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
542
                                                                    ))
543
                                                       ))
544
                                                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 true))
545
                                                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_C_IDL)
546
                                                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
547
                                                            ))
548
                                               ))
549
                                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 true))
550
                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_A_IDL)
551
                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
552
                                                    ))
553
                                       ))
554
                                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 true))
555
                                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_B__TO__CHART_A_1)
556
                                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
557
                                            ))
558
                               ))
559
                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 true))
560
                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_C__TO__CHART_A_1)
561
                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
562
                                    ))
563
                       ))
564
                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 true))
565
                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1149_1)
566
                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
567
                            ))
568
               ))
569
            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 true))
570
               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act POINT__TO__CHART_A_1)
571
                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
572
                    ))
573
       )
574
       )
575
  (chart_chart__POINTChart_Chart_unless chart_chart__POINTChart_Chart_unless.chart_chart__restart_in chart_chart__POINTChart_Chart_unless.chart_chart__state_in chart_chart__POINTChart_Chart_unless.idChart_Chart_1 chart_chart__POINTChart_Chart_unless.E1 chart_chart__POINTChart_Chart_unless.x chart_chart__POINTChart_Chart_unless.chart_chart__restart_act chart_chart__POINTChart_Chart_unless.chart_chart__state_act)
576
))
577
578
; chart_chart__POINT__TO__CHART_A_1_handler_until
579
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
580
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.y_1 Int)
581
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.z_1 Int)
582
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
583
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
584
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
585
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.y_out Int)
586
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.z_out Int)
587
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
588
(declare-rel chart_chart__POINT__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
589
(rule (=> 
590
  (and (= chart_chart__POINT__TO__CHART_A_1_handler_until.z_out chart_chart__POINT__TO__CHART_A_1_handler_until.z_1)
591
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.y_out chart_chart__POINT__TO__CHART_A_1_handler_until.y_1)
592
       (Chart_A_en chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_1
593
                   false
594
                   chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2)
595
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2)
596
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
597
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
598
       )
599
  (chart_chart__POINT__TO__CHART_A_1_handler_until chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_1 chart_chart__POINT__TO__CHART_A_1_handler_until.y_1 chart_chart__POINT__TO__CHART_A_1_handler_until.z_1 chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__restart_in chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__POINT__TO__CHART_A_1_handler_until.y_out chart_chart__POINT__TO__CHART_A_1_handler_until.z_out)
600
))
601
602
; chart_chart__POINT__TO__CHART_A_1_unless
603
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
604
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
605
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
606
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
607
(declare-rel chart_chart__POINT__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
608
(rule (=> 
609
  (and (= chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_in)
610
       (= chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_in)
611
       )
612
  (chart_chart__POINT__TO__CHART_A_1_unless chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_in chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_act)
613
))
614
615
; Chart_Chart_node
616
(declare-var Chart_Chart_node.idChart_Chart_1 Int)
617
(declare-var Chart_Chart_node.E1 Bool)
618
(declare-var Chart_Chart_node.x Int)
619
(declare-var Chart_Chart_node.y_1 Int)
620
(declare-var Chart_Chart_node.z_1 Int)
621
(declare-var Chart_Chart_node.idChart_Chart Int)
622
(declare-var Chart_Chart_node.y Int)
623
(declare-var Chart_Chart_node.z Int)
624
(declare-var Chart_Chart_node.__Chart_Chart_node_58_c Bool)
625
(declare-var Chart_Chart_node.__Chart_Chart_node_59_c chart_chart__type)
626
(declare-var Chart_Chart_node.ni_4._arrow._first_c Bool)
627
(declare-var Chart_Chart_node.__Chart_Chart_node_58_m Bool)
628
(declare-var Chart_Chart_node.__Chart_Chart_node_59_m chart_chart__type)
629
(declare-var Chart_Chart_node.ni_4._arrow._first_m Bool)
630
(declare-var Chart_Chart_node.__Chart_Chart_node_58_x Bool)
631
(declare-var Chart_Chart_node.__Chart_Chart_node_59_x chart_chart__type)
632
(declare-var Chart_Chart_node.ni_4._arrow._first_x Bool)
633
(declare-var Chart_Chart_node.__Chart_Chart_node_1 Bool)
634
(declare-var Chart_Chart_node.__Chart_Chart_node_10 chart_chart__type)
635
(declare-var Chart_Chart_node.__Chart_Chart_node_11 Bool)
636
(declare-var Chart_Chart_node.__Chart_Chart_node_12 chart_chart__type)
637
(declare-var Chart_Chart_node.__Chart_Chart_node_13 Bool)
638
(declare-var Chart_Chart_node.__Chart_Chart_node_14 chart_chart__type)
639
(declare-var Chart_Chart_node.__Chart_Chart_node_15 Bool)
640
(declare-var Chart_Chart_node.__Chart_Chart_node_16 chart_chart__type)
641
(declare-var Chart_Chart_node.__Chart_Chart_node_17 Bool)
642
(declare-var Chart_Chart_node.__Chart_Chart_node_18 chart_chart__type)
643
(declare-var Chart_Chart_node.__Chart_Chart_node_19 Int)
644
(declare-var Chart_Chart_node.__Chart_Chart_node_2 chart_chart__type)
645
(declare-var Chart_Chart_node.__Chart_Chart_node_20 Int)
646
(declare-var Chart_Chart_node.__Chart_Chart_node_21 Int)
647
(declare-var Chart_Chart_node.__Chart_Chart_node_22 Bool)
648
(declare-var Chart_Chart_node.__Chart_Chart_node_23 chart_chart__type)
649
(declare-var Chart_Chart_node.__Chart_Chart_node_24 Int)
650
(declare-var Chart_Chart_node.__Chart_Chart_node_25 Int)
651
(declare-var Chart_Chart_node.__Chart_Chart_node_26 Int)
652
(declare-var Chart_Chart_node.__Chart_Chart_node_27 Bool)
653
(declare-var Chart_Chart_node.__Chart_Chart_node_28 chart_chart__type)
654
(declare-var Chart_Chart_node.__Chart_Chart_node_29 Int)
655
(declare-var Chart_Chart_node.__Chart_Chart_node_3 Bool)
656
(declare-var Chart_Chart_node.__Chart_Chart_node_30 Int)
657
(declare-var Chart_Chart_node.__Chart_Chart_node_31 Int)
658
(declare-var Chart_Chart_node.__Chart_Chart_node_32 Bool)
659
(declare-var Chart_Chart_node.__Chart_Chart_node_33 chart_chart__type)
660
(declare-var Chart_Chart_node.__Chart_Chart_node_34 Int)
661
(declare-var Chart_Chart_node.__Chart_Chart_node_35 Int)
662
(declare-var Chart_Chart_node.__Chart_Chart_node_36 Int)
663
(declare-var Chart_Chart_node.__Chart_Chart_node_37 Bool)
664
(declare-var Chart_Chart_node.__Chart_Chart_node_38 chart_chart__type)
665
(declare-var Chart_Chart_node.__Chart_Chart_node_39 Int)
666
(declare-var Chart_Chart_node.__Chart_Chart_node_4 chart_chart__type)
667
(declare-var Chart_Chart_node.__Chart_Chart_node_40 Int)
668
(declare-var Chart_Chart_node.__Chart_Chart_node_41 Int)
669
(declare-var Chart_Chart_node.__Chart_Chart_node_42 Bool)
670
(declare-var Chart_Chart_node.__Chart_Chart_node_43 chart_chart__type)
671
(declare-var Chart_Chart_node.__Chart_Chart_node_44 Int)
672
(declare-var Chart_Chart_node.__Chart_Chart_node_45 Int)
673
(declare-var Chart_Chart_node.__Chart_Chart_node_46 Int)
674
(declare-var Chart_Chart_node.__Chart_Chart_node_47 Bool)
675
(declare-var Chart_Chart_node.__Chart_Chart_node_48 chart_chart__type)
676
(declare-var Chart_Chart_node.__Chart_Chart_node_49 Int)
677
(declare-var Chart_Chart_node.__Chart_Chart_node_5 Bool)
678
(declare-var Chart_Chart_node.__Chart_Chart_node_50 Int)
679
(declare-var Chart_Chart_node.__Chart_Chart_node_51 Int)
680
(declare-var Chart_Chart_node.__Chart_Chart_node_52 Bool)
681
(declare-var Chart_Chart_node.__Chart_Chart_node_53 chart_chart__type)
682
(declare-var Chart_Chart_node.__Chart_Chart_node_54 Int)
683
(declare-var Chart_Chart_node.__Chart_Chart_node_55 Int)
684
(declare-var Chart_Chart_node.__Chart_Chart_node_56 Int)
685
(declare-var Chart_Chart_node.__Chart_Chart_node_57 Bool)
686
(declare-var Chart_Chart_node.__Chart_Chart_node_6 chart_chart__type)
687
(declare-var Chart_Chart_node.__Chart_Chart_node_7 Bool)
688
(declare-var Chart_Chart_node.__Chart_Chart_node_8 chart_chart__type)
689
(declare-var Chart_Chart_node.__Chart_Chart_node_9 Bool)
690
(declare-var Chart_Chart_node.chart_chart__next_restart_in Bool)
691
(declare-var Chart_Chart_node.chart_chart__next_state_in chart_chart__type)
692
(declare-var Chart_Chart_node.chart_chart__restart_act Bool)
693
(declare-var Chart_Chart_node.chart_chart__restart_in Bool)
694
(declare-var Chart_Chart_node.chart_chart__state_act chart_chart__type)
695
(declare-var Chart_Chart_node.chart_chart__state_in chart_chart__type)
696
(declare-rel Chart_Chart_node_reset (Bool chart_chart__type Bool Bool chart_chart__type Bool))
697
(declare-rel Chart_Chart_node_step (Int Bool Int Int Int Int Int Int Bool chart_chart__type Bool Bool chart_chart__type Bool))
698
699
(rule (=> 
700
  (and 
701
       (= Chart_Chart_node.__Chart_Chart_node_58_m Chart_Chart_node.__Chart_Chart_node_58_c)
702
       (= Chart_Chart_node.__Chart_Chart_node_59_m Chart_Chart_node.__Chart_Chart_node_59_c)
703
       (= Chart_Chart_node.ni_4._arrow._first_m true)
704
  )
705
  (Chart_Chart_node_reset Chart_Chart_node.__Chart_Chart_node_58_c
706
                          Chart_Chart_node.__Chart_Chart_node_59_c
707
                          Chart_Chart_node.ni_4._arrow._first_c
708
                          Chart_Chart_node.__Chart_Chart_node_58_m
709
                          Chart_Chart_node.__Chart_Chart_node_59_m
710
                          Chart_Chart_node.ni_4._arrow._first_m)
711
))
712
713
(rule (=> 
714
  (and (= Chart_Chart_node.ni_4._arrow._first_m Chart_Chart_node.ni_4._arrow._first_c)
715
       (and (= Chart_Chart_node.__Chart_Chart_node_57 (ite Chart_Chart_node.ni_4._arrow._first_m true false))
716
            (= Chart_Chart_node.ni_4._arrow._first_x false))
717
       (and (or (not (= Chart_Chart_node.__Chart_Chart_node_57 false))
718
               (and (= Chart_Chart_node.chart_chart__state_in Chart_Chart_node.__Chart_Chart_node_59_c)
719
                    (= Chart_Chart_node.chart_chart__restart_in Chart_Chart_node.__Chart_Chart_node_58_c)
720
                    ))
721
            (or (not (= Chart_Chart_node.__Chart_Chart_node_57 true))
722
               (and (= Chart_Chart_node.chart_chart__state_in POINTChart_Chart)
723
                    (= Chart_Chart_node.chart_chart__restart_in false)
724
                    ))
725
       )
726
       (and (or (not (= Chart_Chart_node.chart_chart__state_in CHART_A_IDL))
727
               (and (chart_chart__CHART_A_IDL_unless Chart_Chart_node.chart_chart__restart_in
728
                                                     Chart_Chart_node.chart_chart__state_in
729
                                                     Chart_Chart_node.__Chart_Chart_node_5
730
                                                     Chart_Chart_node.__Chart_Chart_node_6)
731
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_6)
732
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_5)
733
                    ))
734
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_A__TO__CHART_CHARTJUNCTION1149_1))
735
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_unless 
736
                    Chart_Chart_node.chart_chart__restart_in
737
                    Chart_Chart_node.chart_chart__state_in
738
                    Chart_Chart_node.__Chart_Chart_node_11
739
                    Chart_Chart_node.__Chart_Chart_node_12)
740
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_12)
741
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_11)
742
                    ))
743
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_B_IDL))
744
               (and (chart_chart__CHART_B_IDL_unless Chart_Chart_node.chart_chart__restart_in
745
                                                     Chart_Chart_node.chart_chart__state_in
746
                                                     Chart_Chart_node.__Chart_Chart_node_1
747
                                                     Chart_Chart_node.__Chart_Chart_node_2)
748
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_2)
749
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_1)
750
                    ))
751
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_B__TO__CHART_A_1))
752
               (and (chart_chart__CHART_B__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
753
                                                                Chart_Chart_node.chart_chart__state_in
754
                                                                Chart_Chart_node.__Chart_Chart_node_7
755
                                                                Chart_Chart_node.__Chart_Chart_node_8)
756
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_8)
757
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_7)
758
                    ))
759
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_C_IDL))
760
               (and (chart_chart__CHART_C_IDL_unless Chart_Chart_node.chart_chart__restart_in
761
                                                     Chart_Chart_node.chart_chart__state_in
762
                                                     Chart_Chart_node.__Chart_Chart_node_3
763
                                                     Chart_Chart_node.__Chart_Chart_node_4)
764
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_4)
765
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_3)
766
                    ))
767
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_C__TO__CHART_A_1))
768
               (and (chart_chart__CHART_C__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
769
                                                                Chart_Chart_node.chart_chart__state_in
770
                                                                Chart_Chart_node.__Chart_Chart_node_9
771
                                                                Chart_Chart_node.__Chart_Chart_node_10)
772
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_10)
773
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_9)
774
                    ))
775
            (or (not (= Chart_Chart_node.chart_chart__state_in POINTChart_Chart))
776
               (and (chart_chart__POINTChart_Chart_unless Chart_Chart_node.chart_chart__restart_in
777
                                                          Chart_Chart_node.chart_chart__state_in
778
                                                          Chart_Chart_node.idChart_Chart_1
779
                                                          Chart_Chart_node.E1
780
                                                          Chart_Chart_node.x
781
                                                          Chart_Chart_node.__Chart_Chart_node_15
782
                                                          Chart_Chart_node.__Chart_Chart_node_16)
783
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_16)
784
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_15)
785
                    ))
786
            (or (not (= Chart_Chart_node.chart_chart__state_in POINT__TO__CHART_A_1))
787
               (and (chart_chart__POINT__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
788
                                                              Chart_Chart_node.chart_chart__state_in
789
                                                              Chart_Chart_node.__Chart_Chart_node_13
790
                                                              Chart_Chart_node.__Chart_Chart_node_14)
791
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_14)
792
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_13)
793
                    ))
794
       )
795
       (and (or (not (= Chart_Chart_node.chart_chart__state_act CHART_A_IDL))
796
               (and (chart_chart__CHART_A_IDL_handler_until Chart_Chart_node.idChart_Chart_1
797
                                                            Chart_Chart_node.y_1
798
                                                            Chart_Chart_node.z_1
799
                                                            Chart_Chart_node.__Chart_Chart_node_27
800
                                                            Chart_Chart_node.__Chart_Chart_node_28
801
                                                            Chart_Chart_node.__Chart_Chart_node_29
802
                                                            Chart_Chart_node.__Chart_Chart_node_30
803
                                                            Chart_Chart_node.__Chart_Chart_node_31)
804
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_31)
805
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_30)
806
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_29)
807
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_28)
808
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_27)
809
                    ))
810
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1149_1))
811
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1149_1_handler_until 
812
                    Chart_Chart_node.idChart_Chart_1
813
                    Chart_Chart_node.x
814
                    Chart_Chart_node.y_1
815
                    Chart_Chart_node.z_1
816
                    Chart_Chart_node.__Chart_Chart_node_42
817
                    Chart_Chart_node.__Chart_Chart_node_43
818
                    Chart_Chart_node.__Chart_Chart_node_44
819
                    Chart_Chart_node.__Chart_Chart_node_45
820
                    Chart_Chart_node.__Chart_Chart_node_46)
821
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_46)
822
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_45)
823
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_44)
824
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_43)
825
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_42)
826
                    ))
827
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_B_IDL))
828
               (and (chart_chart__CHART_B_IDL_handler_until Chart_Chart_node.idChart_Chart_1
829
                                                            Chart_Chart_node.y_1
830
                                                            Chart_Chart_node.z_1
831
                                                            Chart_Chart_node.__Chart_Chart_node_17
832
                                                            Chart_Chart_node.__Chart_Chart_node_18
833
                                                            Chart_Chart_node.__Chart_Chart_node_19
834
                                                            Chart_Chart_node.__Chart_Chart_node_20
835
                                                            Chart_Chart_node.__Chart_Chart_node_21)
836
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_21)
837
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_20)
838
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_19)
839
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_18)
840
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_17)
841
                    ))
842
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_B__TO__CHART_A_1))
843
               (and (chart_chart__CHART_B__TO__CHART_A_1_handler_until 
844
                    Chart_Chart_node.idChart_Chart_1
845
                    Chart_Chart_node.y_1
846
                    Chart_Chart_node.z_1
847
                    Chart_Chart_node.__Chart_Chart_node_32
848
                    Chart_Chart_node.__Chart_Chart_node_33
849
                    Chart_Chart_node.__Chart_Chart_node_34
850
                    Chart_Chart_node.__Chart_Chart_node_35
851
                    Chart_Chart_node.__Chart_Chart_node_36)
852
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_36)
853
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_35)
854
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_34)
855
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_33)
856
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_32)
857
                    ))
858
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_C_IDL))
859
               (and (chart_chart__CHART_C_IDL_handler_until Chart_Chart_node.idChart_Chart_1
860
                                                            Chart_Chart_node.y_1
861
                                                            Chart_Chart_node.z_1
862
                                                            Chart_Chart_node.__Chart_Chart_node_22
863
                                                            Chart_Chart_node.__Chart_Chart_node_23
864
                                                            Chart_Chart_node.__Chart_Chart_node_24
865
                                                            Chart_Chart_node.__Chart_Chart_node_25
866
                                                            Chart_Chart_node.__Chart_Chart_node_26)
867
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_26)
868
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_25)
869
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_24)
870
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_23)
871
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_22)
872
                    ))
873
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_C__TO__CHART_A_1))
874
               (and (chart_chart__CHART_C__TO__CHART_A_1_handler_until 
875
                    Chart_Chart_node.idChart_Chart_1
876
                    Chart_Chart_node.y_1
877
                    Chart_Chart_node.z_1
878
                    Chart_Chart_node.__Chart_Chart_node_37
879
                    Chart_Chart_node.__Chart_Chart_node_38
880
                    Chart_Chart_node.__Chart_Chart_node_39
881
                    Chart_Chart_node.__Chart_Chart_node_40
882
                    Chart_Chart_node.__Chart_Chart_node_41)
883
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_41)
884
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_40)
885
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_39)
886
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_38)
887
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_37)
888
                    ))
889
            (or (not (= Chart_Chart_node.chart_chart__state_act POINTChart_Chart))
890
               (and (chart_chart__POINTChart_Chart_handler_until Chart_Chart_node.idChart_Chart_1
891
                                                                 Chart_Chart_node.y_1
892
                                                                 Chart_Chart_node.z_1
893
                                                                 Chart_Chart_node.__Chart_Chart_node_52
894
                                                                 Chart_Chart_node.__Chart_Chart_node_53
895
                                                                 Chart_Chart_node.__Chart_Chart_node_54
896
                                                                 Chart_Chart_node.__Chart_Chart_node_55
897
                                                                 Chart_Chart_node.__Chart_Chart_node_56)
898
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_56)
899
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_55)
900
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_54)
901
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_53)
902
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_52)
903
                    ))
904
            (or (not (= Chart_Chart_node.chart_chart__state_act POINT__TO__CHART_A_1))
905
               (and (chart_chart__POINT__TO__CHART_A_1_handler_until 
906
                    Chart_Chart_node.idChart_Chart_1
907
                    Chart_Chart_node.y_1
908
                    Chart_Chart_node.z_1
909
                    Chart_Chart_node.__Chart_Chart_node_47
910
                    Chart_Chart_node.__Chart_Chart_node_48
911
                    Chart_Chart_node.__Chart_Chart_node_49
912
                    Chart_Chart_node.__Chart_Chart_node_50
913
                    Chart_Chart_node.__Chart_Chart_node_51)
914
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_51)
915
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_50)
916
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_49)
917
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_48)
918
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_47)
919
                    ))
920
       )
921
       (= Chart_Chart_node.__Chart_Chart_node_59_x Chart_Chart_node.chart_chart__next_state_in)
922
       (= Chart_Chart_node.__Chart_Chart_node_58_x Chart_Chart_node.chart_chart__next_restart_in)
923
       )
924
  (Chart_Chart_node_step Chart_Chart_node.idChart_Chart_1
925
                         Chart_Chart_node.E1
926
                         Chart_Chart_node.x
927
                         Chart_Chart_node.y_1
928
                         Chart_Chart_node.z_1
929
                         Chart_Chart_node.idChart_Chart
930
                         Chart_Chart_node.y
931
                         Chart_Chart_node.z
932
                         Chart_Chart_node.__Chart_Chart_node_58_c
933
                         Chart_Chart_node.__Chart_Chart_node_59_c
934
                         Chart_Chart_node.ni_4._arrow._first_c
935
                         Chart_Chart_node.__Chart_Chart_node_58_x
936
                         Chart_Chart_node.__Chart_Chart_node_59_x
937
                         Chart_Chart_node.ni_4._arrow._first_x)
938
))
939
940
; Junctions1_Chart
941
(declare-var Junctions1_Chart.x Int)
942
(declare-var Junctions1_Chart.E1 Bool)
943
(declare-var Junctions1_Chart.y Int)
944
(declare-var Junctions1_Chart.z Int)
945
(declare-var Junctions1_Chart.__Junctions1_Chart_5_c Int)
946
(declare-var Junctions1_Chart.__Junctions1_Chart_6_c Int)
947
(declare-var Junctions1_Chart.__Junctions1_Chart_7_c Int)
948
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c Bool)
949
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c chart_chart__type)
950
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c Bool)
951
(declare-var Junctions1_Chart.ni_3._arrow._first_c Bool)
952
(declare-var Junctions1_Chart.__Junctions1_Chart_5_m Int)
953
(declare-var Junctions1_Chart.__Junctions1_Chart_6_m Int)
954
(declare-var Junctions1_Chart.__Junctions1_Chart_7_m Int)
955
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Bool)
956
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m chart_chart__type)
957
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Bool)
958
(declare-var Junctions1_Chart.ni_3._arrow._first_m Bool)
959
(declare-var Junctions1_Chart.__Junctions1_Chart_5_x Int)
960
(declare-var Junctions1_Chart.__Junctions1_Chart_6_x Int)
961
(declare-var Junctions1_Chart.__Junctions1_Chart_7_x Int)
962
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x Bool)
963
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x chart_chart__type)
964
(declare-var Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x Bool)
965
(declare-var Junctions1_Chart.ni_3._arrow._first_x Bool)
966
(declare-var Junctions1_Chart.__Junctions1_Chart_1 Int)
967
(declare-var Junctions1_Chart.__Junctions1_Chart_2 Int)
968
(declare-var Junctions1_Chart.__Junctions1_Chart_3 Int)
969
(declare-var Junctions1_Chart.__Junctions1_Chart_4 Bool)
970
(declare-var Junctions1_Chart.idChart_Chart Int)
971
(declare-var Junctions1_Chart.idChart_Chart_1 Int)
972
(declare-var Junctions1_Chart.y_1 Int)
973
(declare-var Junctions1_Chart.z_1 Int)
974
(declare-rel Junctions1_Chart_reset (Int Int Int Bool chart_chart__type Bool Bool Int Int Int Bool chart_chart__type Bool Bool))
975
(declare-rel Junctions1_Chart_step (Int Bool Int Int Int Int Int Bool chart_chart__type Bool Bool Int Int Int Bool chart_chart__type Bool Bool))
976
977
(rule (=> 
978
  (and 
979
       (= Junctions1_Chart.__Junctions1_Chart_5_m Junctions1_Chart.__Junctions1_Chart_5_c)
980
       (= Junctions1_Chart.__Junctions1_Chart_6_m Junctions1_Chart.__Junctions1_Chart_6_c)
981
       (= Junctions1_Chart.__Junctions1_Chart_7_m Junctions1_Chart.__Junctions1_Chart_7_c)
982
       (= Junctions1_Chart.ni_3._arrow._first_m true)
983
       (Chart_Chart_node_reset Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
984
                               Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
985
                               Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
986
                               Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
987
                               Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
988
                               Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m)
989
  )
990
  (Junctions1_Chart_reset Junctions1_Chart.__Junctions1_Chart_5_c
991
                          Junctions1_Chart.__Junctions1_Chart_6_c
992
                          Junctions1_Chart.__Junctions1_Chart_7_c
993
                          Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
994
                          Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
995
                          Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
996
                          Junctions1_Chart.ni_3._arrow._first_c
997
                          Junctions1_Chart.__Junctions1_Chart_5_m
998
                          Junctions1_Chart.__Junctions1_Chart_6_m
999
                          Junctions1_Chart.__Junctions1_Chart_7_m
1000
                          Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1001
                          Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1002
                          Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1003
                          Junctions1_Chart.ni_3._arrow._first_m)
1004
))
1005
1006
(rule (=> 
1007
  (and (= Junctions1_Chart.ni_3._arrow._first_m Junctions1_Chart.ni_3._arrow._first_c)
1008
       (and (= Junctions1_Chart.__Junctions1_Chart_4 (ite Junctions1_Chart.ni_3._arrow._first_m true false))
1009
            (= Junctions1_Chart.ni_3._arrow._first_x false))
1010
       (and (or (not (= Junctions1_Chart.__Junctions1_Chart_4 false))
1011
               (and (= Junctions1_Chart.z_1 Junctions1_Chart.__Junctions1_Chart_6_c)
1012
                    (= Junctions1_Chart.y_1 Junctions1_Chart.__Junctions1_Chart_7_c)
1013
                    (= Junctions1_Chart.idChart_Chart_1 Junctions1_Chart.__Junctions1_Chart_5_c)
1014
                    ))
1015
            (or (not (= Junctions1_Chart.__Junctions1_Chart_4 true))
1016
               (and (= Junctions1_Chart.z_1 2)
1017
                    (= Junctions1_Chart.y_1 1)
1018
                    (= Junctions1_Chart.idChart_Chart_1 0)
1019
                    ))
1020
       )
1021
       (and (= Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c)
1022
            (= Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c)
1023
            (= Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c)
1024
            )
1025
       (Chart_Chart_node_step Junctions1_Chart.idChart_Chart_1
1026
                              Junctions1_Chart.E1
1027
                              Junctions1_Chart.x
1028
                              Junctions1_Chart.y_1
1029
                              Junctions1_Chart.z_1
1030
                              Junctions1_Chart.__Junctions1_Chart_1
1031
                              Junctions1_Chart.__Junctions1_Chart_2
1032
                              Junctions1_Chart.__Junctions1_Chart_3
1033
                              Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1034
                              Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1035
                              Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1036
                              Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1037
                              Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1038
                              Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x)
1039
       (and (or (not (= Junctions1_Chart.E1 false))
1040
               (and (= Junctions1_Chart.z Junctions1_Chart.z_1)
1041
                    (= Junctions1_Chart.y Junctions1_Chart.y_1)
1042
                    (= Junctions1_Chart.idChart_Chart Junctions1_Chart.idChart_Chart_1)
1043
                    ))
1044
            (or (not (= Junctions1_Chart.E1 true))
1045
               (and (= Junctions1_Chart.z Junctions1_Chart.__Junctions1_Chart_3)
1046
                    (= Junctions1_Chart.y Junctions1_Chart.__Junctions1_Chart_2)
1047
                    (= Junctions1_Chart.idChart_Chart Junctions1_Chart.__Junctions1_Chart_1)
1048
                    ))
1049
       )
1050
       (= Junctions1_Chart.__Junctions1_Chart_7_x Junctions1_Chart.y)
1051
       (= Junctions1_Chart.__Junctions1_Chart_6_x Junctions1_Chart.z)
1052
       (= Junctions1_Chart.__Junctions1_Chart_5_x Junctions1_Chart.idChart_Chart)
1053
       )
1054
  (Junctions1_Chart_step Junctions1_Chart.x
1055
                         Junctions1_Chart.E1
1056
                         Junctions1_Chart.y
1057
                         Junctions1_Chart.z
1058
                         Junctions1_Chart.__Junctions1_Chart_5_c
1059
                         Junctions1_Chart.__Junctions1_Chart_6_c
1060
                         Junctions1_Chart.__Junctions1_Chart_7_c
1061
                         Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1062
                         Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1063
                         Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1064
                         Junctions1_Chart.ni_3._arrow._first_c
1065
                         Junctions1_Chart.__Junctions1_Chart_5_x
1066
                         Junctions1_Chart.__Junctions1_Chart_6_x
1067
                         Junctions1_Chart.__Junctions1_Chart_7_x
1068
                         Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1069
                         Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1070
                         Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1071
                         Junctions1_Chart.ni_3._arrow._first_x)
1072
))
1073
1074
; Junctions1
1075
(declare-var Junctions1.x_1_1 Int)
1076
(declare-var Junctions1.E1_1_1 Real)
1077
(declare-var Junctions1.y_1_1 Int)
1078
(declare-var Junctions1.z_2_1 Int)
1079
(declare-var Junctions1.__Junctions1_2_c Real)
1080
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_c Int)
1081
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_c Int)
1082
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_c Int)
1083
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c Bool)
1084
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c chart_chart__type)
1085
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c Bool)
1086
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_c Bool)
1087
(declare-var Junctions1.ni_1._arrow._first_c Bool)
1088
(declare-var Junctions1.__Junctions1_2_m Real)
1089
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_m Int)
1090
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_m Int)
1091
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_m Int)
1092
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Bool)
1093
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m chart_chart__type)
1094
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Bool)
1095
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_m Bool)
1096
(declare-var Junctions1.ni_1._arrow._first_m Bool)
1097
(declare-var Junctions1.__Junctions1_2_x Real)
1098
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_x Int)
1099
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_x Int)
1100
(declare-var Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_x Int)
1101
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x Bool)
1102
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x chart_chart__type)
1103
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x Bool)
1104
(declare-var Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_x Bool)
1105
(declare-var Junctions1.ni_1._arrow._first_x Bool)
1106
(declare-var Junctions1.ChartE1_1_1_event Bool)
1107
(declare-var Junctions1.Chart_1_1 Int)
1108
(declare-var Junctions1.Chart_2_1 Int)
1109
(declare-var Junctions1.__Junctions1_1 Bool)
1110
(declare-var Junctions1.i_virtual_local Real)
1111
(declare-rel Junctions1_reset (Real Int Int Int Bool chart_chart__type Bool Bool Bool Real Int Int Int Bool chart_chart__type Bool Bool Bool))
1112
(declare-rel Junctions1_step (Int Real Int Int Real Int Int Int Bool chart_chart__type Bool Bool Bool Real Int Int Int Bool chart_chart__type Bool Bool Bool))
1113
1114
(rule (=> 
1115
  (and 
1116
       (= Junctions1.__Junctions1_2_m Junctions1.__Junctions1_2_c)
1117
       (= Junctions1.ni_1._arrow._first_m true)
1118
       (Junctions1_Chart_reset Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_c
1119
                               Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_c
1120
                               Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_c
1121
                               Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1122
                               Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1123
                               Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1124
                               Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_c
1125
                               Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_m
1126
                               Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_m
1127
                               Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_m
1128
                               Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1129
                               Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1130
                               Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1131
                               Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_m)
1132
  )
1133
  (Junctions1_reset Junctions1.__Junctions1_2_c
1134
                    Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_c
1135
                    Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_c
1136
                    Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_c
1137
                    Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1138
                    Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1139
                    Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1140
                    Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_c
1141
                    Junctions1.ni_1._arrow._first_c
1142
                    Junctions1.__Junctions1_2_m
1143
                    Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_m
1144
                    Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_m
1145
                    Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_m
1146
                    Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1147
                    Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1148
                    Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1149
                    Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_m
1150
                    Junctions1.ni_1._arrow._first_m)
1151
))
1152
1153
(rule (=> 
1154
  (and (= Junctions1.ni_1._arrow._first_m Junctions1.ni_1._arrow._first_c)
1155
       (and (= Junctions1.__Junctions1_1 (ite Junctions1.ni_1._arrow._first_m true false))
1156
            (= Junctions1.ni_1._arrow._first_x false))
1157
       (and (or (not (= Junctions1.__Junctions1_1 true))
1158
               (= Junctions1.ChartE1_1_1_event false))
1159
            (or (not (= Junctions1.__Junctions1_1 false))
1160
               (= Junctions1.ChartE1_1_1_event (or (and (> Junctions1.__Junctions1_2_c 0.) (<= Junctions1.E1_1_1 0.)) (and (<= Junctions1.__Junctions1_2_c 0.) (> Junctions1.E1_1_1 0.)))))
1161
       )
1162
       (and (= Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_m Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_c)
1163
            (= Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_m Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_c)
1164
            (= Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_m Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_c)
1165
            (= Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c)
1166
            (= Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c)
1167
            (= Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c)
1168
            (= Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_m Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_c)
1169
            )
1170
       (Junctions1_Chart_step Junctions1.x_1_1
1171
                              Junctions1.ChartE1_1_1_event
1172
                              Junctions1.Chart_1_1
1173
                              Junctions1.Chart_2_1
1174
                              Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_m
1175
                              Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_m
1176
                              Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_m
1177
                              Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1178
                              Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1179
                              Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1180
                              Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_m
1181
                              Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_x
1182
                              Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_x
1183
                              Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_x
1184
                              Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1185
                              Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1186
                              Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1187
                              Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_x)
1188
       (= Junctions1.z_2_1 Junctions1.Chart_2_1)
1189
       (= Junctions1.y_1_1 Junctions1.Chart_1_1)
1190
       (and (or (not (= Junctions1.__Junctions1_1 true))
1191
               (= Junctions1.i_virtual_local 0.))
1192
            (or (not (= Junctions1.__Junctions1_1 false))
1193
               (= Junctions1.i_virtual_local 1.))
1194
       )
1195
       (= Junctions1.__Junctions1_2_x Junctions1.E1_1_1)
1196
       )
1197
  (Junctions1_step Junctions1.x_1_1
1198
                   Junctions1.E1_1_1
1199
                   Junctions1.y_1_1
1200
                   Junctions1.z_2_1
1201
                   Junctions1.__Junctions1_2_c
1202
                   Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_c
1203
                   Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_c
1204
                   Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_c
1205
                   Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1206
                   Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1207
                   Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1208
                   Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_c
1209
                   Junctions1.ni_1._arrow._first_c
1210
                   Junctions1.__Junctions1_2_x
1211
                   Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_5_x
1212
                   Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_6_x
1213
                   Junctions1.ni_0.Junctions1_Chart.__Junctions1_Chart_7_x
1214
                   Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1215
                   Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1216
                   Junctions1.ni_0.Junctions1_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1217
                   Junctions1.ni_0.Junctions1_Chart.ni_3._arrow._first_x
1218
                   Junctions1.ni_1._arrow._first_x)
1219
))