Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart1 / Flowchart1.smt2 @ eb639349

History | View | Annotate | Download (102 KB)

1
(declare-datatypes () ((flowchart1_a__type POINTFlowchart1_A POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1)));
2

    
3
(declare-datatypes () ((flowchart1_flowchart1__type POINTFlowchart1_Flowchart1 POINT__TO__FLOWCHART1_A_1 FLOWCHART1_FLOWCHART1_PARALLEL_IDL)));
4

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

    
14
; flowchart1_a__POINTFlowchart1_A_handler_until
15
(declare-var flowchart1_a__POINTFlowchart1_A_handler_until.idFlowchart1_A_1 Int)
16
(declare-var flowchart1_a__POINTFlowchart1_A_handler_until.x_1 Int)
17
(declare-var flowchart1_a__POINTFlowchart1_A_handler_until.flowchart1_a__restart_in Bool)
18
(declare-var flowchart1_a__POINTFlowchart1_A_handler_until.flowchart1_a__state_in flowchart1_a__type)
19
(declare-var flowchart1_a__POINTFlowchart1_A_handler_until.idFlowchart1_A_out Int)
20
(declare-var flowchart1_a__POINTFlowchart1_A_handler_until.x_out Int)
21
(declare-rel flowchart1_a__POINTFlowchart1_A_handler_until (Int Int Bool flowchart1_a__type Int Int))
22
(rule (=> 
23
  (and (= flowchart1_a__POINTFlowchart1_A_handler_until.x_out flowchart1_a__POINTFlowchart1_A_handler_until.x_1)
24
       (= flowchart1_a__POINTFlowchart1_A_handler_until.idFlowchart1_A_out flowchart1_a__POINTFlowchart1_A_handler_until.idFlowchart1_A_1)
25
       (= flowchart1_a__POINTFlowchart1_A_handler_until.flowchart1_a__state_in POINTFlowchart1_A)
26
       (= flowchart1_a__POINTFlowchart1_A_handler_until.flowchart1_a__restart_in false)
27
       )
28
  (flowchart1_a__POINTFlowchart1_A_handler_until flowchart1_a__POINTFlowchart1_A_handler_until.idFlowchart1_A_1 flowchart1_a__POINTFlowchart1_A_handler_until.x_1 flowchart1_a__POINTFlowchart1_A_handler_until.flowchart1_a__restart_in flowchart1_a__POINTFlowchart1_A_handler_until.flowchart1_a__state_in flowchart1_a__POINTFlowchart1_A_handler_until.idFlowchart1_A_out flowchart1_a__POINTFlowchart1_A_handler_until.x_out)
29
))
30

    
31
; flowchart1_a__POINTFlowchart1_A_unless
32
(declare-var flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__restart_in Bool)
33
(declare-var flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__state_in flowchart1_a__type)
34
(declare-var flowchart1_a__POINTFlowchart1_A_unless.idFlowchart1_A_1 Int)
35
(declare-var flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__restart_act Bool)
36
(declare-var flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__state_act flowchart1_a__type)
37
(declare-var flowchart1_a__POINTFlowchart1_A_unless.__flowchart1_a__POINTFlowchart1_A_unless_1 Bool)
38
(declare-rel flowchart1_a__POINTFlowchart1_A_unless (Bool flowchart1_a__type Int Bool flowchart1_a__type))
39
(rule (=> 
40
  (and (= flowchart1_a__POINTFlowchart1_A_unless.__flowchart1_a__POINTFlowchart1_A_unless_1 (= flowchart1_a__POINTFlowchart1_A_unless.idFlowchart1_A_1 0))
41
       (and (or (not (= flowchart1_a__POINTFlowchart1_A_unless.__flowchart1_a__POINTFlowchart1_A_unless_1 false))
42
               (and (= flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__state_act flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__state_in)
43
                    (= flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__restart_act flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__restart_in)
44
                    ))
45
            (or (not (= flowchart1_a__POINTFlowchart1_A_unless.__flowchart1_a__POINTFlowchart1_A_unless_1 true))
46
               (and (= flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__state_act POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1)
47
                    (= flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__restart_act true)
48
                    ))
49
       )
50
       )
51
  (flowchart1_a__POINTFlowchart1_A_unless flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__restart_in flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__state_in flowchart1_a__POINTFlowchart1_A_unless.idFlowchart1_A_1 flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__restart_act flowchart1_a__POINTFlowchart1_A_unless.flowchart1_a__state_act)
52
))
53

    
54
; flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until
55
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.idFlowchart1_A_1 Int)
56
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_1 Int)
57
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.flowchart1_a__restart_in Bool)
58
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.flowchart1_a__state_in flowchart1_a__type)
59
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.idFlowchart1_A_out Int)
60
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_out Int)
61
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_2 Int)
62
(declare-rel flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until (Int Int Bool flowchart1_a__type Int Int))
63
(rule (=> 
64
  (and (POINT__To__Flowchart1_Flowchart1Junction745_1_Condition_Action 
65
       flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_1
66
       flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_2)
67
       (= flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_out flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_2)
68
       (= flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.idFlowchart1_A_out flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.idFlowchart1_A_1)
69
       (= flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.flowchart1_a__state_in POINTFlowchart1_A)
70
       (= flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.flowchart1_a__restart_in true)
71
       )
72
  (flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.idFlowchart1_A_1 flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_1 flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.flowchart1_a__restart_in flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.flowchart1_a__state_in flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.idFlowchart1_A_out flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until.x_out)
73
))
74

    
75
; flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless
76
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__restart_in Bool)
77
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__state_in flowchart1_a__type)
78
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__restart_act Bool)
79
(declare-var flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__state_act flowchart1_a__type)
80
(declare-rel flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless (Bool flowchart1_a__type Bool flowchart1_a__type))
81
(rule (=> 
82
  (and (= flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__state_act flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__state_in)
83
       (= flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__restart_act flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__restart_in)
84
       )
85
  (flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__restart_in flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__state_in flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__restart_act flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless.flowchart1_a__state_act)
86
))
87

    
88
; Flowchart1_A_node
89
(declare-var Flowchart1_A_node.idFlowchart1_A_1 Int)
90
(declare-var Flowchart1_A_node.x_1 Int)
91
(declare-var Flowchart1_A_node.idFlowchart1_A Int)
92
(declare-var Flowchart1_A_node.x Int)
93
(declare-var Flowchart1_A_node.__Flowchart1_A_node_14_c Bool)
94
(declare-var Flowchart1_A_node.__Flowchart1_A_node_15_c flowchart1_a__type)
95
(declare-var Flowchart1_A_node.ni_7._arrow._first_c Bool)
96
(declare-var Flowchart1_A_node.__Flowchart1_A_node_14_m Bool)
97
(declare-var Flowchart1_A_node.__Flowchart1_A_node_15_m flowchart1_a__type)
98
(declare-var Flowchart1_A_node.ni_7._arrow._first_m Bool)
99
(declare-var Flowchart1_A_node.__Flowchart1_A_node_14_x Bool)
100
(declare-var Flowchart1_A_node.__Flowchart1_A_node_15_x flowchart1_a__type)
101
(declare-var Flowchart1_A_node.ni_7._arrow._first_x Bool)
102
(declare-var Flowchart1_A_node.__Flowchart1_A_node_1 Bool)
103
(declare-var Flowchart1_A_node.__Flowchart1_A_node_10 flowchart1_a__type)
104
(declare-var Flowchart1_A_node.__Flowchart1_A_node_11 Int)
105
(declare-var Flowchart1_A_node.__Flowchart1_A_node_12 Int)
106
(declare-var Flowchart1_A_node.__Flowchart1_A_node_13 Bool)
107
(declare-var Flowchart1_A_node.__Flowchart1_A_node_2 flowchart1_a__type)
108
(declare-var Flowchart1_A_node.__Flowchart1_A_node_3 Bool)
109
(declare-var Flowchart1_A_node.__Flowchart1_A_node_4 flowchart1_a__type)
110
(declare-var Flowchart1_A_node.__Flowchart1_A_node_5 Bool)
111
(declare-var Flowchart1_A_node.__Flowchart1_A_node_6 flowchart1_a__type)
112
(declare-var Flowchart1_A_node.__Flowchart1_A_node_7 Int)
113
(declare-var Flowchart1_A_node.__Flowchart1_A_node_8 Int)
114
(declare-var Flowchart1_A_node.__Flowchart1_A_node_9 Bool)
115
(declare-var Flowchart1_A_node.flowchart1_a__next_restart_in Bool)
116
(declare-var Flowchart1_A_node.flowchart1_a__next_state_in flowchart1_a__type)
117
(declare-var Flowchart1_A_node.flowchart1_a__restart_act Bool)
118
(declare-var Flowchart1_A_node.flowchart1_a__restart_in Bool)
119
(declare-var Flowchart1_A_node.flowchart1_a__state_act flowchart1_a__type)
120
(declare-var Flowchart1_A_node.flowchart1_a__state_in flowchart1_a__type)
121
(declare-rel Flowchart1_A_node_reset (Bool flowchart1_a__type Bool Bool flowchart1_a__type Bool))
122
(declare-rel Flowchart1_A_node_step (Int Int Int Int Bool flowchart1_a__type Bool Bool flowchart1_a__type Bool))
123

    
124
(rule (=> 
125
  (and 
126
       (= Flowchart1_A_node.__Flowchart1_A_node_14_m Flowchart1_A_node.__Flowchart1_A_node_14_c)
127
       (= Flowchart1_A_node.__Flowchart1_A_node_15_m Flowchart1_A_node.__Flowchart1_A_node_15_c)
128
       (= Flowchart1_A_node.ni_7._arrow._first_m true)
129
  )
130
  (Flowchart1_A_node_reset Flowchart1_A_node.__Flowchart1_A_node_14_c
131
                           Flowchart1_A_node.__Flowchart1_A_node_15_c
132
                           Flowchart1_A_node.ni_7._arrow._first_c
133
                           Flowchart1_A_node.__Flowchart1_A_node_14_m
134
                           Flowchart1_A_node.__Flowchart1_A_node_15_m
135
                           Flowchart1_A_node.ni_7._arrow._first_m)
136
))
137

    
138
(rule (=> 
139
  (and (= Flowchart1_A_node.ni_7._arrow._first_m Flowchart1_A_node.ni_7._arrow._first_c)
140
       (and (= Flowchart1_A_node.__Flowchart1_A_node_13 (ite Flowchart1_A_node.ni_7._arrow._first_m true false))
141
            (= Flowchart1_A_node.ni_7._arrow._first_x false))
142
       (and (or (not (= Flowchart1_A_node.__Flowchart1_A_node_13 false))
143
               (and (= Flowchart1_A_node.flowchart1_a__state_in Flowchart1_A_node.__Flowchart1_A_node_15_c)
144
                    (= Flowchart1_A_node.flowchart1_a__restart_in Flowchart1_A_node.__Flowchart1_A_node_14_c)
145
                    ))
146
            (or (not (= Flowchart1_A_node.__Flowchart1_A_node_13 true))
147
               (and (= Flowchart1_A_node.flowchart1_a__state_in POINTFlowchart1_A)
148
                    (= Flowchart1_A_node.flowchart1_a__restart_in false)
149
                    ))
150
       )
151
       (and (or (not (= Flowchart1_A_node.flowchart1_a__state_in POINTFlowchart1_A))
152
               (and (flowchart1_a__POINTFlowchart1_A_unless Flowchart1_A_node.flowchart1_a__restart_in
153
                                                            Flowchart1_A_node.flowchart1_a__state_in
154
                                                            Flowchart1_A_node.idFlowchart1_A_1
155
                                                            Flowchart1_A_node.__Flowchart1_A_node_3
156
                                                            Flowchart1_A_node.__Flowchart1_A_node_4)
157
                    (= Flowchart1_A_node.flowchart1_a__state_act Flowchart1_A_node.__Flowchart1_A_node_4)
158
                    (= Flowchart1_A_node.flowchart1_a__restart_act Flowchart1_A_node.__Flowchart1_A_node_3)
159
                    ))
160
            (or (not (= Flowchart1_A_node.flowchart1_a__state_in POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1))
161
               (and (flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_unless 
162
                    Flowchart1_A_node.flowchart1_a__restart_in
163
                    Flowchart1_A_node.flowchart1_a__state_in
164
                    Flowchart1_A_node.__Flowchart1_A_node_1
165
                    Flowchart1_A_node.__Flowchart1_A_node_2)
166
                    (= Flowchart1_A_node.flowchart1_a__state_act Flowchart1_A_node.__Flowchart1_A_node_2)
167
                    (= Flowchart1_A_node.flowchart1_a__restart_act Flowchart1_A_node.__Flowchart1_A_node_1)
168
                    ))
169
       )
170
       (and (or (not (= Flowchart1_A_node.flowchart1_a__state_act POINTFlowchart1_A))
171
               (and (flowchart1_a__POINTFlowchart1_A_handler_until Flowchart1_A_node.idFlowchart1_A_1
172
                                                                   Flowchart1_A_node.x_1
173
                                                                   Flowchart1_A_node.__Flowchart1_A_node_9
174
                                                                   Flowchart1_A_node.__Flowchart1_A_node_10
175
                                                                   Flowchart1_A_node.__Flowchart1_A_node_11
176
                                                                   Flowchart1_A_node.__Flowchart1_A_node_12)
177
                    (= Flowchart1_A_node.x Flowchart1_A_node.__Flowchart1_A_node_12)
178
                    (= Flowchart1_A_node.idFlowchart1_A Flowchart1_A_node.__Flowchart1_A_node_11)
179
                    (= Flowchart1_A_node.flowchart1_a__next_state_in Flowchart1_A_node.__Flowchart1_A_node_10)
180
                    (= Flowchart1_A_node.flowchart1_a__next_restart_in Flowchart1_A_node.__Flowchart1_A_node_9)
181
                    ))
182
            (or (not (= Flowchart1_A_node.flowchart1_a__state_act POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1))
183
               (and (flowchart1_a__POINT__TO__FLOWCHART1_FLOWCHART1JUNCTION745_1_handler_until 
184
                    Flowchart1_A_node.idFlowchart1_A_1
185
                    Flowchart1_A_node.x_1
186
                    Flowchart1_A_node.__Flowchart1_A_node_5
187
                    Flowchart1_A_node.__Flowchart1_A_node_6
188
                    Flowchart1_A_node.__Flowchart1_A_node_7
189
                    Flowchart1_A_node.__Flowchart1_A_node_8)
190
                    (= Flowchart1_A_node.x Flowchart1_A_node.__Flowchart1_A_node_8)
191
                    (= Flowchart1_A_node.idFlowchart1_A Flowchart1_A_node.__Flowchart1_A_node_7)
192
                    (= Flowchart1_A_node.flowchart1_a__next_state_in Flowchart1_A_node.__Flowchart1_A_node_6)
193
                    (= Flowchart1_A_node.flowchart1_a__next_restart_in Flowchart1_A_node.__Flowchart1_A_node_5)
194
                    ))
195
       )
196
       (= Flowchart1_A_node.__Flowchart1_A_node_15_x Flowchart1_A_node.flowchart1_a__next_state_in)
197
       (= Flowchart1_A_node.__Flowchart1_A_node_14_x Flowchart1_A_node.flowchart1_a__next_restart_in)
198
       )
199
  (Flowchart1_A_node_step Flowchart1_A_node.idFlowchart1_A_1
200
                          Flowchart1_A_node.x_1
201
                          Flowchart1_A_node.idFlowchart1_A
202
                          Flowchart1_A_node.x
203
                          Flowchart1_A_node.__Flowchart1_A_node_14_c
204
                          Flowchart1_A_node.__Flowchart1_A_node_15_c
205
                          Flowchart1_A_node.ni_7._arrow._first_c
206
                          Flowchart1_A_node.__Flowchart1_A_node_14_x
207
                          Flowchart1_A_node.__Flowchart1_A_node_15_x
208
                          Flowchart1_A_node.ni_7._arrow._first_x)
209
))
210

    
211
; Flowchart1_A_en
212
(declare-var Flowchart1_A_en.idFlowchart1_A_1 Int)
213
(declare-var Flowchart1_A_en.idFlowchart1_Flowchart1_1 Int)
214
(declare-var Flowchart1_A_en.x_1 Int)
215
(declare-var Flowchart1_A_en.isInner Bool)
216
(declare-var Flowchart1_A_en.idFlowchart1_A Int)
217
(declare-var Flowchart1_A_en.idFlowchart1_Flowchart1 Int)
218
(declare-var Flowchart1_A_en.x Int)
219
(declare-var Flowchart1_A_en.__Flowchart1_A_en_1 Bool)
220
(declare-var Flowchart1_A_en.idFlowchart1_A_2 Int)
221
(declare-var Flowchart1_A_en.idFlowchart1_A_3 Int)
222
(declare-var Flowchart1_A_en.idFlowchart1_Flowchart1_3 Int)
223
(declare-var Flowchart1_A_en.idFlowchart1_Flowchart1_4 Int)
224
(declare-var Flowchart1_A_en.x_2 Int)
225
(declare-var Flowchart1_A_en.x_3 Int)
226
(declare-var Flowchart1_A_en.x_4 Int)
227
(declare-rel Flowchart1_A_en (Int Int Int Bool Int Int Int))
228
(rule (=> 
229
  (and (POINT__To__Flowchart1_Flowchart1Junction745_1_Condition_Action 
230
       Flowchart1_A_en.x_1
231
       Flowchart1_A_en.x_2)
232
       (= Flowchart1_A_en.__Flowchart1_A_en_1 (= Flowchart1_A_en.idFlowchart1_A_1 0))
233
       (and (or (not (= Flowchart1_A_en.__Flowchart1_A_en_1 false))
234
               (and (= Flowchart1_A_en.x_3 Flowchart1_A_en.x_1)
235
                    (= Flowchart1_A_en.idFlowchart1_Flowchart1_3 744)
236
                    (= Flowchart1_A_en.idFlowchart1_A_2 Flowchart1_A_en.idFlowchart1_A_1)
237
                    (= Flowchart1_A_en.x_4 Flowchart1_A_en.x_1)
238
                    (= Flowchart1_A_en.idFlowchart1_Flowchart1_4 744)
239
                    (= Flowchart1_A_en.idFlowchart1_A_3 Flowchart1_A_en.idFlowchart1_A_1)
240
                    ))
241
            (or (not (= Flowchart1_A_en.__Flowchart1_A_en_1 true))
242
               (and (= Flowchart1_A_en.x_3 Flowchart1_A_en.x_2)
243
                    (= Flowchart1_A_en.idFlowchart1_Flowchart1_3 744)
244
                    (= Flowchart1_A_en.idFlowchart1_A_2 Flowchart1_A_en.idFlowchart1_A_1)
245
                    (= Flowchart1_A_en.x_4 Flowchart1_A_en.x_3)
246
                    (= Flowchart1_A_en.idFlowchart1_Flowchart1_4 Flowchart1_A_en.idFlowchart1_Flowchart1_3)
247
                    (= Flowchart1_A_en.idFlowchart1_A_3 Flowchart1_A_en.idFlowchart1_A_2)
248
                    ))
249
       )
250
       (= Flowchart1_A_en.x Flowchart1_A_en.x_4)
251
       (= Flowchart1_A_en.idFlowchart1_Flowchart1 Flowchart1_A_en.idFlowchart1_Flowchart1_4)
252
       (= Flowchart1_A_en.idFlowchart1_A (- 1))
253
       )
254
  (Flowchart1_A_en Flowchart1_A_en.idFlowchart1_A_1 Flowchart1_A_en.idFlowchart1_Flowchart1_1 Flowchart1_A_en.x_1 Flowchart1_A_en.isInner Flowchart1_A_en.idFlowchart1_A Flowchart1_A_en.idFlowchart1_Flowchart1 Flowchart1_A_en.x)
255
))
256

    
257
; flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until
258
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_Flowchart1_1 Int)
259
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_1 Int)
260
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_1 Int)
261
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.flowchart1_flowchart1__restart_in Bool)
262
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.flowchart1_flowchart1__state_in flowchart1_flowchart1__type)
263
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_out Int)
264
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_Flowchart1_out Int)
265
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_out Int)
266
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c Bool)
267
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c flowchart1_a__type)
268
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c Bool)
269
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Bool)
270
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m flowchart1_a__type)
271
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Bool)
272
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x Bool)
273
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x flowchart1_a__type)
274
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x Bool)
275
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_1 Bool)
276
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_2 Int)
277
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_3 Int)
278
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_2 Int)
279
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_2 Int)
280
(declare-rel flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_reset (Bool flowchart1_a__type Bool Bool flowchart1_a__type Bool))
281
(declare-rel flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_step (Int Int Int Bool flowchart1_flowchart1__type Int Int Int Bool flowchart1_a__type Bool Bool flowchart1_a__type Bool))
282

    
283
(rule (=> 
284
  (and 
285
       
286
       (Flowchart1_A_node_reset flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
287
                                flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
288
                                flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
289
                                flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
290
                                flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
291
                                flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m)
292
  )
293
  (flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_reset 
294
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
295
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
296
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
297
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
298
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
299
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m)
300
))
301

    
302
(rule (=> 
303
  (and (and (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c)
304
            (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c)
305
            (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c)
306
            )
307
       (Flowchart1_A_node_step flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_1
308
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_1
309
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_2
310
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_3
311
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
312
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
313
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
314
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
315
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
316
                               flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x)
317
       (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_1 (not (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_1 0)))
318
       (and (or (not (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_1 true))
319
               (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_2 flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_3))
320
            (or (not (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_1 false))
321
               (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_2 flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_1))
322
       )
323
       (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_out flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_2)
324
       (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_Flowchart1_out flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_Flowchart1_1)
325
       (and (or (not (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_1 true))
326
               (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_2 flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_2))
327
            (or (not (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.__flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_1 false))
328
               (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_2 flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_1))
329
       )
330
       (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_out flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_2)
331
       (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.flowchart1_flowchart1__state_in POINTFlowchart1_Flowchart1)
332
       (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.flowchart1_flowchart1__restart_in true)
333
       )
334
  (flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_step 
335
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_Flowchart1_1
336
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_1
337
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_1
338
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.flowchart1_flowchart1__restart_in
339
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.flowchart1_flowchart1__state_in
340
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_A_out
341
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.idFlowchart1_Flowchart1_out
342
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.x_out
343
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
344
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
345
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
346
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
347
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
348
  flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x)
349
))
350

    
351
; flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless
352
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__restart_in Bool)
353
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__state_in flowchart1_flowchart1__type)
354
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__restart_act Bool)
355
(declare-var flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__state_act flowchart1_flowchart1__type)
356
(declare-rel flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless (Bool flowchart1_flowchart1__type Bool flowchart1_flowchart1__type))
357
(rule (=> 
358
  (and (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__state_act flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__state_in)
359
       (= flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__restart_act flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__restart_in)
360
       )
361
  (flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__restart_in flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__state_in flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__restart_act flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless.flowchart1_flowchart1__state_act)
362
))
363

    
364
; flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until
365
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_Flowchart1_1 Int)
366
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_A_1 Int)
367
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.x_1 Int)
368
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.flowchart1_flowchart1__restart_in Bool)
369
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.flowchart1_flowchart1__state_in flowchart1_flowchart1__type)
370
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_A_out Int)
371
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_Flowchart1_out Int)
372
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.x_out Int)
373
(declare-rel flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until (Int Int Int Bool flowchart1_flowchart1__type Int Int Int))
374
(rule (=> 
375
  (and (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.x_out flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.x_1)
376
       (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_Flowchart1_out flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_Flowchart1_1)
377
       (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_A_out flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_A_1)
378
       (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.flowchart1_flowchart1__state_in POINTFlowchart1_Flowchart1)
379
       (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.flowchart1_flowchart1__restart_in false)
380
       )
381
  (flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_Flowchart1_1 flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_A_1 flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.x_1 flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.flowchart1_flowchart1__restart_in flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.flowchart1_flowchart1__state_in flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_A_out flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.idFlowchart1_Flowchart1_out flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until.x_out)
382
))
383

    
384
; flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless
385
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__restart_in Bool)
386
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__state_in flowchart1_flowchart1__type)
387
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.idFlowchart1_Flowchart1_1 Int)
388
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__restart_act Bool)
389
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__state_act flowchart1_flowchart1__type)
390
(declare-var flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.__flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless_1 Bool)
391
(declare-rel flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless (Bool flowchart1_flowchart1__type Int Bool flowchart1_flowchart1__type))
392
(rule (=> 
393
  (and (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.__flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless_1 (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.idFlowchart1_Flowchart1_1 0))
394
       (and (or (not (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.__flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless_1 false))
395
               (and (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__state_act FLOWCHART1_FLOWCHART1_PARALLEL_IDL)
396
                    (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__restart_act true)
397
                    ))
398
            (or (not (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.__flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless_1 true))
399
               (and (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__state_act POINT__TO__FLOWCHART1_A_1)
400
                    (= flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__restart_act true)
401
                    ))
402
       )
403
       )
404
  (flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__restart_in flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__state_in flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.idFlowchart1_Flowchart1_1 flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__restart_act flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless.flowchart1_flowchart1__state_act)
405
))
406

    
407
; flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until
408
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_1 Int)
409
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_1 Int)
410
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_1 Int)
411
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.flowchart1_flowchart1__restart_in Bool)
412
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.flowchart1_flowchart1__state_in flowchart1_flowchart1__type)
413
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_out Int)
414
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_out Int)
415
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_out Int)
416
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_2 Int)
417
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_2 Int)
418
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_2 Int)
419
(declare-rel flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until (Int Int Int Bool flowchart1_flowchart1__type Int Int Int))
420
(rule (=> 
421
  (and (Flowchart1_A_en flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_1
422
                        flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_1
423
                        flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_1
424
                        false
425
                        flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_2
426
                        flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_2
427
                        flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_2)
428
       (= flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_out flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_2)
429
       (= flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_out flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_2)
430
       (= flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_out flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_2)
431
       (= flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.flowchart1_flowchart1__state_in POINTFlowchart1_Flowchart1)
432
       (= flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.flowchart1_flowchart1__restart_in true)
433
       )
434
  (flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_1 flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_1 flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_1 flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.flowchart1_flowchart1__restart_in flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.flowchart1_flowchart1__state_in flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_A_out flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.idFlowchart1_Flowchart1_out flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until.x_out)
435
))
436

    
437
; flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless
438
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__restart_in Bool)
439
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__state_in flowchart1_flowchart1__type)
440
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__restart_act Bool)
441
(declare-var flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__state_act flowchart1_flowchart1__type)
442
(declare-rel flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless (Bool flowchart1_flowchart1__type Bool flowchart1_flowchart1__type))
443
(rule (=> 
444
  (and (= flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__state_act flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__state_in)
445
       (= flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__restart_act flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__restart_in)
446
       )
447
  (flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__restart_in flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__state_in flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__restart_act flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless.flowchart1_flowchart1__state_act)
448
))
449

    
450
; Flowchart1_Flowchart1_node
451
(declare-var Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1_1 Int)
452
(declare-var Flowchart1_Flowchart1_node.idFlowchart1_A_1 Int)
453
(declare-var Flowchart1_Flowchart1_node.x_1 Int)
454
(declare-var Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1 Int)
455
(declare-var Flowchart1_Flowchart1_node.idFlowchart1_A Int)
456
(declare-var Flowchart1_Flowchart1_node.x Int)
457
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c Bool)
458
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c flowchart1_flowchart1__type)
459
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c Bool)
460
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c flowchart1_a__type)
461
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c Bool)
462
(declare-var Flowchart1_Flowchart1_node.ni_5._arrow._first_c Bool)
463
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m Bool)
464
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m flowchart1_flowchart1__type)
465
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Bool)
466
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m flowchart1_a__type)
467
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Bool)
468
(declare-var Flowchart1_Flowchart1_node.ni_5._arrow._first_m Bool)
469
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x Bool)
470
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x flowchart1_flowchart1__type)
471
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x Bool)
472
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x flowchart1_a__type)
473
(declare-var Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x Bool)
474
(declare-var Flowchart1_Flowchart1_node.ni_5._arrow._first_x Bool)
475
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_1 Bool)
476
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_10 Int)
477
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_11 Int)
478
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_12 Bool)
479
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_13 flowchart1_flowchart1__type)
480
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_14 Int)
481
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_15 Int)
482
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_16 Int)
483
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_17 Bool)
484
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_18 flowchart1_flowchart1__type)
485
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_19 Int)
486
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_2 flowchart1_flowchart1__type)
487
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_20 Int)
488
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_21 Int)
489
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_22 Bool)
490
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_3 Bool)
491
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_4 flowchart1_flowchart1__type)
492
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_5 Bool)
493
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_6 flowchart1_flowchart1__type)
494
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_7 Bool)
495
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_8 flowchart1_flowchart1__type)
496
(declare-var Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_9 Int)
497
(declare-var Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_restart_in Bool)
498
(declare-var Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_state_in flowchart1_flowchart1__type)
499
(declare-var Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_act Bool)
500
(declare-var Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_in Bool)
501
(declare-var Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_act flowchart1_flowchart1__type)
502
(declare-var Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in flowchart1_flowchart1__type)
503
(declare-rel Flowchart1_Flowchart1_node_reset (Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool))
504
(declare-rel Flowchart1_Flowchart1_node_step (Int Int Int Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool))
505

    
506
(rule (=> 
507
  (and 
508
       (= Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c)
509
       (= Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c)
510
       (= Flowchart1_Flowchart1_node.ni_5._arrow._first_m true)
511
       (flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_reset 
512
       Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
513
       Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
514
       Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
515
       Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
516
       Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
517
       Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m)
518
  )
519
  (Flowchart1_Flowchart1_node_reset Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
520
                                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
521
                                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
522
                                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
523
                                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
524
                                    Flowchart1_Flowchart1_node.ni_5._arrow._first_c
525
                                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m
526
                                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m
527
                                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
528
                                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
529
                                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
530
                                    Flowchart1_Flowchart1_node.ni_5._arrow._first_m)
531
))
532

    
533
(rule (=> 
534
  (and (= Flowchart1_Flowchart1_node.ni_5._arrow._first_m Flowchart1_Flowchart1_node.ni_5._arrow._first_c)
535
       (and (= Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_22 (ite Flowchart1_Flowchart1_node.ni_5._arrow._first_m true false))
536
            (= Flowchart1_Flowchart1_node.ni_5._arrow._first_x false))
537
       (and (or (not (= Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_22 false))
538
               (and (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c)
539
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c)
540
                    ))
541
            (or (not (= Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_22 true))
542
               (and (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in POINTFlowchart1_Flowchart1)
543
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_in false)
544
                    ))
545
       )
546
       (and (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in FLOWCHART1_FLOWCHART1_PARALLEL_IDL))
547
               (and (flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_unless 
548
                    Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_in
549
                    Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in
550
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_1
551
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_2)
552
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_act Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_2)
553
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_act Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_1)
554
                    ))
555
            (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in POINTFlowchart1_Flowchart1))
556
               (and (flowchart1_flowchart1__POINTFlowchart1_Flowchart1_unless 
557
                    Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_in
558
                    Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in
559
                    Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1_1
560
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_5
561
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_6)
562
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_act Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_6)
563
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_act Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_5)
564
                    ))
565
            (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in POINT__TO__FLOWCHART1_A_1))
566
               (and (flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_unless 
567
                    Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_in
568
                    Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_in
569
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_3
570
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_4)
571
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_act Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_4)
572
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_act Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_3)
573
                    ))
574
       )
575
       (and (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_act FLOWCHART1_FLOWCHART1_PARALLEL_IDL))
576
               (and (and (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_act true))
577
                            (flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_reset 
578
                            Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
579
                            Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
580
                            Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
581
                            Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
582
                            Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
583
                            Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m))
584
                         (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__restart_act false))
585
                            (and (= Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c)
586
                                 (= Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c)
587
                                 (= Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c)
588
                                 )
589
                            )
590
                    )
591
                    (and (= Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c)
592
                         (= Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c)
593
                         (= Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c)
594
                         )
595
                    (flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until_step 
596
                    Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1_1
597
                    Flowchart1_Flowchart1_node.idFlowchart1_A_1
598
                    Flowchart1_Flowchart1_node.x_1
599
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_7
600
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_8
601
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_9
602
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_10
603
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_11
604
                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
605
                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
606
                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
607
                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
608
                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
609
                    Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x)
610
                    (= Flowchart1_Flowchart1_node.x Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_11)
611
                    (= Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1 Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_10)
612
                    (= Flowchart1_Flowchart1_node.idFlowchart1_A Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_9)
613
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_state_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_8)
614
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_restart_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_7)
615
                    ))
616
            (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_act POINTFlowchart1_Flowchart1))
617
               (and (flowchart1_flowchart1__POINTFlowchart1_Flowchart1_handler_until 
618
                    Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1_1
619
                    Flowchart1_Flowchart1_node.idFlowchart1_A_1
620
                    Flowchart1_Flowchart1_node.x_1
621
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_17
622
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_18
623
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_19
624
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_20
625
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_21)
626
                    (= Flowchart1_Flowchart1_node.x Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_21)
627
                    (= Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1 Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_20)
628
                    (= Flowchart1_Flowchart1_node.idFlowchart1_A Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_19)
629
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_state_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_18)
630
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_restart_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_17)
631
                    ))
632
            (or (not (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__state_act POINT__TO__FLOWCHART1_A_1))
633
               (and (flowchart1_flowchart1__POINT__TO__FLOWCHART1_A_1_handler_until 
634
                    Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1_1
635
                    Flowchart1_Flowchart1_node.idFlowchart1_A_1
636
                    Flowchart1_Flowchart1_node.x_1
637
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_12
638
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_13
639
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_14
640
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_15
641
                    Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_16)
642
                    (= Flowchart1_Flowchart1_node.x Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_16)
643
                    (= Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1 Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_15)
644
                    (= Flowchart1_Flowchart1_node.idFlowchart1_A Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_14)
645
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_state_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_13)
646
                    (= Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_restart_in Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_12)
647
                    ))
648
       )
649
       (= Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_state_in)
650
       (= Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x Flowchart1_Flowchart1_node.flowchart1_flowchart1__next_restart_in)
651
       )
652
  (Flowchart1_Flowchart1_node_step Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1_1
653
                                   Flowchart1_Flowchart1_node.idFlowchart1_A_1
654
                                   Flowchart1_Flowchart1_node.x_1
655
                                   Flowchart1_Flowchart1_node.idFlowchart1_Flowchart1
656
                                   Flowchart1_Flowchart1_node.idFlowchart1_A
657
                                   Flowchart1_Flowchart1_node.x
658
                                   Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
659
                                   Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
660
                                   Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
661
                                   Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
662
                                   Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
663
                                   Flowchart1_Flowchart1_node.ni_5._arrow._first_c
664
                                   Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x
665
                                   Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x
666
                                   Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
667
                                   Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
668
                                   Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x
669
                                   Flowchart1_Flowchart1_node.ni_5._arrow._first_x)
670
))
671

    
672
; Flowchart1_Flowchart1
673
(declare-var Flowchart1_Flowchart1.noInput Bool)
674
(declare-var Flowchart1_Flowchart1.x Int)
675
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c Int)
676
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c Int)
677
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c Int)
678
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c Bool)
679
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c flowchart1_flowchart1__type)
680
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c Bool)
681
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c flowchart1_a__type)
682
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c Bool)
683
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c Bool)
684
(declare-var Flowchart1_Flowchart1.ni_3._arrow._first_c Bool)
685
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m Int)
686
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m Int)
687
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m Int)
688
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m Bool)
689
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m flowchart1_flowchart1__type)
690
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Bool)
691
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m flowchart1_a__type)
692
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Bool)
693
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m Bool)
694
(declare-var Flowchart1_Flowchart1.ni_3._arrow._first_m Bool)
695
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_x Int)
696
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_x Int)
697
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_x Int)
698
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x Bool)
699
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x flowchart1_flowchart1__type)
700
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x Bool)
701
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x flowchart1_a__type)
702
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x Bool)
703
(declare-var Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_x Bool)
704
(declare-var Flowchart1_Flowchart1.ni_3._arrow._first_x Bool)
705
(declare-var Flowchart1_Flowchart1.__Flowchart1_Flowchart1_1 Bool)
706
(declare-var Flowchart1_Flowchart1.idFlowchart1_A Int)
707
(declare-var Flowchart1_Flowchart1.idFlowchart1_A_1 Int)
708
(declare-var Flowchart1_Flowchart1.idFlowchart1_Flowchart1 Int)
709
(declare-var Flowchart1_Flowchart1.idFlowchart1_Flowchart1_1 Int)
710
(declare-var Flowchart1_Flowchart1.x_1 Int)
711
(declare-rel Flowchart1_Flowchart1_reset (Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool))
712
(declare-rel Flowchart1_Flowchart1_step (Bool Int Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool))
713

    
714
(rule (=> 
715
  (and 
716
       (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c)
717
       (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c)
718
       (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c)
719
       (= Flowchart1_Flowchart1.ni_3._arrow._first_m true)
720
       (Flowchart1_Flowchart1_node_reset Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
721
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
722
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
723
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
724
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
725
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c
726
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m
727
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m
728
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
729
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
730
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
731
                                         Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m)
732
  )
733
  (Flowchart1_Flowchart1_reset Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c
734
                               Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c
735
                               Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c
736
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
737
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
738
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
739
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
740
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
741
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c
742
                               Flowchart1_Flowchart1.ni_3._arrow._first_c
743
                               Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m
744
                               Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m
745
                               Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m
746
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m
747
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m
748
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
749
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
750
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
751
                               Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m
752
                               Flowchart1_Flowchart1.ni_3._arrow._first_m)
753
))
754

    
755
(rule (=> 
756
  (and (= Flowchart1_Flowchart1.ni_3._arrow._first_m Flowchart1_Flowchart1.ni_3._arrow._first_c)
757
       (and (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_1 (ite Flowchart1_Flowchart1.ni_3._arrow._first_m true false))
758
            (= Flowchart1_Flowchart1.ni_3._arrow._first_x false))
759
       (and (or (not (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_1 false))
760
               (and (= Flowchart1_Flowchart1.x_1 Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c)
761
                    (= Flowchart1_Flowchart1.idFlowchart1_Flowchart1_1 Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c)
762
                    (= Flowchart1_Flowchart1.idFlowchart1_A_1 Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c)
763
                    ))
764
            (or (not (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_1 true))
765
               (and (= Flowchart1_Flowchart1.x_1 0)
766
                    (= Flowchart1_Flowchart1.idFlowchart1_Flowchart1_1 0)
767
                    (= Flowchart1_Flowchart1.idFlowchart1_A_1 0)
768
                    ))
769
       )
770
       (and (= Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c)
771
            (= Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c)
772
            (= Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c)
773
            (= Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c)
774
            (= Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c)
775
            (= Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c)
776
            )
777
       (Flowchart1_Flowchart1_node_step Flowchart1_Flowchart1.idFlowchart1_Flowchart1_1
778
                                        Flowchart1_Flowchart1.idFlowchart1_A_1
779
                                        Flowchart1_Flowchart1.x_1
780
                                        Flowchart1_Flowchart1.idFlowchart1_Flowchart1
781
                                        Flowchart1_Flowchart1.idFlowchart1_A
782
                                        Flowchart1_Flowchart1.x
783
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m
784
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m
785
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
786
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
787
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
788
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m
789
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x
790
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x
791
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
792
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
793
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x
794
                                        Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_x)
795
       (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_x Flowchart1_Flowchart1.x)
796
       (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_x Flowchart1_Flowchart1.idFlowchart1_Flowchart1)
797
       (= Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_x Flowchart1_Flowchart1.idFlowchart1_A)
798
       )
799
  (Flowchart1_Flowchart1_step Flowchart1_Flowchart1.noInput
800
                              Flowchart1_Flowchart1.x
801
                              Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c
802
                              Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c
803
                              Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c
804
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
805
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
806
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
807
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
808
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
809
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c
810
                              Flowchart1_Flowchart1.ni_3._arrow._first_c
811
                              Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_x
812
                              Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_x
813
                              Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_x
814
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x
815
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x
816
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
817
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
818
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x
819
                              Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_x
820
                              Flowchart1_Flowchart1.ni_3._arrow._first_x)
821
))
822

    
823
; Flowchart1_A_ex
824
(declare-var Flowchart1_A_ex.idFlowchart1_Flowchart1_1 Int)
825
(declare-var Flowchart1_A_ex.isInner Bool)
826
(declare-var Flowchart1_A_ex.idFlowchart1_Flowchart1 Int)
827
(declare-var Flowchart1_A_ex.idFlowchart1_Flowchart1_2 Int)
828
(declare-rel Flowchart1_A_ex (Int Bool Int))
829
(rule (=> 
830
  (and (and (or (not (= (not Flowchart1_A_ex.isInner) true))
831
               (= Flowchart1_A_ex.idFlowchart1_Flowchart1_2 0))
832
            (or (not (= (not Flowchart1_A_ex.isInner) false))
833
               (= Flowchart1_A_ex.idFlowchart1_Flowchart1_2 Flowchart1_A_ex.idFlowchart1_Flowchart1_1))
834
       )
835
       (= Flowchart1_A_ex.idFlowchart1_Flowchart1 Flowchart1_A_ex.idFlowchart1_Flowchart1_1)
836
       )
837
  (Flowchart1_A_ex Flowchart1_A_ex.idFlowchart1_Flowchart1_1 Flowchart1_A_ex.isInner Flowchart1_A_ex.idFlowchart1_Flowchart1)
838
))
839

    
840
; Flowchart1
841
(declare-var Flowchart1.i_virtual Real)
842
(declare-var Flowchart1.Out1_1_1 Int)
843
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c Int)
844
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c Int)
845
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c Int)
846
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c Bool)
847
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c flowchart1_flowchart1__type)
848
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c Bool)
849
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c flowchart1_a__type)
850
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c Bool)
851
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c Bool)
852
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_c Bool)
853
(declare-var Flowchart1.ni_1._arrow._first_c Bool)
854
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m Int)
855
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m Int)
856
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m Int)
857
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m Bool)
858
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m flowchart1_flowchart1__type)
859
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Bool)
860
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m flowchart1_a__type)
861
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Bool)
862
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m Bool)
863
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_m Bool)
864
(declare-var Flowchart1.ni_1._arrow._first_m Bool)
865
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_x Int)
866
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_x Int)
867
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_x Int)
868
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x Bool)
869
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x flowchart1_flowchart1__type)
870
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x Bool)
871
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x flowchart1_a__type)
872
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x Bool)
873
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_x Bool)
874
(declare-var Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_x Bool)
875
(declare-var Flowchart1.ni_1._arrow._first_x Bool)
876
(declare-var Flowchart1.Flowchart1_1_1 Int)
877
(declare-var Flowchart1.__Flowchart1_1 Bool)
878
(declare-var Flowchart1.i_virtual_local Real)
879
(declare-rel Flowchart1_reset (Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool Bool Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool Bool))
880
(declare-rel Flowchart1_step (Real Int Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool Bool Int Int Int Bool flowchart1_flowchart1__type Bool flowchart1_a__type Bool Bool Bool Bool))
881

    
882
(rule (=> 
883
  (and 
884
       
885
       (= Flowchart1.ni_1._arrow._first_m true)
886
       (Flowchart1_Flowchart1_reset Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c
887
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c
888
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c
889
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
890
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
891
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
892
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
893
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
894
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c
895
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_c
896
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m
897
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m
898
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m
899
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m
900
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m
901
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
902
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
903
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
904
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m
905
                                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_m)
906
  )
907
  (Flowchart1_reset Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c
908
                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c
909
                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c
910
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
911
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
912
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
913
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
914
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
915
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c
916
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_c
917
                    Flowchart1.ni_1._arrow._first_c
918
                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m
919
                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m
920
                    Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m
921
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m
922
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m
923
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
924
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
925
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
926
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m
927
                    Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_m
928
                    Flowchart1.ni_1._arrow._first_m)
929
))
930

    
931
(rule (=> 
932
  (and (= Flowchart1.ni_1._arrow._first_m Flowchart1.ni_1._arrow._first_c)
933
       (and (= Flowchart1.__Flowchart1_1 (ite Flowchart1.ni_1._arrow._first_m true false))
934
            (= Flowchart1.ni_1._arrow._first_x false))
935
       (and (or (not (= Flowchart1.__Flowchart1_1 true))
936
               (= Flowchart1.i_virtual_local 0.))
937
            (or (not (= Flowchart1.__Flowchart1_1 false))
938
               (= Flowchart1.i_virtual_local 1.))
939
       )
940
       (and (= Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c)
941
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c)
942
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c)
943
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c)
944
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c)
945
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c)
946
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c)
947
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c)
948
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c)
949
            (= Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_m Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_c)
950
            )
951
       (Flowchart1_Flowchart1_step true
952
                                   Flowchart1.Flowchart1_1_1
953
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_m
954
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_m
955
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_m
956
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_m
957
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_m
958
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_m
959
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_m
960
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_m
961
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_m
962
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_m
963
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_x
964
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_x
965
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_x
966
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x
967
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x
968
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
969
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
970
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x
971
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_x
972
                                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_x)
973
       (= Flowchart1.Out1_1_1 Flowchart1.Flowchart1_1_1)
974
       )
975
  (Flowchart1_step Flowchart1.i_virtual
976
                   Flowchart1.Out1_1_1
977
                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_c
978
                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_c
979
                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_c
980
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_c
981
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_c
982
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_c
983
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_c
984
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_c
985
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_c
986
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_c
987
                   Flowchart1.ni_1._arrow._first_c
988
                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_2_x
989
                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_3_x
990
                   Flowchart1.ni_0.Flowchart1_Flowchart1.__Flowchart1_Flowchart1_4_x
991
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_23_x
992
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.__Flowchart1_Flowchart1_node_24_x
993
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_14_x
994
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.__Flowchart1_A_node_15_x
995
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_4.flowchart1_flowchart1__FLOWCHART1_FLOWCHART1_PARALLEL_IDL_handler_until.ni_6.Flowchart1_A_node.ni_7._arrow._first_x
996
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_2.Flowchart1_Flowchart1_node.ni_5._arrow._first_x
997
                   Flowchart1.ni_0.Flowchart1_Flowchart1.ni_3._arrow._first_x
998
                   Flowchart1.ni_1._arrow._first_x)
999
))
1000