Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart4 / Flowchart4.smt2 @ eb639349

History | View | Annotate | Download (130 KB)

1
(declare-datatypes () ((flowchart4_flowchart4__type POINTFlowchart4_Flowchart4 POINT__TO__FLOWCHART4_A_1 FLOWCHART4_A_IDL)));
2

    
3
(declare-datatypes () ((flowchart4_a_INNER__type POINTFlowchart4_A_INNER FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1)));
4

    
5
(declare-datatypes () ((flowchart4_a__type POINTFlowchart4_A)));
6

    
7
; Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action
8
(declare-var Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action.x_1 Int)
9
(declare-var Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action.x Int)
10
(declare-rel Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action (Int Int))
11
(rule (=> 
12
  (= Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action.x (+ Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action.x_1 1))
13
  (Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action.x_1 Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action.x)
14
))
15

    
16
; flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until
17
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_1 Int)
18
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.flowchart4_a_INNER__restart_in Bool)
19
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.flowchart4_a_INNER__state_in flowchart4_a_INNER__type)
20
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_out Int)
21
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_2 Int)
22
(declare-rel flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until (Int Bool flowchart4_a_INNER__type Int))
23
(rule (=> 
24
  (and (Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action 
25
       flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_1
26
       flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_2)
27
       (= flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_out flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_2)
28
       (= flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.flowchart4_a_INNER__state_in POINTFlowchart4_A_INNER)
29
       (= flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.flowchart4_a_INNER__restart_in true)
30
       )
31
  (flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_1 flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.flowchart4_a_INNER__restart_in flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.flowchart4_a_INNER__state_in flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until.x_out)
32
))
33

    
34
; flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless
35
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__restart_in Bool)
36
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__state_in flowchart4_a_INNER__type)
37
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__restart_act Bool)
38
(declare-var flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__state_act flowchart4_a_INNER__type)
39
(declare-rel flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless (Bool flowchart4_a_INNER__type Bool flowchart4_a_INNER__type))
40
(rule (=> 
41
  (and (= flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__state_act flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__state_in)
42
       (= flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__restart_act flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__restart_in)
43
       )
44
  (flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__restart_in flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__state_in flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__restart_act flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless.flowchart4_a_INNER__state_act)
45
))
46

    
47
; flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until
48
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.x_1 Int)
49
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.flowchart4_a_INNER__restart_in Bool)
50
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.flowchart4_a_INNER__state_in flowchart4_a_INNER__type)
51
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.x_out Int)
52
(declare-rel flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until (Int Bool flowchart4_a_INNER__type Int))
53
(rule (=> 
54
  (and (= flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.x_out flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.x_1)
55
       (= flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.flowchart4_a_INNER__state_in POINTFlowchart4_A_INNER)
56
       (= flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.flowchart4_a_INNER__restart_in false)
57
       )
58
  (flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.x_1 flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.flowchart4_a_INNER__restart_in flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.flowchart4_a_INNER__state_in flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until.x_out)
59
))
60

    
61
; flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless
62
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__restart_in Bool)
63
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__state_in flowchart4_a_INNER__type)
64
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__restart_act Bool)
65
(declare-var flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__state_act flowchart4_a_INNER__type)
66
(declare-rel flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless (Bool flowchart4_a_INNER__type Bool flowchart4_a_INNER__type))
67
(rule (=> 
68
  (and (= flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__state_act FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1)
69
       (= flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__restart_act true)
70
       )
71
  (flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__restart_in flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__state_in flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__restart_act flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless.flowchart4_a_INNER__state_act)
72
))
73

    
74
; flowchart4_a__POINTFlowchart4_A_handler_until
75
(declare-var flowchart4_a__POINTFlowchart4_A_handler_until.idFlowchart4_A_1 Int)
76
(declare-var flowchart4_a__POINTFlowchart4_A_handler_until.flowchart4_a__restart_in Bool)
77
(declare-var flowchart4_a__POINTFlowchart4_A_handler_until.flowchart4_a__state_in flowchart4_a__type)
78
(declare-var flowchart4_a__POINTFlowchart4_A_handler_until.idFlowchart4_A_out Int)
79
(declare-rel flowchart4_a__POINTFlowchart4_A_handler_until (Int Bool flowchart4_a__type Int))
80
(rule (=> 
81
  (and (= flowchart4_a__POINTFlowchart4_A_handler_until.idFlowchart4_A_out flowchart4_a__POINTFlowchart4_A_handler_until.idFlowchart4_A_1)
82
       (= flowchart4_a__POINTFlowchart4_A_handler_until.flowchart4_a__state_in POINTFlowchart4_A)
83
       (= flowchart4_a__POINTFlowchart4_A_handler_until.flowchart4_a__restart_in false)
84
       )
85
  (flowchart4_a__POINTFlowchart4_A_handler_until flowchart4_a__POINTFlowchart4_A_handler_until.idFlowchart4_A_1 flowchart4_a__POINTFlowchart4_A_handler_until.flowchart4_a__restart_in flowchart4_a__POINTFlowchart4_A_handler_until.flowchart4_a__state_in flowchart4_a__POINTFlowchart4_A_handler_until.idFlowchart4_A_out)
86
))
87

    
88
; flowchart4_a__POINTFlowchart4_A_unless
89
(declare-var flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__restart_in Bool)
90
(declare-var flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__state_in flowchart4_a__type)
91
(declare-var flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__restart_act Bool)
92
(declare-var flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__state_act flowchart4_a__type)
93
(declare-rel flowchart4_a__POINTFlowchart4_A_unless (Bool flowchart4_a__type Bool flowchart4_a__type))
94
(rule (=> 
95
  (and (= flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__state_act flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__state_in)
96
       (= flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__restart_act flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__restart_in)
97
       )
98
  (flowchart4_a__POINTFlowchart4_A_unless flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__restart_in flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__state_in flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__restart_act flowchart4_a__POINTFlowchart4_A_unless.flowchart4_a__state_act)
99
))
100

    
101
; Flowchart4_A_du
102
(declare-var Flowchart4_A_du.x_1 Int)
103
(declare-var Flowchart4_A_du.x Int)
104
(declare-var Flowchart4_A_du.__Flowchart4_A_du_12_c Bool)
105
(declare-var Flowchart4_A_du.__Flowchart4_A_du_13_c flowchart4_a_INNER__type)
106
(declare-var Flowchart4_A_du.ni_9._arrow._first_c Bool)
107
(declare-var Flowchart4_A_du.__Flowchart4_A_du_12_m Bool)
108
(declare-var Flowchart4_A_du.__Flowchart4_A_du_13_m flowchart4_a_INNER__type)
109
(declare-var Flowchart4_A_du.ni_9._arrow._first_m Bool)
110
(declare-var Flowchart4_A_du.__Flowchart4_A_du_12_x Bool)
111
(declare-var Flowchart4_A_du.__Flowchart4_A_du_13_x flowchart4_a_INNER__type)
112
(declare-var Flowchart4_A_du.ni_9._arrow._first_x Bool)
113
(declare-var Flowchart4_A_du.__Flowchart4_A_du_1 Bool)
114
(declare-var Flowchart4_A_du.__Flowchart4_A_du_10 Int)
115
(declare-var Flowchart4_A_du.__Flowchart4_A_du_11 Bool)
116
(declare-var Flowchart4_A_du.__Flowchart4_A_du_2 flowchart4_a_INNER__type)
117
(declare-var Flowchart4_A_du.__Flowchart4_A_du_3 Bool)
118
(declare-var Flowchart4_A_du.__Flowchart4_A_du_4 flowchart4_a_INNER__type)
119
(declare-var Flowchart4_A_du.__Flowchart4_A_du_5 Bool)
120
(declare-var Flowchart4_A_du.__Flowchart4_A_du_6 flowchart4_a_INNER__type)
121
(declare-var Flowchart4_A_du.__Flowchart4_A_du_7 Int)
122
(declare-var Flowchart4_A_du.__Flowchart4_A_du_8 Bool)
123
(declare-var Flowchart4_A_du.__Flowchart4_A_du_9 flowchart4_a_INNER__type)
124
(declare-var Flowchart4_A_du.flowchart4_a_INNER__next_restart_in Bool)
125
(declare-var Flowchart4_A_du.flowchart4_a_INNER__next_state_in flowchart4_a_INNER__type)
126
(declare-var Flowchart4_A_du.flowchart4_a_INNER__restart_act Bool)
127
(declare-var Flowchart4_A_du.flowchart4_a_INNER__restart_in Bool)
128
(declare-var Flowchart4_A_du.flowchart4_a_INNER__state_act flowchart4_a_INNER__type)
129
(declare-var Flowchart4_A_du.flowchart4_a_INNER__state_in flowchart4_a_INNER__type)
130
(declare-rel Flowchart4_A_du_reset (Bool flowchart4_a_INNER__type Bool Bool flowchart4_a_INNER__type Bool))
131
(declare-rel Flowchart4_A_du_step (Int Int Bool flowchart4_a_INNER__type Bool Bool flowchart4_a_INNER__type Bool))
132

    
133
(rule (=> 
134
  (and 
135
       (= Flowchart4_A_du.__Flowchart4_A_du_12_m Flowchart4_A_du.__Flowchart4_A_du_12_c)
136
       (= Flowchart4_A_du.__Flowchart4_A_du_13_m Flowchart4_A_du.__Flowchart4_A_du_13_c)
137
       (= Flowchart4_A_du.ni_9._arrow._first_m true)
138
  )
139
  (Flowchart4_A_du_reset Flowchart4_A_du.__Flowchart4_A_du_12_c
140
                         Flowchart4_A_du.__Flowchart4_A_du_13_c
141
                         Flowchart4_A_du.ni_9._arrow._first_c
142
                         Flowchart4_A_du.__Flowchart4_A_du_12_m
143
                         Flowchart4_A_du.__Flowchart4_A_du_13_m
144
                         Flowchart4_A_du.ni_9._arrow._first_m)
145
))
146

    
147
(rule (=> 
148
  (and (= Flowchart4_A_du.ni_9._arrow._first_m Flowchart4_A_du.ni_9._arrow._first_c)
149
       (and (= Flowchart4_A_du.__Flowchart4_A_du_11 (ite Flowchart4_A_du.ni_9._arrow._first_m true false))
150
            (= Flowchart4_A_du.ni_9._arrow._first_x false))
151
       (and (or (not (= Flowchart4_A_du.__Flowchart4_A_du_11 false))
152
               (and (= Flowchart4_A_du.flowchart4_a_INNER__state_in Flowchart4_A_du.__Flowchart4_A_du_13_c)
153
                    (= Flowchart4_A_du.flowchart4_a_INNER__restart_in Flowchart4_A_du.__Flowchart4_A_du_12_c)
154
                    ))
155
            (or (not (= Flowchart4_A_du.__Flowchart4_A_du_11 true))
156
               (and (= Flowchart4_A_du.flowchart4_a_INNER__state_in POINTFlowchart4_A_INNER)
157
                    (= Flowchart4_A_du.flowchart4_a_INNER__restart_in false)
158
                    ))
159
       )
160
       (and (or (not (= Flowchart4_A_du.flowchart4_a_INNER__state_in FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1))
161
               (and (flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_unless 
162
                    Flowchart4_A_du.flowchart4_a_INNER__restart_in
163
                    Flowchart4_A_du.flowchart4_a_INNER__state_in
164
                    Flowchart4_A_du.__Flowchart4_A_du_1
165
                    Flowchart4_A_du.__Flowchart4_A_du_2)
166
                    (= Flowchart4_A_du.flowchart4_a_INNER__state_act Flowchart4_A_du.__Flowchart4_A_du_2)
167
                    (= Flowchart4_A_du.flowchart4_a_INNER__restart_act Flowchart4_A_du.__Flowchart4_A_du_1)
168
                    ))
169
            (or (not (= Flowchart4_A_du.flowchart4_a_INNER__state_in POINTFlowchart4_A_INNER))
170
               (and (flowchart4_a_INNER__POINTFlowchart4_A_INNER_unless 
171
                    Flowchart4_A_du.flowchart4_a_INNER__restart_in
172
                    Flowchart4_A_du.flowchart4_a_INNER__state_in
173
                    Flowchart4_A_du.__Flowchart4_A_du_3
174
                    Flowchart4_A_du.__Flowchart4_A_du_4)
175
                    (= Flowchart4_A_du.flowchart4_a_INNER__state_act Flowchart4_A_du.__Flowchart4_A_du_4)
176
                    (= Flowchart4_A_du.flowchart4_a_INNER__restart_act Flowchart4_A_du.__Flowchart4_A_du_3)
177
                    ))
178
       )
179
       (and (or (not (= Flowchart4_A_du.flowchart4_a_INNER__state_act FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1))
180
               (and (flowchart4_a_INNER__FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1_handler_until 
181
                    Flowchart4_A_du.x_1
182
                    Flowchart4_A_du.__Flowchart4_A_du_5
183
                    Flowchart4_A_du.__Flowchart4_A_du_6
184
                    Flowchart4_A_du.__Flowchart4_A_du_7)
185
                    (= Flowchart4_A_du.x Flowchart4_A_du.__Flowchart4_A_du_7)
186
                    (= Flowchart4_A_du.flowchart4_a_INNER__next_state_in Flowchart4_A_du.__Flowchart4_A_du_6)
187
                    (= Flowchart4_A_du.flowchart4_a_INNER__next_restart_in Flowchart4_A_du.__Flowchart4_A_du_5)
188
                    ))
189
            (or (not (= Flowchart4_A_du.flowchart4_a_INNER__state_act POINTFlowchart4_A_INNER))
190
               (and (flowchart4_a_INNER__POINTFlowchart4_A_INNER_handler_until 
191
                    Flowchart4_A_du.x_1
192
                    Flowchart4_A_du.__Flowchart4_A_du_8
193
                    Flowchart4_A_du.__Flowchart4_A_du_9
194
                    Flowchart4_A_du.__Flowchart4_A_du_10)
195
                    (= Flowchart4_A_du.x Flowchart4_A_du.__Flowchart4_A_du_10)
196
                    (= Flowchart4_A_du.flowchart4_a_INNER__next_state_in Flowchart4_A_du.__Flowchart4_A_du_9)
197
                    (= Flowchart4_A_du.flowchart4_a_INNER__next_restart_in Flowchart4_A_du.__Flowchart4_A_du_8)
198
                    ))
199
       )
200
       (= Flowchart4_A_du.__Flowchart4_A_du_13_x Flowchart4_A_du.flowchart4_a_INNER__next_state_in)
201
       (= Flowchart4_A_du.__Flowchart4_A_du_12_x Flowchart4_A_du.flowchart4_a_INNER__next_restart_in)
202
       )
203
  (Flowchart4_A_du_step Flowchart4_A_du.x_1
204
                        Flowchart4_A_du.x
205
                        Flowchart4_A_du.__Flowchart4_A_du_12_c
206
                        Flowchart4_A_du.__Flowchart4_A_du_13_c
207
                        Flowchart4_A_du.ni_9._arrow._first_c
208
                        Flowchart4_A_du.__Flowchart4_A_du_12_x
209
                        Flowchart4_A_du.__Flowchart4_A_du_13_x
210
                        Flowchart4_A_du.ni_9._arrow._first_x)
211
))
212

    
213
; Flowchart4_A_node
214
(declare-var Flowchart4_A_node.idFlowchart4_A_1 Int)
215
(declare-var Flowchart4_A_node.idFlowchart4_A Int)
216
(declare-var Flowchart4_A_node.__Flowchart4_A_node_7_c Bool)
217
(declare-var Flowchart4_A_node.__Flowchart4_A_node_8_c flowchart4_a__type)
218
(declare-var Flowchart4_A_node.ni_8._arrow._first_c Bool)
219
(declare-var Flowchart4_A_node.__Flowchart4_A_node_7_m Bool)
220
(declare-var Flowchart4_A_node.__Flowchart4_A_node_8_m flowchart4_a__type)
221
(declare-var Flowchart4_A_node.ni_8._arrow._first_m Bool)
222
(declare-var Flowchart4_A_node.__Flowchart4_A_node_7_x Bool)
223
(declare-var Flowchart4_A_node.__Flowchart4_A_node_8_x flowchart4_a__type)
224
(declare-var Flowchart4_A_node.ni_8._arrow._first_x Bool)
225
(declare-var Flowchart4_A_node.__Flowchart4_A_node_1 Bool)
226
(declare-var Flowchart4_A_node.__Flowchart4_A_node_2 flowchart4_a__type)
227
(declare-var Flowchart4_A_node.__Flowchart4_A_node_3 Bool)
228
(declare-var Flowchart4_A_node.__Flowchart4_A_node_4 flowchart4_a__type)
229
(declare-var Flowchart4_A_node.__Flowchart4_A_node_5 Int)
230
(declare-var Flowchart4_A_node.__Flowchart4_A_node_6 Bool)
231
(declare-var Flowchart4_A_node.flowchart4_a__next_restart_in Bool)
232
(declare-var Flowchart4_A_node.flowchart4_a__next_state_in flowchart4_a__type)
233
(declare-var Flowchart4_A_node.flowchart4_a__restart_act Bool)
234
(declare-var Flowchart4_A_node.flowchart4_a__restart_in Bool)
235
(declare-var Flowchart4_A_node.flowchart4_a__state_act flowchart4_a__type)
236
(declare-var Flowchart4_A_node.flowchart4_a__state_in flowchart4_a__type)
237
(declare-rel Flowchart4_A_node_reset (Bool flowchart4_a__type Bool Bool flowchart4_a__type Bool))
238
(declare-rel Flowchart4_A_node_step (Int Int Bool flowchart4_a__type Bool Bool flowchart4_a__type Bool))
239

    
240
(rule (=> 
241
  (and 
242
       (= Flowchart4_A_node.__Flowchart4_A_node_7_m Flowchart4_A_node.__Flowchart4_A_node_7_c)
243
       (= Flowchart4_A_node.__Flowchart4_A_node_8_m Flowchart4_A_node.__Flowchart4_A_node_8_c)
244
       (= Flowchart4_A_node.ni_8._arrow._first_m true)
245
  )
246
  (Flowchart4_A_node_reset Flowchart4_A_node.__Flowchart4_A_node_7_c
247
                           Flowchart4_A_node.__Flowchart4_A_node_8_c
248
                           Flowchart4_A_node.ni_8._arrow._first_c
249
                           Flowchart4_A_node.__Flowchart4_A_node_7_m
250
                           Flowchart4_A_node.__Flowchart4_A_node_8_m
251
                           Flowchart4_A_node.ni_8._arrow._first_m)
252
))
253

    
254
(rule (=> 
255
  (and (= Flowchart4_A_node.ni_8._arrow._first_m Flowchart4_A_node.ni_8._arrow._first_c)
256
       (and (= Flowchart4_A_node.__Flowchart4_A_node_6 (ite Flowchart4_A_node.ni_8._arrow._first_m true false))
257
            (= Flowchart4_A_node.ni_8._arrow._first_x false))
258
       (and (or (not (= Flowchart4_A_node.__Flowchart4_A_node_6 false))
259
               (and (= Flowchart4_A_node.flowchart4_a__state_in Flowchart4_A_node.__Flowchart4_A_node_8_c)
260
                    (= Flowchart4_A_node.flowchart4_a__restart_in Flowchart4_A_node.__Flowchart4_A_node_7_c)
261
                    ))
262
            (or (not (= Flowchart4_A_node.__Flowchart4_A_node_6 true))
263
               (and (= Flowchart4_A_node.flowchart4_a__state_in POINTFlowchart4_A)
264
                    (= Flowchart4_A_node.flowchart4_a__restart_in false)
265
                    ))
266
       )
267
       (or (not (= Flowchart4_A_node.flowchart4_a__state_in POINTFlowchart4_A))
268
          (and (flowchart4_a__POINTFlowchart4_A_unless Flowchart4_A_node.flowchart4_a__restart_in
269
                                                       Flowchart4_A_node.flowchart4_a__state_in
270
                                                       Flowchart4_A_node.__Flowchart4_A_node_1
271
                                                       Flowchart4_A_node.__Flowchart4_A_node_2)
272
               (= Flowchart4_A_node.flowchart4_a__state_act Flowchart4_A_node.__Flowchart4_A_node_2)
273
               (= Flowchart4_A_node.flowchart4_a__restart_act Flowchart4_A_node.__Flowchart4_A_node_1)
274
               ))
275
       (or (not (= Flowchart4_A_node.flowchart4_a__state_act POINTFlowchart4_A))
276
          (and (flowchart4_a__POINTFlowchart4_A_handler_until Flowchart4_A_node.idFlowchart4_A_1
277
                                                              Flowchart4_A_node.__Flowchart4_A_node_3
278
                                                              Flowchart4_A_node.__Flowchart4_A_node_4
279
                                                              Flowchart4_A_node.__Flowchart4_A_node_5)
280
               (= Flowchart4_A_node.idFlowchart4_A Flowchart4_A_node.__Flowchart4_A_node_5)
281
               (= Flowchart4_A_node.flowchart4_a__next_state_in Flowchart4_A_node.__Flowchart4_A_node_4)
282
               (= Flowchart4_A_node.flowchart4_a__next_restart_in Flowchart4_A_node.__Flowchart4_A_node_3)
283
               ))
284
       (= Flowchart4_A_node.__Flowchart4_A_node_8_x Flowchart4_A_node.flowchart4_a__next_state_in)
285
       (= Flowchart4_A_node.__Flowchart4_A_node_7_x Flowchart4_A_node.flowchart4_a__next_restart_in)
286
       )
287
  (Flowchart4_A_node_step Flowchart4_A_node.idFlowchart4_A_1
288
                          Flowchart4_A_node.idFlowchart4_A
289
                          Flowchart4_A_node.__Flowchart4_A_node_7_c
290
                          Flowchart4_A_node.__Flowchart4_A_node_8_c
291
                          Flowchart4_A_node.ni_8._arrow._first_c
292
                          Flowchart4_A_node.__Flowchart4_A_node_7_x
293
                          Flowchart4_A_node.__Flowchart4_A_node_8_x
294
                          Flowchart4_A_node.ni_8._arrow._first_x)
295
))
296

    
297
; Flowchart4_A_en
298
(declare-var Flowchart4_A_en.idFlowchart4_A_1 Int)
299
(declare-var Flowchart4_A_en.idFlowchart4_Flowchart4_1 Int)
300
(declare-var Flowchart4_A_en.isInner Bool)
301
(declare-var Flowchart4_A_en.idFlowchart4_A Int)
302
(declare-var Flowchart4_A_en.idFlowchart4_Flowchart4 Int)
303
(declare-rel Flowchart4_A_en (Int Int Bool Int Int))
304
(rule (=> 
305
  (and (= Flowchart4_A_en.idFlowchart4_Flowchart4 798)
306
       (= Flowchart4_A_en.idFlowchart4_A (- 1))
307
       )
308
  (Flowchart4_A_en Flowchart4_A_en.idFlowchart4_A_1 Flowchart4_A_en.idFlowchart4_Flowchart4_1 Flowchart4_A_en.isInner Flowchart4_A_en.idFlowchart4_A Flowchart4_A_en.idFlowchart4_Flowchart4)
309
))
310

    
311
; flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until
312
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_Flowchart4_1 Int)
313
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_1 Int)
314
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_1 Int)
315
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.flowchart4_flowchart4__restart_in Bool)
316
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.flowchart4_flowchart4__state_in flowchart4_flowchart4__type)
317
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_out Int)
318
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_Flowchart4_out Int)
319
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_out Int)
320
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c Bool)
321
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c flowchart4_a__type)
322
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c Bool)
323
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c Bool)
324
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c flowchart4_a_INNER__type)
325
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c Bool)
326
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Bool)
327
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m flowchart4_a__type)
328
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Bool)
329
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Bool)
330
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m flowchart4_a_INNER__type)
331
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Bool)
332
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x Bool)
333
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x flowchart4_a__type)
334
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x Bool)
335
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x Bool)
336
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x flowchart4_a_INNER__type)
337
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x Bool)
338
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_2 Int)
339
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_2 Int)
340
(declare-rel flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until_reset (Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool))
341
(declare-rel flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until_step (Int Int Int Bool flowchart4_flowchart4__type Int Int Int Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool))
342

    
343
(rule (=> 
344
  (and 
345
       
346
       (Flowchart4_A_du_reset flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
347
                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
348
                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
349
                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
350
                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
351
                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m)
352
       (Flowchart4_A_node_reset flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
353
                                flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
354
                                flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
355
                                flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
356
                                flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
357
                                flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m)
358
  )
359
  (flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until_reset flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
360
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
361
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
362
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
363
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
364
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
365
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
366
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
367
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
368
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
369
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
370
                                                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m)
371
))
372

    
373
(rule (=> 
374
  (and (and (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c)
375
            (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c)
376
            (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c)
377
            )
378
       (Flowchart4_A_du_step flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_1
379
                             flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_2
380
                             flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
381
                             flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
382
                             flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
383
                             flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
384
                             flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
385
                             flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x)
386
       (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_out flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_2)
387
       (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_Flowchart4_out flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_Flowchart4_1)
388
       (and (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c)
389
            (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c)
390
            (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c)
391
            )
392
       (Flowchart4_A_node_step flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_1
393
                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_2
394
                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
395
                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
396
                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
397
                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
398
                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
399
                               flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x)
400
       (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_out flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_2)
401
       (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.flowchart4_flowchart4__state_in POINTFlowchart4_Flowchart4)
402
       (= flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.flowchart4_flowchart4__restart_in true)
403
       )
404
  (flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until_step flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_Flowchart4_1
405
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_1
406
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_1
407
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.flowchart4_flowchart4__restart_in
408
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.flowchart4_flowchart4__state_in
409
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_A_out
410
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.idFlowchart4_Flowchart4_out
411
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.x_out
412
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
413
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
414
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
415
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
416
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
417
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
418
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
419
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
420
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x
421
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
422
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
423
                                                              flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x)
424
))
425

    
426
; flowchart4_flowchart4__FLOWCHART4_A_IDL_unless
427
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__restart_in Bool)
428
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__state_in flowchart4_flowchart4__type)
429
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__restart_act Bool)
430
(declare-var flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__state_act flowchart4_flowchart4__type)
431
(declare-rel flowchart4_flowchart4__FLOWCHART4_A_IDL_unless (Bool flowchart4_flowchart4__type Bool flowchart4_flowchart4__type))
432
(rule (=> 
433
  (and (= flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__state_act flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__state_in)
434
       (= flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__restart_act flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__restart_in)
435
       )
436
  (flowchart4_flowchart4__FLOWCHART4_A_IDL_unless flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__restart_in flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__state_in flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__restart_act flowchart4_flowchart4__FLOWCHART4_A_IDL_unless.flowchart4_flowchart4__state_act)
437
))
438

    
439
; flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until
440
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_Flowchart4_1 Int)
441
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_A_1 Int)
442
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.x_1 Int)
443
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.flowchart4_flowchart4__restart_in Bool)
444
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.flowchart4_flowchart4__state_in flowchart4_flowchart4__type)
445
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_A_out Int)
446
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_Flowchart4_out Int)
447
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.x_out Int)
448
(declare-rel flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until (Int Int Int Bool flowchart4_flowchart4__type Int Int Int))
449
(rule (=> 
450
  (and (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.x_out flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.x_1)
451
       (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_Flowchart4_out flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_Flowchart4_1)
452
       (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_A_out flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_A_1)
453
       (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.flowchart4_flowchart4__state_in POINTFlowchart4_Flowchart4)
454
       (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.flowchart4_flowchart4__restart_in false)
455
       )
456
  (flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_Flowchart4_1 flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_A_1 flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.x_1 flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.flowchart4_flowchart4__restart_in flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.flowchart4_flowchart4__state_in flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_A_out flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.idFlowchart4_Flowchart4_out flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until.x_out)
457
))
458

    
459
; flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless
460
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_in Bool)
461
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_in flowchart4_flowchart4__type)
462
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.idFlowchart4_Flowchart4_1 Int)
463
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_act Bool)
464
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_act flowchart4_flowchart4__type)
465
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_1 Bool)
466
(declare-var flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_2 Bool)
467
(declare-rel flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless (Bool flowchart4_flowchart4__type Int Bool flowchart4_flowchart4__type))
468
(rule (=> 
469
  (and (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_2 (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.idFlowchart4_Flowchart4_1 798))
470
       (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_1 (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.idFlowchart4_Flowchart4_1 0))
471
       (and (or (not (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_1 false))
472
               (and (or (not (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_2 false))
473
                       (and (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_act flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_in)
474
                            (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_act flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_in)
475
                            ))
476
                    (or (not (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_2 true))
477
                       (and (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_act FLOWCHART4_A_IDL)
478
                            (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_act true)
479
                            ))
480
               ))
481
            (or (not (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.__flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless_1 true))
482
               (and (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_act POINT__TO__FLOWCHART4_A_1)
483
                    (= flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_act true)
484
                    ))
485
       )
486
       )
487
  (flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_in flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_in flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.idFlowchart4_Flowchart4_1 flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__restart_act flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless.flowchart4_flowchart4__state_act)
488
))
489

    
490
; flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until
491
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_1 Int)
492
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_1 Int)
493
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.x_1 Int)
494
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.flowchart4_flowchart4__restart_in Bool)
495
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.flowchart4_flowchart4__state_in flowchart4_flowchart4__type)
496
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_out Int)
497
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_out Int)
498
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.x_out Int)
499
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_2 Int)
500
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_2 Int)
501
(declare-rel flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until (Int Int Int Bool flowchart4_flowchart4__type Int Int Int))
502
(rule (=> 
503
  (and (= flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.x_out flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.x_1)
504
       (Flowchart4_A_en flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_1
505
                        flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_1
506
                        false
507
                        flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_2
508
                        flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_2)
509
       (= flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_out flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_2)
510
       (= flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_out flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_2)
511
       (= flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.flowchart4_flowchart4__state_in POINTFlowchart4_Flowchart4)
512
       (= flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.flowchart4_flowchart4__restart_in true)
513
       )
514
  (flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_1 flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_1 flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.x_1 flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.flowchart4_flowchart4__restart_in flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.flowchart4_flowchart4__state_in flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_A_out flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.idFlowchart4_Flowchart4_out flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until.x_out)
515
))
516

    
517
; flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless
518
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__restart_in Bool)
519
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__state_in flowchart4_flowchart4__type)
520
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__restart_act Bool)
521
(declare-var flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__state_act flowchart4_flowchart4__type)
522
(declare-rel flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless (Bool flowchart4_flowchart4__type Bool flowchart4_flowchart4__type))
523
(rule (=> 
524
  (and (= flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__state_act flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__state_in)
525
       (= flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__restart_act flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__restart_in)
526
       )
527
  (flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__restart_in flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__state_in flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__restart_act flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless.flowchart4_flowchart4__state_act)
528
))
529

    
530
; Flowchart4_Flowchart4_node
531
(declare-var Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4_1 Int)
532
(declare-var Flowchart4_Flowchart4_node.idFlowchart4_A_1 Int)
533
(declare-var Flowchart4_Flowchart4_node.x_1 Int)
534
(declare-var Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4 Int)
535
(declare-var Flowchart4_Flowchart4_node.idFlowchart4_A Int)
536
(declare-var Flowchart4_Flowchart4_node.x Int)
537
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c Bool)
538
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c flowchart4_flowchart4__type)
539
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c Bool)
540
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c flowchart4_a__type)
541
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c Bool)
542
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c Bool)
543
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c flowchart4_a_INNER__type)
544
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c Bool)
545
(declare-var Flowchart4_Flowchart4_node.ni_5._arrow._first_c Bool)
546
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m Bool)
547
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m flowchart4_flowchart4__type)
548
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Bool)
549
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m flowchart4_a__type)
550
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Bool)
551
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Bool)
552
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m flowchart4_a_INNER__type)
553
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Bool)
554
(declare-var Flowchart4_Flowchart4_node.ni_5._arrow._first_m Bool)
555
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x Bool)
556
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x flowchart4_flowchart4__type)
557
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x Bool)
558
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x flowchart4_a__type)
559
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x Bool)
560
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x Bool)
561
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x flowchart4_a_INNER__type)
562
(declare-var Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x Bool)
563
(declare-var Flowchart4_Flowchart4_node.ni_5._arrow._first_x Bool)
564
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_1 Bool)
565
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_10 Int)
566
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_11 Int)
567
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_12 Bool)
568
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_13 flowchart4_flowchart4__type)
569
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_14 Int)
570
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_15 Int)
571
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_16 Int)
572
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_17 Bool)
573
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_18 flowchart4_flowchart4__type)
574
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_19 Int)
575
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_2 flowchart4_flowchart4__type)
576
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_20 Int)
577
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_21 Int)
578
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_22 Bool)
579
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_3 Bool)
580
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_4 flowchart4_flowchart4__type)
581
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_5 Bool)
582
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_6 flowchart4_flowchart4__type)
583
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_7 Bool)
584
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_8 flowchart4_flowchart4__type)
585
(declare-var Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_9 Int)
586
(declare-var Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_restart_in Bool)
587
(declare-var Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_state_in flowchart4_flowchart4__type)
588
(declare-var Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_act Bool)
589
(declare-var Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_in Bool)
590
(declare-var Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_act flowchart4_flowchart4__type)
591
(declare-var Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in flowchart4_flowchart4__type)
592
(declare-rel Flowchart4_Flowchart4_node_reset (Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool))
593
(declare-rel Flowchart4_Flowchart4_node_step (Int Int Int Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool))
594

    
595
(rule (=> 
596
  (and 
597
       (= Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c)
598
       (= Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c)
599
       (= Flowchart4_Flowchart4_node.ni_5._arrow._first_m true)
600
       (flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until_reset Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
601
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
602
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
603
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
604
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
605
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
606
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
607
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
608
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
609
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
610
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
611
                                                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m)
612
  )
613
  (Flowchart4_Flowchart4_node_reset Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
614
                                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
615
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
616
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
617
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
618
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
619
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
620
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
621
                                    Flowchart4_Flowchart4_node.ni_5._arrow._first_c
622
                                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m
623
                                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m
624
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
625
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
626
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
627
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
628
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
629
                                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
630
                                    Flowchart4_Flowchart4_node.ni_5._arrow._first_m)
631
))
632

    
633
(rule (=> 
634
  (and (= Flowchart4_Flowchart4_node.ni_5._arrow._first_m Flowchart4_Flowchart4_node.ni_5._arrow._first_c)
635
       (and (= Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_22 (ite Flowchart4_Flowchart4_node.ni_5._arrow._first_m true false))
636
            (= Flowchart4_Flowchart4_node.ni_5._arrow._first_x false))
637
       (and (or (not (= Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_22 false))
638
               (and (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c)
639
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c)
640
                    ))
641
            (or (not (= Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_22 true))
642
               (and (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in POINTFlowchart4_Flowchart4)
643
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_in false)
644
                    ))
645
       )
646
       (and (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in FLOWCHART4_A_IDL))
647
               (and (flowchart4_flowchart4__FLOWCHART4_A_IDL_unless Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_in
648
                                                                    Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in
649
                                                                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_1
650
                                                                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_2)
651
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_act Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_2)
652
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_act Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_1)
653
                    ))
654
            (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in POINTFlowchart4_Flowchart4))
655
               (and (flowchart4_flowchart4__POINTFlowchart4_Flowchart4_unless 
656
                    Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_in
657
                    Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in
658
                    Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4_1
659
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_5
660
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_6)
661
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_act Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_6)
662
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_act Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_5)
663
                    ))
664
            (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in POINT__TO__FLOWCHART4_A_1))
665
               (and (flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_unless 
666
                    Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_in
667
                    Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_in
668
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_3
669
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_4)
670
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_act Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_4)
671
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_act Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_3)
672
                    ))
673
       )
674
       (and (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_act FLOWCHART4_A_IDL))
675
               (and (and (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_act true))
676
                            (flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until_reset 
677
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
678
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
679
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
680
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
681
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
682
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
683
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
684
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
685
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
686
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
687
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
688
                            Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m))
689
                         (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__restart_act false))
690
                            (and (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c)
691
                                 (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c)
692
                                 (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c)
693
                                 (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c)
694
                                 (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c)
695
                                 (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c)
696
                                 )
697
                            )
698
                    )
699
                    (and (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c)
700
                         (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c)
701
                         (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c)
702
                         (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c)
703
                         (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c)
704
                         (= Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c)
705
                         )
706
                    (flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until_step 
707
                    Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4_1
708
                    Flowchart4_Flowchart4_node.idFlowchart4_A_1
709
                    Flowchart4_Flowchart4_node.x_1
710
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_7
711
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_8
712
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_9
713
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_10
714
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_11
715
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
716
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
717
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
718
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
719
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
720
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
721
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
722
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
723
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x
724
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
725
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
726
                    Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x)
727
                    (= Flowchart4_Flowchart4_node.x Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_11)
728
                    (= Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4 Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_10)
729
                    (= Flowchart4_Flowchart4_node.idFlowchart4_A Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_9)
730
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_state_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_8)
731
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_restart_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_7)
732
                    ))
733
            (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_act POINTFlowchart4_Flowchart4))
734
               (and (flowchart4_flowchart4__POINTFlowchart4_Flowchart4_handler_until 
735
                    Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4_1
736
                    Flowchart4_Flowchart4_node.idFlowchart4_A_1
737
                    Flowchart4_Flowchart4_node.x_1
738
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_17
739
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_18
740
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_19
741
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_20
742
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_21)
743
                    (= Flowchart4_Flowchart4_node.x Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_21)
744
                    (= Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4 Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_20)
745
                    (= Flowchart4_Flowchart4_node.idFlowchart4_A Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_19)
746
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_state_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_18)
747
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_restart_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_17)
748
                    ))
749
            (or (not (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__state_act POINT__TO__FLOWCHART4_A_1))
750
               (and (flowchart4_flowchart4__POINT__TO__FLOWCHART4_A_1_handler_until 
751
                    Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4_1
752
                    Flowchart4_Flowchart4_node.idFlowchart4_A_1
753
                    Flowchart4_Flowchart4_node.x_1
754
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_12
755
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_13
756
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_14
757
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_15
758
                    Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_16)
759
                    (= Flowchart4_Flowchart4_node.x Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_16)
760
                    (= Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4 Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_15)
761
                    (= Flowchart4_Flowchart4_node.idFlowchart4_A Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_14)
762
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_state_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_13)
763
                    (= Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_restart_in Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_12)
764
                    ))
765
       )
766
       (= Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_state_in)
767
       (= Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x Flowchart4_Flowchart4_node.flowchart4_flowchart4__next_restart_in)
768
       )
769
  (Flowchart4_Flowchart4_node_step Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4_1
770
                                   Flowchart4_Flowchart4_node.idFlowchart4_A_1
771
                                   Flowchart4_Flowchart4_node.x_1
772
                                   Flowchart4_Flowchart4_node.idFlowchart4_Flowchart4
773
                                   Flowchart4_Flowchart4_node.idFlowchart4_A
774
                                   Flowchart4_Flowchart4_node.x
775
                                   Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
776
                                   Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
777
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
778
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
779
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
780
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
781
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
782
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
783
                                   Flowchart4_Flowchart4_node.ni_5._arrow._first_c
784
                                   Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x
785
                                   Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x
786
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
787
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
788
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x
789
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
790
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
791
                                   Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x
792
                                   Flowchart4_Flowchart4_node.ni_5._arrow._first_x)
793
))
794

    
795
; Flowchart4_Flowchart4
796
(declare-var Flowchart4_Flowchart4.noInput Bool)
797
(declare-var Flowchart4_Flowchart4.x Int)
798
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c Int)
799
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c Int)
800
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c Int)
801
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c Bool)
802
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c flowchart4_flowchart4__type)
803
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c Bool)
804
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c flowchart4_a__type)
805
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c Bool)
806
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c Bool)
807
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c flowchart4_a_INNER__type)
808
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c Bool)
809
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c Bool)
810
(declare-var Flowchart4_Flowchart4.ni_3._arrow._first_c Bool)
811
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m Int)
812
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m Int)
813
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m Int)
814
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m Bool)
815
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m flowchart4_flowchart4__type)
816
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Bool)
817
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m flowchart4_a__type)
818
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Bool)
819
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Bool)
820
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m flowchart4_a_INNER__type)
821
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Bool)
822
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m Bool)
823
(declare-var Flowchart4_Flowchart4.ni_3._arrow._first_m Bool)
824
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_x Int)
825
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_x Int)
826
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_x Int)
827
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x Bool)
828
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x flowchart4_flowchart4__type)
829
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x Bool)
830
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x flowchart4_a__type)
831
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x Bool)
832
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x Bool)
833
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x flowchart4_a_INNER__type)
834
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x Bool)
835
(declare-var Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_x Bool)
836
(declare-var Flowchart4_Flowchart4.ni_3._arrow._first_x Bool)
837
(declare-var Flowchart4_Flowchart4.__Flowchart4_Flowchart4_1 Bool)
838
(declare-var Flowchart4_Flowchart4.idFlowchart4_A Int)
839
(declare-var Flowchart4_Flowchart4.idFlowchart4_A_1 Int)
840
(declare-var Flowchart4_Flowchart4.idFlowchart4_Flowchart4 Int)
841
(declare-var Flowchart4_Flowchart4.idFlowchart4_Flowchart4_1 Int)
842
(declare-var Flowchart4_Flowchart4.x_1 Int)
843
(declare-rel Flowchart4_Flowchart4_reset (Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool))
844
(declare-rel Flowchart4_Flowchart4_step (Bool Int Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool))
845

    
846
(rule (=> 
847
  (and 
848
       (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c)
849
       (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c)
850
       (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c)
851
       (= Flowchart4_Flowchart4.ni_3._arrow._first_m true)
852
       (Flowchart4_Flowchart4_node_reset Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
853
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
854
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
855
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
856
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
857
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
858
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
859
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
860
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c
861
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m
862
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m
863
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
864
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
865
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
866
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
867
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
868
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
869
                                         Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m)
870
  )
871
  (Flowchart4_Flowchart4_reset Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c
872
                               Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c
873
                               Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c
874
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
875
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
876
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
877
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
878
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
879
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
880
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
881
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
882
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c
883
                               Flowchart4_Flowchart4.ni_3._arrow._first_c
884
                               Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m
885
                               Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m
886
                               Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m
887
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m
888
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m
889
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
890
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
891
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
892
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
893
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
894
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
895
                               Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m
896
                               Flowchart4_Flowchart4.ni_3._arrow._first_m)
897
))
898

    
899
(rule (=> 
900
  (and (= Flowchart4_Flowchart4.ni_3._arrow._first_m Flowchart4_Flowchart4.ni_3._arrow._first_c)
901
       (and (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_1 (ite Flowchart4_Flowchart4.ni_3._arrow._first_m true false))
902
            (= Flowchart4_Flowchart4.ni_3._arrow._first_x false))
903
       (and (or (not (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_1 false))
904
               (and (= Flowchart4_Flowchart4.x_1 Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c)
905
                    (= Flowchart4_Flowchart4.idFlowchart4_Flowchart4_1 Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c)
906
                    (= Flowchart4_Flowchart4.idFlowchart4_A_1 Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c)
907
                    ))
908
            (or (not (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_1 true))
909
               (and (= Flowchart4_Flowchart4.x_1 0)
910
                    (= Flowchart4_Flowchart4.idFlowchart4_Flowchart4_1 0)
911
                    (= Flowchart4_Flowchart4.idFlowchart4_A_1 0)
912
                    ))
913
       )
914
       (and (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c)
915
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c)
916
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c)
917
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c)
918
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c)
919
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c)
920
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c)
921
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c)
922
            (= Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c)
923
            )
924
       (Flowchart4_Flowchart4_node_step Flowchart4_Flowchart4.idFlowchart4_Flowchart4_1
925
                                        Flowchart4_Flowchart4.idFlowchart4_A_1
926
                                        Flowchart4_Flowchart4.x_1
927
                                        Flowchart4_Flowchart4.idFlowchart4_Flowchart4
928
                                        Flowchart4_Flowchart4.idFlowchart4_A
929
                                        Flowchart4_Flowchart4.x
930
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m
931
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m
932
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
933
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
934
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
935
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
936
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
937
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
938
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m
939
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x
940
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x
941
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
942
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
943
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x
944
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
945
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
946
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x
947
                                        Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_x)
948
       (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_x Flowchart4_Flowchart4.x)
949
       (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_x Flowchart4_Flowchart4.idFlowchart4_Flowchart4)
950
       (= Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_x Flowchart4_Flowchart4.idFlowchart4_A)
951
       )
952
  (Flowchart4_Flowchart4_step Flowchart4_Flowchart4.noInput
953
                              Flowchart4_Flowchart4.x
954
                              Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c
955
                              Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c
956
                              Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c
957
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
958
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
959
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
960
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
961
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
962
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
963
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
964
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
965
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c
966
                              Flowchart4_Flowchart4.ni_3._arrow._first_c
967
                              Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_x
968
                              Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_x
969
                              Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_x
970
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x
971
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x
972
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
973
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
974
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x
975
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
976
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
977
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x
978
                              Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_x
979
                              Flowchart4_Flowchart4.ni_3._arrow._first_x)
980
))
981

    
982
; Flowchart4_A_ex
983
(declare-var Flowchart4_A_ex.idFlowchart4_Flowchart4_1 Int)
984
(declare-var Flowchart4_A_ex.isInner Bool)
985
(declare-var Flowchart4_A_ex.idFlowchart4_Flowchart4 Int)
986
(declare-var Flowchart4_A_ex.idFlowchart4_Flowchart4_2 Int)
987
(declare-rel Flowchart4_A_ex (Int Bool Int))
988
(rule (=> 
989
  (and (and (or (not (= (not Flowchart4_A_ex.isInner) true))
990
               (= Flowchart4_A_ex.idFlowchart4_Flowchart4_2 0))
991
            (or (not (= (not Flowchart4_A_ex.isInner) false))
992
               (= Flowchart4_A_ex.idFlowchart4_Flowchart4_2 Flowchart4_A_ex.idFlowchart4_Flowchart4_1))
993
       )
994
       (= Flowchart4_A_ex.idFlowchart4_Flowchart4 Flowchart4_A_ex.idFlowchart4_Flowchart4_1)
995
       )
996
  (Flowchart4_A_ex Flowchart4_A_ex.idFlowchart4_Flowchart4_1 Flowchart4_A_ex.isInner Flowchart4_A_ex.idFlowchart4_Flowchart4)
997
))
998

    
999
; Flowchart4
1000
(declare-var Flowchart4.i_virtual Real)
1001
(declare-var Flowchart4.Out1_1_1 Int)
1002
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c Int)
1003
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c Int)
1004
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c Int)
1005
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c Bool)
1006
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c flowchart4_flowchart4__type)
1007
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c Bool)
1008
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c flowchart4_a__type)
1009
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c Bool)
1010
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c Bool)
1011
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c flowchart4_a_INNER__type)
1012
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c Bool)
1013
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c Bool)
1014
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_c Bool)
1015
(declare-var Flowchart4.ni_1._arrow._first_c Bool)
1016
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m Int)
1017
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m Int)
1018
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m Int)
1019
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m Bool)
1020
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m flowchart4_flowchart4__type)
1021
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Bool)
1022
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m flowchart4_a__type)
1023
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Bool)
1024
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Bool)
1025
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m flowchart4_a_INNER__type)
1026
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Bool)
1027
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m Bool)
1028
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_m Bool)
1029
(declare-var Flowchart4.ni_1._arrow._first_m Bool)
1030
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_x Int)
1031
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_x Int)
1032
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_x Int)
1033
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x Bool)
1034
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x flowchart4_flowchart4__type)
1035
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x Bool)
1036
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x flowchart4_a__type)
1037
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x Bool)
1038
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x Bool)
1039
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x flowchart4_a_INNER__type)
1040
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x Bool)
1041
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_x Bool)
1042
(declare-var Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_x Bool)
1043
(declare-var Flowchart4.ni_1._arrow._first_x Bool)
1044
(declare-var Flowchart4.Flowchart4_1_1 Int)
1045
(declare-var Flowchart4.__Flowchart4_1 Bool)
1046
(declare-var Flowchart4.i_virtual_local Real)
1047
(declare-rel Flowchart4_reset (Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool Bool Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool Bool))
1048
(declare-rel Flowchart4_step (Real Int Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool Bool Int Int Int Bool flowchart4_flowchart4__type Bool flowchart4_a__type Bool Bool flowchart4_a_INNER__type Bool Bool Bool Bool))
1049

    
1050
(rule (=> 
1051
  (and 
1052
       
1053
       (= Flowchart4.ni_1._arrow._first_m true)
1054
       (Flowchart4_Flowchart4_reset Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c
1055
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c
1056
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c
1057
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
1058
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
1059
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
1060
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
1061
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
1062
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
1063
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
1064
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
1065
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c
1066
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_c
1067
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m
1068
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m
1069
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m
1070
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m
1071
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m
1072
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
1073
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
1074
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
1075
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
1076
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
1077
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
1078
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m
1079
                                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_m)
1080
  )
1081
  (Flowchart4_reset Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c
1082
                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c
1083
                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c
1084
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
1085
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
1086
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
1087
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
1088
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
1089
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
1090
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
1091
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
1092
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c
1093
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_c
1094
                    Flowchart4.ni_1._arrow._first_c
1095
                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m
1096
                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m
1097
                    Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m
1098
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m
1099
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m
1100
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
1101
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
1102
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
1103
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
1104
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
1105
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
1106
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m
1107
                    Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_m
1108
                    Flowchart4.ni_1._arrow._first_m)
1109
))
1110

    
1111
(rule (=> 
1112
  (and (= Flowchart4.ni_1._arrow._first_m Flowchart4.ni_1._arrow._first_c)
1113
       (and (= Flowchart4.__Flowchart4_1 (ite Flowchart4.ni_1._arrow._first_m true false))
1114
            (= Flowchart4.ni_1._arrow._first_x false))
1115
       (and (or (not (= Flowchart4.__Flowchart4_1 true))
1116
               (= Flowchart4.i_virtual_local 0.))
1117
            (or (not (= Flowchart4.__Flowchart4_1 false))
1118
               (= Flowchart4.i_virtual_local 1.))
1119
       )
1120
       (and (= Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c)
1121
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c)
1122
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c)
1123
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c)
1124
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c)
1125
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c)
1126
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c)
1127
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c)
1128
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c)
1129
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c)
1130
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c)
1131
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c)
1132
            (= Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_m Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_c)
1133
            )
1134
       (Flowchart4_Flowchart4_step true
1135
                                   Flowchart4.Flowchart4_1_1
1136
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_m
1137
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_m
1138
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_m
1139
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_m
1140
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_m
1141
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_m
1142
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_m
1143
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_m
1144
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_m
1145
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_m
1146
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_m
1147
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_m
1148
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_m
1149
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_x
1150
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_x
1151
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_x
1152
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x
1153
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x
1154
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
1155
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
1156
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x
1157
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
1158
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
1159
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x
1160
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_x
1161
                                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_x)
1162
       (= Flowchart4.Out1_1_1 Flowchart4.Flowchart4_1_1)
1163
       )
1164
  (Flowchart4_step Flowchart4.i_virtual
1165
                   Flowchart4.Out1_1_1
1166
                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_c
1167
                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_c
1168
                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_c
1169
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_c
1170
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_c
1171
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_c
1172
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_c
1173
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_c
1174
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_c
1175
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_c
1176
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_c
1177
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_c
1178
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_c
1179
                   Flowchart4.ni_1._arrow._first_c
1180
                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_2_x
1181
                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_3_x
1182
                   Flowchart4.ni_0.Flowchart4_Flowchart4.__Flowchart4_Flowchart4_4_x
1183
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_23_x
1184
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.__Flowchart4_Flowchart4_node_24_x
1185
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_7_x
1186
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.__Flowchart4_A_node_8_x
1187
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_6.Flowchart4_A_node.ni_8._arrow._first_x
1188
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_12_x
1189
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.__Flowchart4_A_du_13_x
1190
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_4.flowchart4_flowchart4__FLOWCHART4_A_IDL_handler_until.ni_7.Flowchart4_A_du.ni_9._arrow._first_x
1191
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_2.Flowchart4_Flowchart4_node.ni_5._arrow._first_x
1192
                   Flowchart4.ni_0.Flowchart4_Flowchart4.ni_3._arrow._first_x
1193
                   Flowchart4.ni_1._arrow._first_x)
1194
))
1195