Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart5 / Flowchart5.smt2 @ eb639349

History | View | Annotate | Download (116 KB)

1
(declare-datatypes () ((flowchart5_a__type POINTFlowchart5_A POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1)));
2

    
3
(declare-datatypes () ((flowchart5_flowchart5__type POINTFlowchart5_Flowchart5 POINT__TO__FLOWCHART5_A_1 FLOWCHART5_FLOWCHART5_PARALLEL_IDL)));
4

    
5
(declare-datatypes () ((flowchart5_a_INNER__type POINTFlowchart5_A_INNER FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1)));
6

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

    
16
; flowchart5_a__POINTFlowchart5_A_handler_until
17
(declare-var flowchart5_a__POINTFlowchart5_A_handler_until.idFlowchart5_A_1 Int)
18
(declare-var flowchart5_a__POINTFlowchart5_A_handler_until.x_1 Int)
19
(declare-var flowchart5_a__POINTFlowchart5_A_handler_until.flowchart5_a__restart_in Bool)
20
(declare-var flowchart5_a__POINTFlowchart5_A_handler_until.flowchart5_a__state_in flowchart5_a__type)
21
(declare-var flowchart5_a__POINTFlowchart5_A_handler_until.idFlowchart5_A_out Int)
22
(declare-var flowchart5_a__POINTFlowchart5_A_handler_until.x_out Int)
23
(declare-rel flowchart5_a__POINTFlowchart5_A_handler_until (Int Int Bool flowchart5_a__type Int Int))
24
(rule (=> 
25
  (and (= flowchart5_a__POINTFlowchart5_A_handler_until.x_out flowchart5_a__POINTFlowchart5_A_handler_until.x_1)
26
       (= flowchart5_a__POINTFlowchart5_A_handler_until.idFlowchart5_A_out flowchart5_a__POINTFlowchart5_A_handler_until.idFlowchart5_A_1)
27
       (= flowchart5_a__POINTFlowchart5_A_handler_until.flowchart5_a__state_in POINTFlowchart5_A)
28
       (= flowchart5_a__POINTFlowchart5_A_handler_until.flowchart5_a__restart_in false)
29
       )
30
  (flowchart5_a__POINTFlowchart5_A_handler_until flowchart5_a__POINTFlowchart5_A_handler_until.idFlowchart5_A_1 flowchart5_a__POINTFlowchart5_A_handler_until.x_1 flowchart5_a__POINTFlowchart5_A_handler_until.flowchart5_a__restart_in flowchart5_a__POINTFlowchart5_A_handler_until.flowchart5_a__state_in flowchart5_a__POINTFlowchart5_A_handler_until.idFlowchart5_A_out flowchart5_a__POINTFlowchart5_A_handler_until.x_out)
31
))
32

    
33
; flowchart5_a__POINTFlowchart5_A_unless
34
(declare-var flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__restart_in Bool)
35
(declare-var flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__state_in flowchart5_a__type)
36
(declare-var flowchart5_a__POINTFlowchart5_A_unless.idFlowchart5_A_1 Int)
37
(declare-var flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__restart_act Bool)
38
(declare-var flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__state_act flowchart5_a__type)
39
(declare-var flowchart5_a__POINTFlowchart5_A_unless.__flowchart5_a__POINTFlowchart5_A_unless_1 Bool)
40
(declare-rel flowchart5_a__POINTFlowchart5_A_unless (Bool flowchart5_a__type Int Bool flowchart5_a__type))
41
(rule (=> 
42
  (and (= flowchart5_a__POINTFlowchart5_A_unless.__flowchart5_a__POINTFlowchart5_A_unless_1 (= flowchart5_a__POINTFlowchart5_A_unless.idFlowchart5_A_1 0))
43
       (and (or (not (= flowchart5_a__POINTFlowchart5_A_unless.__flowchart5_a__POINTFlowchart5_A_unless_1 false))
44
               (and (= flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__state_act flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__state_in)
45
                    (= flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__restart_act flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__restart_in)
46
                    ))
47
            (or (not (= flowchart5_a__POINTFlowchart5_A_unless.__flowchart5_a__POINTFlowchart5_A_unless_1 true))
48
               (and (= flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__state_act POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1)
49
                    (= flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__restart_act true)
50
                    ))
51
       )
52
       )
53
  (flowchart5_a__POINTFlowchart5_A_unless flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__restart_in flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__state_in flowchart5_a__POINTFlowchart5_A_unless.idFlowchart5_A_1 flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__restart_act flowchart5_a__POINTFlowchart5_A_unless.flowchart5_a__state_act)
54
))
55

    
56
; flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until
57
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.idFlowchart5_A_1 Int)
58
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_1 Int)
59
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a__restart_in Bool)
60
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a__state_in flowchart5_a__type)
61
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.idFlowchart5_A_out Int)
62
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_out Int)
63
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_2 Int)
64
(declare-rel flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until (Int Int Bool flowchart5_a__type Int Int))
65
(rule (=> 
66
  (and (Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action 
67
       flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_1
68
       flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_2)
69
       (= flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_out flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_2)
70
       (= flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.idFlowchart5_A_out flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.idFlowchart5_A_1)
71
       (= flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a__state_in POINTFlowchart5_A)
72
       (= flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a__restart_in true)
73
       )
74
  (flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.idFlowchart5_A_1 flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_1 flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a__restart_in flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a__state_in flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.idFlowchart5_A_out flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_out)
75
))
76

    
77
; flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless
78
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__restart_in Bool)
79
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__state_in flowchart5_a__type)
80
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__restart_act Bool)
81
(declare-var flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__state_act flowchart5_a__type)
82
(declare-rel flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless (Bool flowchart5_a__type Bool flowchart5_a__type))
83
(rule (=> 
84
  (and (= flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__state_act flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__state_in)
85
       (= flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__restart_act flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__restart_in)
86
       )
87
  (flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__restart_in flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__state_in flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__restart_act flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a__state_act)
88
))
89

    
90
; Flowchart5_A_node
91
(declare-var Flowchart5_A_node.idFlowchart5_A_1 Int)
92
(declare-var Flowchart5_A_node.x_1 Int)
93
(declare-var Flowchart5_A_node.idFlowchart5_A Int)
94
(declare-var Flowchart5_A_node.x Int)
95
(declare-var Flowchart5_A_node.__Flowchart5_A_node_14_c Bool)
96
(declare-var Flowchart5_A_node.__Flowchart5_A_node_15_c flowchart5_a__type)
97
(declare-var Flowchart5_A_node.ni_8._arrow._first_c Bool)
98
(declare-var Flowchart5_A_node.__Flowchart5_A_node_14_m Bool)
99
(declare-var Flowchart5_A_node.__Flowchart5_A_node_15_m flowchart5_a__type)
100
(declare-var Flowchart5_A_node.ni_8._arrow._first_m Bool)
101
(declare-var Flowchart5_A_node.__Flowchart5_A_node_14_x Bool)
102
(declare-var Flowchart5_A_node.__Flowchart5_A_node_15_x flowchart5_a__type)
103
(declare-var Flowchart5_A_node.ni_8._arrow._first_x Bool)
104
(declare-var Flowchart5_A_node.__Flowchart5_A_node_1 Bool)
105
(declare-var Flowchart5_A_node.__Flowchart5_A_node_10 flowchart5_a__type)
106
(declare-var Flowchart5_A_node.__Flowchart5_A_node_11 Int)
107
(declare-var Flowchart5_A_node.__Flowchart5_A_node_12 Int)
108
(declare-var Flowchart5_A_node.__Flowchart5_A_node_13 Bool)
109
(declare-var Flowchart5_A_node.__Flowchart5_A_node_2 flowchart5_a__type)
110
(declare-var Flowchart5_A_node.__Flowchart5_A_node_3 Bool)
111
(declare-var Flowchart5_A_node.__Flowchart5_A_node_4 flowchart5_a__type)
112
(declare-var Flowchart5_A_node.__Flowchart5_A_node_5 Bool)
113
(declare-var Flowchart5_A_node.__Flowchart5_A_node_6 flowchart5_a__type)
114
(declare-var Flowchart5_A_node.__Flowchart5_A_node_7 Int)
115
(declare-var Flowchart5_A_node.__Flowchart5_A_node_8 Int)
116
(declare-var Flowchart5_A_node.__Flowchart5_A_node_9 Bool)
117
(declare-var Flowchart5_A_node.flowchart5_a__next_restart_in Bool)
118
(declare-var Flowchart5_A_node.flowchart5_a__next_state_in flowchart5_a__type)
119
(declare-var Flowchart5_A_node.flowchart5_a__restart_act Bool)
120
(declare-var Flowchart5_A_node.flowchart5_a__restart_in Bool)
121
(declare-var Flowchart5_A_node.flowchart5_a__state_act flowchart5_a__type)
122
(declare-var Flowchart5_A_node.flowchart5_a__state_in flowchart5_a__type)
123
(declare-rel Flowchart5_A_node_reset (Bool flowchart5_a__type Bool Bool flowchart5_a__type Bool))
124
(declare-rel Flowchart5_A_node_step (Int Int Int Int Bool flowchart5_a__type Bool Bool flowchart5_a__type Bool))
125

    
126
(rule (=> 
127
  (and 
128
       (= Flowchart5_A_node.__Flowchart5_A_node_14_m Flowchart5_A_node.__Flowchart5_A_node_14_c)
129
       (= Flowchart5_A_node.__Flowchart5_A_node_15_m Flowchart5_A_node.__Flowchart5_A_node_15_c)
130
       (= Flowchart5_A_node.ni_8._arrow._first_m true)
131
  )
132
  (Flowchart5_A_node_reset Flowchart5_A_node.__Flowchart5_A_node_14_c
133
                           Flowchart5_A_node.__Flowchart5_A_node_15_c
134
                           Flowchart5_A_node.ni_8._arrow._first_c
135
                           Flowchart5_A_node.__Flowchart5_A_node_14_m
136
                           Flowchart5_A_node.__Flowchart5_A_node_15_m
137
                           Flowchart5_A_node.ni_8._arrow._first_m)
138
))
139

    
140
(rule (=> 
141
  (and (= Flowchart5_A_node.ni_8._arrow._first_m Flowchart5_A_node.ni_8._arrow._first_c)
142
       (and (= Flowchart5_A_node.__Flowchart5_A_node_13 (ite Flowchart5_A_node.ni_8._arrow._first_m true false))
143
            (= Flowchart5_A_node.ni_8._arrow._first_x false))
144
       (and (or (not (= Flowchart5_A_node.__Flowchart5_A_node_13 false))
145
               (and (= Flowchart5_A_node.flowchart5_a__state_in Flowchart5_A_node.__Flowchart5_A_node_15_c)
146
                    (= Flowchart5_A_node.flowchart5_a__restart_in Flowchart5_A_node.__Flowchart5_A_node_14_c)
147
                    ))
148
            (or (not (= Flowchart5_A_node.__Flowchart5_A_node_13 true))
149
               (and (= Flowchart5_A_node.flowchart5_a__state_in POINTFlowchart5_A)
150
                    (= Flowchart5_A_node.flowchart5_a__restart_in false)
151
                    ))
152
       )
153
       (and (or (not (= Flowchart5_A_node.flowchart5_a__state_in POINTFlowchart5_A))
154
               (and (flowchart5_a__POINTFlowchart5_A_unless Flowchart5_A_node.flowchart5_a__restart_in
155
                                                            Flowchart5_A_node.flowchart5_a__state_in
156
                                                            Flowchart5_A_node.idFlowchart5_A_1
157
                                                            Flowchart5_A_node.__Flowchart5_A_node_3
158
                                                            Flowchart5_A_node.__Flowchart5_A_node_4)
159
                    (= Flowchart5_A_node.flowchart5_a__state_act Flowchart5_A_node.__Flowchart5_A_node_4)
160
                    (= Flowchart5_A_node.flowchart5_a__restart_act Flowchart5_A_node.__Flowchart5_A_node_3)
161
                    ))
162
            (or (not (= Flowchart5_A_node.flowchart5_a__state_in POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1))
163
               (and (flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless 
164
                    Flowchart5_A_node.flowchart5_a__restart_in
165
                    Flowchart5_A_node.flowchart5_a__state_in
166
                    Flowchart5_A_node.__Flowchart5_A_node_1
167
                    Flowchart5_A_node.__Flowchart5_A_node_2)
168
                    (= Flowchart5_A_node.flowchart5_a__state_act Flowchart5_A_node.__Flowchart5_A_node_2)
169
                    (= Flowchart5_A_node.flowchart5_a__restart_act Flowchart5_A_node.__Flowchart5_A_node_1)
170
                    ))
171
       )
172
       (and (or (not (= Flowchart5_A_node.flowchart5_a__state_act POINTFlowchart5_A))
173
               (and (flowchart5_a__POINTFlowchart5_A_handler_until Flowchart5_A_node.idFlowchart5_A_1
174
                                                                   Flowchart5_A_node.x_1
175
                                                                   Flowchart5_A_node.__Flowchart5_A_node_9
176
                                                                   Flowchart5_A_node.__Flowchart5_A_node_10
177
                                                                   Flowchart5_A_node.__Flowchart5_A_node_11
178
                                                                   Flowchart5_A_node.__Flowchart5_A_node_12)
179
                    (= Flowchart5_A_node.x Flowchart5_A_node.__Flowchart5_A_node_12)
180
                    (= Flowchart5_A_node.idFlowchart5_A Flowchart5_A_node.__Flowchart5_A_node_11)
181
                    (= Flowchart5_A_node.flowchart5_a__next_state_in Flowchart5_A_node.__Flowchart5_A_node_10)
182
                    (= Flowchart5_A_node.flowchart5_a__next_restart_in Flowchart5_A_node.__Flowchart5_A_node_9)
183
                    ))
184
            (or (not (= Flowchart5_A_node.flowchart5_a__state_act POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1))
185
               (and (flowchart5_a__POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until 
186
                    Flowchart5_A_node.idFlowchart5_A_1
187
                    Flowchart5_A_node.x_1
188
                    Flowchart5_A_node.__Flowchart5_A_node_5
189
                    Flowchart5_A_node.__Flowchart5_A_node_6
190
                    Flowchart5_A_node.__Flowchart5_A_node_7
191
                    Flowchart5_A_node.__Flowchart5_A_node_8)
192
                    (= Flowchart5_A_node.x Flowchart5_A_node.__Flowchart5_A_node_8)
193
                    (= Flowchart5_A_node.idFlowchart5_A Flowchart5_A_node.__Flowchart5_A_node_7)
194
                    (= Flowchart5_A_node.flowchart5_a__next_state_in Flowchart5_A_node.__Flowchart5_A_node_6)
195
                    (= Flowchart5_A_node.flowchart5_a__next_restart_in Flowchart5_A_node.__Flowchart5_A_node_5)
196
                    ))
197
       )
198
       (= Flowchart5_A_node.__Flowchart5_A_node_15_x Flowchart5_A_node.flowchart5_a__next_state_in)
199
       (= Flowchart5_A_node.__Flowchart5_A_node_14_x Flowchart5_A_node.flowchart5_a__next_restart_in)
200
       )
201
  (Flowchart5_A_node_step Flowchart5_A_node.idFlowchart5_A_1
202
                          Flowchart5_A_node.x_1
203
                          Flowchart5_A_node.idFlowchart5_A
204
                          Flowchart5_A_node.x
205
                          Flowchart5_A_node.__Flowchart5_A_node_14_c
206
                          Flowchart5_A_node.__Flowchart5_A_node_15_c
207
                          Flowchart5_A_node.ni_8._arrow._first_c
208
                          Flowchart5_A_node.__Flowchart5_A_node_14_x
209
                          Flowchart5_A_node.__Flowchart5_A_node_15_x
210
                          Flowchart5_A_node.ni_8._arrow._first_x)
211
))
212

    
213
; Flowchart5_A_en
214
(declare-var Flowchart5_A_en.idFlowchart5_A_1 Int)
215
(declare-var Flowchart5_A_en.idFlowchart5_Flowchart5_1 Int)
216
(declare-var Flowchart5_A_en.x_1 Int)
217
(declare-var Flowchart5_A_en.isInner Bool)
218
(declare-var Flowchart5_A_en.idFlowchart5_A Int)
219
(declare-var Flowchart5_A_en.idFlowchart5_Flowchart5 Int)
220
(declare-var Flowchart5_A_en.x Int)
221
(declare-var Flowchart5_A_en.__Flowchart5_A_en_1 Bool)
222
(declare-var Flowchart5_A_en.idFlowchart5_A_2 Int)
223
(declare-var Flowchart5_A_en.idFlowchart5_A_3 Int)
224
(declare-var Flowchart5_A_en.idFlowchart5_Flowchart5_3 Int)
225
(declare-var Flowchart5_A_en.idFlowchart5_Flowchart5_4 Int)
226
(declare-var Flowchart5_A_en.x_2 Int)
227
(declare-var Flowchart5_A_en.x_3 Int)
228
(declare-var Flowchart5_A_en.x_4 Int)
229
(declare-rel Flowchart5_A_en (Int Int Int Bool Int Int Int))
230
(rule (=> 
231
  (and (Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action 
232
       Flowchart5_A_en.x_1
233
       Flowchart5_A_en.x_2)
234
       (= Flowchart5_A_en.__Flowchart5_A_en_1 (= Flowchart5_A_en.idFlowchart5_A_1 0))
235
       (and (or (not (= Flowchart5_A_en.__Flowchart5_A_en_1 false))
236
               (and (= Flowchart5_A_en.x_3 Flowchart5_A_en.x_1)
237
                    (= Flowchart5_A_en.idFlowchart5_Flowchart5_3 806)
238
                    (= Flowchart5_A_en.idFlowchart5_A_2 Flowchart5_A_en.idFlowchart5_A_1)
239
                    (= Flowchart5_A_en.x_4 Flowchart5_A_en.x_1)
240
                    (= Flowchart5_A_en.idFlowchart5_Flowchart5_4 806)
241
                    (= Flowchart5_A_en.idFlowchart5_A_3 Flowchart5_A_en.idFlowchart5_A_1)
242
                    ))
243
            (or (not (= Flowchart5_A_en.__Flowchart5_A_en_1 true))
244
               (and (= Flowchart5_A_en.x_3 Flowchart5_A_en.x_2)
245
                    (= Flowchart5_A_en.idFlowchart5_Flowchart5_3 806)
246
                    (= Flowchart5_A_en.idFlowchart5_A_2 Flowchart5_A_en.idFlowchart5_A_1)
247
                    (= Flowchart5_A_en.x_4 Flowchart5_A_en.x_3)
248
                    (= Flowchart5_A_en.idFlowchart5_Flowchart5_4 Flowchart5_A_en.idFlowchart5_Flowchart5_3)
249
                    (= Flowchart5_A_en.idFlowchart5_A_3 Flowchart5_A_en.idFlowchart5_A_2)
250
                    ))
251
       )
252
       (= Flowchart5_A_en.x Flowchart5_A_en.x_4)
253
       (= Flowchart5_A_en.idFlowchart5_Flowchart5 Flowchart5_A_en.idFlowchart5_Flowchart5_4)
254
       (= Flowchart5_A_en.idFlowchart5_A (- 1))
255
       )
256
  (Flowchart5_A_en Flowchart5_A_en.idFlowchart5_A_1 Flowchart5_A_en.idFlowchart5_Flowchart5_1 Flowchart5_A_en.x_1 Flowchart5_A_en.isInner Flowchart5_A_en.idFlowchart5_A Flowchart5_A_en.idFlowchart5_Flowchart5 Flowchart5_A_en.x)
257
))
258

    
259
; flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until
260
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_Flowchart5_1 Int)
261
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_1 Int)
262
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_1 Int)
263
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.flowchart5_flowchart5__restart_in Bool)
264
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.flowchart5_flowchart5__state_in flowchart5_flowchart5__type)
265
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_out Int)
266
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_Flowchart5_out Int)
267
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_out Int)
268
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c Bool)
269
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c flowchart5_a__type)
270
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c Bool)
271
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Bool)
272
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m flowchart5_a__type)
273
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Bool)
274
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x Bool)
275
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x flowchart5_a__type)
276
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x Bool)
277
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_1 Bool)
278
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_2 Int)
279
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_3 Int)
280
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_2 Int)
281
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_2 Int)
282
(declare-rel flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_reset (Bool flowchart5_a__type Bool Bool flowchart5_a__type Bool))
283
(declare-rel flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_step (Int Int Int Bool flowchart5_flowchart5__type Int Int Int Bool flowchart5_a__type Bool Bool flowchart5_a__type Bool))
284

    
285
(rule (=> 
286
  (and 
287
       
288
       (Flowchart5_A_node_reset flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
289
                                flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
290
                                flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
291
                                flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
292
                                flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
293
                                flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m)
294
  )
295
  (flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_reset 
296
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
297
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
298
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
299
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
300
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
301
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m)
302
))
303

    
304
(rule (=> 
305
  (and (and (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c)
306
            (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c)
307
            (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c)
308
            )
309
       (Flowchart5_A_node_step flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_1
310
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_1
311
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_2
312
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_3
313
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
314
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
315
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
316
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
317
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
318
                               flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x)
319
       (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_1 (not (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_1 0)))
320
       (and (or (not (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_1 true))
321
               (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_2 flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_3))
322
            (or (not (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_1 false))
323
               (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_2 flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_1))
324
       )
325
       (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_out flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_2)
326
       (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_Flowchart5_out flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_Flowchart5_1)
327
       (and (or (not (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_1 true))
328
               (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_2 flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_2))
329
            (or (not (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.__flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_1 false))
330
               (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_2 flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_1))
331
       )
332
       (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_out flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_2)
333
       (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.flowchart5_flowchart5__state_in POINTFlowchart5_Flowchart5)
334
       (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.flowchart5_flowchart5__restart_in true)
335
       )
336
  (flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_step 
337
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_Flowchart5_1
338
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_1
339
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_1
340
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.flowchart5_flowchart5__restart_in
341
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.flowchart5_flowchart5__state_in
342
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_A_out
343
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.idFlowchart5_Flowchart5_out
344
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.x_out
345
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
346
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
347
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
348
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
349
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
350
  flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x)
351
))
352

    
353
; flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless
354
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__restart_in Bool)
355
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__state_in flowchart5_flowchart5__type)
356
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__restart_act Bool)
357
(declare-var flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__state_act flowchart5_flowchart5__type)
358
(declare-rel flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless (Bool flowchart5_flowchart5__type Bool flowchart5_flowchart5__type))
359
(rule (=> 
360
  (and (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__state_act flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__state_in)
361
       (= flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__restart_act flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__restart_in)
362
       )
363
  (flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__restart_in flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__state_in flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__restart_act flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless.flowchart5_flowchart5__state_act)
364
))
365

    
366
; flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until
367
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_Flowchart5_1 Int)
368
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_A_1 Int)
369
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.x_1 Int)
370
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.flowchart5_flowchart5__restart_in Bool)
371
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.flowchart5_flowchart5__state_in flowchart5_flowchart5__type)
372
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_A_out Int)
373
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_Flowchart5_out Int)
374
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.x_out Int)
375
(declare-rel flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until (Int Int Int Bool flowchart5_flowchart5__type Int Int Int))
376
(rule (=> 
377
  (and (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.x_out flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.x_1)
378
       (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_Flowchart5_out flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_Flowchart5_1)
379
       (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_A_out flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_A_1)
380
       (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.flowchart5_flowchart5__state_in POINTFlowchart5_Flowchart5)
381
       (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.flowchart5_flowchart5__restart_in false)
382
       )
383
  (flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_Flowchart5_1 flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_A_1 flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.x_1 flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.flowchart5_flowchart5__restart_in flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.flowchart5_flowchart5__state_in flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_A_out flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.idFlowchart5_Flowchart5_out flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until.x_out)
384
))
385

    
386
; flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless
387
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__restart_in Bool)
388
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__state_in flowchart5_flowchart5__type)
389
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.idFlowchart5_Flowchart5_1 Int)
390
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__restart_act Bool)
391
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__state_act flowchart5_flowchart5__type)
392
(declare-var flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.__flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless_1 Bool)
393
(declare-rel flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless (Bool flowchart5_flowchart5__type Int Bool flowchart5_flowchart5__type))
394
(rule (=> 
395
  (and (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.__flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless_1 (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.idFlowchart5_Flowchart5_1 0))
396
       (and (or (not (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.__flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless_1 false))
397
               (and (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__state_act FLOWCHART5_FLOWCHART5_PARALLEL_IDL)
398
                    (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__restart_act true)
399
                    ))
400
            (or (not (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.__flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless_1 true))
401
               (and (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__state_act POINT__TO__FLOWCHART5_A_1)
402
                    (= flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__restart_act true)
403
                    ))
404
       )
405
       )
406
  (flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__restart_in flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__state_in flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.idFlowchart5_Flowchart5_1 flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__restart_act flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless.flowchart5_flowchart5__state_act)
407
))
408

    
409
; flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until
410
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_1 Int)
411
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_1 Int)
412
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_1 Int)
413
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.flowchart5_flowchart5__restart_in Bool)
414
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.flowchart5_flowchart5__state_in flowchart5_flowchart5__type)
415
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_out Int)
416
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_out Int)
417
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_out Int)
418
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_2 Int)
419
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_2 Int)
420
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_2 Int)
421
(declare-rel flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until (Int Int Int Bool flowchart5_flowchart5__type Int Int Int))
422
(rule (=> 
423
  (and (Flowchart5_A_en flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_1
424
                        flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_1
425
                        flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_1
426
                        false
427
                        flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_2
428
                        flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_2
429
                        flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_2)
430
       (= flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_out flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_2)
431
       (= flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_out flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_2)
432
       (= flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_out flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_2)
433
       (= flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.flowchart5_flowchart5__state_in POINTFlowchart5_Flowchart5)
434
       (= flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.flowchart5_flowchart5__restart_in true)
435
       )
436
  (flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_1 flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_1 flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_1 flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.flowchart5_flowchart5__restart_in flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.flowchart5_flowchart5__state_in flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_A_out flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.idFlowchart5_Flowchart5_out flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until.x_out)
437
))
438

    
439
; flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless
440
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__restart_in Bool)
441
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__state_in flowchart5_flowchart5__type)
442
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__restart_act Bool)
443
(declare-var flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__state_act flowchart5_flowchart5__type)
444
(declare-rel flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless (Bool flowchart5_flowchart5__type Bool flowchart5_flowchart5__type))
445
(rule (=> 
446
  (and (= flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__state_act flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__state_in)
447
       (= flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__restart_act flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__restart_in)
448
       )
449
  (flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__restart_in flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__state_in flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__restart_act flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless.flowchart5_flowchart5__state_act)
450
))
451

    
452
; Flowchart5_Flowchart5_node
453
(declare-var Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5_1 Int)
454
(declare-var Flowchart5_Flowchart5_node.idFlowchart5_A_1 Int)
455
(declare-var Flowchart5_Flowchart5_node.x_1 Int)
456
(declare-var Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5 Int)
457
(declare-var Flowchart5_Flowchart5_node.idFlowchart5_A Int)
458
(declare-var Flowchart5_Flowchart5_node.x Int)
459
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c Bool)
460
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c flowchart5_flowchart5__type)
461
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c Bool)
462
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c flowchart5_a__type)
463
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c Bool)
464
(declare-var Flowchart5_Flowchart5_node.ni_6._arrow._first_c Bool)
465
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m Bool)
466
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m flowchart5_flowchart5__type)
467
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Bool)
468
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m flowchart5_a__type)
469
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Bool)
470
(declare-var Flowchart5_Flowchart5_node.ni_6._arrow._first_m Bool)
471
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x Bool)
472
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x flowchart5_flowchart5__type)
473
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x Bool)
474
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x flowchart5_a__type)
475
(declare-var Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x Bool)
476
(declare-var Flowchart5_Flowchart5_node.ni_6._arrow._first_x Bool)
477
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_1 Bool)
478
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_10 Int)
479
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_11 Int)
480
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_12 Bool)
481
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_13 flowchart5_flowchart5__type)
482
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_14 Int)
483
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_15 Int)
484
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_16 Int)
485
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_17 Bool)
486
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_18 flowchart5_flowchart5__type)
487
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_19 Int)
488
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_2 flowchart5_flowchart5__type)
489
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_20 Int)
490
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_21 Int)
491
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_22 Bool)
492
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_3 Bool)
493
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_4 flowchart5_flowchart5__type)
494
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_5 Bool)
495
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_6 flowchart5_flowchart5__type)
496
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_7 Bool)
497
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_8 flowchart5_flowchart5__type)
498
(declare-var Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_9 Int)
499
(declare-var Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_restart_in Bool)
500
(declare-var Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_state_in flowchart5_flowchart5__type)
501
(declare-var Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_act Bool)
502
(declare-var Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_in Bool)
503
(declare-var Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_act flowchart5_flowchart5__type)
504
(declare-var Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in flowchart5_flowchart5__type)
505
(declare-rel Flowchart5_Flowchart5_node_reset (Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool))
506
(declare-rel Flowchart5_Flowchart5_node_step (Int Int Int Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool))
507

    
508
(rule (=> 
509
  (and 
510
       (= Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c)
511
       (= Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c)
512
       (= Flowchart5_Flowchart5_node.ni_6._arrow._first_m true)
513
       (flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_reset 
514
       Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
515
       Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
516
       Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
517
       Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
518
       Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
519
       Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m)
520
  )
521
  (Flowchart5_Flowchart5_node_reset Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
522
                                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
523
                                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
524
                                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
525
                                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
526
                                    Flowchart5_Flowchart5_node.ni_6._arrow._first_c
527
                                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m
528
                                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m
529
                                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
530
                                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
531
                                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
532
                                    Flowchart5_Flowchart5_node.ni_6._arrow._first_m)
533
))
534

    
535
(rule (=> 
536
  (and (= Flowchart5_Flowchart5_node.ni_6._arrow._first_m Flowchart5_Flowchart5_node.ni_6._arrow._first_c)
537
       (and (= Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_22 (ite Flowchart5_Flowchart5_node.ni_6._arrow._first_m true false))
538
            (= Flowchart5_Flowchart5_node.ni_6._arrow._first_x false))
539
       (and (or (not (= Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_22 false))
540
               (and (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c)
541
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c)
542
                    ))
543
            (or (not (= Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_22 true))
544
               (and (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in POINTFlowchart5_Flowchart5)
545
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_in false)
546
                    ))
547
       )
548
       (and (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in FLOWCHART5_FLOWCHART5_PARALLEL_IDL))
549
               (and (flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_unless 
550
                    Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_in
551
                    Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in
552
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_1
553
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_2)
554
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_act Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_2)
555
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_act Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_1)
556
                    ))
557
            (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in POINTFlowchart5_Flowchart5))
558
               (and (flowchart5_flowchart5__POINTFlowchart5_Flowchart5_unless 
559
                    Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_in
560
                    Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in
561
                    Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5_1
562
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_5
563
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_6)
564
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_act Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_6)
565
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_act Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_5)
566
                    ))
567
            (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in POINT__TO__FLOWCHART5_A_1))
568
               (and (flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_unless 
569
                    Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_in
570
                    Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_in
571
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_3
572
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_4)
573
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_act Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_4)
574
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_act Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_3)
575
                    ))
576
       )
577
       (and (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_act FLOWCHART5_FLOWCHART5_PARALLEL_IDL))
578
               (and (and (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_act true))
579
                            (flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_reset 
580
                            Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
581
                            Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
582
                            Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
583
                            Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
584
                            Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
585
                            Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m))
586
                         (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__restart_act false))
587
                            (and (= Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c)
588
                                 (= Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c)
589
                                 (= Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c)
590
                                 )
591
                            )
592
                    )
593
                    (and (= Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c)
594
                         (= Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c)
595
                         (= Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c)
596
                         )
597
                    (flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until_step 
598
                    Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5_1
599
                    Flowchart5_Flowchart5_node.idFlowchart5_A_1
600
                    Flowchart5_Flowchart5_node.x_1
601
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_7
602
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_8
603
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_9
604
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_10
605
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_11
606
                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
607
                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
608
                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
609
                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
610
                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
611
                    Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x)
612
                    (= Flowchart5_Flowchart5_node.x Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_11)
613
                    (= Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5 Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_10)
614
                    (= Flowchart5_Flowchart5_node.idFlowchart5_A Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_9)
615
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_state_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_8)
616
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_restart_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_7)
617
                    ))
618
            (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_act POINTFlowchart5_Flowchart5))
619
               (and (flowchart5_flowchart5__POINTFlowchart5_Flowchart5_handler_until 
620
                    Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5_1
621
                    Flowchart5_Flowchart5_node.idFlowchart5_A_1
622
                    Flowchart5_Flowchart5_node.x_1
623
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_17
624
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_18
625
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_19
626
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_20
627
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_21)
628
                    (= Flowchart5_Flowchart5_node.x Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_21)
629
                    (= Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5 Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_20)
630
                    (= Flowchart5_Flowchart5_node.idFlowchart5_A Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_19)
631
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_state_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_18)
632
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_restart_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_17)
633
                    ))
634
            (or (not (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__state_act POINT__TO__FLOWCHART5_A_1))
635
               (and (flowchart5_flowchart5__POINT__TO__FLOWCHART5_A_1_handler_until 
636
                    Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5_1
637
                    Flowchart5_Flowchart5_node.idFlowchart5_A_1
638
                    Flowchart5_Flowchart5_node.x_1
639
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_12
640
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_13
641
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_14
642
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_15
643
                    Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_16)
644
                    (= Flowchart5_Flowchart5_node.x Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_16)
645
                    (= Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5 Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_15)
646
                    (= Flowchart5_Flowchart5_node.idFlowchart5_A Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_14)
647
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_state_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_13)
648
                    (= Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_restart_in Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_12)
649
                    ))
650
       )
651
       (= Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_state_in)
652
       (= Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x Flowchart5_Flowchart5_node.flowchart5_flowchart5__next_restart_in)
653
       )
654
  (Flowchart5_Flowchart5_node_step Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5_1
655
                                   Flowchart5_Flowchart5_node.idFlowchart5_A_1
656
                                   Flowchart5_Flowchart5_node.x_1
657
                                   Flowchart5_Flowchart5_node.idFlowchart5_Flowchart5
658
                                   Flowchart5_Flowchart5_node.idFlowchart5_A
659
                                   Flowchart5_Flowchart5_node.x
660
                                   Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
661
                                   Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
662
                                   Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
663
                                   Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
664
                                   Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
665
                                   Flowchart5_Flowchart5_node.ni_6._arrow._first_c
666
                                   Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x
667
                                   Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x
668
                                   Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
669
                                   Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
670
                                   Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x
671
                                   Flowchart5_Flowchart5_node.ni_6._arrow._first_x)
672
))
673

    
674
; Flowchart5_Flowchart5
675
(declare-var Flowchart5_Flowchart5.noInput Bool)
676
(declare-var Flowchart5_Flowchart5.x Int)
677
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c Int)
678
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c Int)
679
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c Int)
680
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c Bool)
681
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c flowchart5_flowchart5__type)
682
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c Bool)
683
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c flowchart5_a__type)
684
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c Bool)
685
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c Bool)
686
(declare-var Flowchart5_Flowchart5.ni_4._arrow._first_c Bool)
687
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m Int)
688
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m Int)
689
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m Int)
690
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m Bool)
691
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m flowchart5_flowchart5__type)
692
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Bool)
693
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m flowchart5_a__type)
694
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Bool)
695
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m Bool)
696
(declare-var Flowchart5_Flowchart5.ni_4._arrow._first_m Bool)
697
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_x Int)
698
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_x Int)
699
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_x Int)
700
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x Bool)
701
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x flowchart5_flowchart5__type)
702
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x Bool)
703
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x flowchart5_a__type)
704
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x Bool)
705
(declare-var Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_x Bool)
706
(declare-var Flowchart5_Flowchart5.ni_4._arrow._first_x Bool)
707
(declare-var Flowchart5_Flowchart5.__Flowchart5_Flowchart5_1 Bool)
708
(declare-var Flowchart5_Flowchart5.idFlowchart5_A Int)
709
(declare-var Flowchart5_Flowchart5.idFlowchart5_A_1 Int)
710
(declare-var Flowchart5_Flowchart5.idFlowchart5_Flowchart5 Int)
711
(declare-var Flowchart5_Flowchart5.idFlowchart5_Flowchart5_1 Int)
712
(declare-var Flowchart5_Flowchart5.x_1 Int)
713
(declare-rel Flowchart5_Flowchart5_reset (Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool))
714
(declare-rel Flowchart5_Flowchart5_step (Bool Int Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool))
715

    
716
(rule (=> 
717
  (and 
718
       (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c)
719
       (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c)
720
       (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c)
721
       (= Flowchart5_Flowchart5.ni_4._arrow._first_m true)
722
       (Flowchart5_Flowchart5_node_reset Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
723
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
724
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
725
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
726
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
727
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c
728
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m
729
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m
730
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
731
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
732
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
733
                                         Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m)
734
  )
735
  (Flowchart5_Flowchart5_reset Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c
736
                               Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c
737
                               Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c
738
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
739
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
740
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
741
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
742
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
743
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c
744
                               Flowchart5_Flowchart5.ni_4._arrow._first_c
745
                               Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m
746
                               Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m
747
                               Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m
748
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m
749
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m
750
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
751
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
752
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
753
                               Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m
754
                               Flowchart5_Flowchart5.ni_4._arrow._first_m)
755
))
756

    
757
(rule (=> 
758
  (and (= Flowchart5_Flowchart5.ni_4._arrow._first_m Flowchart5_Flowchart5.ni_4._arrow._first_c)
759
       (and (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_1 (ite Flowchart5_Flowchart5.ni_4._arrow._first_m true false))
760
            (= Flowchart5_Flowchart5.ni_4._arrow._first_x false))
761
       (and (or (not (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_1 false))
762
               (and (= Flowchart5_Flowchart5.x_1 Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c)
763
                    (= Flowchart5_Flowchart5.idFlowchart5_Flowchart5_1 Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c)
764
                    (= Flowchart5_Flowchart5.idFlowchart5_A_1 Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c)
765
                    ))
766
            (or (not (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_1 true))
767
               (and (= Flowchart5_Flowchart5.x_1 0)
768
                    (= Flowchart5_Flowchart5.idFlowchart5_Flowchart5_1 0)
769
                    (= Flowchart5_Flowchart5.idFlowchart5_A_1 0)
770
                    ))
771
       )
772
       (and (= Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c)
773
            (= Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c)
774
            (= Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c)
775
            (= Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c)
776
            (= Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c)
777
            (= Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c)
778
            )
779
       (Flowchart5_Flowchart5_node_step Flowchart5_Flowchart5.idFlowchart5_Flowchart5_1
780
                                        Flowchart5_Flowchart5.idFlowchart5_A_1
781
                                        Flowchart5_Flowchart5.x_1
782
                                        Flowchart5_Flowchart5.idFlowchart5_Flowchart5
783
                                        Flowchart5_Flowchart5.idFlowchart5_A
784
                                        Flowchart5_Flowchart5.x
785
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m
786
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m
787
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
788
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
789
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
790
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m
791
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x
792
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x
793
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
794
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
795
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x
796
                                        Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_x)
797
       (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_x Flowchart5_Flowchart5.x)
798
       (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_x Flowchart5_Flowchart5.idFlowchart5_Flowchart5)
799
       (= Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_x Flowchart5_Flowchart5.idFlowchart5_A)
800
       )
801
  (Flowchart5_Flowchart5_step Flowchart5_Flowchart5.noInput
802
                              Flowchart5_Flowchart5.x
803
                              Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c
804
                              Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c
805
                              Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c
806
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
807
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
808
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
809
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
810
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
811
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c
812
                              Flowchart5_Flowchart5.ni_4._arrow._first_c
813
                              Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_x
814
                              Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_x
815
                              Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_x
816
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x
817
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x
818
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
819
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
820
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x
821
                              Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_x
822
                              Flowchart5_Flowchart5.ni_4._arrow._first_x)
823
))
824

    
825
; flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until
826
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_1 Int)
827
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a_INNER__restart_in Bool)
828
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a_INNER__state_in flowchart5_a_INNER__type)
829
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_out Int)
830
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_2 Int)
831
(declare-rel flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until (Int Bool flowchart5_a_INNER__type Int))
832
(rule (=> 
833
  (and (Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action 
834
       flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_1
835
       flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_2)
836
       (= flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_out flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_2)
837
       (= flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a_INNER__state_in POINTFlowchart5_A_INNER)
838
       (= flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a_INNER__restart_in true)
839
       )
840
  (flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_1 flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a_INNER__restart_in flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.flowchart5_a_INNER__state_in flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until.x_out)
841
))
842

    
843
; flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless
844
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__restart_in Bool)
845
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__state_in flowchart5_a_INNER__type)
846
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__restart_act Bool)
847
(declare-var flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__state_act flowchart5_a_INNER__type)
848
(declare-rel flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless (Bool flowchart5_a_INNER__type Bool flowchart5_a_INNER__type))
849
(rule (=> 
850
  (and (= flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__state_act flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__state_in)
851
       (= flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__restart_act flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__restart_in)
852
       )
853
  (flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__restart_in flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__state_in flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__restart_act flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless.flowchart5_a_INNER__state_act)
854
))
855

    
856
; flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until
857
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.x_1 Int)
858
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.flowchart5_a_INNER__restart_in Bool)
859
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.flowchart5_a_INNER__state_in flowchart5_a_INNER__type)
860
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.x_out Int)
861
(declare-rel flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until (Int Bool flowchart5_a_INNER__type Int))
862
(rule (=> 
863
  (and (= flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.x_out flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.x_1)
864
       (= flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.flowchart5_a_INNER__state_in POINTFlowchart5_A_INNER)
865
       (= flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.flowchart5_a_INNER__restart_in false)
866
       )
867
  (flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.x_1 flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.flowchart5_a_INNER__restart_in flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.flowchart5_a_INNER__state_in flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until.x_out)
868
))
869

    
870
; flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless
871
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__restart_in Bool)
872
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__state_in flowchart5_a_INNER__type)
873
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__restart_act Bool)
874
(declare-var flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__state_act flowchart5_a_INNER__type)
875
(declare-rel flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless (Bool flowchart5_a_INNER__type Bool flowchart5_a_INNER__type))
876
(rule (=> 
877
  (and (= flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__state_act FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1)
878
       (= flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__restart_act true)
879
       )
880
  (flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__restart_in flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__state_in flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__restart_act flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless.flowchart5_a_INNER__state_act)
881
))
882

    
883
; Flowchart5
884
(declare-var Flowchart5.i_virtual Real)
885
(declare-var Flowchart5.Out1_1_1 Int)
886
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c Int)
887
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c Int)
888
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c Int)
889
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c Bool)
890
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c flowchart5_flowchart5__type)
891
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c Bool)
892
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c flowchart5_a__type)
893
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c Bool)
894
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c Bool)
895
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_c Bool)
896
(declare-var Flowchart5.ni_2._arrow._first_c Bool)
897
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m Int)
898
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m Int)
899
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m Int)
900
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m Bool)
901
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m flowchart5_flowchart5__type)
902
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Bool)
903
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m flowchart5_a__type)
904
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Bool)
905
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m Bool)
906
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_m Bool)
907
(declare-var Flowchart5.ni_2._arrow._first_m Bool)
908
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_x Int)
909
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_x Int)
910
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_x Int)
911
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x Bool)
912
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x flowchart5_flowchart5__type)
913
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x Bool)
914
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x flowchart5_a__type)
915
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x Bool)
916
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_x Bool)
917
(declare-var Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_x Bool)
918
(declare-var Flowchart5.ni_2._arrow._first_x Bool)
919
(declare-var Flowchart5.Flowchart5_1_1 Int)
920
(declare-var Flowchart5.__Flowchart5_1 Bool)
921
(declare-var Flowchart5.i_virtual_local Real)
922
(declare-rel Flowchart5_reset (Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool Bool Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool Bool))
923
(declare-rel Flowchart5_step (Real Int Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool Bool Int Int Int Bool flowchart5_flowchart5__type Bool flowchart5_a__type Bool Bool Bool Bool))
924

    
925
(rule (=> 
926
  (and 
927
       
928
       (= Flowchart5.ni_2._arrow._first_m true)
929
       (Flowchart5_Flowchart5_reset Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c
930
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c
931
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c
932
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
933
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
934
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
935
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
936
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
937
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c
938
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_c
939
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m
940
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m
941
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m
942
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m
943
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m
944
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
945
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
946
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
947
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m
948
                                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_m)
949
  )
950
  (Flowchart5_reset Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c
951
                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c
952
                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c
953
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
954
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
955
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
956
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
957
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
958
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c
959
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_c
960
                    Flowchart5.ni_2._arrow._first_c
961
                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m
962
                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m
963
                    Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m
964
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m
965
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m
966
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
967
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
968
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
969
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m
970
                    Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_m
971
                    Flowchart5.ni_2._arrow._first_m)
972
))
973

    
974
(rule (=> 
975
  (and (= Flowchart5.ni_2._arrow._first_m Flowchart5.ni_2._arrow._first_c)
976
       (and (= Flowchart5.__Flowchart5_1 (ite Flowchart5.ni_2._arrow._first_m true false))
977
            (= Flowchart5.ni_2._arrow._first_x false))
978
       (and (or (not (= Flowchart5.__Flowchart5_1 true))
979
               (= Flowchart5.i_virtual_local 0.))
980
            (or (not (= Flowchart5.__Flowchart5_1 false))
981
               (= Flowchart5.i_virtual_local 1.))
982
       )
983
       (and (= Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c)
984
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c)
985
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c)
986
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c)
987
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c)
988
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c)
989
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c)
990
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c)
991
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c)
992
            (= Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_m Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_c)
993
            )
994
       (Flowchart5_Flowchart5_step true
995
                                   Flowchart5.Flowchart5_1_1
996
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_m
997
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_m
998
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_m
999
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_m
1000
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_m
1001
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_m
1002
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_m
1003
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_m
1004
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_m
1005
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_m
1006
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_x
1007
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_x
1008
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_x
1009
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x
1010
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x
1011
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
1012
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
1013
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x
1014
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_x
1015
                                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_x)
1016
       (= Flowchart5.Out1_1_1 Flowchart5.Flowchart5_1_1)
1017
       )
1018
  (Flowchart5_step Flowchart5.i_virtual
1019
                   Flowchart5.Out1_1_1
1020
                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_c
1021
                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_c
1022
                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_c
1023
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_c
1024
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_c
1025
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_c
1026
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_c
1027
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_c
1028
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_c
1029
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_c
1030
                   Flowchart5.ni_2._arrow._first_c
1031
                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_2_x
1032
                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_3_x
1033
                   Flowchart5.ni_1.Flowchart5_Flowchart5.__Flowchart5_Flowchart5_4_x
1034
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_23_x
1035
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.__Flowchart5_Flowchart5_node_24_x
1036
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_14_x
1037
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.__Flowchart5_A_node_15_x
1038
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_5.flowchart5_flowchart5__FLOWCHART5_FLOWCHART5_PARALLEL_IDL_handler_until.ni_7.Flowchart5_A_node.ni_8._arrow._first_x
1039
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_3.Flowchart5_Flowchart5_node.ni_6._arrow._first_x
1040
                   Flowchart5.ni_1.Flowchart5_Flowchart5.ni_4._arrow._first_x
1041
                   Flowchart5.ni_2._arrow._first_x)
1042
))
1043

    
1044
; Flowchart5_A_du
1045
(declare-var Flowchart5_A_du.x_1 Int)
1046
(declare-var Flowchart5_A_du.x Int)
1047
(declare-var Flowchart5_A_du.__Flowchart5_A_du_12_c Bool)
1048
(declare-var Flowchart5_A_du.__Flowchart5_A_du_13_c flowchart5_a_INNER__type)
1049
(declare-var Flowchart5_A_du.ni_0._arrow._first_c Bool)
1050
(declare-var Flowchart5_A_du.__Flowchart5_A_du_12_m Bool)
1051
(declare-var Flowchart5_A_du.__Flowchart5_A_du_13_m flowchart5_a_INNER__type)
1052
(declare-var Flowchart5_A_du.ni_0._arrow._first_m Bool)
1053
(declare-var Flowchart5_A_du.__Flowchart5_A_du_12_x Bool)
1054
(declare-var Flowchart5_A_du.__Flowchart5_A_du_13_x flowchart5_a_INNER__type)
1055
(declare-var Flowchart5_A_du.ni_0._arrow._first_x Bool)
1056
(declare-var Flowchart5_A_du.__Flowchart5_A_du_1 Bool)
1057
(declare-var Flowchart5_A_du.__Flowchart5_A_du_10 Int)
1058
(declare-var Flowchart5_A_du.__Flowchart5_A_du_11 Bool)
1059
(declare-var Flowchart5_A_du.__Flowchart5_A_du_2 flowchart5_a_INNER__type)
1060
(declare-var Flowchart5_A_du.__Flowchart5_A_du_3 Bool)
1061
(declare-var Flowchart5_A_du.__Flowchart5_A_du_4 flowchart5_a_INNER__type)
1062
(declare-var Flowchart5_A_du.__Flowchart5_A_du_5 Bool)
1063
(declare-var Flowchart5_A_du.__Flowchart5_A_du_6 flowchart5_a_INNER__type)
1064
(declare-var Flowchart5_A_du.__Flowchart5_A_du_7 Int)
1065
(declare-var Flowchart5_A_du.__Flowchart5_A_du_8 Bool)
1066
(declare-var Flowchart5_A_du.__Flowchart5_A_du_9 flowchart5_a_INNER__type)
1067
(declare-var Flowchart5_A_du.flowchart5_a_INNER__next_restart_in Bool)
1068
(declare-var Flowchart5_A_du.flowchart5_a_INNER__next_state_in flowchart5_a_INNER__type)
1069
(declare-var Flowchart5_A_du.flowchart5_a_INNER__restart_act Bool)
1070
(declare-var Flowchart5_A_du.flowchart5_a_INNER__restart_in Bool)
1071
(declare-var Flowchart5_A_du.flowchart5_a_INNER__state_act flowchart5_a_INNER__type)
1072
(declare-var Flowchart5_A_du.flowchart5_a_INNER__state_in flowchart5_a_INNER__type)
1073
(declare-rel Flowchart5_A_du_reset (Bool flowchart5_a_INNER__type Bool Bool flowchart5_a_INNER__type Bool))
1074
(declare-rel Flowchart5_A_du_step (Int Int Bool flowchart5_a_INNER__type Bool Bool flowchart5_a_INNER__type Bool))
1075

    
1076
(rule (=> 
1077
  (and 
1078
       (= Flowchart5_A_du.__Flowchart5_A_du_12_m Flowchart5_A_du.__Flowchart5_A_du_12_c)
1079
       (= Flowchart5_A_du.__Flowchart5_A_du_13_m Flowchart5_A_du.__Flowchart5_A_du_13_c)
1080
       (= Flowchart5_A_du.ni_0._arrow._first_m true)
1081
  )
1082
  (Flowchart5_A_du_reset Flowchart5_A_du.__Flowchart5_A_du_12_c
1083
                         Flowchart5_A_du.__Flowchart5_A_du_13_c
1084
                         Flowchart5_A_du.ni_0._arrow._first_c
1085
                         Flowchart5_A_du.__Flowchart5_A_du_12_m
1086
                         Flowchart5_A_du.__Flowchart5_A_du_13_m
1087
                         Flowchart5_A_du.ni_0._arrow._first_m)
1088
))
1089

    
1090
(rule (=> 
1091
  (and (= Flowchart5_A_du.ni_0._arrow._first_m Flowchart5_A_du.ni_0._arrow._first_c)
1092
       (and (= Flowchart5_A_du.__Flowchart5_A_du_11 (ite Flowchart5_A_du.ni_0._arrow._first_m true false))
1093
            (= Flowchart5_A_du.ni_0._arrow._first_x false))
1094
       (and (or (not (= Flowchart5_A_du.__Flowchart5_A_du_11 false))
1095
               (and (= Flowchart5_A_du.flowchart5_a_INNER__state_in Flowchart5_A_du.__Flowchart5_A_du_13_c)
1096
                    (= Flowchart5_A_du.flowchart5_a_INNER__restart_in Flowchart5_A_du.__Flowchart5_A_du_12_c)
1097
                    ))
1098
            (or (not (= Flowchart5_A_du.__Flowchart5_A_du_11 true))
1099
               (and (= Flowchart5_A_du.flowchart5_a_INNER__state_in POINTFlowchart5_A_INNER)
1100
                    (= Flowchart5_A_du.flowchart5_a_INNER__restart_in false)
1101
                    ))
1102
       )
1103
       (and (or (not (= Flowchart5_A_du.flowchart5_a_INNER__state_in FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1))
1104
               (and (flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_unless 
1105
                    Flowchart5_A_du.flowchart5_a_INNER__restart_in
1106
                    Flowchart5_A_du.flowchart5_a_INNER__state_in
1107
                    Flowchart5_A_du.__Flowchart5_A_du_1
1108
                    Flowchart5_A_du.__Flowchart5_A_du_2)
1109
                    (= Flowchart5_A_du.flowchart5_a_INNER__state_act Flowchart5_A_du.__Flowchart5_A_du_2)
1110
                    (= Flowchart5_A_du.flowchart5_a_INNER__restart_act Flowchart5_A_du.__Flowchart5_A_du_1)
1111
                    ))
1112
            (or (not (= Flowchart5_A_du.flowchart5_a_INNER__state_in POINTFlowchart5_A_INNER))
1113
               (and (flowchart5_a_INNER__POINTFlowchart5_A_INNER_unless 
1114
                    Flowchart5_A_du.flowchart5_a_INNER__restart_in
1115
                    Flowchart5_A_du.flowchart5_a_INNER__state_in
1116
                    Flowchart5_A_du.__Flowchart5_A_du_3
1117
                    Flowchart5_A_du.__Flowchart5_A_du_4)
1118
                    (= Flowchart5_A_du.flowchart5_a_INNER__state_act Flowchart5_A_du.__Flowchart5_A_du_4)
1119
                    (= Flowchart5_A_du.flowchart5_a_INNER__restart_act Flowchart5_A_du.__Flowchart5_A_du_3)
1120
                    ))
1121
       )
1122
       (and (or (not (= Flowchart5_A_du.flowchart5_a_INNER__state_act FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1))
1123
               (and (flowchart5_a_INNER__FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1_handler_until 
1124
                    Flowchart5_A_du.x_1
1125
                    Flowchart5_A_du.__Flowchart5_A_du_5
1126
                    Flowchart5_A_du.__Flowchart5_A_du_6
1127
                    Flowchart5_A_du.__Flowchart5_A_du_7)
1128
                    (= Flowchart5_A_du.x Flowchart5_A_du.__Flowchart5_A_du_7)
1129
                    (= Flowchart5_A_du.flowchart5_a_INNER__next_state_in Flowchart5_A_du.__Flowchart5_A_du_6)
1130
                    (= Flowchart5_A_du.flowchart5_a_INNER__next_restart_in Flowchart5_A_du.__Flowchart5_A_du_5)
1131
                    ))
1132
            (or (not (= Flowchart5_A_du.flowchart5_a_INNER__state_act POINTFlowchart5_A_INNER))
1133
               (and (flowchart5_a_INNER__POINTFlowchart5_A_INNER_handler_until 
1134
                    Flowchart5_A_du.x_1
1135
                    Flowchart5_A_du.__Flowchart5_A_du_8
1136
                    Flowchart5_A_du.__Flowchart5_A_du_9
1137
                    Flowchart5_A_du.__Flowchart5_A_du_10)
1138
                    (= Flowchart5_A_du.x Flowchart5_A_du.__Flowchart5_A_du_10)
1139
                    (= Flowchart5_A_du.flowchart5_a_INNER__next_state_in Flowchart5_A_du.__Flowchart5_A_du_9)
1140
                    (= Flowchart5_A_du.flowchart5_a_INNER__next_restart_in Flowchart5_A_du.__Flowchart5_A_du_8)
1141
                    ))
1142
       )
1143
       (= Flowchart5_A_du.__Flowchart5_A_du_13_x Flowchart5_A_du.flowchart5_a_INNER__next_state_in)
1144
       (= Flowchart5_A_du.__Flowchart5_A_du_12_x Flowchart5_A_du.flowchart5_a_INNER__next_restart_in)
1145
       )
1146
  (Flowchart5_A_du_step Flowchart5_A_du.x_1
1147
                        Flowchart5_A_du.x
1148
                        Flowchart5_A_du.__Flowchart5_A_du_12_c
1149
                        Flowchart5_A_du.__Flowchart5_A_du_13_c
1150
                        Flowchart5_A_du.ni_0._arrow._first_c
1151
                        Flowchart5_A_du.__Flowchart5_A_du_12_x
1152
                        Flowchart5_A_du.__Flowchart5_A_du_13_x
1153
                        Flowchart5_A_du.ni_0._arrow._first_x)
1154
))
1155

    
1156
; Flowchart5_A_ex
1157
(declare-var Flowchart5_A_ex.idFlowchart5_Flowchart5_1 Int)
1158
(declare-var Flowchart5_A_ex.isInner Bool)
1159
(declare-var Flowchart5_A_ex.idFlowchart5_Flowchart5 Int)
1160
(declare-var Flowchart5_A_ex.idFlowchart5_Flowchart5_2 Int)
1161
(declare-rel Flowchart5_A_ex (Int Bool Int))
1162
(rule (=> 
1163
  (and (and (or (not (= (not Flowchart5_A_ex.isInner) true))
1164
               (= Flowchart5_A_ex.idFlowchart5_Flowchart5_2 0))
1165
            (or (not (= (not Flowchart5_A_ex.isInner) false))
1166
               (= Flowchart5_A_ex.idFlowchart5_Flowchart5_2 Flowchart5_A_ex.idFlowchart5_Flowchart5_1))
1167
       )
1168
       (= Flowchart5_A_ex.idFlowchart5_Flowchart5 Flowchart5_A_ex.idFlowchart5_Flowchart5_1)
1169
       )
1170
  (Flowchart5_A_ex Flowchart5_A_ex.idFlowchart5_Flowchart5_1 Flowchart5_A_ex.isInner Flowchart5_A_ex.idFlowchart5_Flowchart5)
1171
))
1172