Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions1V0 / Junctions1V0.smt2 @ eb639349

History | View | Annotate | Download (97 KB)

1
(declare-datatypes () ((chart_chart__type POINTChart_Chart POINT__TO__CHART_A_1 CHART_A__TO__CHART_CHARTJUNCTION1192_1 CHART_B__TO__CHART_A_1 CHART_C__TO__CHART_A_1 CHART_A_IDL CHART_B_IDL CHART_C_IDL)));
2

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

    
12
; Chart_A__To__Chart_ChartJunction1192_1_Transition_Action
13
(declare-var Chart_A__To__Chart_ChartJunction1192_1_Transition_Action.z_1 Int)
14
(declare-var Chart_A__To__Chart_ChartJunction1192_1_Transition_Action.z Int)
15
(declare-rel Chart_A__To__Chart_ChartJunction1192_1_Transition_Action (Int Int))
16
(rule (=> 
17
  (= Chart_A__To__Chart_ChartJunction1192_1_Transition_Action.z (+ Chart_A__To__Chart_ChartJunction1192_1_Transition_Action.z_1 2))
18
  (Chart_A__To__Chart_ChartJunction1192_1_Transition_Action Chart_A__To__Chart_ChartJunction1192_1_Transition_Action.z_1 Chart_A__To__Chart_ChartJunction1192_1_Transition_Action.z)
19
))
20

    
21
; Chart_A_ex
22
(declare-var Chart_A_ex.idChart_Chart_1 Int)
23
(declare-var Chart_A_ex.isInner Bool)
24
(declare-var Chart_A_ex.idChart_Chart Int)
25
(declare-var Chart_A_ex.idChart_Chart_2 Int)
26
(declare-rel Chart_A_ex (Int Bool Int))
27
(rule (=> 
28
  (and (and (or (not (= (not Chart_A_ex.isInner) true))
29
               (= Chart_A_ex.idChart_Chart_2 0))
30
            (or (not (= (not Chart_A_ex.isInner) false))
31
               (= Chart_A_ex.idChart_Chart_2 Chart_A_ex.idChart_Chart_1))
32
       )
33
       (= Chart_A_ex.idChart_Chart Chart_A_ex.idChart_Chart_1)
34
       )
35
  (Chart_A_ex Chart_A_ex.idChart_Chart_1 Chart_A_ex.isInner Chart_A_ex.idChart_Chart)
36
))
37

    
38
; Chart_B_en
39
(declare-var Chart_B_en.idChart_Chart_1 Int)
40
(declare-var Chart_B_en.isInner Bool)
41
(declare-var Chart_B_en.idChart_Chart Int)
42
(declare-rel Chart_B_en (Int Bool Int))
43
(rule (=> 
44
  (= Chart_B_en.idChart_Chart 1186)
45
  (Chart_B_en Chart_B_en.idChart_Chart_1 Chart_B_en.isInner Chart_B_en.idChart_Chart)
46
))
47

    
48
; Chart_C_en
49
(declare-var Chart_C_en.idChart_Chart_1 Int)
50
(declare-var Chart_C_en.isInner Bool)
51
(declare-var Chart_C_en.idChart_Chart Int)
52
(declare-rel Chart_C_en (Int Bool Int))
53
(rule (=> 
54
  (= Chart_C_en.idChart_Chart 1187)
55
  (Chart_C_en Chart_C_en.idChart_Chart_1 Chart_C_en.isInner Chart_C_en.idChart_Chart)
56
))
57

    
58
; Chart_ChartJunction1192__To__Chart_B_1_Condition_Action
59
(declare-var Chart_ChartJunction1192__To__Chart_B_1_Condition_Action.y_1 Int)
60
(declare-var Chart_ChartJunction1192__To__Chart_B_1_Condition_Action.y Int)
61
(declare-rel Chart_ChartJunction1192__To__Chart_B_1_Condition_Action (Int Int))
62
(rule (=> 
63
  (= Chart_ChartJunction1192__To__Chart_B_1_Condition_Action.y (+ Chart_ChartJunction1192__To__Chart_B_1_Condition_Action.y_1 2))
64
  (Chart_ChartJunction1192__To__Chart_B_1_Condition_Action Chart_ChartJunction1192__To__Chart_B_1_Condition_Action.y_1 Chart_ChartJunction1192__To__Chart_B_1_Condition_Action.y)
65
))
66

    
67
; Chart_ChartJunction1192__To__Chart_B_1_Transition_Action
68
(declare-var Chart_ChartJunction1192__To__Chart_B_1_Transition_Action.z_1 Int)
69
(declare-var Chart_ChartJunction1192__To__Chart_B_1_Transition_Action.z Int)
70
(declare-rel Chart_ChartJunction1192__To__Chart_B_1_Transition_Action (Int Int))
71
(rule (=> 
72
  (= Chart_ChartJunction1192__To__Chart_B_1_Transition_Action.z (+ (+ Chart_ChartJunction1192__To__Chart_B_1_Transition_Action.z_1 1) 1))
73
  (Chart_ChartJunction1192__To__Chart_B_1_Transition_Action Chart_ChartJunction1192__To__Chart_B_1_Transition_Action.z_1 Chart_ChartJunction1192__To__Chart_B_1_Transition_Action.z)
74
))
75

    
76
; Chart_ChartJunction1192__To__Chart_C_2_Condition_Action
77
(declare-var Chart_ChartJunction1192__To__Chart_C_2_Condition_Action.y_1 Int)
78
(declare-var Chart_ChartJunction1192__To__Chart_C_2_Condition_Action.y Int)
79
(declare-rel Chart_ChartJunction1192__To__Chart_C_2_Condition_Action (Int Int))
80
(rule (=> 
81
  (= Chart_ChartJunction1192__To__Chart_C_2_Condition_Action.y (+ Chart_ChartJunction1192__To__Chart_C_2_Condition_Action.y_1 1))
82
  (Chart_ChartJunction1192__To__Chart_C_2_Condition_Action Chart_ChartJunction1192__To__Chart_C_2_Condition_Action.y_1 Chart_ChartJunction1192__To__Chart_C_2_Condition_Action.y)
83
))
84

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

    
94
; Chart_A_en
95
(declare-var Chart_A_en.idChart_Chart_1 Int)
96
(declare-var Chart_A_en.isInner Bool)
97
(declare-var Chart_A_en.idChart_Chart Int)
98
(declare-rel Chart_A_en (Int Bool Int))
99
(rule (=> 
100
  (= Chart_A_en.idChart_Chart 1185)
101
  (Chart_A_en Chart_A_en.idChart_Chart_1 Chart_A_en.isInner Chart_A_en.idChart_Chart)
102
))
103

    
104
; Chart_B_ex
105
(declare-var Chart_B_ex.idChart_Chart_1 Int)
106
(declare-var Chart_B_ex.isInner Bool)
107
(declare-var Chart_B_ex.idChart_Chart Int)
108
(declare-var Chart_B_ex.idChart_Chart_2 Int)
109
(declare-rel Chart_B_ex (Int Bool Int))
110
(rule (=> 
111
  (and (and (or (not (= (not Chart_B_ex.isInner) true))
112
               (= Chart_B_ex.idChart_Chart_2 0))
113
            (or (not (= (not Chart_B_ex.isInner) false))
114
               (= Chart_B_ex.idChart_Chart_2 Chart_B_ex.idChart_Chart_1))
115
       )
116
       (= Chart_B_ex.idChart_Chart Chart_B_ex.idChart_Chart_1)
117
       )
118
  (Chart_B_ex Chart_B_ex.idChart_Chart_1 Chart_B_ex.isInner Chart_B_ex.idChart_Chart)
119
))
120

    
121
; Chart_C_ex
122
(declare-var Chart_C_ex.idChart_Chart_1 Int)
123
(declare-var Chart_C_ex.isInner Bool)
124
(declare-var Chart_C_ex.idChart_Chart Int)
125
(declare-var Chart_C_ex.idChart_Chart_2 Int)
126
(declare-rel Chart_C_ex (Int Bool Int))
127
(rule (=> 
128
  (and (and (or (not (= (not Chart_C_ex.isInner) true))
129
               (= Chart_C_ex.idChart_Chart_2 0))
130
            (or (not (= (not Chart_C_ex.isInner) false))
131
               (= Chart_C_ex.idChart_Chart_2 Chart_C_ex.idChart_Chart_1))
132
       )
133
       (= Chart_C_ex.idChart_Chart Chart_C_ex.idChart_Chart_1)
134
       )
135
  (Chart_C_ex Chart_C_ex.idChart_Chart_1 Chart_C_ex.isInner Chart_C_ex.idChart_Chart)
136
))
137

    
138
; chart_chart__CHART_A_IDL_handler_until
139
(declare-var chart_chart__CHART_A_IDL_handler_until.idChart_Chart_1 Int)
140
(declare-var chart_chart__CHART_A_IDL_handler_until.y_1 Int)
141
(declare-var chart_chart__CHART_A_IDL_handler_until.z_1 Int)
142
(declare-var chart_chart__CHART_A_IDL_handler_until.chart_chart__restart_in Bool)
143
(declare-var chart_chart__CHART_A_IDL_handler_until.chart_chart__state_in chart_chart__type)
144
(declare-var chart_chart__CHART_A_IDL_handler_until.idChart_Chart_out Int)
145
(declare-var chart_chart__CHART_A_IDL_handler_until.y_out Int)
146
(declare-var chart_chart__CHART_A_IDL_handler_until.z_out Int)
147
(declare-rel chart_chart__CHART_A_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
148
(rule (=> 
149
  (and (= chart_chart__CHART_A_IDL_handler_until.z_out chart_chart__CHART_A_IDL_handler_until.z_1)
150
       (= chart_chart__CHART_A_IDL_handler_until.y_out chart_chart__CHART_A_IDL_handler_until.y_1)
151
       (= chart_chart__CHART_A_IDL_handler_until.idChart_Chart_out chart_chart__CHART_A_IDL_handler_until.idChart_Chart_1)
152
       (= chart_chart__CHART_A_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
153
       (= chart_chart__CHART_A_IDL_handler_until.chart_chart__restart_in true)
154
       )
155
  (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)
156
))
157

    
158
; chart_chart__CHART_A_IDL_unless
159
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__restart_in Bool)
160
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__state_in chart_chart__type)
161
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__restart_act Bool)
162
(declare-var chart_chart__CHART_A_IDL_unless.chart_chart__state_act chart_chart__type)
163
(declare-rel chart_chart__CHART_A_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
164
(rule (=> 
165
  (and (= chart_chart__CHART_A_IDL_unless.chart_chart__state_act chart_chart__CHART_A_IDL_unless.chart_chart__state_in)
166
       (= chart_chart__CHART_A_IDL_unless.chart_chart__restart_act chart_chart__CHART_A_IDL_unless.chart_chart__restart_in)
167
       )
168
  (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)
169
))
170

    
171
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until
172
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_1 Int)
173
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.x Int)
174
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_1 Int)
175
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_1 Int)
176
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.chart_chart__restart_in Bool)
177
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.chart_chart__state_in chart_chart__type)
178
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_out Int)
179
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_out Int)
180
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_out Int)
181
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 Bool)
182
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_10 Int)
183
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 Bool)
184
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_3 Int)
185
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_4 Int)
186
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_5 Int)
187
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_6 Int)
188
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_7 Int)
189
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_8 Int)
190
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_9 Int)
191
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart Int)
192
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_2 Int)
193
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_3 Int)
194
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_4 Int)
195
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_5 Int)
196
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y Int)
197
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_2 Int)
198
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_3 Int)
199
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_4 Int)
200
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_5 Int)
201
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z Int)
202
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_2 Int)
203
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_3 Int)
204
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_4 Int)
205
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_5 Int)
206
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until (Int Int Int Int Bool chart_chart__type Int Int Int))
207
(rule (=> 
208
  (and (Chart_A__To__Chart_ChartJunction1192_1_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_1
209
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_5)
210
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 (<= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.x 2))
211
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
212
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_5))
213
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
214
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_1))
215
       )
216
       (Chart_ChartJunction1192__To__Chart_C_2_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_4
217
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_4)
218
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
219
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_4))
220
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
221
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_4))
222
       )
223
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 (> chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.x 2))
224
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 true))
225
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_5))
226
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 false))
227
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_1))
228
       )
229
       (Chart_ChartJunction1192__To__Chart_B_1_Transition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_2
230
                                                                 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_9)
231
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 false))
232
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_2)
233
                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
234
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_5))
235
                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
236
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_1))
237
                    )
238
                    ))
239
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 true))
240
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_9)
241
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_3)
242
                    ))
243
       )
244
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z)
245
       (Chart_A__To__Chart_ChartJunction1192_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_1
246
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_4)
247
       (Chart_ChartJunction1192__To__Chart_C_2_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_4
248
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_7)
249
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
250
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_7))
251
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
252
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_4))
253
       )
254
       (Chart_A__To__Chart_ChartJunction1192_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_1
255
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_2)
256
       (Chart_ChartJunction1192__To__Chart_B_1_Condition_Action chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_2
257
                                                                chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_10)
258
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 false))
259
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_2)
260
                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
261
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_5))
262
                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
263
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_4))
264
                    )
265
                    ))
266
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 true))
267
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_10)
268
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_3)
269
                    ))
270
       )
271
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y)
272
       (Chart_A_ex chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_1
273
                   false
274
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_6)
275
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
276
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_6))
277
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
278
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_4 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_1))
279
       )
280
       (Chart_C_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_4
281
                   false
282
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_3)
283
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
284
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_3))
285
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
286
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_5 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_4))
287
       )
288
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 true))
289
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_6))
290
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 false))
291
               (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_2 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_1))
292
       )
293
       (Chart_B_en chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_2
294
                   false
295
                   chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_8)
296
       (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 false))
297
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_2)
298
                    (and (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 true))
299
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_5))
300
                         (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_2 false))
301
                            (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_1))
302
                    )
303
                    ))
304
            (or (not (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_1 true))
305
               (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_3 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.__chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until_8)
306
                    (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_3)
307
                    ))
308
       )
309
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart)
310
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.chart_chart__state_in POINTChart_Chart)
311
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.chart_chart__restart_in true)
312
       )
313
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.x chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_1 chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.idChart_Chart_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.y_out chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until.z_out)
314
))
315

    
316
; chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless
317
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__restart_in Bool)
318
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__state_in chart_chart__type)
319
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__restart_act Bool)
320
(declare-var chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__state_act chart_chart__type)
321
(declare-rel chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless (Bool chart_chart__type Bool chart_chart__type))
322
(rule (=> 
323
  (and (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__state_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__state_in)
324
       (= chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__restart_in)
325
       )
326
  (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__restart_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__state_in chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__restart_act chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless.chart_chart__state_act)
327
))
328

    
329
; chart_chart__CHART_B_IDL_handler_until
330
(declare-var chart_chart__CHART_B_IDL_handler_until.idChart_Chart_1 Int)
331
(declare-var chart_chart__CHART_B_IDL_handler_until.y_1 Int)
332
(declare-var chart_chart__CHART_B_IDL_handler_until.z_1 Int)
333
(declare-var chart_chart__CHART_B_IDL_handler_until.chart_chart__restart_in Bool)
334
(declare-var chart_chart__CHART_B_IDL_handler_until.chart_chart__state_in chart_chart__type)
335
(declare-var chart_chart__CHART_B_IDL_handler_until.idChart_Chart_out Int)
336
(declare-var chart_chart__CHART_B_IDL_handler_until.y_out Int)
337
(declare-var chart_chart__CHART_B_IDL_handler_until.z_out Int)
338
(declare-rel chart_chart__CHART_B_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
339
(rule (=> 
340
  (and (= chart_chart__CHART_B_IDL_handler_until.z_out chart_chart__CHART_B_IDL_handler_until.z_1)
341
       (= chart_chart__CHART_B_IDL_handler_until.y_out chart_chart__CHART_B_IDL_handler_until.y_1)
342
       (= chart_chart__CHART_B_IDL_handler_until.idChart_Chart_out chart_chart__CHART_B_IDL_handler_until.idChart_Chart_1)
343
       (= chart_chart__CHART_B_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
344
       (= chart_chart__CHART_B_IDL_handler_until.chart_chart__restart_in true)
345
       )
346
  (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)
347
))
348

    
349
; chart_chart__CHART_B_IDL_unless
350
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__restart_in Bool)
351
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__state_in chart_chart__type)
352
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__restart_act Bool)
353
(declare-var chart_chart__CHART_B_IDL_unless.chart_chart__state_act chart_chart__type)
354
(declare-rel chart_chart__CHART_B_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
355
(rule (=> 
356
  (and (= chart_chart__CHART_B_IDL_unless.chart_chart__state_act chart_chart__CHART_B_IDL_unless.chart_chart__state_in)
357
       (= chart_chart__CHART_B_IDL_unless.chart_chart__restart_act chart_chart__CHART_B_IDL_unless.chart_chart__restart_in)
358
       )
359
  (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)
360
))
361

    
362
; chart_chart__CHART_B__TO__CHART_A_1_handler_until
363
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
364
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_1 Int)
365
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_1 Int)
366
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
367
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
368
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
369
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_out Int)
370
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.z_out Int)
371
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
372
(declare-var chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_3 Int)
373
(declare-rel chart_chart__CHART_B__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
374
(rule (=> 
375
  (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)
376
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_B__TO__CHART_A_1_handler_until.y_1)
377
       (Chart_B_ex chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_1
378
                   false
379
                   chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2)
380
       (Chart_A_en chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_2
381
                   false
382
                   chart_chart__CHART_B__TO__CHART_A_1_handler_until.idChart_Chart_3)
383
       (= 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)
384
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
385
       (= chart_chart__CHART_B__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
386
       )
387
  (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)
388
))
389

    
390
; chart_chart__CHART_B__TO__CHART_A_1_unless
391
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
392
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
393
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
394
(declare-var chart_chart__CHART_B__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
395
(declare-rel chart_chart__CHART_B__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
396
(rule (=> 
397
  (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)
398
       (= 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)
399
       )
400
  (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)
401
))
402

    
403
; chart_chart__CHART_C_IDL_handler_until
404
(declare-var chart_chart__CHART_C_IDL_handler_until.idChart_Chart_1 Int)
405
(declare-var chart_chart__CHART_C_IDL_handler_until.y_1 Int)
406
(declare-var chart_chart__CHART_C_IDL_handler_until.z_1 Int)
407
(declare-var chart_chart__CHART_C_IDL_handler_until.chart_chart__restart_in Bool)
408
(declare-var chart_chart__CHART_C_IDL_handler_until.chart_chart__state_in chart_chart__type)
409
(declare-var chart_chart__CHART_C_IDL_handler_until.idChart_Chart_out Int)
410
(declare-var chart_chart__CHART_C_IDL_handler_until.y_out Int)
411
(declare-var chart_chart__CHART_C_IDL_handler_until.z_out Int)
412
(declare-rel chart_chart__CHART_C_IDL_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
413
(rule (=> 
414
  (and (= chart_chart__CHART_C_IDL_handler_until.z_out chart_chart__CHART_C_IDL_handler_until.z_1)
415
       (= chart_chart__CHART_C_IDL_handler_until.y_out chart_chart__CHART_C_IDL_handler_until.y_1)
416
       (= chart_chart__CHART_C_IDL_handler_until.idChart_Chart_out chart_chart__CHART_C_IDL_handler_until.idChart_Chart_1)
417
       (= chart_chart__CHART_C_IDL_handler_until.chart_chart__state_in POINTChart_Chart)
418
       (= chart_chart__CHART_C_IDL_handler_until.chart_chart__restart_in true)
419
       )
420
  (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)
421
))
422

    
423
; chart_chart__CHART_C_IDL_unless
424
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__restart_in Bool)
425
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__state_in chart_chart__type)
426
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__restart_act Bool)
427
(declare-var chart_chart__CHART_C_IDL_unless.chart_chart__state_act chart_chart__type)
428
(declare-rel chart_chart__CHART_C_IDL_unless (Bool chart_chart__type Bool chart_chart__type))
429
(rule (=> 
430
  (and (= chart_chart__CHART_C_IDL_unless.chart_chart__state_act chart_chart__CHART_C_IDL_unless.chart_chart__state_in)
431
       (= chart_chart__CHART_C_IDL_unless.chart_chart__restart_act chart_chart__CHART_C_IDL_unless.chart_chart__restart_in)
432
       )
433
  (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)
434
))
435

    
436
; chart_chart__CHART_C__TO__CHART_A_1_handler_until
437
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
438
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_1 Int)
439
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_1 Int)
440
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
441
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
442
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
443
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_out Int)
444
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.z_out Int)
445
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
446
(declare-var chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_3 Int)
447
(declare-rel chart_chart__CHART_C__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
448
(rule (=> 
449
  (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)
450
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_out chart_chart__CHART_C__TO__CHART_A_1_handler_until.y_1)
451
       (Chart_C_ex chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_1
452
                   false
453
                   chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2)
454
       (Chart_A_en chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_2
455
                   false
456
                   chart_chart__CHART_C__TO__CHART_A_1_handler_until.idChart_Chart_3)
457
       (= 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)
458
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
459
       (= chart_chart__CHART_C__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
460
       )
461
  (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)
462
))
463

    
464
; chart_chart__CHART_C__TO__CHART_A_1_unless
465
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
466
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
467
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
468
(declare-var chart_chart__CHART_C__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
469
(declare-rel chart_chart__CHART_C__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
470
(rule (=> 
471
  (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)
472
       (= 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)
473
       )
474
  (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)
475
))
476

    
477
; chart_chart__POINTChart_Chart_handler_until
478
(declare-var chart_chart__POINTChart_Chart_handler_until.idChart_Chart_1 Int)
479
(declare-var chart_chart__POINTChart_Chart_handler_until.y_1 Int)
480
(declare-var chart_chart__POINTChart_Chart_handler_until.z_1 Int)
481
(declare-var chart_chart__POINTChart_Chart_handler_until.chart_chart__restart_in Bool)
482
(declare-var chart_chart__POINTChart_Chart_handler_until.chart_chart__state_in chart_chart__type)
483
(declare-var chart_chart__POINTChart_Chart_handler_until.idChart_Chart_out Int)
484
(declare-var chart_chart__POINTChart_Chart_handler_until.y_out Int)
485
(declare-var chart_chart__POINTChart_Chart_handler_until.z_out Int)
486
(declare-rel chart_chart__POINTChart_Chart_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
487
(rule (=> 
488
  (and (= chart_chart__POINTChart_Chart_handler_until.z_out chart_chart__POINTChart_Chart_handler_until.z_1)
489
       (= chart_chart__POINTChart_Chart_handler_until.y_out chart_chart__POINTChart_Chart_handler_until.y_1)
490
       (= chart_chart__POINTChart_Chart_handler_until.idChart_Chart_out chart_chart__POINTChart_Chart_handler_until.idChart_Chart_1)
491
       (= chart_chart__POINTChart_Chart_handler_until.chart_chart__state_in POINTChart_Chart)
492
       (= chart_chart__POINTChart_Chart_handler_until.chart_chart__restart_in false)
493
       )
494
  (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)
495
))
496

    
497
; chart_chart__POINTChart_Chart_unless
498
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__restart_in Bool)
499
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__state_in chart_chart__type)
500
(declare-var chart_chart__POINTChart_Chart_unless.idChart_Chart_1 Int)
501
(declare-var chart_chart__POINTChart_Chart_unless.E1 Bool)
502
(declare-var chart_chart__POINTChart_Chart_unless.x Int)
503
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__restart_act Bool)
504
(declare-var chart_chart__POINTChart_Chart_unless.chart_chart__state_act chart_chart__type)
505
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 Bool)
506
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 Bool)
507
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 Bool)
508
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 Bool)
509
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 Bool)
510
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 Bool)
511
(declare-var chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 Bool)
512
(declare-rel chart_chart__POINTChart_Chart_unless (Bool chart_chart__type Int Bool Int Bool chart_chart__type))
513
(rule (=> 
514
  (and (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1187))
515
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1186))
516
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1185))
517
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1187) (> chart_chart__POINTChart_Chart_unless.x 3)))
518
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1186) (> chart_chart__POINTChart_Chart_unless.x 3)))
519
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 (and (and (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 1185) chart_chart__POINTChart_Chart_unless.E1) (> chart_chart__POINTChart_Chart_unless.x 0)))
520
       (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 (= chart_chart__POINTChart_Chart_unless.idChart_Chart_1 0))
521
       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 false))
522
               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 false))
523
                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 false))
524
                               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 false))
525
                                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 false))
526
                                               (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 false))
527
                                                       (and (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 false))
528
                                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act chart_chart__POINTChart_Chart_unless.chart_chart__state_in)
529
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act chart_chart__POINTChart_Chart_unless.chart_chart__restart_in)
530
                                                                    ))
531
                                                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_7 true))
532
                                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_C_IDL)
533
                                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
534
                                                                    ))
535
                                                       ))
536
                                                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_6 true))
537
                                                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_B_IDL)
538
                                                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
539
                                                            ))
540
                                               ))
541
                                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_5 true))
542
                                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_A_IDL)
543
                                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
544
                                                    ))
545
                                       ))
546
                                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_4 true))
547
                                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_C__TO__CHART_A_1)
548
                                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
549
                                            ))
550
                               ))
551
                            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_3 true))
552
                               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_B__TO__CHART_A_1)
553
                                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
554
                                    ))
555
                       ))
556
                    (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_2 true))
557
                       (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1192_1)
558
                            (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
559
                            ))
560
               ))
561
            (or (not (= chart_chart__POINTChart_Chart_unless.__chart_chart__POINTChart_Chart_unless_1 true))
562
               (and (= chart_chart__POINTChart_Chart_unless.chart_chart__state_act POINT__TO__CHART_A_1)
563
                    (= chart_chart__POINTChart_Chart_unless.chart_chart__restart_act true)
564
                    ))
565
       )
566
       )
567
  (chart_chart__POINTChart_Chart_unless chart_chart__POINTChart_Chart_unless.chart_chart__restart_in chart_chart__POINTChart_Chart_unless.chart_chart__state_in chart_chart__POINTChart_Chart_unless.idChart_Chart_1 chart_chart__POINTChart_Chart_unless.E1 chart_chart__POINTChart_Chart_unless.x chart_chart__POINTChart_Chart_unless.chart_chart__restart_act chart_chart__POINTChart_Chart_unless.chart_chart__state_act)
568
))
569

    
570
; chart_chart__POINT__TO__CHART_A_1_handler_until
571
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_1 Int)
572
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.y_1 Int)
573
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.z_1 Int)
574
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__restart_in Bool)
575
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__state_in chart_chart__type)
576
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_out Int)
577
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.y_out Int)
578
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.z_out Int)
579
(declare-var chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2 Int)
580
(declare-rel chart_chart__POINT__TO__CHART_A_1_handler_until (Int Int Int Bool chart_chart__type Int Int Int))
581
(rule (=> 
582
  (and (= chart_chart__POINT__TO__CHART_A_1_handler_until.z_out chart_chart__POINT__TO__CHART_A_1_handler_until.z_1)
583
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.y_out chart_chart__POINT__TO__CHART_A_1_handler_until.y_1)
584
       (Chart_A_en chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_1
585
                   false
586
                   chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2)
587
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_out chart_chart__POINT__TO__CHART_A_1_handler_until.idChart_Chart_2)
588
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__state_in POINTChart_Chart)
589
       (= chart_chart__POINT__TO__CHART_A_1_handler_until.chart_chart__restart_in true)
590
       )
591
  (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)
592
))
593

    
594
; chart_chart__POINT__TO__CHART_A_1_unless
595
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_in Bool)
596
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_in chart_chart__type)
597
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_act Bool)
598
(declare-var chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__state_act chart_chart__type)
599
(declare-rel chart_chart__POINT__TO__CHART_A_1_unless (Bool chart_chart__type Bool chart_chart__type))
600
(rule (=> 
601
  (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)
602
       (= chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_act chart_chart__POINT__TO__CHART_A_1_unless.chart_chart__restart_in)
603
       )
604
  (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)
605
))
606

    
607
; Chart_Chart_node
608
(declare-var Chart_Chart_node.idChart_Chart_1 Int)
609
(declare-var Chart_Chart_node.E1 Bool)
610
(declare-var Chart_Chart_node.x Int)
611
(declare-var Chart_Chart_node.y_1 Int)
612
(declare-var Chart_Chart_node.z_1 Int)
613
(declare-var Chart_Chart_node.idChart_Chart Int)
614
(declare-var Chart_Chart_node.y Int)
615
(declare-var Chart_Chart_node.z Int)
616
(declare-var Chart_Chart_node.__Chart_Chart_node_58_c Bool)
617
(declare-var Chart_Chart_node.__Chart_Chart_node_59_c chart_chart__type)
618
(declare-var Chart_Chart_node.ni_4._arrow._first_c Bool)
619
(declare-var Chart_Chart_node.__Chart_Chart_node_58_m Bool)
620
(declare-var Chart_Chart_node.__Chart_Chart_node_59_m chart_chart__type)
621
(declare-var Chart_Chart_node.ni_4._arrow._first_m Bool)
622
(declare-var Chart_Chart_node.__Chart_Chart_node_58_x Bool)
623
(declare-var Chart_Chart_node.__Chart_Chart_node_59_x chart_chart__type)
624
(declare-var Chart_Chart_node.ni_4._arrow._first_x Bool)
625
(declare-var Chart_Chart_node.__Chart_Chart_node_1 Bool)
626
(declare-var Chart_Chart_node.__Chart_Chart_node_10 chart_chart__type)
627
(declare-var Chart_Chart_node.__Chart_Chart_node_11 Bool)
628
(declare-var Chart_Chart_node.__Chart_Chart_node_12 chart_chart__type)
629
(declare-var Chart_Chart_node.__Chart_Chart_node_13 Bool)
630
(declare-var Chart_Chart_node.__Chart_Chart_node_14 chart_chart__type)
631
(declare-var Chart_Chart_node.__Chart_Chart_node_15 Bool)
632
(declare-var Chart_Chart_node.__Chart_Chart_node_16 chart_chart__type)
633
(declare-var Chart_Chart_node.__Chart_Chart_node_17 Bool)
634
(declare-var Chart_Chart_node.__Chart_Chart_node_18 chart_chart__type)
635
(declare-var Chart_Chart_node.__Chart_Chart_node_19 Int)
636
(declare-var Chart_Chart_node.__Chart_Chart_node_2 chart_chart__type)
637
(declare-var Chart_Chart_node.__Chart_Chart_node_20 Int)
638
(declare-var Chart_Chart_node.__Chart_Chart_node_21 Int)
639
(declare-var Chart_Chart_node.__Chart_Chart_node_22 Bool)
640
(declare-var Chart_Chart_node.__Chart_Chart_node_23 chart_chart__type)
641
(declare-var Chart_Chart_node.__Chart_Chart_node_24 Int)
642
(declare-var Chart_Chart_node.__Chart_Chart_node_25 Int)
643
(declare-var Chart_Chart_node.__Chart_Chart_node_26 Int)
644
(declare-var Chart_Chart_node.__Chart_Chart_node_27 Bool)
645
(declare-var Chart_Chart_node.__Chart_Chart_node_28 chart_chart__type)
646
(declare-var Chart_Chart_node.__Chart_Chart_node_29 Int)
647
(declare-var Chart_Chart_node.__Chart_Chart_node_3 Bool)
648
(declare-var Chart_Chart_node.__Chart_Chart_node_30 Int)
649
(declare-var Chart_Chart_node.__Chart_Chart_node_31 Int)
650
(declare-var Chart_Chart_node.__Chart_Chart_node_32 Bool)
651
(declare-var Chart_Chart_node.__Chart_Chart_node_33 chart_chart__type)
652
(declare-var Chart_Chart_node.__Chart_Chart_node_34 Int)
653
(declare-var Chart_Chart_node.__Chart_Chart_node_35 Int)
654
(declare-var Chart_Chart_node.__Chart_Chart_node_36 Int)
655
(declare-var Chart_Chart_node.__Chart_Chart_node_37 Bool)
656
(declare-var Chart_Chart_node.__Chart_Chart_node_38 chart_chart__type)
657
(declare-var Chart_Chart_node.__Chart_Chart_node_39 Int)
658
(declare-var Chart_Chart_node.__Chart_Chart_node_4 chart_chart__type)
659
(declare-var Chart_Chart_node.__Chart_Chart_node_40 Int)
660
(declare-var Chart_Chart_node.__Chart_Chart_node_41 Int)
661
(declare-var Chart_Chart_node.__Chart_Chart_node_42 Bool)
662
(declare-var Chart_Chart_node.__Chart_Chart_node_43 chart_chart__type)
663
(declare-var Chart_Chart_node.__Chart_Chart_node_44 Int)
664
(declare-var Chart_Chart_node.__Chart_Chart_node_45 Int)
665
(declare-var Chart_Chart_node.__Chart_Chart_node_46 Int)
666
(declare-var Chart_Chart_node.__Chart_Chart_node_47 Bool)
667
(declare-var Chart_Chart_node.__Chart_Chart_node_48 chart_chart__type)
668
(declare-var Chart_Chart_node.__Chart_Chart_node_49 Int)
669
(declare-var Chart_Chart_node.__Chart_Chart_node_5 Bool)
670
(declare-var Chart_Chart_node.__Chart_Chart_node_50 Int)
671
(declare-var Chart_Chart_node.__Chart_Chart_node_51 Int)
672
(declare-var Chart_Chart_node.__Chart_Chart_node_52 Bool)
673
(declare-var Chart_Chart_node.__Chart_Chart_node_53 chart_chart__type)
674
(declare-var Chart_Chart_node.__Chart_Chart_node_54 Int)
675
(declare-var Chart_Chart_node.__Chart_Chart_node_55 Int)
676
(declare-var Chart_Chart_node.__Chart_Chart_node_56 Int)
677
(declare-var Chart_Chart_node.__Chart_Chart_node_57 Bool)
678
(declare-var Chart_Chart_node.__Chart_Chart_node_6 chart_chart__type)
679
(declare-var Chart_Chart_node.__Chart_Chart_node_7 Bool)
680
(declare-var Chart_Chart_node.__Chart_Chart_node_8 chart_chart__type)
681
(declare-var Chart_Chart_node.__Chart_Chart_node_9 Bool)
682
(declare-var Chart_Chart_node.chart_chart__next_restart_in Bool)
683
(declare-var Chart_Chart_node.chart_chart__next_state_in chart_chart__type)
684
(declare-var Chart_Chart_node.chart_chart__restart_act Bool)
685
(declare-var Chart_Chart_node.chart_chart__restart_in Bool)
686
(declare-var Chart_Chart_node.chart_chart__state_act chart_chart__type)
687
(declare-var Chart_Chart_node.chart_chart__state_in chart_chart__type)
688
(declare-rel Chart_Chart_node_reset (Bool chart_chart__type Bool Bool chart_chart__type Bool))
689
(declare-rel Chart_Chart_node_step (Int Bool Int Int Int Int Int Int Bool chart_chart__type Bool Bool chart_chart__type Bool))
690

    
691
(rule (=> 
692
  (and 
693
       (= Chart_Chart_node.__Chart_Chart_node_58_m Chart_Chart_node.__Chart_Chart_node_58_c)
694
       (= Chart_Chart_node.__Chart_Chart_node_59_m Chart_Chart_node.__Chart_Chart_node_59_c)
695
       (= Chart_Chart_node.ni_4._arrow._first_m true)
696
  )
697
  (Chart_Chart_node_reset Chart_Chart_node.__Chart_Chart_node_58_c
698
                          Chart_Chart_node.__Chart_Chart_node_59_c
699
                          Chart_Chart_node.ni_4._arrow._first_c
700
                          Chart_Chart_node.__Chart_Chart_node_58_m
701
                          Chart_Chart_node.__Chart_Chart_node_59_m
702
                          Chart_Chart_node.ni_4._arrow._first_m)
703
))
704

    
705
(rule (=> 
706
  (and (= Chart_Chart_node.ni_4._arrow._first_m Chart_Chart_node.ni_4._arrow._first_c)
707
       (and (= Chart_Chart_node.__Chart_Chart_node_57 (ite Chart_Chart_node.ni_4._arrow._first_m true false))
708
            (= Chart_Chart_node.ni_4._arrow._first_x false))
709
       (and (or (not (= Chart_Chart_node.__Chart_Chart_node_57 false))
710
               (and (= Chart_Chart_node.chart_chart__state_in Chart_Chart_node.__Chart_Chart_node_59_c)
711
                    (= Chart_Chart_node.chart_chart__restart_in Chart_Chart_node.__Chart_Chart_node_58_c)
712
                    ))
713
            (or (not (= Chart_Chart_node.__Chart_Chart_node_57 true))
714
               (and (= Chart_Chart_node.chart_chart__state_in POINTChart_Chart)
715
                    (= Chart_Chart_node.chart_chart__restart_in false)
716
                    ))
717
       )
718
       (and (or (not (= Chart_Chart_node.chart_chart__state_in CHART_A_IDL))
719
               (and (chart_chart__CHART_A_IDL_unless Chart_Chart_node.chart_chart__restart_in
720
                                                     Chart_Chart_node.chart_chart__state_in
721
                                                     Chart_Chart_node.__Chart_Chart_node_5
722
                                                     Chart_Chart_node.__Chart_Chart_node_6)
723
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_6)
724
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_5)
725
                    ))
726
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_A__TO__CHART_CHARTJUNCTION1192_1))
727
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_unless 
728
                    Chart_Chart_node.chart_chart__restart_in
729
                    Chart_Chart_node.chart_chart__state_in
730
                    Chart_Chart_node.__Chart_Chart_node_11
731
                    Chart_Chart_node.__Chart_Chart_node_12)
732
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_12)
733
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_11)
734
                    ))
735
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_B_IDL))
736
               (and (chart_chart__CHART_B_IDL_unless Chart_Chart_node.chart_chart__restart_in
737
                                                     Chart_Chart_node.chart_chart__state_in
738
                                                     Chart_Chart_node.__Chart_Chart_node_3
739
                                                     Chart_Chart_node.__Chart_Chart_node_4)
740
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_4)
741
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_3)
742
                    ))
743
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_B__TO__CHART_A_1))
744
               (and (chart_chart__CHART_B__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
745
                                                                Chart_Chart_node.chart_chart__state_in
746
                                                                Chart_Chart_node.__Chart_Chart_node_9
747
                                                                Chart_Chart_node.__Chart_Chart_node_10)
748
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_10)
749
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_9)
750
                    ))
751
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_C_IDL))
752
               (and (chart_chart__CHART_C_IDL_unless Chart_Chart_node.chart_chart__restart_in
753
                                                     Chart_Chart_node.chart_chart__state_in
754
                                                     Chart_Chart_node.__Chart_Chart_node_1
755
                                                     Chart_Chart_node.__Chart_Chart_node_2)
756
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_2)
757
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_1)
758
                    ))
759
            (or (not (= Chart_Chart_node.chart_chart__state_in CHART_C__TO__CHART_A_1))
760
               (and (chart_chart__CHART_C__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
761
                                                                Chart_Chart_node.chart_chart__state_in
762
                                                                Chart_Chart_node.__Chart_Chart_node_7
763
                                                                Chart_Chart_node.__Chart_Chart_node_8)
764
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_8)
765
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_7)
766
                    ))
767
            (or (not (= Chart_Chart_node.chart_chart__state_in POINTChart_Chart))
768
               (and (chart_chart__POINTChart_Chart_unless Chart_Chart_node.chart_chart__restart_in
769
                                                          Chart_Chart_node.chart_chart__state_in
770
                                                          Chart_Chart_node.idChart_Chart_1
771
                                                          Chart_Chart_node.E1
772
                                                          Chart_Chart_node.x
773
                                                          Chart_Chart_node.__Chart_Chart_node_15
774
                                                          Chart_Chart_node.__Chart_Chart_node_16)
775
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_16)
776
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_15)
777
                    ))
778
            (or (not (= Chart_Chart_node.chart_chart__state_in POINT__TO__CHART_A_1))
779
               (and (chart_chart__POINT__TO__CHART_A_1_unless Chart_Chart_node.chart_chart__restart_in
780
                                                              Chart_Chart_node.chart_chart__state_in
781
                                                              Chart_Chart_node.__Chart_Chart_node_13
782
                                                              Chart_Chart_node.__Chart_Chart_node_14)
783
                    (= Chart_Chart_node.chart_chart__state_act Chart_Chart_node.__Chart_Chart_node_14)
784
                    (= Chart_Chart_node.chart_chart__restart_act Chart_Chart_node.__Chart_Chart_node_13)
785
                    ))
786
       )
787
       (and (or (not (= Chart_Chart_node.chart_chart__state_act CHART_A_IDL))
788
               (and (chart_chart__CHART_A_IDL_handler_until Chart_Chart_node.idChart_Chart_1
789
                                                            Chart_Chart_node.y_1
790
                                                            Chart_Chart_node.z_1
791
                                                            Chart_Chart_node.__Chart_Chart_node_27
792
                                                            Chart_Chart_node.__Chart_Chart_node_28
793
                                                            Chart_Chart_node.__Chart_Chart_node_29
794
                                                            Chart_Chart_node.__Chart_Chart_node_30
795
                                                            Chart_Chart_node.__Chart_Chart_node_31)
796
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_31)
797
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_30)
798
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_29)
799
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_28)
800
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_27)
801
                    ))
802
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_A__TO__CHART_CHARTJUNCTION1192_1))
803
               (and (chart_chart__CHART_A__TO__CHART_CHARTJUNCTION1192_1_handler_until 
804
                    Chart_Chart_node.idChart_Chart_1
805
                    Chart_Chart_node.x
806
                    Chart_Chart_node.y_1
807
                    Chart_Chart_node.z_1
808
                    Chart_Chart_node.__Chart_Chart_node_42
809
                    Chart_Chart_node.__Chart_Chart_node_43
810
                    Chart_Chart_node.__Chart_Chart_node_44
811
                    Chart_Chart_node.__Chart_Chart_node_45
812
                    Chart_Chart_node.__Chart_Chart_node_46)
813
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_46)
814
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_45)
815
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_44)
816
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_43)
817
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_42)
818
                    ))
819
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_B_IDL))
820
               (and (chart_chart__CHART_B_IDL_handler_until Chart_Chart_node.idChart_Chart_1
821
                                                            Chart_Chart_node.y_1
822
                                                            Chart_Chart_node.z_1
823
                                                            Chart_Chart_node.__Chart_Chart_node_22
824
                                                            Chart_Chart_node.__Chart_Chart_node_23
825
                                                            Chart_Chart_node.__Chart_Chart_node_24
826
                                                            Chart_Chart_node.__Chart_Chart_node_25
827
                                                            Chart_Chart_node.__Chart_Chart_node_26)
828
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_26)
829
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_25)
830
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_24)
831
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_23)
832
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_22)
833
                    ))
834
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_B__TO__CHART_A_1))
835
               (and (chart_chart__CHART_B__TO__CHART_A_1_handler_until 
836
                    Chart_Chart_node.idChart_Chart_1
837
                    Chart_Chart_node.y_1
838
                    Chart_Chart_node.z_1
839
                    Chart_Chart_node.__Chart_Chart_node_37
840
                    Chart_Chart_node.__Chart_Chart_node_38
841
                    Chart_Chart_node.__Chart_Chart_node_39
842
                    Chart_Chart_node.__Chart_Chart_node_40
843
                    Chart_Chart_node.__Chart_Chart_node_41)
844
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_41)
845
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_40)
846
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_39)
847
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_38)
848
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_37)
849
                    ))
850
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_C_IDL))
851
               (and (chart_chart__CHART_C_IDL_handler_until Chart_Chart_node.idChart_Chart_1
852
                                                            Chart_Chart_node.y_1
853
                                                            Chart_Chart_node.z_1
854
                                                            Chart_Chart_node.__Chart_Chart_node_17
855
                                                            Chart_Chart_node.__Chart_Chart_node_18
856
                                                            Chart_Chart_node.__Chart_Chart_node_19
857
                                                            Chart_Chart_node.__Chart_Chart_node_20
858
                                                            Chart_Chart_node.__Chart_Chart_node_21)
859
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_21)
860
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_20)
861
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_19)
862
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_18)
863
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_17)
864
                    ))
865
            (or (not (= Chart_Chart_node.chart_chart__state_act CHART_C__TO__CHART_A_1))
866
               (and (chart_chart__CHART_C__TO__CHART_A_1_handler_until 
867
                    Chart_Chart_node.idChart_Chart_1
868
                    Chart_Chart_node.y_1
869
                    Chart_Chart_node.z_1
870
                    Chart_Chart_node.__Chart_Chart_node_32
871
                    Chart_Chart_node.__Chart_Chart_node_33
872
                    Chart_Chart_node.__Chart_Chart_node_34
873
                    Chart_Chart_node.__Chart_Chart_node_35
874
                    Chart_Chart_node.__Chart_Chart_node_36)
875
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_36)
876
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_35)
877
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_34)
878
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_33)
879
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_32)
880
                    ))
881
            (or (not (= Chart_Chart_node.chart_chart__state_act POINTChart_Chart))
882
               (and (chart_chart__POINTChart_Chart_handler_until Chart_Chart_node.idChart_Chart_1
883
                                                                 Chart_Chart_node.y_1
884
                                                                 Chart_Chart_node.z_1
885
                                                                 Chart_Chart_node.__Chart_Chart_node_52
886
                                                                 Chart_Chart_node.__Chart_Chart_node_53
887
                                                                 Chart_Chart_node.__Chart_Chart_node_54
888
                                                                 Chart_Chart_node.__Chart_Chart_node_55
889
                                                                 Chart_Chart_node.__Chart_Chart_node_56)
890
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_56)
891
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_55)
892
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_54)
893
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_53)
894
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_52)
895
                    ))
896
            (or (not (= Chart_Chart_node.chart_chart__state_act POINT__TO__CHART_A_1))
897
               (and (chart_chart__POINT__TO__CHART_A_1_handler_until 
898
                    Chart_Chart_node.idChart_Chart_1
899
                    Chart_Chart_node.y_1
900
                    Chart_Chart_node.z_1
901
                    Chart_Chart_node.__Chart_Chart_node_47
902
                    Chart_Chart_node.__Chart_Chart_node_48
903
                    Chart_Chart_node.__Chart_Chart_node_49
904
                    Chart_Chart_node.__Chart_Chart_node_50
905
                    Chart_Chart_node.__Chart_Chart_node_51)
906
                    (= Chart_Chart_node.z Chart_Chart_node.__Chart_Chart_node_51)
907
                    (= Chart_Chart_node.y Chart_Chart_node.__Chart_Chart_node_50)
908
                    (= Chart_Chart_node.idChart_Chart Chart_Chart_node.__Chart_Chart_node_49)
909
                    (= Chart_Chart_node.chart_chart__next_state_in Chart_Chart_node.__Chart_Chart_node_48)
910
                    (= Chart_Chart_node.chart_chart__next_restart_in Chart_Chart_node.__Chart_Chart_node_47)
911
                    ))
912
       )
913
       (= Chart_Chart_node.__Chart_Chart_node_59_x Chart_Chart_node.chart_chart__next_state_in)
914
       (= Chart_Chart_node.__Chart_Chart_node_58_x Chart_Chart_node.chart_chart__next_restart_in)
915
       )
916
  (Chart_Chart_node_step Chart_Chart_node.idChart_Chart_1
917
                         Chart_Chart_node.E1
918
                         Chart_Chart_node.x
919
                         Chart_Chart_node.y_1
920
                         Chart_Chart_node.z_1
921
                         Chart_Chart_node.idChart_Chart
922
                         Chart_Chart_node.y
923
                         Chart_Chart_node.z
924
                         Chart_Chart_node.__Chart_Chart_node_58_c
925
                         Chart_Chart_node.__Chart_Chart_node_59_c
926
                         Chart_Chart_node.ni_4._arrow._first_c
927
                         Chart_Chart_node.__Chart_Chart_node_58_x
928
                         Chart_Chart_node.__Chart_Chart_node_59_x
929
                         Chart_Chart_node.ni_4._arrow._first_x)
930
))
931

    
932
; Junctions1V0_Chart
933
(declare-var Junctions1V0_Chart.x Int)
934
(declare-var Junctions1V0_Chart.E1 Bool)
935
(declare-var Junctions1V0_Chart.y Int)
936
(declare-var Junctions1V0_Chart.z Int)
937
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_5_c Int)
938
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_6_c Int)
939
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_7_c Int)
940
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c Bool)
941
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c chart_chart__type)
942
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c Bool)
943
(declare-var Junctions1V0_Chart.ni_3._arrow._first_c Bool)
944
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_5_m Int)
945
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_6_m Int)
946
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_7_m Int)
947
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Bool)
948
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m chart_chart__type)
949
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Bool)
950
(declare-var Junctions1V0_Chart.ni_3._arrow._first_m Bool)
951
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_5_x Int)
952
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_6_x Int)
953
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_7_x Int)
954
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x Bool)
955
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x chart_chart__type)
956
(declare-var Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x Bool)
957
(declare-var Junctions1V0_Chart.ni_3._arrow._first_x Bool)
958
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_1 Int)
959
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_2 Int)
960
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_3 Int)
961
(declare-var Junctions1V0_Chart.__Junctions1V0_Chart_4 Bool)
962
(declare-var Junctions1V0_Chart.idChart_Chart Int)
963
(declare-var Junctions1V0_Chart.idChart_Chart_1 Int)
964
(declare-var Junctions1V0_Chart.y_1 Int)
965
(declare-var Junctions1V0_Chart.z_1 Int)
966
(declare-rel Junctions1V0_Chart_reset (Int Int Int Bool chart_chart__type Bool Bool Int Int Int Bool chart_chart__type Bool Bool))
967
(declare-rel Junctions1V0_Chart_step (Int Bool Int Int Int Int Int Bool chart_chart__type Bool Bool Int Int Int Bool chart_chart__type Bool Bool))
968

    
969
(rule (=> 
970
  (and 
971
       (= Junctions1V0_Chart.__Junctions1V0_Chart_5_m Junctions1V0_Chart.__Junctions1V0_Chart_5_c)
972
       (= Junctions1V0_Chart.__Junctions1V0_Chart_6_m Junctions1V0_Chart.__Junctions1V0_Chart_6_c)
973
       (= Junctions1V0_Chart.__Junctions1V0_Chart_7_m Junctions1V0_Chart.__Junctions1V0_Chart_7_c)
974
       (= Junctions1V0_Chart.ni_3._arrow._first_m true)
975
       (Chart_Chart_node_reset Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
976
                               Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
977
                               Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
978
                               Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
979
                               Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
980
                               Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m)
981
  )
982
  (Junctions1V0_Chart_reset Junctions1V0_Chart.__Junctions1V0_Chart_5_c
983
                            Junctions1V0_Chart.__Junctions1V0_Chart_6_c
984
                            Junctions1V0_Chart.__Junctions1V0_Chart_7_c
985
                            Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
986
                            Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
987
                            Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
988
                            Junctions1V0_Chart.ni_3._arrow._first_c
989
                            Junctions1V0_Chart.__Junctions1V0_Chart_5_m
990
                            Junctions1V0_Chart.__Junctions1V0_Chart_6_m
991
                            Junctions1V0_Chart.__Junctions1V0_Chart_7_m
992
                            Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
993
                            Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
994
                            Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
995
                            Junctions1V0_Chart.ni_3._arrow._first_m)
996
))
997

    
998
(rule (=> 
999
  (and (= Junctions1V0_Chart.ni_3._arrow._first_m Junctions1V0_Chart.ni_3._arrow._first_c)
1000
       (and (= Junctions1V0_Chart.__Junctions1V0_Chart_4 (ite Junctions1V0_Chart.ni_3._arrow._first_m true false))
1001
            (= Junctions1V0_Chart.ni_3._arrow._first_x false))
1002
       (and (or (not (= Junctions1V0_Chart.__Junctions1V0_Chart_4 false))
1003
               (and (= Junctions1V0_Chart.z_1 Junctions1V0_Chart.__Junctions1V0_Chart_6_c)
1004
                    (= Junctions1V0_Chart.y_1 Junctions1V0_Chart.__Junctions1V0_Chart_7_c)
1005
                    (= Junctions1V0_Chart.idChart_Chart_1 Junctions1V0_Chart.__Junctions1V0_Chart_5_c)
1006
                    ))
1007
            (or (not (= Junctions1V0_Chart.__Junctions1V0_Chart_4 true))
1008
               (and (= Junctions1V0_Chart.z_1 2)
1009
                    (= Junctions1V0_Chart.y_1 1)
1010
                    (= Junctions1V0_Chart.idChart_Chart_1 0)
1011
                    ))
1012
       )
1013
       (and (= Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c)
1014
            (= Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c)
1015
            (= Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c)
1016
            )
1017
       (Chart_Chart_node_step Junctions1V0_Chart.idChart_Chart_1
1018
                              Junctions1V0_Chart.E1
1019
                              Junctions1V0_Chart.x
1020
                              Junctions1V0_Chart.y_1
1021
                              Junctions1V0_Chart.z_1
1022
                              Junctions1V0_Chart.__Junctions1V0_Chart_1
1023
                              Junctions1V0_Chart.__Junctions1V0_Chart_2
1024
                              Junctions1V0_Chart.__Junctions1V0_Chart_3
1025
                              Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1026
                              Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1027
                              Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1028
                              Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1029
                              Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1030
                              Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x)
1031
       (and (or (not (= Junctions1V0_Chart.E1 false))
1032
               (and (= Junctions1V0_Chart.z Junctions1V0_Chart.z_1)
1033
                    (= Junctions1V0_Chart.y Junctions1V0_Chart.y_1)
1034
                    (= Junctions1V0_Chart.idChart_Chart Junctions1V0_Chart.idChart_Chart_1)
1035
                    ))
1036
            (or (not (= Junctions1V0_Chart.E1 true))
1037
               (and (= Junctions1V0_Chart.z Junctions1V0_Chart.__Junctions1V0_Chart_3)
1038
                    (= Junctions1V0_Chart.y Junctions1V0_Chart.__Junctions1V0_Chart_2)
1039
                    (= Junctions1V0_Chart.idChart_Chart Junctions1V0_Chart.__Junctions1V0_Chart_1)
1040
                    ))
1041
       )
1042
       (= Junctions1V0_Chart.__Junctions1V0_Chart_7_x Junctions1V0_Chart.y)
1043
       (= Junctions1V0_Chart.__Junctions1V0_Chart_6_x Junctions1V0_Chart.z)
1044
       (= Junctions1V0_Chart.__Junctions1V0_Chart_5_x Junctions1V0_Chart.idChart_Chart)
1045
       )
1046
  (Junctions1V0_Chart_step Junctions1V0_Chart.x
1047
                           Junctions1V0_Chart.E1
1048
                           Junctions1V0_Chart.y
1049
                           Junctions1V0_Chart.z
1050
                           Junctions1V0_Chart.__Junctions1V0_Chart_5_c
1051
                           Junctions1V0_Chart.__Junctions1V0_Chart_6_c
1052
                           Junctions1V0_Chart.__Junctions1V0_Chart_7_c
1053
                           Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1054
                           Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1055
                           Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1056
                           Junctions1V0_Chart.ni_3._arrow._first_c
1057
                           Junctions1V0_Chart.__Junctions1V0_Chart_5_x
1058
                           Junctions1V0_Chart.__Junctions1V0_Chart_6_x
1059
                           Junctions1V0_Chart.__Junctions1V0_Chart_7_x
1060
                           Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1061
                           Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1062
                           Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1063
                           Junctions1V0_Chart.ni_3._arrow._first_x)
1064
))
1065

    
1066
; Junctions1V0
1067
(declare-var Junctions1V0.x_1_1 Int)
1068
(declare-var Junctions1V0.E1_1_1 Real)
1069
(declare-var Junctions1V0.y_1_1 Int)
1070
(declare-var Junctions1V0.z_2_1 Int)
1071
(declare-var Junctions1V0.__Junctions1V0_2_c Real)
1072
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_c Int)
1073
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_c Int)
1074
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_c Int)
1075
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c Bool)
1076
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c chart_chart__type)
1077
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c Bool)
1078
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_c Bool)
1079
(declare-var Junctions1V0.ni_1._arrow._first_c Bool)
1080
(declare-var Junctions1V0.__Junctions1V0_2_m Real)
1081
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_m Int)
1082
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_m Int)
1083
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_m Int)
1084
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Bool)
1085
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m chart_chart__type)
1086
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Bool)
1087
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_m Bool)
1088
(declare-var Junctions1V0.ni_1._arrow._first_m Bool)
1089
(declare-var Junctions1V0.__Junctions1V0_2_x Real)
1090
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_x Int)
1091
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_x Int)
1092
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_x Int)
1093
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x Bool)
1094
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x chart_chart__type)
1095
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x Bool)
1096
(declare-var Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_x Bool)
1097
(declare-var Junctions1V0.ni_1._arrow._first_x Bool)
1098
(declare-var Junctions1V0.ChartE1_1_1_event Bool)
1099
(declare-var Junctions1V0.Chart_1_1 Int)
1100
(declare-var Junctions1V0.Chart_2_1 Int)
1101
(declare-var Junctions1V0.__Junctions1V0_1 Bool)
1102
(declare-var Junctions1V0.i_virtual_local Real)
1103
(declare-rel Junctions1V0_reset (Real Int Int Int Bool chart_chart__type Bool Bool Bool Real Int Int Int Bool chart_chart__type Bool Bool Bool))
1104
(declare-rel Junctions1V0_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))
1105

    
1106
(rule (=> 
1107
  (and 
1108
       (= Junctions1V0.__Junctions1V0_2_m Junctions1V0.__Junctions1V0_2_c)
1109
       (= Junctions1V0.ni_1._arrow._first_m true)
1110
       (Junctions1V0_Chart_reset Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_c
1111
                                 Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_c
1112
                                 Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_c
1113
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1114
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1115
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1116
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_c
1117
                                 Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_m
1118
                                 Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_m
1119
                                 Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_m
1120
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1121
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1122
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1123
                                 Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_m)
1124
  )
1125
  (Junctions1V0_reset Junctions1V0.__Junctions1V0_2_c
1126
                      Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_c
1127
                      Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_c
1128
                      Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_c
1129
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1130
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1131
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1132
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_c
1133
                      Junctions1V0.ni_1._arrow._first_c
1134
                      Junctions1V0.__Junctions1V0_2_m
1135
                      Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_m
1136
                      Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_m
1137
                      Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_m
1138
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1139
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1140
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1141
                      Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_m
1142
                      Junctions1V0.ni_1._arrow._first_m)
1143
))
1144

    
1145
(rule (=> 
1146
  (and (= Junctions1V0.ni_1._arrow._first_m Junctions1V0.ni_1._arrow._first_c)
1147
       (and (= Junctions1V0.__Junctions1V0_1 (ite Junctions1V0.ni_1._arrow._first_m true false))
1148
            (= Junctions1V0.ni_1._arrow._first_x false))
1149
       (and (or (not (= Junctions1V0.__Junctions1V0_1 true))
1150
               (= Junctions1V0.ChartE1_1_1_event false))
1151
            (or (not (= Junctions1V0.__Junctions1V0_1 false))
1152
               (= Junctions1V0.ChartE1_1_1_event (or (and (> Junctions1V0.__Junctions1V0_2_c 0.) (<= Junctions1V0.E1_1_1 0.)) (and (<= Junctions1V0.__Junctions1V0_2_c 0.) (> Junctions1V0.E1_1_1 0.)))))
1153
       )
1154
       (and (= Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_m Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_c)
1155
            (= Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_m Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_c)
1156
            (= Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_m Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_c)
1157
            (= Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c)
1158
            (= Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c)
1159
            (= Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c)
1160
            (= Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_m Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_c)
1161
            )
1162
       (Junctions1V0_Chart_step Junctions1V0.x_1_1
1163
                                Junctions1V0.ChartE1_1_1_event
1164
                                Junctions1V0.Chart_1_1
1165
                                Junctions1V0.Chart_2_1
1166
                                Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_m
1167
                                Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_m
1168
                                Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_m
1169
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_m
1170
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_m
1171
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_m
1172
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_m
1173
                                Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_x
1174
                                Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_x
1175
                                Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_x
1176
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1177
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1178
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1179
                                Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_x)
1180
       (= Junctions1V0.z_2_1 Junctions1V0.Chart_2_1)
1181
       (= Junctions1V0.y_1_1 Junctions1V0.Chart_1_1)
1182
       (and (or (not (= Junctions1V0.__Junctions1V0_1 true))
1183
               (= Junctions1V0.i_virtual_local 0.))
1184
            (or (not (= Junctions1V0.__Junctions1V0_1 false))
1185
               (= Junctions1V0.i_virtual_local 1.))
1186
       )
1187
       (= Junctions1V0.__Junctions1V0_2_x Junctions1V0.E1_1_1)
1188
       )
1189
  (Junctions1V0_step Junctions1V0.x_1_1
1190
                     Junctions1V0.E1_1_1
1191
                     Junctions1V0.y_1_1
1192
                     Junctions1V0.z_2_1
1193
                     Junctions1V0.__Junctions1V0_2_c
1194
                     Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_c
1195
                     Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_c
1196
                     Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_c
1197
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_c
1198
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_c
1199
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_c
1200
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_c
1201
                     Junctions1V0.ni_1._arrow._first_c
1202
                     Junctions1V0.__Junctions1V0_2_x
1203
                     Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_5_x
1204
                     Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_6_x
1205
                     Junctions1V0.ni_0.Junctions1V0_Chart.__Junctions1V0_Chart_7_x
1206
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_58_x
1207
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.__Chart_Chart_node_59_x
1208
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_2.Chart_Chart_node.ni_4._arrow._first_x
1209
                     Junctions1V0.ni_0.Junctions1V0_Chart.ni_3._arrow._first_x
1210
                     Junctions1V0.ni_1._arrow._first_x)
1211
))
1212