Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart2 / Flowchart2.smt2 @ eb639349

History | View | Annotate | Download (99 KB)

1
(declare-datatypes () ((flowchart2_flowchart2__type POINTFlowchart2_Flowchart2 POINT__TO__FLOWCHART2_A_1 FLOWCHART2_A_IDL)));
2

    
3
(declare-datatypes () ((flowchart2_a__type POINTFlowchart2_A POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1)));
4

    
5
; POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action
6
(declare-var POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action.x_1 Int)
7
(declare-var POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action.x Int)
8
(declare-rel POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action (Int Int))
9
(rule (=> 
10
  (= POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action.x (+ POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action.x_1 1))
11
  (POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action.x_1 POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action.x)
12
))
13

    
14
; flowchart2_a__POINTFlowchart2_A_handler_until
15
(declare-var flowchart2_a__POINTFlowchart2_A_handler_until.idFlowchart2_A_1 Int)
16
(declare-var flowchart2_a__POINTFlowchart2_A_handler_until.x_1 Int)
17
(declare-var flowchart2_a__POINTFlowchart2_A_handler_until.flowchart2_a__restart_in Bool)
18
(declare-var flowchart2_a__POINTFlowchart2_A_handler_until.flowchart2_a__state_in flowchart2_a__type)
19
(declare-var flowchart2_a__POINTFlowchart2_A_handler_until.idFlowchart2_A_out Int)
20
(declare-var flowchart2_a__POINTFlowchart2_A_handler_until.x_out Int)
21
(declare-rel flowchart2_a__POINTFlowchart2_A_handler_until (Int Int Bool flowchart2_a__type Int Int))
22
(rule (=> 
23
  (and (= flowchart2_a__POINTFlowchart2_A_handler_until.x_out flowchart2_a__POINTFlowchart2_A_handler_until.x_1)
24
       (= flowchart2_a__POINTFlowchart2_A_handler_until.idFlowchart2_A_out flowchart2_a__POINTFlowchart2_A_handler_until.idFlowchart2_A_1)
25
       (= flowchart2_a__POINTFlowchart2_A_handler_until.flowchart2_a__state_in POINTFlowchart2_A)
26
       (= flowchart2_a__POINTFlowchart2_A_handler_until.flowchart2_a__restart_in false)
27
       )
28
  (flowchart2_a__POINTFlowchart2_A_handler_until flowchart2_a__POINTFlowchart2_A_handler_until.idFlowchart2_A_1 flowchart2_a__POINTFlowchart2_A_handler_until.x_1 flowchart2_a__POINTFlowchart2_A_handler_until.flowchart2_a__restart_in flowchart2_a__POINTFlowchart2_A_handler_until.flowchart2_a__state_in flowchart2_a__POINTFlowchart2_A_handler_until.idFlowchart2_A_out flowchart2_a__POINTFlowchart2_A_handler_until.x_out)
29
))
30

    
31
; flowchart2_a__POINTFlowchart2_A_unless
32
(declare-var flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__restart_in Bool)
33
(declare-var flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__state_in flowchart2_a__type)
34
(declare-var flowchart2_a__POINTFlowchart2_A_unless.idFlowchart2_A_1 Int)
35
(declare-var flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__restart_act Bool)
36
(declare-var flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__state_act flowchart2_a__type)
37
(declare-var flowchart2_a__POINTFlowchart2_A_unless.__flowchart2_a__POINTFlowchart2_A_unless_1 Bool)
38
(declare-rel flowchart2_a__POINTFlowchart2_A_unless (Bool flowchart2_a__type Int Bool flowchart2_a__type))
39
(rule (=> 
40
  (and (= flowchart2_a__POINTFlowchart2_A_unless.__flowchart2_a__POINTFlowchart2_A_unless_1 (= flowchart2_a__POINTFlowchart2_A_unless.idFlowchart2_A_1 0))
41
       (and (or (not (= flowchart2_a__POINTFlowchart2_A_unless.__flowchart2_a__POINTFlowchart2_A_unless_1 false))
42
               (and (= flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__state_act flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__state_in)
43
                    (= flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__restart_act flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__restart_in)
44
                    ))
45
            (or (not (= flowchart2_a__POINTFlowchart2_A_unless.__flowchart2_a__POINTFlowchart2_A_unless_1 true))
46
               (and (= flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__state_act POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1)
47
                    (= flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__restart_act true)
48
                    ))
49
       )
50
       )
51
  (flowchart2_a__POINTFlowchart2_A_unless flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__restart_in flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__state_in flowchart2_a__POINTFlowchart2_A_unless.idFlowchart2_A_1 flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__restart_act flowchart2_a__POINTFlowchart2_A_unless.flowchart2_a__state_act)
52
))
53

    
54
; flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until
55
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.idFlowchart2_A_1 Int)
56
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_1 Int)
57
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.flowchart2_a__restart_in Bool)
58
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.flowchart2_a__state_in flowchart2_a__type)
59
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.idFlowchart2_A_out Int)
60
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_out Int)
61
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_2 Int)
62
(declare-rel flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until (Int Int Bool flowchart2_a__type Int Int))
63
(rule (=> 
64
  (and (POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action 
65
       flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_1
66
       flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_2)
67
       (= flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_out flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_2)
68
       (= flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.idFlowchart2_A_out flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.idFlowchart2_A_1)
69
       (= flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.flowchart2_a__state_in POINTFlowchart2_A)
70
       (= flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.flowchart2_a__restart_in true)
71
       )
72
  (flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.idFlowchart2_A_1 flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_1 flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.flowchart2_a__restart_in flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.flowchart2_a__state_in flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.idFlowchart2_A_out flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until.x_out)
73
))
74

    
75
; flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless
76
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__restart_in Bool)
77
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__state_in flowchart2_a__type)
78
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__restart_act Bool)
79
(declare-var flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__state_act flowchart2_a__type)
80
(declare-rel flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless (Bool flowchart2_a__type Bool flowchart2_a__type))
81
(rule (=> 
82
  (and (= flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__state_act flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__state_in)
83
       (= flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__restart_act flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__restart_in)
84
       )
85
  (flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__restart_in flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__state_in flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__restart_act flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless.flowchart2_a__state_act)
86
))
87

    
88
; Flowchart2_A_du
89
(declare-var Flowchart2_A_du.x_1 Int)
90
(declare-var Flowchart2_A_du.x Int)
91
(declare-rel Flowchart2_A_du (Int Int))
92
(rule (=> 
93
  (= Flowchart2_A_du.x (- Flowchart2_A_du.x_1 1))
94
  (Flowchart2_A_du Flowchart2_A_du.x_1 Flowchart2_A_du.x)
95
))
96

    
97
; Flowchart2_A_node
98
(declare-var Flowchart2_A_node.idFlowchart2_A_1 Int)
99
(declare-var Flowchart2_A_node.x_1 Int)
100
(declare-var Flowchart2_A_node.idFlowchart2_A Int)
101
(declare-var Flowchart2_A_node.x Int)
102
(declare-var Flowchart2_A_node.__Flowchart2_A_node_14_c Bool)
103
(declare-var Flowchart2_A_node.__Flowchart2_A_node_15_c flowchart2_a__type)
104
(declare-var Flowchart2_A_node.ni_7._arrow._first_c Bool)
105
(declare-var Flowchart2_A_node.__Flowchart2_A_node_14_m Bool)
106
(declare-var Flowchart2_A_node.__Flowchart2_A_node_15_m flowchart2_a__type)
107
(declare-var Flowchart2_A_node.ni_7._arrow._first_m Bool)
108
(declare-var Flowchart2_A_node.__Flowchart2_A_node_14_x Bool)
109
(declare-var Flowchart2_A_node.__Flowchart2_A_node_15_x flowchart2_a__type)
110
(declare-var Flowchart2_A_node.ni_7._arrow._first_x Bool)
111
(declare-var Flowchart2_A_node.__Flowchart2_A_node_1 Bool)
112
(declare-var Flowchart2_A_node.__Flowchart2_A_node_10 flowchart2_a__type)
113
(declare-var Flowchart2_A_node.__Flowchart2_A_node_11 Int)
114
(declare-var Flowchart2_A_node.__Flowchart2_A_node_12 Int)
115
(declare-var Flowchart2_A_node.__Flowchart2_A_node_13 Bool)
116
(declare-var Flowchart2_A_node.__Flowchart2_A_node_2 flowchart2_a__type)
117
(declare-var Flowchart2_A_node.__Flowchart2_A_node_3 Bool)
118
(declare-var Flowchart2_A_node.__Flowchart2_A_node_4 flowchart2_a__type)
119
(declare-var Flowchart2_A_node.__Flowchart2_A_node_5 Bool)
120
(declare-var Flowchart2_A_node.__Flowchart2_A_node_6 flowchart2_a__type)
121
(declare-var Flowchart2_A_node.__Flowchart2_A_node_7 Int)
122
(declare-var Flowchart2_A_node.__Flowchart2_A_node_8 Int)
123
(declare-var Flowchart2_A_node.__Flowchart2_A_node_9 Bool)
124
(declare-var Flowchart2_A_node.flowchart2_a__next_restart_in Bool)
125
(declare-var Flowchart2_A_node.flowchart2_a__next_state_in flowchart2_a__type)
126
(declare-var Flowchart2_A_node.flowchart2_a__restart_act Bool)
127
(declare-var Flowchart2_A_node.flowchart2_a__restart_in Bool)
128
(declare-var Flowchart2_A_node.flowchart2_a__state_act flowchart2_a__type)
129
(declare-var Flowchart2_A_node.flowchart2_a__state_in flowchart2_a__type)
130
(declare-rel Flowchart2_A_node_reset (Bool flowchart2_a__type Bool Bool flowchart2_a__type Bool))
131
(declare-rel Flowchart2_A_node_step (Int Int Int Int Bool flowchart2_a__type Bool Bool flowchart2_a__type Bool))
132

    
133
(rule (=> 
134
  (and 
135
       (= Flowchart2_A_node.__Flowchart2_A_node_14_m Flowchart2_A_node.__Flowchart2_A_node_14_c)
136
       (= Flowchart2_A_node.__Flowchart2_A_node_15_m Flowchart2_A_node.__Flowchart2_A_node_15_c)
137
       (= Flowchart2_A_node.ni_7._arrow._first_m true)
138
  )
139
  (Flowchart2_A_node_reset Flowchart2_A_node.__Flowchart2_A_node_14_c
140
                           Flowchart2_A_node.__Flowchart2_A_node_15_c
141
                           Flowchart2_A_node.ni_7._arrow._first_c
142
                           Flowchart2_A_node.__Flowchart2_A_node_14_m
143
                           Flowchart2_A_node.__Flowchart2_A_node_15_m
144
                           Flowchart2_A_node.ni_7._arrow._first_m)
145
))
146

    
147
(rule (=> 
148
  (and (= Flowchart2_A_node.ni_7._arrow._first_m Flowchart2_A_node.ni_7._arrow._first_c)
149
       (and (= Flowchart2_A_node.__Flowchart2_A_node_13 (ite Flowchart2_A_node.ni_7._arrow._first_m true false))
150
            (= Flowchart2_A_node.ni_7._arrow._first_x false))
151
       (and (or (not (= Flowchart2_A_node.__Flowchart2_A_node_13 false))
152
               (and (= Flowchart2_A_node.flowchart2_a__state_in Flowchart2_A_node.__Flowchart2_A_node_15_c)
153
                    (= Flowchart2_A_node.flowchart2_a__restart_in Flowchart2_A_node.__Flowchart2_A_node_14_c)
154
                    ))
155
            (or (not (= Flowchart2_A_node.__Flowchart2_A_node_13 true))
156
               (and (= Flowchart2_A_node.flowchart2_a__state_in POINTFlowchart2_A)
157
                    (= Flowchart2_A_node.flowchart2_a__restart_in false)
158
                    ))
159
       )
160
       (and (or (not (= Flowchart2_A_node.flowchart2_a__state_in POINTFlowchart2_A))
161
               (and (flowchart2_a__POINTFlowchart2_A_unless Flowchart2_A_node.flowchart2_a__restart_in
162
                                                            Flowchart2_A_node.flowchart2_a__state_in
163
                                                            Flowchart2_A_node.idFlowchart2_A_1
164
                                                            Flowchart2_A_node.__Flowchart2_A_node_3
165
                                                            Flowchart2_A_node.__Flowchart2_A_node_4)
166
                    (= Flowchart2_A_node.flowchart2_a__state_act Flowchart2_A_node.__Flowchart2_A_node_4)
167
                    (= Flowchart2_A_node.flowchart2_a__restart_act Flowchart2_A_node.__Flowchart2_A_node_3)
168
                    ))
169
            (or (not (= Flowchart2_A_node.flowchart2_a__state_in POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1))
170
               (and (flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_unless 
171
                    Flowchart2_A_node.flowchart2_a__restart_in
172
                    Flowchart2_A_node.flowchart2_a__state_in
173
                    Flowchart2_A_node.__Flowchart2_A_node_1
174
                    Flowchart2_A_node.__Flowchart2_A_node_2)
175
                    (= Flowchart2_A_node.flowchart2_a__state_act Flowchart2_A_node.__Flowchart2_A_node_2)
176
                    (= Flowchart2_A_node.flowchart2_a__restart_act Flowchart2_A_node.__Flowchart2_A_node_1)
177
                    ))
178
       )
179
       (and (or (not (= Flowchart2_A_node.flowchart2_a__state_act POINTFlowchart2_A))
180
               (and (flowchart2_a__POINTFlowchart2_A_handler_until Flowchart2_A_node.idFlowchart2_A_1
181
                                                                   Flowchart2_A_node.x_1
182
                                                                   Flowchart2_A_node.__Flowchart2_A_node_9
183
                                                                   Flowchart2_A_node.__Flowchart2_A_node_10
184
                                                                   Flowchart2_A_node.__Flowchart2_A_node_11
185
                                                                   Flowchart2_A_node.__Flowchart2_A_node_12)
186
                    (= Flowchart2_A_node.x Flowchart2_A_node.__Flowchart2_A_node_12)
187
                    (= Flowchart2_A_node.idFlowchart2_A Flowchart2_A_node.__Flowchart2_A_node_11)
188
                    (= Flowchart2_A_node.flowchart2_a__next_state_in Flowchart2_A_node.__Flowchart2_A_node_10)
189
                    (= Flowchart2_A_node.flowchart2_a__next_restart_in Flowchart2_A_node.__Flowchart2_A_node_9)
190
                    ))
191
            (or (not (= Flowchart2_A_node.flowchart2_a__state_act POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1))
192
               (and (flowchart2_a__POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1_handler_until 
193
                    Flowchart2_A_node.idFlowchart2_A_1
194
                    Flowchart2_A_node.x_1
195
                    Flowchart2_A_node.__Flowchart2_A_node_5
196
                    Flowchart2_A_node.__Flowchart2_A_node_6
197
                    Flowchart2_A_node.__Flowchart2_A_node_7
198
                    Flowchart2_A_node.__Flowchart2_A_node_8)
199
                    (= Flowchart2_A_node.x Flowchart2_A_node.__Flowchart2_A_node_8)
200
                    (= Flowchart2_A_node.idFlowchart2_A Flowchart2_A_node.__Flowchart2_A_node_7)
201
                    (= Flowchart2_A_node.flowchart2_a__next_state_in Flowchart2_A_node.__Flowchart2_A_node_6)
202
                    (= Flowchart2_A_node.flowchart2_a__next_restart_in Flowchart2_A_node.__Flowchart2_A_node_5)
203
                    ))
204
       )
205
       (= Flowchart2_A_node.__Flowchart2_A_node_15_x Flowchart2_A_node.flowchart2_a__next_state_in)
206
       (= Flowchart2_A_node.__Flowchart2_A_node_14_x Flowchart2_A_node.flowchart2_a__next_restart_in)
207
       )
208
  (Flowchart2_A_node_step Flowchart2_A_node.idFlowchart2_A_1
209
                          Flowchart2_A_node.x_1
210
                          Flowchart2_A_node.idFlowchart2_A
211
                          Flowchart2_A_node.x
212
                          Flowchart2_A_node.__Flowchart2_A_node_14_c
213
                          Flowchart2_A_node.__Flowchart2_A_node_15_c
214
                          Flowchart2_A_node.ni_7._arrow._first_c
215
                          Flowchart2_A_node.__Flowchart2_A_node_14_x
216
                          Flowchart2_A_node.__Flowchart2_A_node_15_x
217
                          Flowchart2_A_node.ni_7._arrow._first_x)
218
))
219

    
220
; Flowchart2_A_en
221
(declare-var Flowchart2_A_en.idFlowchart2_A_1 Int)
222
(declare-var Flowchart2_A_en.idFlowchart2_Flowchart2_1 Int)
223
(declare-var Flowchart2_A_en.x_1 Int)
224
(declare-var Flowchart2_A_en.isInner Bool)
225
(declare-var Flowchart2_A_en.idFlowchart2_A Int)
226
(declare-var Flowchart2_A_en.idFlowchart2_Flowchart2 Int)
227
(declare-var Flowchart2_A_en.x Int)
228
(declare-var Flowchart2_A_en.__Flowchart2_A_en_1 Bool)
229
(declare-var Flowchart2_A_en.idFlowchart2_A_2 Int)
230
(declare-var Flowchart2_A_en.idFlowchart2_A_3 Int)
231
(declare-var Flowchart2_A_en.idFlowchart2_Flowchart2_3 Int)
232
(declare-var Flowchart2_A_en.idFlowchart2_Flowchart2_4 Int)
233
(declare-var Flowchart2_A_en.x_2 Int)
234
(declare-var Flowchart2_A_en.x_3 Int)
235
(declare-var Flowchart2_A_en.x_4 Int)
236
(declare-var Flowchart2_A_en.x_5 Int)
237
(declare-rel Flowchart2_A_en (Int Int Int Bool Int Int Int))
238
(rule (=> 
239
  (and (and (or (not (= (not Flowchart2_A_en.isInner) true))
240
               (= Flowchart2_A_en.x_2 1000))
241
            (or (not (= (not Flowchart2_A_en.isInner) false))
242
               (= Flowchart2_A_en.x_2 Flowchart2_A_en.x_1))
243
       )
244
       (POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action 
245
       Flowchart2_A_en.x_2
246
       Flowchart2_A_en.x_3)
247
       (= Flowchart2_A_en.__Flowchart2_A_en_1 (= Flowchart2_A_en.idFlowchart2_A_1 0))
248
       (and (or (not (= Flowchart2_A_en.__Flowchart2_A_en_1 false))
249
               (and (= Flowchart2_A_en.x_4 Flowchart2_A_en.x_2)
250
                    (= Flowchart2_A_en.idFlowchart2_Flowchart2_3 782)
251
                    (= Flowchart2_A_en.idFlowchart2_A_2 Flowchart2_A_en.idFlowchart2_A_1)
252
                    (= Flowchart2_A_en.x_5 Flowchart2_A_en.x_2)
253
                    (= Flowchart2_A_en.idFlowchart2_Flowchart2_4 782)
254
                    (= Flowchart2_A_en.idFlowchart2_A_3 Flowchart2_A_en.idFlowchart2_A_1)
255
                    ))
256
            (or (not (= Flowchart2_A_en.__Flowchart2_A_en_1 true))
257
               (and (= Flowchart2_A_en.x_4 Flowchart2_A_en.x_3)
258
                    (= Flowchart2_A_en.idFlowchart2_Flowchart2_3 782)
259
                    (= Flowchart2_A_en.idFlowchart2_A_2 Flowchart2_A_en.idFlowchart2_A_1)
260
                    (= Flowchart2_A_en.x_5 Flowchart2_A_en.x_4)
261
                    (= Flowchart2_A_en.idFlowchart2_Flowchart2_4 Flowchart2_A_en.idFlowchart2_Flowchart2_3)
262
                    (= Flowchart2_A_en.idFlowchart2_A_3 Flowchart2_A_en.idFlowchart2_A_2)
263
                    ))
264
       )
265
       (= Flowchart2_A_en.x Flowchart2_A_en.x_5)
266
       (= Flowchart2_A_en.idFlowchart2_Flowchart2 Flowchart2_A_en.idFlowchart2_Flowchart2_4)
267
       (= Flowchart2_A_en.idFlowchart2_A (- 1))
268
       )
269
  (Flowchart2_A_en Flowchart2_A_en.idFlowchart2_A_1 Flowchart2_A_en.idFlowchart2_Flowchart2_1 Flowchart2_A_en.x_1 Flowchart2_A_en.isInner Flowchart2_A_en.idFlowchart2_A Flowchart2_A_en.idFlowchart2_Flowchart2 Flowchart2_A_en.x)
270
))
271

    
272
; flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until
273
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_Flowchart2_1 Int)
274
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_1 Int)
275
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_1 Int)
276
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.flowchart2_flowchart2__restart_in Bool)
277
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.flowchart2_flowchart2__state_in flowchart2_flowchart2__type)
278
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_out Int)
279
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_Flowchart2_out Int)
280
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_out Int)
281
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c Bool)
282
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c flowchart2_a__type)
283
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c Bool)
284
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Bool)
285
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m flowchart2_a__type)
286
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Bool)
287
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x Bool)
288
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x flowchart2_a__type)
289
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x Bool)
290
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_2 Int)
291
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_2 Int)
292
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_3 Int)
293
(declare-rel flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until_reset (Bool flowchart2_a__type Bool Bool flowchart2_a__type Bool))
294
(declare-rel flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until_step (Int Int Int Bool flowchart2_flowchart2__type Int Int Int Bool flowchart2_a__type Bool Bool flowchart2_a__type Bool))
295

    
296
(rule (=> 
297
  (and 
298
       
299
       (Flowchart2_A_node_reset flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
300
                                flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
301
                                flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
302
                                flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
303
                                flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
304
                                flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m)
305
  )
306
  (flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until_reset flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
307
                                                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
308
                                                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
309
                                                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
310
                                                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
311
                                                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m)
312
))
313

    
314
(rule (=> 
315
  (and (Flowchart2_A_du flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_1
316
                        flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_2)
317
       (and (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c)
318
            (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c)
319
            (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c)
320
            )
321
       (Flowchart2_A_node_step flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_1
322
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_2
323
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_2
324
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_3
325
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
326
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
327
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
328
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
329
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
330
                               flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x)
331
       (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_out flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_3)
332
       (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_Flowchart2_out flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_Flowchart2_1)
333
       (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_out flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_2)
334
       (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.flowchart2_flowchart2__state_in POINTFlowchart2_Flowchart2)
335
       (= flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.flowchart2_flowchart2__restart_in true)
336
       )
337
  (flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until_step flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_Flowchart2_1
338
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_1
339
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_1
340
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.flowchart2_flowchart2__restart_in
341
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.flowchart2_flowchart2__state_in
342
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_A_out
343
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.idFlowchart2_Flowchart2_out
344
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.x_out
345
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
346
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
347
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
348
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
349
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
350
                                                              flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x)
351
))
352

    
353
; flowchart2_flowchart2__FLOWCHART2_A_IDL_unless
354
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__restart_in Bool)
355
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__state_in flowchart2_flowchart2__type)
356
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__restart_act Bool)
357
(declare-var flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__state_act flowchart2_flowchart2__type)
358
(declare-rel flowchart2_flowchart2__FLOWCHART2_A_IDL_unless (Bool flowchart2_flowchart2__type Bool flowchart2_flowchart2__type))
359
(rule (=> 
360
  (and (= flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__state_act flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__state_in)
361
       (= flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__restart_act flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__restart_in)
362
       )
363
  (flowchart2_flowchart2__FLOWCHART2_A_IDL_unless flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__restart_in flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__state_in flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__restart_act flowchart2_flowchart2__FLOWCHART2_A_IDL_unless.flowchart2_flowchart2__state_act)
364
))
365

    
366
; flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until
367
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_Flowchart2_1 Int)
368
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_A_1 Int)
369
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.x_1 Int)
370
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.flowchart2_flowchart2__restart_in Bool)
371
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.flowchart2_flowchart2__state_in flowchart2_flowchart2__type)
372
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_A_out Int)
373
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_Flowchart2_out Int)
374
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.x_out Int)
375
(declare-rel flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until (Int Int Int Bool flowchart2_flowchart2__type Int Int Int))
376
(rule (=> 
377
  (and (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.x_out flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.x_1)
378
       (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_Flowchart2_out flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_Flowchart2_1)
379
       (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_A_out flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_A_1)
380
       (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.flowchart2_flowchart2__state_in POINTFlowchart2_Flowchart2)
381
       (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.flowchart2_flowchart2__restart_in false)
382
       )
383
  (flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_Flowchart2_1 flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_A_1 flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.x_1 flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.flowchart2_flowchart2__restart_in flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.flowchart2_flowchart2__state_in flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_A_out flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.idFlowchart2_Flowchart2_out flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until.x_out)
384
))
385

    
386
; flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless
387
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_in Bool)
388
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_in flowchart2_flowchart2__type)
389
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.idFlowchart2_Flowchart2_1 Int)
390
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_act Bool)
391
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_act flowchart2_flowchart2__type)
392
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_1 Bool)
393
(declare-var flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_2 Bool)
394
(declare-rel flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless (Bool flowchart2_flowchart2__type Int Bool flowchart2_flowchart2__type))
395
(rule (=> 
396
  (and (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_2 (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.idFlowchart2_Flowchart2_1 782))
397
       (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_1 (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.idFlowchart2_Flowchart2_1 0))
398
       (and (or (not (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_1 false))
399
               (and (or (not (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_2 false))
400
                       (and (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_act flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_in)
401
                            (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_act flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_in)
402
                            ))
403
                    (or (not (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_2 true))
404
                       (and (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_act FLOWCHART2_A_IDL)
405
                            (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_act true)
406
                            ))
407
               ))
408
            (or (not (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.__flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless_1 true))
409
               (and (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_act POINT__TO__FLOWCHART2_A_1)
410
                    (= flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_act true)
411
                    ))
412
       )
413
       )
414
  (flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_in flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_in flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.idFlowchart2_Flowchart2_1 flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__restart_act flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless.flowchart2_flowchart2__state_act)
415
))
416

    
417
; flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until
418
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_1 Int)
419
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_1 Int)
420
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_1 Int)
421
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.flowchart2_flowchart2__restart_in Bool)
422
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.flowchart2_flowchart2__state_in flowchart2_flowchart2__type)
423
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_out Int)
424
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_out Int)
425
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_out Int)
426
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_2 Int)
427
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_2 Int)
428
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_2 Int)
429
(declare-rel flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until (Int Int Int Bool flowchart2_flowchart2__type Int Int Int))
430
(rule (=> 
431
  (and (Flowchart2_A_en flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_1
432
                        flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_1
433
                        flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_1
434
                        false
435
                        flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_2
436
                        flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_2
437
                        flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_2)
438
       (= flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_out flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_2)
439
       (= flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_out flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_2)
440
       (= flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_out flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_2)
441
       (= flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.flowchart2_flowchart2__state_in POINTFlowchart2_Flowchart2)
442
       (= flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.flowchart2_flowchart2__restart_in true)
443
       )
444
  (flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_1 flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_1 flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_1 flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.flowchart2_flowchart2__restart_in flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.flowchart2_flowchart2__state_in flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_A_out flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.idFlowchart2_Flowchart2_out flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until.x_out)
445
))
446

    
447
; flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless
448
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__restart_in Bool)
449
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__state_in flowchart2_flowchart2__type)
450
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__restart_act Bool)
451
(declare-var flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__state_act flowchart2_flowchart2__type)
452
(declare-rel flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless (Bool flowchart2_flowchart2__type Bool flowchart2_flowchart2__type))
453
(rule (=> 
454
  (and (= flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__state_act flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__state_in)
455
       (= flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__restart_act flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__restart_in)
456
       )
457
  (flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__restart_in flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__state_in flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__restart_act flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless.flowchart2_flowchart2__state_act)
458
))
459

    
460
; Flowchart2_Flowchart2_node
461
(declare-var Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2_1 Int)
462
(declare-var Flowchart2_Flowchart2_node.idFlowchart2_A_1 Int)
463
(declare-var Flowchart2_Flowchart2_node.x_1 Int)
464
(declare-var Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2 Int)
465
(declare-var Flowchart2_Flowchart2_node.idFlowchart2_A Int)
466
(declare-var Flowchart2_Flowchart2_node.x Int)
467
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c Bool)
468
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c flowchart2_flowchart2__type)
469
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c Bool)
470
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c flowchart2_a__type)
471
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c Bool)
472
(declare-var Flowchart2_Flowchart2_node.ni_5._arrow._first_c Bool)
473
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m Bool)
474
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m flowchart2_flowchart2__type)
475
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Bool)
476
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m flowchart2_a__type)
477
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Bool)
478
(declare-var Flowchart2_Flowchart2_node.ni_5._arrow._first_m Bool)
479
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x Bool)
480
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x flowchart2_flowchart2__type)
481
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x Bool)
482
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x flowchart2_a__type)
483
(declare-var Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x Bool)
484
(declare-var Flowchart2_Flowchart2_node.ni_5._arrow._first_x Bool)
485
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_1 Bool)
486
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_10 Int)
487
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_11 Int)
488
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_12 Bool)
489
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_13 flowchart2_flowchart2__type)
490
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_14 Int)
491
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_15 Int)
492
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_16 Int)
493
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_17 Bool)
494
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_18 flowchart2_flowchart2__type)
495
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_19 Int)
496
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_2 flowchart2_flowchart2__type)
497
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_20 Int)
498
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_21 Int)
499
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_22 Bool)
500
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_3 Bool)
501
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_4 flowchart2_flowchart2__type)
502
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_5 Bool)
503
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_6 flowchart2_flowchart2__type)
504
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_7 Bool)
505
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_8 flowchart2_flowchart2__type)
506
(declare-var Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_9 Int)
507
(declare-var Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_restart_in Bool)
508
(declare-var Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_state_in flowchart2_flowchart2__type)
509
(declare-var Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_act Bool)
510
(declare-var Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_in Bool)
511
(declare-var Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_act flowchart2_flowchart2__type)
512
(declare-var Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in flowchart2_flowchart2__type)
513
(declare-rel Flowchart2_Flowchart2_node_reset (Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool))
514
(declare-rel Flowchart2_Flowchart2_node_step (Int Int Int Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool))
515

    
516
(rule (=> 
517
  (and 
518
       (= Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c)
519
       (= Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c)
520
       (= Flowchart2_Flowchart2_node.ni_5._arrow._first_m true)
521
       (flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until_reset Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
522
                                                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
523
                                                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
524
                                                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
525
                                                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
526
                                                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m)
527
  )
528
  (Flowchart2_Flowchart2_node_reset Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
529
                                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
530
                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
531
                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
532
                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
533
                                    Flowchart2_Flowchart2_node.ni_5._arrow._first_c
534
                                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m
535
                                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m
536
                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
537
                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
538
                                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
539
                                    Flowchart2_Flowchart2_node.ni_5._arrow._first_m)
540
))
541

    
542
(rule (=> 
543
  (and (= Flowchart2_Flowchart2_node.ni_5._arrow._first_m Flowchart2_Flowchart2_node.ni_5._arrow._first_c)
544
       (and (= Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_22 (ite Flowchart2_Flowchart2_node.ni_5._arrow._first_m true false))
545
            (= Flowchart2_Flowchart2_node.ni_5._arrow._first_x false))
546
       (and (or (not (= Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_22 false))
547
               (and (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c)
548
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c)
549
                    ))
550
            (or (not (= Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_22 true))
551
               (and (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in POINTFlowchart2_Flowchart2)
552
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_in false)
553
                    ))
554
       )
555
       (and (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in FLOWCHART2_A_IDL))
556
               (and (flowchart2_flowchart2__FLOWCHART2_A_IDL_unless Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_in
557
                                                                    Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in
558
                                                                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_1
559
                                                                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_2)
560
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_act Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_2)
561
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_act Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_1)
562
                    ))
563
            (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in POINTFlowchart2_Flowchart2))
564
               (and (flowchart2_flowchart2__POINTFlowchart2_Flowchart2_unless 
565
                    Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_in
566
                    Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in
567
                    Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2_1
568
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_5
569
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_6)
570
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_act Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_6)
571
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_act Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_5)
572
                    ))
573
            (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in POINT__TO__FLOWCHART2_A_1))
574
               (and (flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_unless 
575
                    Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_in
576
                    Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_in
577
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_3
578
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_4)
579
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_act Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_4)
580
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_act Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_3)
581
                    ))
582
       )
583
       (and (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_act FLOWCHART2_A_IDL))
584
               (and (and (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_act true))
585
                            (flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until_reset 
586
                            Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
587
                            Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
588
                            Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
589
                            Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
590
                            Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
591
                            Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m))
592
                         (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__restart_act false))
593
                            (and (= Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c)
594
                                 (= Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c)
595
                                 (= Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c)
596
                                 )
597
                            )
598
                    )
599
                    (and (= Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c)
600
                         (= Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c)
601
                         (= Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c)
602
                         )
603
                    (flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until_step 
604
                    Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2_1
605
                    Flowchart2_Flowchart2_node.idFlowchart2_A_1
606
                    Flowchart2_Flowchart2_node.x_1
607
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_7
608
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_8
609
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_9
610
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_10
611
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_11
612
                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
613
                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
614
                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
615
                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
616
                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
617
                    Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x)
618
                    (= Flowchart2_Flowchart2_node.x Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_11)
619
                    (= Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2 Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_10)
620
                    (= Flowchart2_Flowchart2_node.idFlowchart2_A Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_9)
621
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_state_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_8)
622
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_restart_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_7)
623
                    ))
624
            (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_act POINTFlowchart2_Flowchart2))
625
               (and (flowchart2_flowchart2__POINTFlowchart2_Flowchart2_handler_until 
626
                    Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2_1
627
                    Flowchart2_Flowchart2_node.idFlowchart2_A_1
628
                    Flowchart2_Flowchart2_node.x_1
629
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_17
630
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_18
631
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_19
632
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_20
633
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_21)
634
                    (= Flowchart2_Flowchart2_node.x Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_21)
635
                    (= Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2 Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_20)
636
                    (= Flowchart2_Flowchart2_node.idFlowchart2_A Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_19)
637
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_state_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_18)
638
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_restart_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_17)
639
                    ))
640
            (or (not (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__state_act POINT__TO__FLOWCHART2_A_1))
641
               (and (flowchart2_flowchart2__POINT__TO__FLOWCHART2_A_1_handler_until 
642
                    Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2_1
643
                    Flowchart2_Flowchart2_node.idFlowchart2_A_1
644
                    Flowchart2_Flowchart2_node.x_1
645
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_12
646
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_13
647
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_14
648
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_15
649
                    Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_16)
650
                    (= Flowchart2_Flowchart2_node.x Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_16)
651
                    (= Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2 Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_15)
652
                    (= Flowchart2_Flowchart2_node.idFlowchart2_A Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_14)
653
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_state_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_13)
654
                    (= Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_restart_in Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_12)
655
                    ))
656
       )
657
       (= Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_state_in)
658
       (= Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x Flowchart2_Flowchart2_node.flowchart2_flowchart2__next_restart_in)
659
       )
660
  (Flowchart2_Flowchart2_node_step Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2_1
661
                                   Flowchart2_Flowchart2_node.idFlowchart2_A_1
662
                                   Flowchart2_Flowchart2_node.x_1
663
                                   Flowchart2_Flowchart2_node.idFlowchart2_Flowchart2
664
                                   Flowchart2_Flowchart2_node.idFlowchart2_A
665
                                   Flowchart2_Flowchart2_node.x
666
                                   Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
667
                                   Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
668
                                   Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
669
                                   Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
670
                                   Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
671
                                   Flowchart2_Flowchart2_node.ni_5._arrow._first_c
672
                                   Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x
673
                                   Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x
674
                                   Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
675
                                   Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
676
                                   Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x
677
                                   Flowchart2_Flowchart2_node.ni_5._arrow._first_x)
678
))
679

    
680
; Flowchart2_Flowchart2
681
(declare-var Flowchart2_Flowchart2.noInput Bool)
682
(declare-var Flowchart2_Flowchart2.x Int)
683
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c Int)
684
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c Int)
685
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c Int)
686
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c Bool)
687
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c flowchart2_flowchart2__type)
688
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c Bool)
689
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c flowchart2_a__type)
690
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c Bool)
691
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c Bool)
692
(declare-var Flowchart2_Flowchart2.ni_3._arrow._first_c Bool)
693
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m Int)
694
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m Int)
695
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m Int)
696
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m Bool)
697
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m flowchart2_flowchart2__type)
698
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Bool)
699
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m flowchart2_a__type)
700
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Bool)
701
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m Bool)
702
(declare-var Flowchart2_Flowchart2.ni_3._arrow._first_m Bool)
703
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_x Int)
704
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_x Int)
705
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_x Int)
706
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x Bool)
707
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x flowchart2_flowchart2__type)
708
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x Bool)
709
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x flowchart2_a__type)
710
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x Bool)
711
(declare-var Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_x Bool)
712
(declare-var Flowchart2_Flowchart2.ni_3._arrow._first_x Bool)
713
(declare-var Flowchart2_Flowchart2.__Flowchart2_Flowchart2_1 Bool)
714
(declare-var Flowchart2_Flowchart2.idFlowchart2_A Int)
715
(declare-var Flowchart2_Flowchart2.idFlowchart2_A_1 Int)
716
(declare-var Flowchart2_Flowchart2.idFlowchart2_Flowchart2 Int)
717
(declare-var Flowchart2_Flowchart2.idFlowchart2_Flowchart2_1 Int)
718
(declare-var Flowchart2_Flowchart2.x_1 Int)
719
(declare-rel Flowchart2_Flowchart2_reset (Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool))
720
(declare-rel Flowchart2_Flowchart2_step (Bool Int Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool))
721

    
722
(rule (=> 
723
  (and 
724
       (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c)
725
       (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c)
726
       (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c)
727
       (= Flowchart2_Flowchart2.ni_3._arrow._first_m true)
728
       (Flowchart2_Flowchart2_node_reset Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
729
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
730
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
731
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
732
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
733
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c
734
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m
735
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m
736
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
737
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
738
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
739
                                         Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m)
740
  )
741
  (Flowchart2_Flowchart2_reset Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c
742
                               Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c
743
                               Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c
744
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
745
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
746
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
747
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
748
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
749
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c
750
                               Flowchart2_Flowchart2.ni_3._arrow._first_c
751
                               Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m
752
                               Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m
753
                               Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m
754
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m
755
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m
756
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
757
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
758
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
759
                               Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m
760
                               Flowchart2_Flowchart2.ni_3._arrow._first_m)
761
))
762

    
763
(rule (=> 
764
  (and (= Flowchart2_Flowchart2.ni_3._arrow._first_m Flowchart2_Flowchart2.ni_3._arrow._first_c)
765
       (and (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_1 (ite Flowchart2_Flowchart2.ni_3._arrow._first_m true false))
766
            (= Flowchart2_Flowchart2.ni_3._arrow._first_x false))
767
       (and (or (not (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_1 false))
768
               (and (= Flowchart2_Flowchart2.x_1 Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c)
769
                    (= Flowchart2_Flowchart2.idFlowchart2_Flowchart2_1 Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c)
770
                    (= Flowchart2_Flowchart2.idFlowchart2_A_1 Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c)
771
                    ))
772
            (or (not (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_1 true))
773
               (and (= Flowchart2_Flowchart2.x_1 0)
774
                    (= Flowchart2_Flowchart2.idFlowchart2_Flowchart2_1 0)
775
                    (= Flowchart2_Flowchart2.idFlowchart2_A_1 0)
776
                    ))
777
       )
778
       (and (= Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c)
779
            (= Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c)
780
            (= Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c)
781
            (= Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c)
782
            (= Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c)
783
            (= Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c)
784
            )
785
       (Flowchart2_Flowchart2_node_step Flowchart2_Flowchart2.idFlowchart2_Flowchart2_1
786
                                        Flowchart2_Flowchart2.idFlowchart2_A_1
787
                                        Flowchart2_Flowchart2.x_1
788
                                        Flowchart2_Flowchart2.idFlowchart2_Flowchart2
789
                                        Flowchart2_Flowchart2.idFlowchart2_A
790
                                        Flowchart2_Flowchart2.x
791
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m
792
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m
793
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
794
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
795
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
796
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m
797
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x
798
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x
799
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
800
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
801
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x
802
                                        Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_x)
803
       (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_x Flowchart2_Flowchart2.x)
804
       (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_x Flowchart2_Flowchart2.idFlowchart2_Flowchart2)
805
       (= Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_x Flowchart2_Flowchart2.idFlowchart2_A)
806
       )
807
  (Flowchart2_Flowchart2_step Flowchart2_Flowchart2.noInput
808
                              Flowchart2_Flowchart2.x
809
                              Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c
810
                              Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c
811
                              Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c
812
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
813
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
814
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
815
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
816
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
817
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c
818
                              Flowchart2_Flowchart2.ni_3._arrow._first_c
819
                              Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_x
820
                              Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_x
821
                              Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_x
822
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x
823
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x
824
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
825
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
826
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x
827
                              Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_x
828
                              Flowchart2_Flowchart2.ni_3._arrow._first_x)
829
))
830

    
831
; Flowchart2
832
(declare-var Flowchart2.i_virtual Real)
833
(declare-var Flowchart2.Out1_1_1 Int)
834
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c Int)
835
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c Int)
836
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c Int)
837
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c Bool)
838
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c flowchart2_flowchart2__type)
839
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c Bool)
840
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c flowchart2_a__type)
841
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c Bool)
842
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c Bool)
843
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_c Bool)
844
(declare-var Flowchart2.ni_1._arrow._first_c Bool)
845
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m Int)
846
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m Int)
847
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m Int)
848
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m Bool)
849
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m flowchart2_flowchart2__type)
850
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Bool)
851
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m flowchart2_a__type)
852
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Bool)
853
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m Bool)
854
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_m Bool)
855
(declare-var Flowchart2.ni_1._arrow._first_m Bool)
856
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_x Int)
857
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_x Int)
858
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_x Int)
859
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x Bool)
860
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x flowchart2_flowchart2__type)
861
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x Bool)
862
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x flowchart2_a__type)
863
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x Bool)
864
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_x Bool)
865
(declare-var Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_x Bool)
866
(declare-var Flowchart2.ni_1._arrow._first_x Bool)
867
(declare-var Flowchart2.Flowchart2_1_1 Int)
868
(declare-var Flowchart2.__Flowchart2_1 Bool)
869
(declare-var Flowchart2.i_virtual_local Real)
870
(declare-rel Flowchart2_reset (Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool Bool Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool Bool))
871
(declare-rel Flowchart2_step (Real Int Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool Bool Int Int Int Bool flowchart2_flowchart2__type Bool flowchart2_a__type Bool Bool Bool Bool))
872

    
873
(rule (=> 
874
  (and 
875
       
876
       (= Flowchart2.ni_1._arrow._first_m true)
877
       (Flowchart2_Flowchart2_reset Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c
878
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c
879
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c
880
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
881
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
882
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
883
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
884
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
885
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c
886
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_c
887
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m
888
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m
889
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m
890
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m
891
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m
892
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
893
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
894
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
895
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m
896
                                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_m)
897
  )
898
  (Flowchart2_reset Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c
899
                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c
900
                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c
901
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
902
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
903
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
904
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
905
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
906
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c
907
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_c
908
                    Flowchart2.ni_1._arrow._first_c
909
                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m
910
                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m
911
                    Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m
912
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m
913
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m
914
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
915
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
916
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
917
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m
918
                    Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_m
919
                    Flowchart2.ni_1._arrow._first_m)
920
))
921

    
922
(rule (=> 
923
  (and (= Flowchart2.ni_1._arrow._first_m Flowchart2.ni_1._arrow._first_c)
924
       (and (= Flowchart2.__Flowchart2_1 (ite Flowchart2.ni_1._arrow._first_m true false))
925
            (= Flowchart2.ni_1._arrow._first_x false))
926
       (and (or (not (= Flowchart2.__Flowchart2_1 true))
927
               (= Flowchart2.i_virtual_local 0.))
928
            (or (not (= Flowchart2.__Flowchart2_1 false))
929
               (= Flowchart2.i_virtual_local 1.))
930
       )
931
       (and (= Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c)
932
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c)
933
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c)
934
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c)
935
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c)
936
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c)
937
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c)
938
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c)
939
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c)
940
            (= Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_m Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_c)
941
            )
942
       (Flowchart2_Flowchart2_step true
943
                                   Flowchart2.Flowchart2_1_1
944
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_m
945
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_m
946
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_m
947
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_m
948
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_m
949
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_m
950
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_m
951
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_m
952
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_m
953
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_m
954
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_x
955
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_x
956
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_x
957
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x
958
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x
959
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
960
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
961
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x
962
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_x
963
                                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_x)
964
       (= Flowchart2.Out1_1_1 Flowchart2.Flowchart2_1_1)
965
       )
966
  (Flowchart2_step Flowchart2.i_virtual
967
                   Flowchart2.Out1_1_1
968
                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_c
969
                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_c
970
                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_c
971
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_c
972
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_c
973
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_c
974
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_c
975
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_c
976
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_c
977
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_c
978
                   Flowchart2.ni_1._arrow._first_c
979
                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_2_x
980
                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_3_x
981
                   Flowchart2.ni_0.Flowchart2_Flowchart2.__Flowchart2_Flowchart2_4_x
982
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_23_x
983
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.__Flowchart2_Flowchart2_node_24_x
984
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_14_x
985
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.__Flowchart2_A_node_15_x
986
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_4.flowchart2_flowchart2__FLOWCHART2_A_IDL_handler_until.ni_6.Flowchart2_A_node.ni_7._arrow._first_x
987
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_2.Flowchart2_Flowchart2_node.ni_5._arrow._first_x
988
                   Flowchart2.ni_0.Flowchart2_Flowchart2.ni_3._arrow._first_x
989
                   Flowchart2.ni_1._arrow._first_x)
990
))
991

    
992
; Flowchart2_A_ex
993
(declare-var Flowchart2_A_ex.idFlowchart2_Flowchart2_1 Int)
994
(declare-var Flowchart2_A_ex.isInner Bool)
995
(declare-var Flowchart2_A_ex.idFlowchart2_Flowchart2 Int)
996
(declare-var Flowchart2_A_ex.idFlowchart2_Flowchart2_2 Int)
997
(declare-rel Flowchart2_A_ex (Int Bool Int))
998
(rule (=> 
999
  (and (and (or (not (= (not Flowchart2_A_ex.isInner) true))
1000
               (= Flowchart2_A_ex.idFlowchart2_Flowchart2_2 0))
1001
            (or (not (= (not Flowchart2_A_ex.isInner) false))
1002
               (= Flowchart2_A_ex.idFlowchart2_Flowchart2_2 Flowchart2_A_ex.idFlowchart2_Flowchart2_1))
1003
       )
1004
       (= Flowchart2_A_ex.idFlowchart2_Flowchart2 Flowchart2_A_ex.idFlowchart2_Flowchart2_1)
1005
       )
1006
  (Flowchart2_A_ex Flowchart2_A_ex.idFlowchart2_Flowchart2_1 Flowchart2_A_ex.isInner Flowchart2_A_ex.idFlowchart2_Flowchart2)
1007
))
1008