Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions1False / Junctions1False.smt2 @ eb639349

History | View | Annotate | Download (146 KB)

1
(declare-datatypes () ((chart_chart__type POINTChart_Chart POINT__TO__CHART_A_1 CHART_A__TO__CHART_CHARTJUNCTION1168_1 CHART_A__TO__CHART_CHARTJUNCTION1167_2 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_ex
4
(declare-var Chart_A_ex.y_1 Int)
5
(declare-var Chart_A_ex.idChart_Chart_1 Int)
6
(declare-var Chart_A_ex.isInner Bool)
7
(declare-var Chart_A_ex.y Int)
8
(declare-var Chart_A_ex.idChart_Chart Int)
9
(declare-var Chart_A_ex.__Chart_A_ex_1 Bool)
10
(declare-var Chart_A_ex.idChart_Chart_2 Int)
11
(declare-var Chart_A_ex.y_2 Int)
12
(declare-rel Chart_A_ex (Int Int Bool Int Int))
13
(rule (=> 
14
  (and (= Chart_A_ex.__Chart_A_ex_1 (not Chart_A_ex.isInner))
15
       (and (or (not (= Chart_A_ex.__Chart_A_ex_1 false))
16
               (and (= Chart_A_ex.y_2 Chart_A_ex.y_1)
17
                    (= Chart_A_ex.idChart_Chart_2 Chart_A_ex.idChart_Chart_1)
18
                    ))
19
            (or (not (= Chart_A_ex.__Chart_A_ex_1 true))
20
               (and (= Chart_A_ex.y_2 (* Chart_A_ex.y_1 2))
21
                    (= Chart_A_ex.idChart_Chart_2 0)
22
                    ))
23
       )
24
       (= Chart_A_ex.y Chart_A_ex.y_2)
25
       (= Chart_A_ex.idChart_Chart Chart_A_ex.idChart_Chart_1)
26
       )
27
  (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)
28
))
29

    
30
; Chart_C_en
31
(declare-var Chart_C_en.idChart_Chart_1 Int)
32
(declare-var Chart_C_en.isInner Bool)
33
(declare-var Chart_C_en.idChart_Chart Int)
34
(declare-rel Chart_C_en (Int Bool Int))
35
(rule (=> 
36
  (= Chart_C_en.idChart_Chart 1161)
37
  (Chart_C_en Chart_C_en.idChart_Chart_1 Chart_C_en.isInner Chart_C_en.idChart_Chart)
38
))
39

    
40
; Chart_ChartJunction1167__To__Chart_C_1_Transition_Action
41
(declare-var Chart_ChartJunction1167__To__Chart_C_1_Transition_Action.z_1 Int)
42
(declare-var Chart_ChartJunction1167__To__Chart_C_1_Transition_Action.z Int)
43
(declare-rel Chart_ChartJunction1167__To__Chart_C_1_Transition_Action (Int Int))
44
(rule (=> 
45
  (= Chart_ChartJunction1167__To__Chart_C_1_Transition_Action.z (+ Chart_ChartJunction1167__To__Chart_C_1_Transition_Action.z_1 1))
46
  (Chart_ChartJunction1167__To__Chart_C_1_Transition_Action Chart_ChartJunction1167__To__Chart_C_1_Transition_Action.z_1 Chart_ChartJunction1167__To__Chart_C_1_Transition_Action.z)
47
))
48

    
49
; Chart_A__To__Chart_ChartJunction1168_1_Condition_Action
50
(declare-var Chart_A__To__Chart_ChartJunction1168_1_Condition_Action.y_1 Int)
51
(declare-var Chart_A__To__Chart_ChartJunction1168_1_Condition_Action.y Int)
52
(declare-rel Chart_A__To__Chart_ChartJunction1168_1_Condition_Action (Int Int))
53
(rule (=> 
54
  (= Chart_A__To__Chart_ChartJunction1168_1_Condition_Action.y (+ Chart_A__To__Chart_ChartJunction1168_1_Condition_Action.y_1 1))
55
  (Chart_A__To__Chart_ChartJunction1168_1_Condition_Action Chart_A__To__Chart_ChartJunction1168_1_Condition_Action.y_1 Chart_A__To__Chart_ChartJunction1168_1_Condition_Action.y)
56
))
57

    
58
; Chart_A__To__Chart_ChartJunction1168_1_Transition_Action
59
(declare-var Chart_A__To__Chart_ChartJunction1168_1_Transition_Action.z_1 Int)
60
(declare-var Chart_A__To__Chart_ChartJunction1168_1_Transition_Action.z Int)
61
(declare-rel Chart_A__To__Chart_ChartJunction1168_1_Transition_Action (Int Int))
62
(rule (=> 
63
  (= Chart_A__To__Chart_ChartJunction1168_1_Transition_Action.z (+ Chart_A__To__Chart_ChartJunction1168_1_Transition_Action.z_1 2))
64
  (Chart_A__To__Chart_ChartJunction1168_1_Transition_Action Chart_A__To__Chart_ChartJunction1168_1_Transition_Action.z_1 Chart_A__To__Chart_ChartJunction1168_1_Transition_Action.z)
65
))
66

    
67
; Chart_B_en
68
(declare-var Chart_B_en.idChart_Chart_1 Int)
69
(declare-var Chart_B_en.isInner Bool)
70
(declare-var Chart_B_en.idChart_Chart Int)
71
(declare-rel Chart_B_en (Int Bool Int))
72
(rule (=> 
73
  (= Chart_B_en.idChart_Chart 1162)
74
  (Chart_B_en Chart_B_en.idChart_Chart_1 Chart_B_en.isInner Chart_B_en.idChart_Chart)
75
))
76

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

    
86
; Chart_ChartJunction1168__To__Chart_B_1_Transition_Action
87
(declare-var Chart_ChartJunction1168__To__Chart_B_1_Transition_Action.z_1 Int)
88
(declare-var Chart_ChartJunction1168__To__Chart_B_1_Transition_Action.z Int)
89
(declare-rel Chart_ChartJunction1168__To__Chart_B_1_Transition_Action (Int Int))
90
(rule (=> 
91
  (= Chart_ChartJunction1168__To__Chart_B_1_Transition_Action.z (+ Chart_ChartJunction1168__To__Chart_B_1_Transition_Action.z_1 1))
92
  (Chart_ChartJunction1168__To__Chart_B_1_Transition_Action Chart_ChartJunction1168__To__Chart_B_1_Transition_Action.z_1 Chart_ChartJunction1168__To__Chart_B_1_Transition_Action.z)
93
))
94

    
95
; Chart_ChartJunction1168__To__Chart_C_3_Condition_Action
96
(declare-var Chart_ChartJunction1168__To__Chart_C_3_Condition_Action.y_1 Int)
97
(declare-var Chart_ChartJunction1168__To__Chart_C_3_Condition_Action.y Int)
98
(declare-rel Chart_ChartJunction1168__To__Chart_C_3_Condition_Action (Int Int))
99
(rule (=> 
100
  (= Chart_ChartJunction1168__To__Chart_C_3_Condition_Action.y (+ Chart_ChartJunction1168__To__Chart_C_3_Condition_Action.y_1 1))
101
  (Chart_ChartJunction1168__To__Chart_C_3_Condition_Action Chart_ChartJunction1168__To__Chart_C_3_Condition_Action.y_1 Chart_ChartJunction1168__To__Chart_C_3_Condition_Action.y)
102
))
103

    
104
; Chart_ChartJunction1168__To__Chart_C_3_Transition_Action
105
(declare-var Chart_ChartJunction1168__To__Chart_C_3_Transition_Action.z_1 Int)
106
(declare-var Chart_ChartJunction1168__To__Chart_C_3_Transition_Action.z Int)
107
(declare-rel Chart_ChartJunction1168__To__Chart_C_3_Transition_Action (Int Int))
108
(rule (=> 
109
  (= Chart_ChartJunction1168__To__Chart_C_3_Transition_Action.z (+ Chart_ChartJunction1168__To__Chart_C_3_Transition_Action.z_1 1))
110
  (Chart_ChartJunction1168__To__Chart_C_3_Transition_Action Chart_ChartJunction1168__To__Chart_C_3_Transition_Action.z_1 Chart_ChartJunction1168__To__Chart_C_3_Transition_Action.z)
111
))
112

    
113
; Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action
114
(declare-var Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action.y_1 Int)
115
(declare-var Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action.y Int)
116
(declare-rel Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action (Int Int))
117
(rule (=> 
118
  (= Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action.y (+ Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action.y_1 1))
119
  (Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action.y_1 Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action.y)
120
))
121

    
122
; Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action
123
(declare-var Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action.z_1 Int)
124
(declare-var Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action.z Int)
125
(declare-rel Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action (Int Int))
126
(rule (=> 
127
  (= Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action.z (+ Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action.z_1 1))
128
  (Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action.z_1 Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action.z)
129
))
130

    
131
; Chart_ChartJunction1169__To__Chart_B_1_Condition_Action
132
(declare-var Chart_ChartJunction1169__To__Chart_B_1_Condition_Action.y_1 Int)
133
(declare-var Chart_ChartJunction1169__To__Chart_B_1_Condition_Action.y Int)
134
(declare-rel Chart_ChartJunction1169__To__Chart_B_1_Condition_Action (Int Int))
135
(rule (=> 
136
  (= Chart_ChartJunction1169__To__Chart_B_1_Condition_Action.y (+ Chart_ChartJunction1169__To__Chart_B_1_Condition_Action.y_1 2))
137
  (Chart_ChartJunction1169__To__Chart_B_1_Condition_Action Chart_ChartJunction1169__To__Chart_B_1_Condition_Action.y_1 Chart_ChartJunction1169__To__Chart_B_1_Condition_Action.y)
138
))
139

    
140
; Chart_ChartJunction1169__To__Chart_B_1_Transition_Action
141
(declare-var Chart_ChartJunction1169__To__Chart_B_1_Transition_Action.z_1 Int)
142
(declare-var Chart_ChartJunction1169__To__Chart_B_1_Transition_Action.z Int)
143
(declare-rel Chart_ChartJunction1169__To__Chart_B_1_Transition_Action (Int Int))
144
(rule (=> 
145
  (= Chart_ChartJunction1169__To__Chart_B_1_Transition_Action.z (+ Chart_ChartJunction1169__To__Chart_B_1_Transition_Action.z_1 1))
146
  (Chart_ChartJunction1169__To__Chart_B_1_Transition_Action Chart_ChartJunction1169__To__Chart_B_1_Transition_Action.z_1 Chart_ChartJunction1169__To__Chart_B_1_Transition_Action.z)
147
))
148

    
149
; Chart_ChartJunction1169__To__Chart_C_2_Condition_Action
150
(declare-var Chart_ChartJunction1169__To__Chart_C_2_Condition_Action.y_1 Int)
151
(declare-var Chart_ChartJunction1169__To__Chart_C_2_Condition_Action.y Int)
152
(declare-rel Chart_ChartJunction1169__To__Chart_C_2_Condition_Action (Int Int))
153
(rule (=> 
154
  (= Chart_ChartJunction1169__To__Chart_C_2_Condition_Action.y (+ Chart_ChartJunction1169__To__Chart_C_2_Condition_Action.y_1 1))
155
  (Chart_ChartJunction1169__To__Chart_C_2_Condition_Action Chart_ChartJunction1169__To__Chart_C_2_Condition_Action.y_1 Chart_ChartJunction1169__To__Chart_C_2_Condition_Action.y)
156
))
157

    
158
; Chart_A_en
159
(declare-var Chart_A_en.idChart_Chart_1 Int)
160
(declare-var Chart_A_en.isInner Bool)
161
(declare-var Chart_A_en.idChart_Chart Int)
162
(declare-rel Chart_A_en (Int Bool Int))
163
(rule (=> 
164
  (= Chart_A_en.idChart_Chart 1160)
165
  (Chart_A_en Chart_A_en.idChart_Chart_1 Chart_A_en.isInner Chart_A_en.idChart_Chart)
166
))
167

    
168
; Chart_B_ex
169
(declare-var Chart_B_ex.idChart_Chart_1 Int)
170
(declare-var Chart_B_ex.isInner Bool)
171
(declare-var Chart_B_ex.idChart_Chart Int)
172
(declare-var Chart_B_ex.idChart_Chart_2 Int)
173
(declare-rel Chart_B_ex (Int Bool Int))
174
(rule (=> 
175
  (and (and (or (not (= (not Chart_B_ex.isInner) true))
176
               (= Chart_B_ex.idChart_Chart_2 0))
177
            (or (not (= (not Chart_B_ex.isInner) false))
178
               (= Chart_B_ex.idChart_Chart_2 Chart_B_ex.idChart_Chart_1))
179
       )
180
       (= Chart_B_ex.idChart_Chart Chart_B_ex.idChart_Chart_1)
181
       )
182
  (Chart_B_ex Chart_B_ex.idChart_Chart_1 Chart_B_ex.isInner Chart_B_ex.idChart_Chart)
183
))
184

    
185
; Chart_C_ex
186
(declare-var Chart_C_ex.idChart_Chart_1 Int)
187
(declare-var Chart_C_ex.isInner Bool)
188
(declare-var Chart_C_ex.idChart_Chart Int)
189
(declare-var Chart_C_ex.idChart_Chart_2 Int)
190
(declare-rel Chart_C_ex (Int Bool Int))
191
(rule (=> 
192
  (and (and (or (not (= (not Chart_C_ex.isInner) true))
193
               (= Chart_C_ex.idChart_Chart_2 0))
194
            (or (not (= (not Chart_C_ex.isInner) false))
195
               (= Chart_C_ex.idChart_Chart_2 Chart_C_ex.idChart_Chart_1))
196
       )
197
       (= Chart_C_ex.idChart_Chart Chart_C_ex.idChart_Chart_1)
198
       )
199
  (Chart_C_ex Chart_C_ex.idChart_Chart_1 Chart_C_ex.isInner Chart_C_ex.idChart_Chart)
200
))
201

    
202
; chart_chart__CHART_A_IDL_handler_until
203
(declare-var chart_chart__CHART_A_IDL_handler_until.idChart_Chart_1 Int)
204
(declare-var chart_chart__CHART_A_IDL_handler_until.y_1 Int)
205
(declare-var chart_chart__CHART_A_IDL_handler_until.z_1 Int)
206
(declare-var chart_chart__CHART_A_IDL_handler_until.chart_chart__restart_in Bool)
207
(declare-var chart_chart__CHART_A_IDL_handler_until.chart_chart__state_in chart_chart__type)
208
(declare-var chart_chart__CHART_A_IDL_handler_until.idChart_Chart_out Int)
209
(declare-var chart_chart__CHART_A_IDL_handler_until.y_out Int)
210
(declare-var chart_chart__CHART_A_IDL_handler_until.z_out Int)
211
(declare-rel chart_chart__CHART_A_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
212
(rule (=> 
213
  (and (= chart_chart__CHART_A_IDL_handler_until.z_out chart_chart__CHART_A_IDL_handler_until.z_1)
214
       (= chart_chart__CHART_A_IDL_handler_until.y_out chart_chart__CHART_A_IDL_handler_until.y_1)
215
       (= chart_chart__CHART_A_IDL_handler_until.idChart_Chart_out chart_chart__CHART_A_IDL_handler_until.idChart_Chart_1)
216
       (= chart_chart__CHART_A_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
217
       (= chart_chart__CHART_A_IDL_handler_until.chart_chart__restart_in true)
218
       )
219
  (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)
220
))
221

    
222
; chart_chart__CHART_A_IDL_unless
223
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__restart_in Bool)
224
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__state_in chart_chart__type)
225
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__restart_act Bool)
226
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__state_act chart_chart__type)
227
(declare-rel chart_chart__CHART_A_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
228
(rule (=> 
229
  (and (= chart_chart__CHART_A_IDL_unless.chart_chart__state_act chart_chart__CHART_A_IDL_unless.chart_chart__state_in)
230
       (= chart_chart__CHART_A_IDL_unless.chart_chart__restart_act chart_chart__CHART_A_IDL_unless.chart_chart__restart_in)
231
       )
232
  (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)
233
))
234

    
235
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until
236
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_1 Int)
237
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.x Int)
238
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_1 Int)
239
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_1 Int)
240
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.chart_chart__restart_in Bool)
241
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.chart_chart__state_in chart_chart__type)
242
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_out Int)
243
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_out Int)
244
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_out Int)
245
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 Bool)
246
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_2 Int)
247
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_3 Int)
248
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_4 Int)
249
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_5 Int)
250
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart Int)
251
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_2 Int)
252
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_3 Int)
253
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y Int)
254
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_2 Int)
255
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z Int)
256
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_2 Int)
257
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until (Int Int Int Int Bool chart_chart__type Int Int Int))
258
(rule (=> 
259
  (and (Chart_ChartJunction1167__To__Chart_C_1_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_1
260
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_3)
261
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.x 2))
262
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 false))
263
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_1)
264
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_1)
265
                    ))
266
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 true))
267
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_3)
268
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_2)
269
                    ))
270
       )
271
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z)
272
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_1
273
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_1
274
                   false
275
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_4
276
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_5)
277
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 false))
278
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_1)
279
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_1)
280
                    ))
281
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 true))
282
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_4)
283
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_2)
284
                    ))
285
       )
286
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y)
287
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 true))
288
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_5))
289
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 false))
290
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_1))
291
       )
292
       (Chart_C_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_2
293
                   false
294
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_2)
295
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 false))
296
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_2)
297
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_1)
298
                    ))
299
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_1 true))
300
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until_2)
301
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_3)
302
                    ))
303
       )
304
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart)
305
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.chart_chart__state_in POINTChart_Chart)
306
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.chart_chart__restart_in true)
307
       )
308
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.x chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until.z_out)
309
))
310

    
311
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless
312
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__restart_in Bool)
313
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__state_in chart_chart__type)
314
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__restart_act Bool)
315
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__state_act chart_chart__type)
316
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless (Bool chart_chart__type Bool chart_chart__type))
317
(rule (=> 
318
  (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__state_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__state_in)
319
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__restart_in)
320
       )
321
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless.chart_chart__state_act)
322
))
323

    
324
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until
325
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1 Int)
326
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.x Int)
327
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_1 Int)
328
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1 Int)
329
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.chart_chart__restart_in Bool)
330
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.chart_chart__state_in chart_chart__type)
331
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_out Int)
332
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_out Int)
333
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_out Int)
334
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 Bool)
335
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_10 Int)
336
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_11 Int)
337
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_12 Int)
338
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_13 Int)
339
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_14 Int)
340
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_15 Int)
341
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_16 Int)
342
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_17 Int)
343
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_18 Int)
344
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_19 Int)
345
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 Bool)
346
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_20 Int)
347
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_21 Int)
348
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_22 Int)
349
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_23 Int)
350
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_24 Int)
351
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_25 Int)
352
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_26 Int)
353
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_27 Int)
354
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_28 Int)
355
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_29 Int)
356
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 Bool)
357
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 Bool)
358
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 Bool)
359
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_6 Int)
360
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_7 Int)
361
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_8 Int)
362
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_9 Int)
363
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart Int)
364
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_2 Int)
365
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_3 Int)
366
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_4 Int)
367
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_5 Int)
368
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_6 Int)
369
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_7 Int)
370
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_8 Int)
371
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_9 Int)
372
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y Int)
373
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_10 Int)
374
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_11 Int)
375
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_12 Int)
376
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_13 Int)
377
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_14 Int)
378
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_15 Int)
379
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_2 Int)
380
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_3 Int)
381
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_4 Int)
382
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_5 Int)
383
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_6 Int)
384
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_7 Int)
385
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_8 Int)
386
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_9 Int)
387
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z Int)
388
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_10 Int)
389
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_2 Int)
390
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_3 Int)
391
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_4 Int)
392
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_5 Int)
393
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_6 Int)
394
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_7 Int)
395
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_8 Int)
396
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_9 Int)
397
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until (Int Int Int Int Bool chart_chart__type Int Int Int))
398
(rule (=> 
399
  (and (Chart_A__To__Chart_ChartJunction1168_1_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1
400
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_8)
401
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 (< chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.x 2))
402
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
403
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_9 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_8))
404
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
405
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_9 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1))
406
       )
407
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 (> chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.x 2))
408
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
409
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_8))
410
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
411
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1))
412
       )
413
       (Chart_ChartJunction1168__To__Chart_B_1_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_2
414
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_26)
415
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
416
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_26))
417
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
418
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_2))
419
       )
420
       (Chart_A__To__Chart_ChartJunction1168_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_1
421
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_5)
422
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.x 2))
423
       (Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action 
424
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_5
425
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_24)
426
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 true))
427
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_24))
428
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 false))
429
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_5))
430
       )
431
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.x 2) (> chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_3)))
432
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
433
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_8))
434
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
435
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1))
436
       )
437
       (Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action 
438
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_4
439
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_20)
440
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
441
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_20))
442
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
443
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_4))
444
       )
445
       (Chart_ChartJunction1169__To__Chart_B_1_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_5
446
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_19)
447
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
448
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_19))
449
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
450
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_5))
451
       )
452
       (Chart_A__To__Chart_ChartJunction1168_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_1
453
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_9)
454
       (Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Condition_Action 
455
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_9
456
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_17)
457
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 true))
458
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_10 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_17))
459
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 false))
460
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_10 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_9))
461
       )
462
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.x 2) (<= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_10 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_6)))
463
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
464
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_8))
465
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
466
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1))
467
       )
468
       (Chart_ChartJunction1168__To__Chart_ChartJunction1169_2_Transition_Action 
469
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_7
470
       chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_13)
471
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
472
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_8 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_13))
473
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
474
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_8 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_7))
475
       )
476
       (Chart_ChartJunction1168__To__Chart_C_3_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_9
477
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_7)
478
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
479
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_10 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_7))
480
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
481
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_10 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_9))
482
       )
483
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
484
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_3))
485
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
486
               (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
487
                       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_6))
488
                    (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
489
                       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
490
                               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_8))
491
                            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
492
                               (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 true))
493
                                       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1))
494
                                    (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 false))
495
                                       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
496
                                               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_10))
497
                                            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
498
                                               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1))
499
                                       ))
500
                               ))
501
                       ))
502
               ))
503
       )
504
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z)
505
       (Chart_ChartJunction1169__To__Chart_B_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_6
506
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_23)
507
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
508
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_23))
509
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
510
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_6))
511
       )
512
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_7
513
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1
514
                   false
515
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_21
516
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_22)
517
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
518
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_8 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_21))
519
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
520
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_8 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_7))
521
       )
522
       (Chart_A__To__Chart_ChartJunction1168_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_1
523
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_2)
524
       (Chart_ChartJunction1168__To__Chart_B_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_2
525
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_29)
526
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
527
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_29))
528
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
529
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_2))
530
       )
531
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_3
532
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1
533
                   false
534
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_27
535
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_28)
536
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
537
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_27))
538
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
539
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_3))
540
       )
541
       (Chart_A__To__Chart_ChartJunction1168_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_1
542
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_13)
543
       (Chart_ChartJunction1168__To__Chart_C_3_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_13
544
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_11)
545
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
546
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_14 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_11))
547
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
548
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_14 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_13))
549
       )
550
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_14
551
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1
552
                   false
553
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_9
554
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_10)
555
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
556
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_15 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_9))
557
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
558
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_15 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_14))
559
       )
560
       (Chart_ChartJunction1169__To__Chart_C_2_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_10
561
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_16)
562
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
563
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_11 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_16))
564
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
565
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_11 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_10))
566
       )
567
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_11
568
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1
569
                   false
570
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_14
571
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_15)
572
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
573
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_12 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_14))
574
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
575
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_12 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_11))
576
       )
577
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
578
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_4))
579
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
580
               (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
581
                       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_8))
582
                    (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
583
                       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
584
                               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_12))
585
                            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
586
                               (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 true))
587
                                       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_10))
588
                                    (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 false))
589
                                       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
590
                                               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_15))
591
                                            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
592
                                               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_13))
593
                                       ))
594
                               ))
595
                       ))
596
               ))
597
       )
598
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y)
599
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
600
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_8 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_10))
601
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
602
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_8 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1))
603
       )
604
       (Chart_C_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_8
605
                   false
606
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_6)
607
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
608
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_9 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_6))
609
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
610
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_9 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_8))
611
       )
612
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
613
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_15))
614
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
615
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_6 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1))
616
       )
617
       (Chart_C_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_6
618
                   false
619
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_12)
620
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
621
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_12))
622
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
623
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_7 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_6))
624
       )
625
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
626
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_22))
627
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
628
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1))
629
       )
630
       (Chart_B_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_4
631
                   false
632
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_18)
633
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
634
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_18))
635
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
636
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_4))
637
       )
638
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
639
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_28))
640
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
641
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1))
642
       )
643
       (Chart_B_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_2
644
                   false
645
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_25)
646
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 false))
647
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_2)
648
                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 true))
649
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_5))
650
                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_2 false))
651
                            (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 true))
652
                                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_7))
653
                                 (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_3 false))
654
                                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 true))
655
                                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1))
656
                                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_4 false))
657
                                            (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 true))
658
                                                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_9))
659
                                                 (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_5 false))
660
                                                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1))
661
                                            ))
662
                                    ))
663
                            ))
664
                    )
665
                    ))
666
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_1 true))
667
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until_25)
668
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_3)
669
                    ))
670
       )
671
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart)
672
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.chart_chart__state_in POINTChart_Chart)
673
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.chart_chart__restart_in true)
674
       )
675
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.x chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until.z_out)
676
))
677

    
678
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless
679
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__restart_in Bool)
680
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__state_in chart_chart__type)
681
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__restart_act Bool)
682
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__state_act chart_chart__type)
683
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless (Bool chart_chart__type Bool chart_chart__type))
684
(rule (=> 
685
  (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__state_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__state_in)
686
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__restart_in)
687
       )
688
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless.chart_chart__state_act)
689
))
690

    
691
; chart_chart__CHART_B_IDL_handler_until
692
(declare-var chart_chart__CHART_B_IDL_handler_until.idChart_Chart_1 Int)
693
(declare-var chart_chart__CHART_B_IDL_handler_until.y_1 Int)
694
(declare-var chart_chart__CHART_B_IDL_handler_until.z_1 Int)
695
(declare-var chart_chart__CHART_B_IDL_handler_until.chart_chart__restart_in Bool)
696
(declare-var chart_chart__CHART_B_IDL_handler_until.chart_chart__state_in chart_chart__type)
697
(declare-var chart_chart__CHART_B_IDL_handler_until.idChart_Chart_out Int)
698
(declare-var chart_chart__CHART_B_IDL_handler_until.y_out Int)
699
(declare-var chart_chart__CHART_B_IDL_handler_until.z_out Int)
700
(declare-rel chart_chart__CHART_B_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
701
(rule (=> 
702
  (and (= chart_chart__CHART_B_IDL_handler_until.z_out chart_chart__CHART_B_IDL_handler_until.z_1)
703
       (= chart_chart__CHART_B_IDL_handler_until.y_out chart_chart__CHART_B_IDL_handler_until.y_1)
704
       (= chart_chart__CHART_B_IDL_handler_until.idChart_Chart_out chart_chart__CHART_B_IDL_handler_until.idChart_Chart_1)
705
       (= chart_chart__CHART_B_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
706
       (= chart_chart__CHART_B_IDL_handler_until.chart_chart__restart_in true)
707
       )
708
  (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)
709
))
710

    
711
; chart_chart__CHART_B_IDL_unless
712
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__restart_in Bool)
713
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__state_in chart_chart__type)
714
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__restart_act Bool)
715
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__state_act chart_chart__type)
716
(declare-rel chart_chart__CHART_B_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
717
(rule (=> 
718
  (and (= chart_chart__CHART_B_IDL_unless.chart_chart__state_act chart_chart__CHART_B_IDL_unless.chart_chart__state_in)
719
       (= chart_chart__CHART_B_IDL_unless.chart_chart__restart_act chart_chart__CHART_B_IDL_unless.chart_chart__restart_in)
720
       )
721
  (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)
722
))
723

    
724
; chart_chart__CHART_B__TO__CHART_A_1_handler_until
725
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
726
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_1 Int)
727
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_1 Int)
728
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
729
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
730
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
731
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_out Int)
732
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_out Int)
733
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
734
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_3 Int)
735
(declare-rel chart_chart__CHART_B__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
736
(rule (=> 
737
  (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)
738
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_1)
739
       (Chart_B_ex chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_1
740
                   false
741
                   chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2)
742
       (Chart_A_en chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2
743
                   false
744
                   chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_3)
745
       (= 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)
746
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
747
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
748
       )
749
  (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)
750
))
751

    
752
; chart_chart__CHART_B__TO__CHART_A_1_unless
753
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
754
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
755
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
756
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
757
(declare-rel chart_chart__CHART_B__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
758
(rule (=> 
759
  (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)
760
       (= 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)
761
       )
762
  (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)
763
))
764

    
765
; chart_chart__CHART_C_IDL_handler_until
766
(declare-var chart_chart__CHART_C_IDL_handler_until.idChart_Chart_1 Int)
767
(declare-var chart_chart__CHART_C_IDL_handler_until.y_1 Int)
768
(declare-var chart_chart__CHART_C_IDL_handler_until.z_1 Int)
769
(declare-var chart_chart__CHART_C_IDL_handler_until.chart_chart__restart_in Bool)
770
(declare-var chart_chart__CHART_C_IDL_handler_until.chart_chart__state_in chart_chart__type)
771
(declare-var chart_chart__CHART_C_IDL_handler_until.idChart_Chart_out Int)
772
(declare-var chart_chart__CHART_C_IDL_handler_until.y_out Int)
773
(declare-var chart_chart__CHART_C_IDL_handler_until.z_out Int)
774
(declare-rel chart_chart__CHART_C_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
775
(rule (=> 
776
  (and (= chart_chart__CHART_C_IDL_handler_until.z_out chart_chart__CHART_C_IDL_handler_until.z_1)
777
       (= chart_chart__CHART_C_IDL_handler_until.y_out chart_chart__CHART_C_IDL_handler_until.y_1)
778
       (= chart_chart__CHART_C_IDL_handler_until.idChart_Chart_out chart_chart__CHART_C_IDL_handler_until.idChart_Chart_1)
779
       (= chart_chart__CHART_C_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
780
       (= chart_chart__CHART_C_IDL_handler_until.chart_chart__restart_in true)
781
       )
782
  (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)
783
))
784

    
785
; chart_chart__CHART_C_IDL_unless
786
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__restart_in Bool)
787
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__state_in chart_chart__type)
788
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__restart_act Bool)
789
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__state_act chart_chart__type)
790
(declare-rel chart_chart__CHART_C_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
791
(rule (=> 
792
  (and (= chart_chart__CHART_C_IDL_unless.chart_chart__state_act chart_chart__CHART_C_IDL_unless.chart_chart__state_in)
793
       (= chart_chart__CHART_C_IDL_unless.chart_chart__restart_act chart_chart__CHART_C_IDL_unless.chart_chart__restart_in)
794
       )
795
  (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)
796
))
797

    
798
; chart_chart__CHART_C__TO__CHART_A_1_handler_until
799
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
800
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_1 Int)
801
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_1 Int)
802
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
803
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
804
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
805
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_out Int)
806
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_out Int)
807
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
808
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_3 Int)
809
(declare-rel chart_chart__CHART_C__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
810
(rule (=> 
811
  (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)
812
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_1)
813
       (Chart_C_ex chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_1
814
                   false
815
                   chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2)
816
       (Chart_A_en chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2
817
                   false
818
                   chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_3)
819
       (= 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)
820
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
821
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
822
       )
823
  (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)
824
))
825

    
826
; chart_chart__CHART_C__TO__CHART_A_1_unless
827
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
828
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
829
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
830
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
831
(declare-rel chart_chart__CHART_C__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
832
(rule (=> 
833
  (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)
834
       (= 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)
835
       )
836
  (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)
837
))
838

    
839
; chart_chart__POINTChart_Chart_handler_until
840
(declare-var chart_chart__POINTChart_Chart_handler_until.idChart_Chart_1 Int)
841
(declare-var chart_chart__POINTChart_Chart_handler_until.y_1 Int)
842
(declare-var chart_chart__POINTChart_Chart_handler_until.z_1 Int)
843
(declare-var chart_chart__POINTChart_Chart_handler_until.chart_chart__restart_in Bool)
844
(declare-var chart_chart__POINTChart_Chart_handler_until.chart_chart__state_in chart_chart__type)
845
(declare-var chart_chart__POINTChart_Chart_handler_until.idChart_Chart_out Int)
846
(declare-var chart_chart__POINTChart_Chart_handler_until.y_out Int)
847
(declare-var chart_chart__POINTChart_Chart_handler_until.z_out Int)
848
(declare-rel chart_chart__POINTChart_Chart_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
849
(rule (=> 
850
  (and (= chart_chart__POINTChart_Chart_handler_until.z_out chart_chart__POINTChart_Chart_handler_until.z_1)
851
       (= chart_chart__POINTChart_Chart_handler_until.y_out chart_chart__POINTChart_Chart_handler_until.y_1)
852
       (= chart_chart__POINTChart_Chart_handler_until.idChart_Chart_out chart_chart__POINTChart_Chart_handler_until.idChart_Chart_1)
853
       (= chart_chart__POINTChart_Chart_handler_until.chart_chart__state_in POINTChart_Chart)
854
       (= chart_chart__POINTChart_Chart_handler_until.chart_chart__restart_in false)
855
       )
856
  (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)
857
))
858

    
859
; chart_chart__POINTChart_Chart_unless
860
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__restart_in Bool)
861
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__state_in chart_chart__type)
862
(declare-var chart_chart__POINTChart_Chart_unless.idChart_Chart_1 Int)
863
(declare-var chart_chart__POINTChart_Chart_unless.E1 Bool)
864
(declare-var chart_chart__POINTChart_Chart_unless.x Int)
865
(declare-var chart_chart__POINTChart_Chart_unless.y_1 Int)
866
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__restart_act Bool)
867
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__state_act chart_chart__type)
868
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 Bool)
869
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 Bool)
870
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 Bool)
871
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 Bool)
872
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 Bool)
873
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 Bool)
874
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 Bool)
875
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_8 Bool)
876
(declare-rel chart_chart__POINTChart_Chart_unless (Bool chart_chart__type Int Bool Int Int Bool chart_chart__type))
877
(rule (=> 
878
  (and (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_8 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1162))
879
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1161))
880
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1160))
881
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1162) (> chart_chart__POINTChart_Chart_unless.x 3)))
882
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1161) (> chart_chart__POINTChart_Chart_unless.x 3)))
883
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1160) (> chart_chart__POINTChart_Chart_unless.y_1 1)))
884
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 (and (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1160) chart_chart__POINTChart_Chart_unless.E1) (> chart_chart__POINTChart_Chart_unless.x 0)))
885
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 0))
886
       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 false))
887
               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 false))
888
                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 false))
889
                               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 false))
890
                                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 false))
891
                                               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 false))
892
                                                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 false))
893
                                                               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_8 false))
894
                                                                    (and 
895
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act chart_chart__POINTChart_Chart_unless.chart_chart__state_in)
896
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act chart_chart__POINTChart_Chart_unless.chart_chart__restart_in)
897
                                                                    ))
898
                                                                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_8 true))
899
                                                                    (and 
900
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_B_IDL)
901
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
902
                                                                    ))
903
                                                               ))
904
                                                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 true))
905
                                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_C_IDL)
906
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
907
                                                                    ))
908
                                                       ))
909
                                                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 true))
910
                                                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_A_IDL)
911
                                                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
912
                                                            ))
913
                                               ))
914
                                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 true))
915
                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_B__TO__CHART_A_1)
916
                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
917
                                                    ))
918
                                       ))
919
                                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 true))
920
                                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_C__TO__CHART_A_1)
921
                                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
922
                                            ))
923
                               ))
924
                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 true))
925
                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1167_2)
926
                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
927
                                    ))
928
                       ))
929
                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 true))
930
                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1168_1)
931
                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
932
                            ))
933
               ))
934
            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 true))
935
               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act POINT__TO__CHART_A_1)
936
                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
937
                    ))
938
       )
939
       )
940
  (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.y_1 chart_chart__POINTChart_Chart_unless.chart_chart__restart_act chart_chart__POINTChart_Chart_unless.chart_chart__state_act)
941
))
942

    
943
; chart_chart__POINT__TO__CHART_A_1_handler_until
944
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
945
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.y_1 Int)
946
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.z_1 Int)
947
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
948
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
949
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
950
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.y_out Int)
951
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.z_out Int)
952
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
953
(declare-rel chart_chart__POINT__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
954
(rule (=> 
955
  (and (= chart_chart__POINT__TO__CHART_A_1_handler_until.z_out chart_chart__POINT__TO__CHART_A_1_handler_until.z_1)
956
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.y_out chart_chart__POINT__TO__CHART_A_1_handler_until.y_1)
957
       (Chart_A_en chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_1
958
                   false
959
                   chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2)
960
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2)
961
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
962
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
963
       )
964
  (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)
965
))
966

    
967
; chart_chart__POINT__TO__CHART_A_1_unless
968
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
969
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
970
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
971
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
972
(declare-rel chart_chart__POINT__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
973
(rule (=> 
974
  (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)
975
       (= chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_in)
976
       )
977
  (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)
978
))
979

    
980
; Chart_Chart_node
981
(declare-var Chart_Chart_node.idChart_Chart_1 Int)
982
(declare-var Chart_Chart_node.E1 Bool)
983
(declare-var Chart_Chart_node.x Int)
984
(declare-var Chart_Chart_node.y_1 Int)
985
(declare-var Chart_Chart_node.z_1 Int)
986
(declare-var Chart_Chart_node.idChart_Chart Int)
987
(declare-var Chart_Chart_node.y Int)
988
(declare-var Chart_Chart_node.z Int)
989
(declare-var Chart_Chart_node.__Chart_Chart_node_65_c Bool)
990
(declare-var Chart_Chart_node.__Chart_Chart_node_66_c chart_chart__type)
991
(declare-var Chart_Chart_node.ni_4._arrow._first_c Bool)
992
(declare-var Chart_Chart_node.__Chart_Chart_node_65_m Bool)
993
(declare-var Chart_Chart_node.__Chart_Chart_node_66_m chart_chart__type)
994
(declare-var Chart_Chart_node.ni_4._arrow._first_m Bool)
995
(declare-var Chart_Chart_node.__Chart_Chart_node_65_x Bool)
996
(declare-var Chart_Chart_node.__Chart_Chart_node_66_x chart_chart__type)
997
(declare-var Chart_Chart_node.ni_4._arrow._first_x Bool)
998
(declare-var Chart_Chart_node.__Chart_Chart_node_1 Bool)
999
(declare-var Chart_Chart_node.__Chart_Chart_node_10 chart_chart__type)
1000
(declare-var Chart_Chart_node.__Chart_Chart_node_11 Bool)
1001
(declare-var Chart_Chart_node.__Chart_Chart_node_12 chart_chart__type)
1002
(declare-var Chart_Chart_node.__Chart_Chart_node_13 Bool)
1003
(declare-var Chart_Chart_node.__Chart_Chart_node_14 chart_chart__type)
1004
(declare-var Chart_Chart_node.__Chart_Chart_node_15 Bool)
1005
(declare-var Chart_Chart_node.__Chart_Chart_node_16 chart_chart__type)
1006
(declare-var Chart_Chart_node.__Chart_Chart_node_17 Bool)
1007
(declare-var Chart_Chart_node.__Chart_Chart_node_18 chart_chart__type)
1008
(declare-var Chart_Chart_node.__Chart_Chart_node_19 Bool)
1009
(declare-var Chart_Chart_node.__Chart_Chart_node_2 chart_chart__type)
1010
(declare-var Chart_Chart_node.__Chart_Chart_node_20 chart_chart__type)
1011
(declare-var Chart_Chart_node.__Chart_Chart_node_21 Int)
1012
(declare-var Chart_Chart_node.__Chart_Chart_node_22 Int)
1013
(declare-var Chart_Chart_node.__Chart_Chart_node_23 Int)
1014
(declare-var Chart_Chart_node.__Chart_Chart_node_24 Bool)
1015
(declare-var Chart_Chart_node.__Chart_Chart_node_25 chart_chart__type)
1016
(declare-var Chart_Chart_node.__Chart_Chart_node_26 Int)
1017
(declare-var Chart_Chart_node.__Chart_Chart_node_27 Int)
1018
(declare-var Chart_Chart_node.__Chart_Chart_node_28 Int)
1019
(declare-var Chart_Chart_node.__Chart_Chart_node_29 Bool)
1020
(declare-var Chart_Chart_node.__Chart_Chart_node_3 Bool)
1021
(declare-var Chart_Chart_node.__Chart_Chart_node_30 chart_chart__type)
1022
(declare-var Chart_Chart_node.__Chart_Chart_node_31 Int)
1023
(declare-var Chart_Chart_node.__Chart_Chart_node_32 Int)
1024
(declare-var Chart_Chart_node.__Chart_Chart_node_33 Int)
1025
(declare-var Chart_Chart_node.__Chart_Chart_node_34 Bool)
1026
(declare-var Chart_Chart_node.__Chart_Chart_node_35 chart_chart__type)
1027
(declare-var Chart_Chart_node.__Chart_Chart_node_36 Int)
1028
(declare-var Chart_Chart_node.__Chart_Chart_node_37 Int)
1029
(declare-var Chart_Chart_node.__Chart_Chart_node_38 Int)
1030
(declare-var Chart_Chart_node.__Chart_Chart_node_39 Bool)
1031
(declare-var Chart_Chart_node.__Chart_Chart_node_4 chart_chart__type)
1032
(declare-var Chart_Chart_node.__Chart_Chart_node_40 chart_chart__type)
1033
(declare-var Chart_Chart_node.__Chart_Chart_node_41 Int)
1034
(declare-var Chart_Chart_node.__Chart_Chart_node_42 Int)
1035
(declare-var Chart_Chart_node.__Chart_Chart_node_43 Int)
1036
(declare-var Chart_Chart_node.__Chart_Chart_node_44 Bool)
1037
(declare-var Chart_Chart_node.__Chart_Chart_node_45 chart_chart__type)
1038
(declare-var Chart_Chart_node.__Chart_Chart_node_46 Int)
1039
(declare-var Chart_Chart_node.__Chart_Chart_node_47 Int)
1040
(declare-var Chart_Chart_node.__Chart_Chart_node_48 Int)
1041
(declare-var Chart_Chart_node.__Chart_Chart_node_49 Bool)
1042
(declare-var Chart_Chart_node.__Chart_Chart_node_5 Bool)
1043
(declare-var Chart_Chart_node.__Chart_Chart_node_50 chart_chart__type)
1044
(declare-var Chart_Chart_node.__Chart_Chart_node_51 Int)
1045
(declare-var Chart_Chart_node.__Chart_Chart_node_52 Int)
1046
(declare-var Chart_Chart_node.__Chart_Chart_node_53 Int)
1047
(declare-var Chart_Chart_node.__Chart_Chart_node_54 Bool)
1048
(declare-var Chart_Chart_node.__Chart_Chart_node_55 chart_chart__type)
1049
(declare-var Chart_Chart_node.__Chart_Chart_node_56 Int)
1050
(declare-var Chart_Chart_node.__Chart_Chart_node_57 Int)
1051
(declare-var Chart_Chart_node.__Chart_Chart_node_58 Int)
1052
(declare-var Chart_Chart_node.__Chart_Chart_node_59 Bool)
1053
(declare-var Chart_Chart_node.__Chart_Chart_node_6 chart_chart__type)
1054
(declare-var Chart_Chart_node.__Chart_Chart_node_60 chart_chart__type)
1055
(declare-var Chart_Chart_node.__Chart_Chart_node_61 Int)
1056
(declare-var Chart_Chart_node.__Chart_Chart_node_62 Int)
1057
(declare-var Chart_Chart_node.__Chart_Chart_node_63 Int)
1058
(declare-var Chart_Chart_node.__Chart_Chart_node_64 Bool)
1059
(declare-var Chart_Chart_node.__Chart_Chart_node_7 Bool)
1060
(declare-var Chart_Chart_node.__Chart_Chart_node_8 chart_chart__type)
1061
(declare-var Chart_Chart_node.__Chart_Chart_node_9 Bool)
1062
(declare-var Chart_Chart_node.chart_chart__next_restart_in Bool)
1063
(declare-var Chart_Chart_node.chart_chart__next_state_in chart_chart__type)
1064
(declare-var Chart_Chart_node.chart_chart__restart_act Bool)
1065
(declare-var Chart_Chart_node.chart_chart__restart_in Bool)
1066
(declare-var Chart_Chart_node.chart_chart__state_act chart_chart__type)
1067
(declare-var Chart_Chart_node.chart_chart__state_in chart_chart__type)
1068
(declare-rel Chart_Chart_node_reset (Bool chart_chart__type Bool Bool chart_chart__type Bool))
1069
(declare-rel Chart_Chart_node_step (Int Bool Int Int Int Int Int Int Bool chart_chart__type Bool Bool chart_chart__type Bool))
1070

    
1071
(rule (=> 
1072
  (and 
1073
       (= Chart_Chart_node.__Chart_Chart_node_65_m Chart_Chart_node.__Chart_Chart_node_65_c)
1074
       (= Chart_Chart_node.__Chart_Chart_node_66_m Chart_Chart_node.__Chart_Chart_node_66_c)
1075
       (= Chart_Chart_node.ni_4._arrow._first_m true)
1076
  )
1077
  (Chart_Chart_node_reset Chart_Chart_node.__Chart_Chart_node_65_c
1078
                          Chart_Chart_node.__Chart_Chart_node_66_c
1079
                          Chart_Chart_node.ni_4._arrow._first_c
1080
                          Chart_Chart_node.__Chart_Chart_node_65_m
1081
                          Chart_Chart_node.__Chart_Chart_node_66_m
1082
                          Chart_Chart_node.ni_4._arrow._first_m)
1083
))
1084

    
1085
(rule (=> 
1086
  (and (= Chart_Chart_node.ni_4._arrow._first_m Chart_Chart_node.ni_4._arrow._first_c)
1087
       (and (= Chart_Chart_node.__Chart_Chart_node_64 (ite Chart_Chart_node.ni_4._arrow._first_m true false))
1088
            (= Chart_Chart_node.ni_4._arrow._first_x false))
1089
       (and (or (not (= Chart_Chart_node.__Chart_Chart_node_64 false))
1090
               (and (= Chart_Chart_node.chart_chart__state_in Chart_Chart_node.__Chart_Chart_node_66_c)
1091
                    (= Chart_Chart_node.chart_chart__restart_in Chart_Chart_node.__Chart_Chart_node_65_c)
1092
                    ))
1093
            (or (not (= Chart_Chart_node.__Chart_Chart_node_64 true))
1094
               (and (= Chart_Chart_node.chart_chart__state_in POINTChart_Chart)
1095
                    (= Chart_Chart_node.chart_chart__restart_in false)
1096
                    ))
1097
       )
1098
       (and (or (not (= Chart_Chart_node.chart_chart__state_in CHART_A_IDL))
1099
               (and (chart_chart__CHART_A_IDL_unless Chart_Chart_node.chart_chart__restart_in
1100
                                                     Chart_Chart_node.chart_chart__state_in
1101
                                                     Chart_Chart_node.__Chart_Chart_node_5
1102
                                                     Chart_Chart_node.__Chart_Chart_node_6)
1103
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_6)
1104
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_5)
1105
                    ))
1106
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_A__TO__CHART_CHARTJUNCTION1167_2))
1107
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_unless 
1108
                    Chart_Chart_node.chart_chart__restart_in
1109
                    Chart_Chart_node.chart_chart__state_in
1110
                    Chart_Chart_node.__Chart_Chart_node_11
1111
                    Chart_Chart_node.__Chart_Chart_node_12)
1112
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_12)
1113
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_11)
1114
                    ))
1115
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_A__TO__CHART_CHARTJUNCTION1168_1))
1116
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_unless 
1117
                    Chart_Chart_node.chart_chart__restart_in
1118
                    Chart_Chart_node.chart_chart__state_in
1119
                    Chart_Chart_node.__Chart_Chart_node_13
1120
                    Chart_Chart_node.__Chart_Chart_node_14)
1121
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_14)
1122
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_13)
1123
                    ))
1124
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_B_IDL))
1125
               (and (chart_chart__CHART_B_IDL_unless Chart_Chart_node.chart_chart__restart_in
1126
                                                     Chart_Chart_node.chart_chart__state_in
1127
                                                     Chart_Chart_node.__Chart_Chart_node_1
1128
                                                     Chart_Chart_node.__Chart_Chart_node_2)
1129
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_2)
1130
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_1)
1131
                    ))
1132
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_B__TO__CHART_A_1))
1133
               (and (chart_chart__CHART_B__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
1134
                                                                Chart_Chart_node.chart_chart__state_in
1135
                                                                Chart_Chart_node.__Chart_Chart_node_7
1136
                                                                Chart_Chart_node.__Chart_Chart_node_8)
1137
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_8)
1138
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_7)
1139
                    ))
1140
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_C_IDL))
1141
               (and (chart_chart__CHART_C_IDL_unless Chart_Chart_node.chart_chart__restart_in
1142
                                                     Chart_Chart_node.chart_chart__state_in
1143
                                                     Chart_Chart_node.__Chart_Chart_node_3
1144
                                                     Chart_Chart_node.__Chart_Chart_node_4)
1145
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_4)
1146
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_3)
1147
                    ))
1148
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_C__TO__CHART_A_1))
1149
               (and (chart_chart__CHART_C__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
1150
                                                                Chart_Chart_node.chart_chart__state_in
1151
                                                                Chart_Chart_node.__Chart_Chart_node_9
1152
                                                                Chart_Chart_node.__Chart_Chart_node_10)
1153
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_10)
1154
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_9)
1155
                    ))
1156
            (or (not (= Chart_Chart_node.chart_chart__state_in POINTChart_Chart))
1157
               (and (chart_chart__POINTChart_Chart_unless Chart_Chart_node.chart_chart__restart_in
1158
                                                          Chart_Chart_node.chart_chart__state_in
1159
                                                          Chart_Chart_node.idChart_Chart_1
1160
                                                          Chart_Chart_node.E1
1161
                                                          Chart_Chart_node.x
1162
                                                          Chart_Chart_node.y_1
1163
                                                          Chart_Chart_node.__Chart_Chart_node_17
1164
                                                          Chart_Chart_node.__Chart_Chart_node_18)
1165
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_18)
1166
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_17)
1167
                    ))
1168
            (or (not (= Chart_Chart_node.chart_chart__state_in POINT__TO__CHART_A_1))
1169
               (and (chart_chart__POINT__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
1170
                                                              Chart_Chart_node.chart_chart__state_in
1171
                                                              Chart_Chart_node.__Chart_Chart_node_15
1172
                                                              Chart_Chart_node.__Chart_Chart_node_16)
1173
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_16)
1174
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_15)
1175
                    ))
1176
       )
1177
       (and (or (not (= Chart_Chart_node.chart_chart__state_act CHART_A_IDL))
1178
               (and (chart_chart__CHART_A_IDL_handler_until Chart_Chart_node.idChart_Chart_1
1179
                                                            Chart_Chart_node.y_1
1180
                                                            Chart_Chart_node.z_1
1181
                                                            Chart_Chart_node.__Chart_Chart_node_29
1182
                                                            Chart_Chart_node.__Chart_Chart_node_30
1183
                                                            Chart_Chart_node.__Chart_Chart_node_31
1184
                                                            Chart_Chart_node.__Chart_Chart_node_32
1185
                                                            Chart_Chart_node.__Chart_Chart_node_33)
1186
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_33)
1187
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_32)
1188
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_31)
1189
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_30)
1190
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_29)
1191
                    ))
1192
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1167_2))
1193
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1167_2_handler_until 
1194
                    Chart_Chart_node.idChart_Chart_1
1195
                    Chart_Chart_node.x
1196
                    Chart_Chart_node.y_1
1197
                    Chart_Chart_node.z_1
1198
                    Chart_Chart_node.__Chart_Chart_node_44
1199
                    Chart_Chart_node.__Chart_Chart_node_45
1200
                    Chart_Chart_node.__Chart_Chart_node_46
1201
                    Chart_Chart_node.__Chart_Chart_node_47
1202
                    Chart_Chart_node.__Chart_Chart_node_48)
1203
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_48)
1204
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_47)
1205
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_46)
1206
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_45)
1207
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_44)
1208
                    ))
1209
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1168_1))
1210
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1168_1_handler_until 
1211
                    Chart_Chart_node.idChart_Chart_1
1212
                    Chart_Chart_node.x
1213
                    Chart_Chart_node.y_1
1214
                    Chart_Chart_node.z_1
1215
                    Chart_Chart_node.__Chart_Chart_node_49
1216
                    Chart_Chart_node.__Chart_Chart_node_50
1217
                    Chart_Chart_node.__Chart_Chart_node_51
1218
                    Chart_Chart_node.__Chart_Chart_node_52
1219
                    Chart_Chart_node.__Chart_Chart_node_53)
1220
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_53)
1221
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_52)
1222
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_51)
1223
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_50)
1224
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_49)
1225
                    ))
1226
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_B_IDL))
1227
               (and (chart_chart__CHART_B_IDL_handler_until Chart_Chart_node.idChart_Chart_1
1228
                                                            Chart_Chart_node.y_1
1229
                                                            Chart_Chart_node.z_1
1230
                                                            Chart_Chart_node.__Chart_Chart_node_19
1231
                                                            Chart_Chart_node.__Chart_Chart_node_20
1232
                                                            Chart_Chart_node.__Chart_Chart_node_21
1233
                                                            Chart_Chart_node.__Chart_Chart_node_22
1234
                                                            Chart_Chart_node.__Chart_Chart_node_23)
1235
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_23)
1236
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_22)
1237
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_21)
1238
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_20)
1239
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_19)
1240
                    ))
1241
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_B__TO__CHART_A_1))
1242
               (and (chart_chart__CHART_B__TO__CHART_A_1_handler_until 
1243
                    Chart_Chart_node.idChart_Chart_1
1244
                    Chart_Chart_node.y_1
1245
                    Chart_Chart_node.z_1
1246
                    Chart_Chart_node.__Chart_Chart_node_34
1247
                    Chart_Chart_node.__Chart_Chart_node_35
1248
                    Chart_Chart_node.__Chart_Chart_node_36
1249
                    Chart_Chart_node.__Chart_Chart_node_37
1250
                    Chart_Chart_node.__Chart_Chart_node_38)
1251
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_38)
1252
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_37)
1253
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_36)
1254
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_35)
1255
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_34)
1256
                    ))
1257
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_C_IDL))
1258
               (and (chart_chart__CHART_C_IDL_handler_until Chart_Chart_node.idChart_Chart_1
1259
                                                            Chart_Chart_node.y_1
1260
                                                            Chart_Chart_node.z_1
1261
                                                            Chart_Chart_node.__Chart_Chart_node_24
1262
                                                            Chart_Chart_node.__Chart_Chart_node_25
1263
                                                            Chart_Chart_node.__Chart_Chart_node_26
1264
                                                            Chart_Chart_node.__Chart_Chart_node_27
1265
                                                            Chart_Chart_node.__Chart_Chart_node_28)
1266
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_28)
1267
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_27)
1268
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_26)
1269
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_25)
1270
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_24)
1271
                    ))
1272
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_C__TO__CHART_A_1))
1273
               (and (chart_chart__CHART_C__TO__CHART_A_1_handler_until 
1274
                    Chart_Chart_node.idChart_Chart_1
1275
                    Chart_Chart_node.y_1
1276
                    Chart_Chart_node.z_1
1277
                    Chart_Chart_node.__Chart_Chart_node_39
1278
                    Chart_Chart_node.__Chart_Chart_node_40
1279
                    Chart_Chart_node.__Chart_Chart_node_41
1280
                    Chart_Chart_node.__Chart_Chart_node_42
1281
                    Chart_Chart_node.__Chart_Chart_node_43)
1282
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_43)
1283
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_42)
1284
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_41)
1285
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_40)
1286
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_39)
1287
                    ))
1288
            (or (not (= Chart_Chart_node.chart_chart__state_act POINTChart_Chart))
1289
               (and (chart_chart__POINTChart_Chart_handler_until Chart_Chart_node.idChart_Chart_1
1290
                                                                 Chart_Chart_node.y_1
1291
                                                                 Chart_Chart_node.z_1
1292
                                                                 Chart_Chart_node.__Chart_Chart_node_59
1293
                                                                 Chart_Chart_node.__Chart_Chart_node_60
1294
                                                                 Chart_Chart_node.__Chart_Chart_node_61
1295
                                                                 Chart_Chart_node.__Chart_Chart_node_62
1296
                                                                 Chart_Chart_node.__Chart_Chart_node_63)
1297
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_63)
1298
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_62)
1299
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_61)
1300
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_60)
1301
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_59)
1302
                    ))
1303
            (or (not (= Chart_Chart_node.chart_chart__state_act POINT__TO__CHART_A_1))
1304
               (and (chart_chart__POINT__TO__CHART_A_1_handler_until 
1305
                    Chart_Chart_node.idChart_Chart_1
1306
                    Chart_Chart_node.y_1
1307
                    Chart_Chart_node.z_1
1308
                    Chart_Chart_node.__Chart_Chart_node_54
1309
                    Chart_Chart_node.__Chart_Chart_node_55
1310
                    Chart_Chart_node.__Chart_Chart_node_56
1311
                    Chart_Chart_node.__Chart_Chart_node_57
1312
                    Chart_Chart_node.__Chart_Chart_node_58)
1313
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_58)
1314
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_57)
1315
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_56)
1316
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_55)
1317
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_54)
1318
                    ))
1319
       )
1320
       (= Chart_Chart_node.__Chart_Chart_node_66_x Chart_Chart_node.chart_chart__next_state_in)
1321
       (= Chart_Chart_node.__Chart_Chart_node_65_x Chart_Chart_node.chart_chart__next_restart_in)
1322
       )
1323
  (Chart_Chart_node_step Chart_Chart_node.idChart_Chart_1
1324
                         Chart_Chart_node.E1
1325
                         Chart_Chart_node.x
1326
                         Chart_Chart_node.y_1
1327
                         Chart_Chart_node.z_1
1328
                         Chart_Chart_node.idChart_Chart
1329
                         Chart_Chart_node.y
1330
                         Chart_Chart_node.z
1331
                         Chart_Chart_node.__Chart_Chart_node_65_c
1332
                         Chart_Chart_node.__Chart_Chart_node_66_c
1333
                         Chart_Chart_node.ni_4._arrow._first_c
1334
                         Chart_Chart_node.__Chart_Chart_node_65_x
1335
                         Chart_Chart_node.__Chart_Chart_node_66_x
1336
                         Chart_Chart_node.ni_4._arrow._first_x)
1337
))
1338

    
1339
; Junctions1False_Chart
1340
(declare-var Junctions1False_Chart.x Int)
1341
(declare-var Junctions1False_Chart.E1 Bool)
1342
(declare-var Junctions1False_Chart.y Int)
1343
(declare-var Junctions1False_Chart.z Int)
1344
(declare-var Junctions1False_Chart.__Junctions1False_Chart_5_c Int)
1345
(declare-var Junctions1False_Chart.__Junctions1False_Chart_6_c Int)
1346
(declare-var Junctions1False_Chart.__Junctions1False_Chart_7_c Int)
1347
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c Bool)
1348
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c chart_chart__type)
1349
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c Bool)
1350
(declare-var Junctions1False_Chart.ni_3._arrow._first_c Bool)
1351
(declare-var Junctions1False_Chart.__Junctions1False_Chart_5_m Int)
1352
(declare-var Junctions1False_Chart.__Junctions1False_Chart_6_m Int)
1353
(declare-var Junctions1False_Chart.__Junctions1False_Chart_7_m Int)
1354
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m Bool)
1355
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m chart_chart__type)
1356
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Bool)
1357
(declare-var Junctions1False_Chart.ni_3._arrow._first_m Bool)
1358
(declare-var Junctions1False_Chart.__Junctions1False_Chart_5_x Int)
1359
(declare-var Junctions1False_Chart.__Junctions1False_Chart_6_x Int)
1360
(declare-var Junctions1False_Chart.__Junctions1False_Chart_7_x Int)
1361
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_x Bool)
1362
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_x chart_chart__type)
1363
(declare-var Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x Bool)
1364
(declare-var Junctions1False_Chart.ni_3._arrow._first_x Bool)
1365
(declare-var Junctions1False_Chart.__Junctions1False_Chart_1 Int)
1366
(declare-var Junctions1False_Chart.__Junctions1False_Chart_2 Int)
1367
(declare-var Junctions1False_Chart.__Junctions1False_Chart_3 Int)
1368
(declare-var Junctions1False_Chart.__Junctions1False_Chart_4 Bool)
1369
(declare-var Junctions1False_Chart.idChart_Chart Int)
1370
(declare-var Junctions1False_Chart.idChart_Chart_1 Int)
1371
(declare-var Junctions1False_Chart.y_1 Int)
1372
(declare-var Junctions1False_Chart.z_1 Int)
1373
(declare-rel Junctions1False_Chart_reset (Int Int Int Bool chart_chart__type Bool Bool Int Int Int Bool chart_chart__type Bool Bool))
1374
(declare-rel Junctions1False_Chart_step (Int Bool Int Int Int Int Int Bool chart_chart__type Bool Bool Int Int Int Bool chart_chart__type Bool Bool))
1375

    
1376
(rule (=> 
1377
  (and 
1378
       (= Junctions1False_Chart.__Junctions1False_Chart_5_m Junctions1False_Chart.__Junctions1False_Chart_5_c)
1379
       (= Junctions1False_Chart.__Junctions1False_Chart_6_m Junctions1False_Chart.__Junctions1False_Chart_6_c)
1380
       (= Junctions1False_Chart.__Junctions1False_Chart_7_m Junctions1False_Chart.__Junctions1False_Chart_7_c)
1381
       (= Junctions1False_Chart.ni_3._arrow._first_m true)
1382
       (Chart_Chart_node_reset Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c
1383
                               Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c
1384
                               Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1385
                               Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m
1386
                               Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m
1387
                               Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m)
1388
  )
1389
  (Junctions1False_Chart_reset Junctions1False_Chart.__Junctions1False_Chart_5_c
1390
                               Junctions1False_Chart.__Junctions1False_Chart_6_c
1391
                               Junctions1False_Chart.__Junctions1False_Chart_7_c
1392
                               Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c
1393
                               Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c
1394
                               Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1395
                               Junctions1False_Chart.ni_3._arrow._first_c
1396
                               Junctions1False_Chart.__Junctions1False_Chart_5_m
1397
                               Junctions1False_Chart.__Junctions1False_Chart_6_m
1398
                               Junctions1False_Chart.__Junctions1False_Chart_7_m
1399
                               Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m
1400
                               Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m
1401
                               Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1402
                               Junctions1False_Chart.ni_3._arrow._first_m)
1403
))
1404

    
1405
(rule (=> 
1406
  (and (= Junctions1False_Chart.ni_3._arrow._first_m Junctions1False_Chart.ni_3._arrow._first_c)
1407
       (and (= Junctions1False_Chart.__Junctions1False_Chart_4 (ite Junctions1False_Chart.ni_3._arrow._first_m true false))
1408
            (= Junctions1False_Chart.ni_3._arrow._first_x false))
1409
       (and (or (not (= Junctions1False_Chart.__Junctions1False_Chart_4 false))
1410
               (and (= Junctions1False_Chart.z_1 Junctions1False_Chart.__Junctions1False_Chart_6_c)
1411
                    (= Junctions1False_Chart.y_1 Junctions1False_Chart.__Junctions1False_Chart_7_c)
1412
                    (= Junctions1False_Chart.idChart_Chart_1 Junctions1False_Chart.__Junctions1False_Chart_5_c)
1413
                    ))
1414
            (or (not (= Junctions1False_Chart.__Junctions1False_Chart_4 true))
1415
               (and (= Junctions1False_Chart.z_1 2)
1416
                    (= Junctions1False_Chart.y_1 1)
1417
                    (= Junctions1False_Chart.idChart_Chart_1 0)
1418
                    ))
1419
       )
1420
       (and (= Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c)
1421
            (= Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c)
1422
            (= Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c)
1423
            )
1424
       (Chart_Chart_node_step Junctions1False_Chart.idChart_Chart_1
1425
                              Junctions1False_Chart.E1
1426
                              Junctions1False_Chart.x
1427
                              Junctions1False_Chart.y_1
1428
                              Junctions1False_Chart.z_1
1429
                              Junctions1False_Chart.__Junctions1False_Chart_1
1430
                              Junctions1False_Chart.__Junctions1False_Chart_2
1431
                              Junctions1False_Chart.__Junctions1False_Chart_3
1432
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m
1433
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m
1434
                              Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1435
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_x
1436
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_x
1437
                              Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x)
1438
       (and (or (not (= Junctions1False_Chart.E1 false))
1439
               (and (= Junctions1False_Chart.z Junctions1False_Chart.z_1)
1440
                    (= Junctions1False_Chart.y Junctions1False_Chart.y_1)
1441
                    (= Junctions1False_Chart.idChart_Chart Junctions1False_Chart.idChart_Chart_1)
1442
                    ))
1443
            (or (not (= Junctions1False_Chart.E1 true))
1444
               (and (= Junctions1False_Chart.z Junctions1False_Chart.__Junctions1False_Chart_3)
1445
                    (= Junctions1False_Chart.y Junctions1False_Chart.__Junctions1False_Chart_2)
1446
                    (= Junctions1False_Chart.idChart_Chart Junctions1False_Chart.__Junctions1False_Chart_1)
1447
                    ))
1448
       )
1449
       (= Junctions1False_Chart.__Junctions1False_Chart_7_x Junctions1False_Chart.y)
1450
       (= Junctions1False_Chart.__Junctions1False_Chart_6_x Junctions1False_Chart.z)
1451
       (= Junctions1False_Chart.__Junctions1False_Chart_5_x Junctions1False_Chart.idChart_Chart)
1452
       )
1453
  (Junctions1False_Chart_step Junctions1False_Chart.x
1454
                              Junctions1False_Chart.E1
1455
                              Junctions1False_Chart.y
1456
                              Junctions1False_Chart.z
1457
                              Junctions1False_Chart.__Junctions1False_Chart_5_c
1458
                              Junctions1False_Chart.__Junctions1False_Chart_6_c
1459
                              Junctions1False_Chart.__Junctions1False_Chart_7_c
1460
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c
1461
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c
1462
                              Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1463
                              Junctions1False_Chart.ni_3._arrow._first_c
1464
                              Junctions1False_Chart.__Junctions1False_Chart_5_x
1465
                              Junctions1False_Chart.__Junctions1False_Chart_6_x
1466
                              Junctions1False_Chart.__Junctions1False_Chart_7_x
1467
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_x
1468
                              Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_x
1469
                              Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1470
                              Junctions1False_Chart.ni_3._arrow._first_x)
1471
))
1472

    
1473
; Junctions1False
1474
(declare-var Junctions1False.x_1_1 Int)
1475
(declare-var Junctions1False.E1_1_1 Real)
1476
(declare-var Junctions1False.y_1_1 Int)
1477
(declare-var Junctions1False.z_2_1 Int)
1478
(declare-var Junctions1False.__Junctions1False_2_c Real)
1479
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_c Int)
1480
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_c Int)
1481
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_c Int)
1482
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c Bool)
1483
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c chart_chart__type)
1484
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c Bool)
1485
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_c Bool)
1486
(declare-var Junctions1False.ni_1._arrow._first_c Bool)
1487
(declare-var Junctions1False.__Junctions1False_2_m Real)
1488
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_m Int)
1489
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_m Int)
1490
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_m Int)
1491
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m Bool)
1492
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m chart_chart__type)
1493
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Bool)
1494
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_m Bool)
1495
(declare-var Junctions1False.ni_1._arrow._first_m Bool)
1496
(declare-var Junctions1False.__Junctions1False_2_x Real)
1497
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_x Int)
1498
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_x Int)
1499
(declare-var Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_x Int)
1500
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_x Bool)
1501
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_x chart_chart__type)
1502
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x Bool)
1503
(declare-var Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_x Bool)
1504
(declare-var Junctions1False.ni_1._arrow._first_x Bool)
1505
(declare-var Junctions1False.ChartE1_1_1_event Bool)
1506
(declare-var Junctions1False.Chart_1_1 Int)
1507
(declare-var Junctions1False.Chart_2_1 Int)
1508
(declare-var Junctions1False.__Junctions1False_1 Bool)
1509
(declare-var Junctions1False.i_virtual_local Real)
1510
(declare-rel Junctions1False_reset (Real Int Int Int Bool chart_chart__type Bool Bool Bool Real Int Int Int Bool chart_chart__type Bool Bool Bool))
1511
(declare-rel Junctions1False_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))
1512

    
1513
(rule (=> 
1514
  (and 
1515
       (= Junctions1False.__Junctions1False_2_m Junctions1False.__Junctions1False_2_c)
1516
       (= Junctions1False.ni_1._arrow._first_m true)
1517
       (Junctions1False_Chart_reset Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_c
1518
                                    Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_c
1519
                                    Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_c
1520
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c
1521
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c
1522
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1523
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_c
1524
                                    Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_m
1525
                                    Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_m
1526
                                    Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_m
1527
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m
1528
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m
1529
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1530
                                    Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_m)
1531
  )
1532
  (Junctions1False_reset Junctions1False.__Junctions1False_2_c
1533
                         Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_c
1534
                         Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_c
1535
                         Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_c
1536
                         Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c
1537
                         Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c
1538
                         Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1539
                         Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_c
1540
                         Junctions1False.ni_1._arrow._first_c
1541
                         Junctions1False.__Junctions1False_2_m
1542
                         Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_m
1543
                         Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_m
1544
                         Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_m
1545
                         Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m
1546
                         Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m
1547
                         Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1548
                         Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_m
1549
                         Junctions1False.ni_1._arrow._first_m)
1550
))
1551

    
1552
(rule (=> 
1553
  (and (= Junctions1False.ni_1._arrow._first_m Junctions1False.ni_1._arrow._first_c)
1554
       (and (= Junctions1False.__Junctions1False_1 (ite Junctions1False.ni_1._arrow._first_m true false))
1555
            (= Junctions1False.ni_1._arrow._first_x false))
1556
       (and (or (not (= Junctions1False.__Junctions1False_1 true))
1557
               (= Junctions1False.ChartE1_1_1_event false))
1558
            (or (not (= Junctions1False.__Junctions1False_1 false))
1559
               (= Junctions1False.ChartE1_1_1_event (or (and (> Junctions1False.__Junctions1False_2_c 0.) (<= Junctions1False.E1_1_1 0.)) (and (<= Junctions1False.__Junctions1False_2_c 0.) (> Junctions1False.E1_1_1 0.)))))
1560
       )
1561
       (and (= Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_m Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_c)
1562
            (= Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_m Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_c)
1563
            (= Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_m Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_c)
1564
            (= Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c)
1565
            (= Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c)
1566
            (= Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c)
1567
            (= Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_m Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_c)
1568
            )
1569
       (Junctions1False_Chart_step Junctions1False.x_1_1
1570
                                   Junctions1False.ChartE1_1_1_event
1571
                                   Junctions1False.Chart_1_1
1572
                                   Junctions1False.Chart_2_1
1573
                                   Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_m
1574
                                   Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_m
1575
                                   Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_m
1576
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_m
1577
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_m
1578
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1579
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_m
1580
                                   Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_x
1581
                                   Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_x
1582
                                   Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_x
1583
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_x
1584
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_x
1585
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1586
                                   Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_x)
1587
       (= Junctions1False.z_2_1 Junctions1False.Chart_2_1)
1588
       (= Junctions1False.y_1_1 Junctions1False.Chart_1_1)
1589
       (and (or (not (= Junctions1False.__Junctions1False_1 true))
1590
               (= Junctions1False.i_virtual_local 0.))
1591
            (or (not (= Junctions1False.__Junctions1False_1 false))
1592
               (= Junctions1False.i_virtual_local 1.))
1593
       )
1594
       (= Junctions1False.__Junctions1False_2_x Junctions1False.E1_1_1)
1595
       )
1596
  (Junctions1False_step Junctions1False.x_1_1
1597
                        Junctions1False.E1_1_1
1598
                        Junctions1False.y_1_1
1599
                        Junctions1False.z_2_1
1600
                        Junctions1False.__Junctions1False_2_c
1601
                        Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_c
1602
                        Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_c
1603
                        Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_c
1604
                        Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_c
1605
                        Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_c
1606
                        Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1607
                        Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_c
1608
                        Junctions1False.ni_1._arrow._first_c
1609
                        Junctions1False.__Junctions1False_2_x
1610
                        Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_5_x
1611
                        Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_6_x
1612
                        Junctions1False.ni_0.Junctions1False_Chart.__Junctions1False_Chart_7_x
1613
                        Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_65_x
1614
                        Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_66_x
1615
                        Junctions1False.ni_0.Junctions1False_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1616
                        Junctions1False.ni_0.Junctions1False_Chart.ni_3._arrow._first_x
1617
                        Junctions1False.ni_1._arrow._first_x)
1618
))
1619