Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart3 / Flowchart3.smt2 @ eb639349

History | View | Annotate | Download (101 KB)

1
(declare-datatypes () ((flowchart3_flowchart3__type POINTFlowchart3_Flowchart3 POINT__TO__FLOWCHART3_A_1 FLOWCHART3_FLOWCHART3_PARALLEL_IDL)));
2

    
3
(declare-datatypes () ((flowchart3_a__type POINTFlowchart3_A)));
4

    
5
(declare-datatypes () ((flowchart3_a_INNER__type POINTFlowchart3_A_INNER FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1)));
6

    
7
; flowchart3_a__POINTFlowchart3_A_handler_until
8
(declare-var flowchart3_a__POINTFlowchart3_A_handler_until.idFlowchart3_A_1 Int)
9
(declare-var flowchart3_a__POINTFlowchart3_A_handler_until.flowchart3_a__restart_in Bool)
10
(declare-var flowchart3_a__POINTFlowchart3_A_handler_until.flowchart3_a__state_in flowchart3_a__type)
11
(declare-var flowchart3_a__POINTFlowchart3_A_handler_until.idFlowchart3_A_out Int)
12
(declare-rel flowchart3_a__POINTFlowchart3_A_handler_until (Int Bool flowchart3_a__type Int))
13
(rule (=> 
14
  (and (= flowchart3_a__POINTFlowchart3_A_handler_until.idFlowchart3_A_out flowchart3_a__POINTFlowchart3_A_handler_until.idFlowchart3_A_1)
15
       (= flowchart3_a__POINTFlowchart3_A_handler_until.flowchart3_a__state_in POINTFlowchart3_A)
16
       (= flowchart3_a__POINTFlowchart3_A_handler_until.flowchart3_a__restart_in false)
17
       )
18
  (flowchart3_a__POINTFlowchart3_A_handler_until flowchart3_a__POINTFlowchart3_A_handler_until.idFlowchart3_A_1 flowchart3_a__POINTFlowchart3_A_handler_until.flowchart3_a__restart_in flowchart3_a__POINTFlowchart3_A_handler_until.flowchart3_a__state_in flowchart3_a__POINTFlowchart3_A_handler_until.idFlowchart3_A_out)
19
))
20

    
21
; flowchart3_a__POINTFlowchart3_A_unless
22
(declare-var flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__restart_in Bool)
23
(declare-var flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__state_in flowchart3_a__type)
24
(declare-var flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__restart_act Bool)
25
(declare-var flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__state_act flowchart3_a__type)
26
(declare-rel flowchart3_a__POINTFlowchart3_A_unless (Bool flowchart3_a__type Bool flowchart3_a__type))
27
(rule (=> 
28
  (and (= flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__state_act flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__state_in)
29
       (= flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__restart_act flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__restart_in)
30
       )
31
  (flowchart3_a__POINTFlowchart3_A_unless flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__restart_in flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__state_in flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__restart_act flowchart3_a__POINTFlowchart3_A_unless.flowchart3_a__state_act)
32
))
33

    
34
; Flowchart3_A_node
35
(declare-var Flowchart3_A_node.idFlowchart3_A_1 Int)
36
(declare-var Flowchart3_A_node.idFlowchart3_A Int)
37
(declare-var Flowchart3_A_node.__Flowchart3_A_node_7_c Bool)
38
(declare-var Flowchart3_A_node.__Flowchart3_A_node_8_c flowchart3_a__type)
39
(declare-var Flowchart3_A_node.ni_8._arrow._first_c Bool)
40
(declare-var Flowchart3_A_node.__Flowchart3_A_node_7_m Bool)
41
(declare-var Flowchart3_A_node.__Flowchart3_A_node_8_m flowchart3_a__type)
42
(declare-var Flowchart3_A_node.ni_8._arrow._first_m Bool)
43
(declare-var Flowchart3_A_node.__Flowchart3_A_node_7_x Bool)
44
(declare-var Flowchart3_A_node.__Flowchart3_A_node_8_x flowchart3_a__type)
45
(declare-var Flowchart3_A_node.ni_8._arrow._first_x Bool)
46
(declare-var Flowchart3_A_node.__Flowchart3_A_node_1 Bool)
47
(declare-var Flowchart3_A_node.__Flowchart3_A_node_2 flowchart3_a__type)
48
(declare-var Flowchart3_A_node.__Flowchart3_A_node_3 Bool)
49
(declare-var Flowchart3_A_node.__Flowchart3_A_node_4 flowchart3_a__type)
50
(declare-var Flowchart3_A_node.__Flowchart3_A_node_5 Int)
51
(declare-var Flowchart3_A_node.__Flowchart3_A_node_6 Bool)
52
(declare-var Flowchart3_A_node.flowchart3_a__next_restart_in Bool)
53
(declare-var Flowchart3_A_node.flowchart3_a__next_state_in flowchart3_a__type)
54
(declare-var Flowchart3_A_node.flowchart3_a__restart_act Bool)
55
(declare-var Flowchart3_A_node.flowchart3_a__restart_in Bool)
56
(declare-var Flowchart3_A_node.flowchart3_a__state_act flowchart3_a__type)
57
(declare-var Flowchart3_A_node.flowchart3_a__state_in flowchart3_a__type)
58
(declare-rel Flowchart3_A_node_reset (Bool flowchart3_a__type Bool Bool flowchart3_a__type Bool))
59
(declare-rel Flowchart3_A_node_step (Int Int Bool flowchart3_a__type Bool Bool flowchart3_a__type Bool))
60

    
61
(rule (=> 
62
  (and 
63
       (= Flowchart3_A_node.__Flowchart3_A_node_7_m Flowchart3_A_node.__Flowchart3_A_node_7_c)
64
       (= Flowchart3_A_node.__Flowchart3_A_node_8_m Flowchart3_A_node.__Flowchart3_A_node_8_c)
65
       (= Flowchart3_A_node.ni_8._arrow._first_m true)
66
  )
67
  (Flowchart3_A_node_reset Flowchart3_A_node.__Flowchart3_A_node_7_c
68
                           Flowchart3_A_node.__Flowchart3_A_node_8_c
69
                           Flowchart3_A_node.ni_8._arrow._first_c
70
                           Flowchart3_A_node.__Flowchart3_A_node_7_m
71
                           Flowchart3_A_node.__Flowchart3_A_node_8_m
72
                           Flowchart3_A_node.ni_8._arrow._first_m)
73
))
74

    
75
(rule (=> 
76
  (and (= Flowchart3_A_node.ni_8._arrow._first_m Flowchart3_A_node.ni_8._arrow._first_c)
77
       (and (= Flowchart3_A_node.__Flowchart3_A_node_6 (ite Flowchart3_A_node.ni_8._arrow._first_m true false))
78
            (= Flowchart3_A_node.ni_8._arrow._first_x false))
79
       (and (or (not (= Flowchart3_A_node.__Flowchart3_A_node_6 false))
80
               (and (= Flowchart3_A_node.flowchart3_a__state_in Flowchart3_A_node.__Flowchart3_A_node_8_c)
81
                    (= Flowchart3_A_node.flowchart3_a__restart_in Flowchart3_A_node.__Flowchart3_A_node_7_c)
82
                    ))
83
            (or (not (= Flowchart3_A_node.__Flowchart3_A_node_6 true))
84
               (and (= Flowchart3_A_node.flowchart3_a__state_in POINTFlowchart3_A)
85
                    (= Flowchart3_A_node.flowchart3_a__restart_in false)
86
                    ))
87
       )
88
       (or (not (= Flowchart3_A_node.flowchart3_a__state_in POINTFlowchart3_A))
89
          (and (flowchart3_a__POINTFlowchart3_A_unless Flowchart3_A_node.flowchart3_a__restart_in
90
                                                       Flowchart3_A_node.flowchart3_a__state_in
91
                                                       Flowchart3_A_node.__Flowchart3_A_node_1
92
                                                       Flowchart3_A_node.__Flowchart3_A_node_2)
93
               (= Flowchart3_A_node.flowchart3_a__state_act Flowchart3_A_node.__Flowchart3_A_node_2)
94
               (= Flowchart3_A_node.flowchart3_a__restart_act Flowchart3_A_node.__Flowchart3_A_node_1)
95
               ))
96
       (or (not (= Flowchart3_A_node.flowchart3_a__state_act POINTFlowchart3_A))
97
          (and (flowchart3_a__POINTFlowchart3_A_handler_until Flowchart3_A_node.idFlowchart3_A_1
98
                                                              Flowchart3_A_node.__Flowchart3_A_node_3
99
                                                              Flowchart3_A_node.__Flowchart3_A_node_4
100
                                                              Flowchart3_A_node.__Flowchart3_A_node_5)
101
               (= Flowchart3_A_node.idFlowchart3_A Flowchart3_A_node.__Flowchart3_A_node_5)
102
               (= Flowchart3_A_node.flowchart3_a__next_state_in Flowchart3_A_node.__Flowchart3_A_node_4)
103
               (= Flowchart3_A_node.flowchart3_a__next_restart_in Flowchart3_A_node.__Flowchart3_A_node_3)
104
               ))
105
       (= Flowchart3_A_node.__Flowchart3_A_node_8_x Flowchart3_A_node.flowchart3_a__next_state_in)
106
       (= Flowchart3_A_node.__Flowchart3_A_node_7_x Flowchart3_A_node.flowchart3_a__next_restart_in)
107
       )
108
  (Flowchart3_A_node_step Flowchart3_A_node.idFlowchart3_A_1
109
                          Flowchart3_A_node.idFlowchart3_A
110
                          Flowchart3_A_node.__Flowchart3_A_node_7_c
111
                          Flowchart3_A_node.__Flowchart3_A_node_8_c
112
                          Flowchart3_A_node.ni_8._arrow._first_c
113
                          Flowchart3_A_node.__Flowchart3_A_node_7_x
114
                          Flowchart3_A_node.__Flowchart3_A_node_8_x
115
                          Flowchart3_A_node.ni_8._arrow._first_x)
116
))
117

    
118
; Flowchart3_A_en
119
(declare-var Flowchart3_A_en.idFlowchart3_A_1 Int)
120
(declare-var Flowchart3_A_en.idFlowchart3_Flowchart3_1 Int)
121
(declare-var Flowchart3_A_en.isInner Bool)
122
(declare-var Flowchart3_A_en.idFlowchart3_A Int)
123
(declare-var Flowchart3_A_en.idFlowchart3_Flowchart3 Int)
124
(declare-rel Flowchart3_A_en (Int Int Bool Int Int))
125
(rule (=> 
126
  (and (= Flowchart3_A_en.idFlowchart3_Flowchart3 790)
127
       (= Flowchart3_A_en.idFlowchart3_A (- 1))
128
       )
129
  (Flowchart3_A_en Flowchart3_A_en.idFlowchart3_A_1 Flowchart3_A_en.idFlowchart3_Flowchart3_1 Flowchart3_A_en.isInner Flowchart3_A_en.idFlowchart3_A Flowchart3_A_en.idFlowchart3_Flowchart3)
130
))
131

    
132
; flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until
133
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_Flowchart3_1 Int)
134
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_1 Int)
135
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.flowchart3_flowchart3__restart_in Bool)
136
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.flowchart3_flowchart3__state_in flowchart3_flowchart3__type)
137
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_out Int)
138
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_Flowchart3_out Int)
139
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c Bool)
140
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c flowchart3_a__type)
141
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c Bool)
142
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Bool)
143
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m flowchart3_a__type)
144
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Bool)
145
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x Bool)
146
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x flowchart3_a__type)
147
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x Bool)
148
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.__flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_2 Int)
149
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_2 Int)
150
(declare-rel flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_reset (Bool flowchart3_a__type Bool Bool flowchart3_a__type Bool))
151
(declare-rel flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_step (Int Int Bool flowchart3_flowchart3__type Int Int Bool flowchart3_a__type Bool Bool flowchart3_a__type Bool))
152

    
153
(rule (=> 
154
  (and 
155
       
156
       (Flowchart3_A_node_reset flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
157
                                flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
158
                                flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
159
                                flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
160
                                flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
161
                                flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m)
162
  )
163
  (flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_reset 
164
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
165
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
166
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
167
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
168
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
169
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m)
170
))
171

    
172
(rule (=> 
173
  (and (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_Flowchart3_out flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_Flowchart3_1)
174
       (and (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c)
175
            (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c)
176
            (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c)
177
            )
178
       (Flowchart3_A_node_step flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_1
179
                               flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.__flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_2
180
                               flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
181
                               flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
182
                               flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
183
                               flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
184
                               flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
185
                               flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x)
186
       (and (or (not (= (not (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_1 0)) true))
187
               (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_2 flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.__flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_2))
188
            (or (not (= (not (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_1 0)) false))
189
               (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_2 flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_1))
190
       )
191
       (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_out flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_2)
192
       (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.flowchart3_flowchart3__state_in POINTFlowchart3_Flowchart3)
193
       (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.flowchart3_flowchart3__restart_in true)
194
       )
195
  (flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_step 
196
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_Flowchart3_1
197
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_1
198
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.flowchart3_flowchart3__restart_in
199
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.flowchart3_flowchart3__state_in
200
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_A_out
201
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.idFlowchart3_Flowchart3_out
202
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
203
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
204
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
205
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
206
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
207
  flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x)
208
))
209

    
210
; flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless
211
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__restart_in Bool)
212
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__state_in flowchart3_flowchart3__type)
213
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__restart_act Bool)
214
(declare-var flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__state_act flowchart3_flowchart3__type)
215
(declare-rel flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless (Bool flowchart3_flowchart3__type Bool flowchart3_flowchart3__type))
216
(rule (=> 
217
  (and (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__state_act flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__state_in)
218
       (= flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__restart_act flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__restart_in)
219
       )
220
  (flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__restart_in flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__state_in flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__restart_act flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless.flowchart3_flowchart3__state_act)
221
))
222

    
223
; flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until
224
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_Flowchart3_1 Int)
225
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_A_1 Int)
226
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.flowchart3_flowchart3__restart_in Bool)
227
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.flowchart3_flowchart3__state_in flowchart3_flowchart3__type)
228
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_A_out Int)
229
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_Flowchart3_out Int)
230
(declare-rel flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until (Int Int Bool flowchart3_flowchart3__type Int Int))
231
(rule (=> 
232
  (and (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_Flowchart3_out flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_Flowchart3_1)
233
       (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_A_out flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_A_1)
234
       (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.flowchart3_flowchart3__state_in POINTFlowchart3_Flowchart3)
235
       (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.flowchart3_flowchart3__restart_in false)
236
       )
237
  (flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_Flowchart3_1 flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_A_1 flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.flowchart3_flowchart3__restart_in flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.flowchart3_flowchart3__state_in flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_A_out flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until.idFlowchart3_Flowchart3_out)
238
))
239

    
240
; flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless
241
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__restart_in Bool)
242
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__state_in flowchart3_flowchart3__type)
243
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.idFlowchart3_Flowchart3_1 Int)
244
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__restart_act Bool)
245
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__state_act flowchart3_flowchart3__type)
246
(declare-var flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.__flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless_1 Bool)
247
(declare-rel flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless (Bool flowchart3_flowchart3__type Int Bool flowchart3_flowchart3__type))
248
(rule (=> 
249
  (and (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.__flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless_1 (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.idFlowchart3_Flowchart3_1 0))
250
       (and (or (not (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.__flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless_1 false))
251
               (and (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__state_act FLOWCHART3_FLOWCHART3_PARALLEL_IDL)
252
                    (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__restart_act true)
253
                    ))
254
            (or (not (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.__flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless_1 true))
255
               (and (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__state_act POINT__TO__FLOWCHART3_A_1)
256
                    (= flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__restart_act true)
257
                    ))
258
       )
259
       )
260
  (flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__restart_in flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__state_in flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.idFlowchart3_Flowchart3_1 flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__restart_act flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless.flowchart3_flowchart3__state_act)
261
))
262

    
263
; flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until
264
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_1 Int)
265
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_1 Int)
266
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.flowchart3_flowchart3__restart_in Bool)
267
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.flowchart3_flowchart3__state_in flowchart3_flowchart3__type)
268
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_out Int)
269
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_out Int)
270
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_2 Int)
271
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_2 Int)
272
(declare-rel flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until (Int Int Bool flowchart3_flowchart3__type Int Int))
273
(rule (=> 
274
  (and (Flowchart3_A_en flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_1
275
                        flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_1
276
                        false
277
                        flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_2
278
                        flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_2)
279
       (= flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_out flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_2)
280
       (= flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_out flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_2)
281
       (= flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.flowchart3_flowchart3__state_in POINTFlowchart3_Flowchart3)
282
       (= flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.flowchart3_flowchart3__restart_in true)
283
       )
284
  (flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_1 flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_1 flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.flowchart3_flowchart3__restart_in flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.flowchart3_flowchart3__state_in flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_A_out flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until.idFlowchart3_Flowchart3_out)
285
))
286

    
287
; flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless
288
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__restart_in Bool)
289
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__state_in flowchart3_flowchart3__type)
290
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__restart_act Bool)
291
(declare-var flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__state_act flowchart3_flowchart3__type)
292
(declare-rel flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless (Bool flowchart3_flowchart3__type Bool flowchart3_flowchart3__type))
293
(rule (=> 
294
  (and (= flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__state_act flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__state_in)
295
       (= flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__restart_act flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__restart_in)
296
       )
297
  (flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__restart_in flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__state_in flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__restart_act flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless.flowchart3_flowchart3__state_act)
298
))
299

    
300
; Flowchart3_Flowchart3_node
301
(declare-var Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3_1 Int)
302
(declare-var Flowchart3_Flowchart3_node.idFlowchart3_A_1 Int)
303
(declare-var Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3 Int)
304
(declare-var Flowchart3_Flowchart3_node.idFlowchart3_A Int)
305
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c Bool)
306
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c flowchart3_flowchart3__type)
307
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c Bool)
308
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c flowchart3_a__type)
309
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c Bool)
310
(declare-var Flowchart3_Flowchart3_node.ni_6._arrow._first_c Bool)
311
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m Bool)
312
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m flowchart3_flowchart3__type)
313
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Bool)
314
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m flowchart3_a__type)
315
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Bool)
316
(declare-var Flowchart3_Flowchart3_node.ni_6._arrow._first_m Bool)
317
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x Bool)
318
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x flowchart3_flowchart3__type)
319
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x Bool)
320
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x flowchart3_a__type)
321
(declare-var Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x Bool)
322
(declare-var Flowchart3_Flowchart3_node.ni_6._arrow._first_x Bool)
323
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_1 Bool)
324
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_10 Int)
325
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_11 Bool)
326
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_12 flowchart3_flowchart3__type)
327
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_13 Int)
328
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_14 Int)
329
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_15 Bool)
330
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_16 flowchart3_flowchart3__type)
331
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_17 Int)
332
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_18 Int)
333
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_19 Bool)
334
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_2 flowchart3_flowchart3__type)
335
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_3 Bool)
336
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_4 flowchart3_flowchart3__type)
337
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_5 Bool)
338
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_6 flowchart3_flowchart3__type)
339
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_7 Bool)
340
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_8 flowchart3_flowchart3__type)
341
(declare-var Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_9 Int)
342
(declare-var Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_restart_in Bool)
343
(declare-var Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_state_in flowchart3_flowchart3__type)
344
(declare-var Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_act Bool)
345
(declare-var Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_in Bool)
346
(declare-var Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_act flowchart3_flowchart3__type)
347
(declare-var Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in flowchart3_flowchart3__type)
348
(declare-rel Flowchart3_Flowchart3_node_reset (Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool))
349
(declare-rel Flowchart3_Flowchart3_node_step (Int Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool))
350

    
351
(rule (=> 
352
  (and 
353
       (= Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c)
354
       (= Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c)
355
       (= Flowchart3_Flowchart3_node.ni_6._arrow._first_m true)
356
       (flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_reset 
357
       Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
358
       Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
359
       Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
360
       Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
361
       Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
362
       Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m)
363
  )
364
  (Flowchart3_Flowchart3_node_reset Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
365
                                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
366
                                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
367
                                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
368
                                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
369
                                    Flowchart3_Flowchart3_node.ni_6._arrow._first_c
370
                                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m
371
                                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m
372
                                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
373
                                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
374
                                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
375
                                    Flowchart3_Flowchart3_node.ni_6._arrow._first_m)
376
))
377

    
378
(rule (=> 
379
  (and (= Flowchart3_Flowchart3_node.ni_6._arrow._first_m Flowchart3_Flowchart3_node.ni_6._arrow._first_c)
380
       (and (= Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_19 (ite Flowchart3_Flowchart3_node.ni_6._arrow._first_m true false))
381
            (= Flowchart3_Flowchart3_node.ni_6._arrow._first_x false))
382
       (and (or (not (= Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_19 false))
383
               (and (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c)
384
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c)
385
                    ))
386
            (or (not (= Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_19 true))
387
               (and (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in POINTFlowchart3_Flowchart3)
388
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_in false)
389
                    ))
390
       )
391
       (and (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in FLOWCHART3_FLOWCHART3_PARALLEL_IDL))
392
               (and (flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_unless 
393
                    Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_in
394
                    Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in
395
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_1
396
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_2)
397
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_act Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_2)
398
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_act Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_1)
399
                    ))
400
            (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in POINTFlowchart3_Flowchart3))
401
               (and (flowchart3_flowchart3__POINTFlowchart3_Flowchart3_unless 
402
                    Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_in
403
                    Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in
404
                    Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3_1
405
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_5
406
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_6)
407
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_act Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_6)
408
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_act Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_5)
409
                    ))
410
            (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in POINT__TO__FLOWCHART3_A_1))
411
               (and (flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_unless 
412
                    Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_in
413
                    Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_in
414
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_3
415
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_4)
416
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_act Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_4)
417
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_act Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_3)
418
                    ))
419
       )
420
       (and (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_act FLOWCHART3_FLOWCHART3_PARALLEL_IDL))
421
               (and (and (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_act true))
422
                            (flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_reset 
423
                            Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
424
                            Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
425
                            Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
426
                            Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
427
                            Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
428
                            Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m))
429
                         (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__restart_act false))
430
                            (and (= Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c)
431
                                 (= Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c)
432
                                 (= Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c)
433
                                 )
434
                            )
435
                    )
436
                    (and (= Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c)
437
                         (= Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c)
438
                         (= Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c)
439
                         )
440
                    (flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until_step 
441
                    Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3_1
442
                    Flowchart3_Flowchart3_node.idFlowchart3_A_1
443
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_7
444
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_8
445
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_9
446
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_10
447
                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
448
                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
449
                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
450
                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
451
                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
452
                    Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x)
453
                    (= Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3 Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_10)
454
                    (= Flowchart3_Flowchart3_node.idFlowchart3_A Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_9)
455
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_state_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_8)
456
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_restart_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_7)
457
                    ))
458
            (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_act POINTFlowchart3_Flowchart3))
459
               (and (flowchart3_flowchart3__POINTFlowchart3_Flowchart3_handler_until 
460
                    Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3_1
461
                    Flowchart3_Flowchart3_node.idFlowchart3_A_1
462
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_15
463
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_16
464
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_17
465
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_18)
466
                    (= Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3 Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_18)
467
                    (= Flowchart3_Flowchart3_node.idFlowchart3_A Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_17)
468
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_state_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_16)
469
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_restart_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_15)
470
                    ))
471
            (or (not (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__state_act POINT__TO__FLOWCHART3_A_1))
472
               (and (flowchart3_flowchart3__POINT__TO__FLOWCHART3_A_1_handler_until 
473
                    Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3_1
474
                    Flowchart3_Flowchart3_node.idFlowchart3_A_1
475
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_11
476
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_12
477
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_13
478
                    Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_14)
479
                    (= Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3 Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_14)
480
                    (= Flowchart3_Flowchart3_node.idFlowchart3_A Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_13)
481
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_state_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_12)
482
                    (= Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_restart_in Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_11)
483
                    ))
484
       )
485
       (= Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_state_in)
486
       (= Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x Flowchart3_Flowchart3_node.flowchart3_flowchart3__next_restart_in)
487
       )
488
  (Flowchart3_Flowchart3_node_step Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3_1
489
                                   Flowchart3_Flowchart3_node.idFlowchart3_A_1
490
                                   Flowchart3_Flowchart3_node.idFlowchart3_Flowchart3
491
                                   Flowchart3_Flowchart3_node.idFlowchart3_A
492
                                   Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
493
                                   Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
494
                                   Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
495
                                   Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
496
                                   Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
497
                                   Flowchart3_Flowchart3_node.ni_6._arrow._first_c
498
                                   Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x
499
                                   Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x
500
                                   Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
501
                                   Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
502
                                   Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x
503
                                   Flowchart3_Flowchart3_node.ni_6._arrow._first_x)
504
))
505

    
506
; Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action
507
(declare-var Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action.x_1 Int)
508
(declare-var Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action.x Int)
509
(declare-rel Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action (Int Int))
510
(rule (=> 
511
  (= Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action.x (+ Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action.x_1 1))
512
  (Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action.x_1 Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action.x)
513
))
514

    
515
; Flowchart3_Flowchart3
516
(declare-var Flowchart3_Flowchart3.noInput Bool)
517
(declare-var Flowchart3_Flowchart3.x Int)
518
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c Int)
519
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c Int)
520
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c Int)
521
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c Bool)
522
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c flowchart3_flowchart3__type)
523
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c Bool)
524
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c flowchart3_a__type)
525
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c Bool)
526
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c Bool)
527
(declare-var Flowchart3_Flowchart3.ni_4._arrow._first_c Bool)
528
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m Int)
529
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m Int)
530
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m Int)
531
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m Bool)
532
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m flowchart3_flowchart3__type)
533
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Bool)
534
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m flowchart3_a__type)
535
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Bool)
536
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m Bool)
537
(declare-var Flowchart3_Flowchart3.ni_4._arrow._first_m Bool)
538
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_x Int)
539
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_x Int)
540
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_x Int)
541
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x Bool)
542
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x flowchart3_flowchart3__type)
543
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x Bool)
544
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x flowchart3_a__type)
545
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x Bool)
546
(declare-var Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_x Bool)
547
(declare-var Flowchart3_Flowchart3.ni_4._arrow._first_x Bool)
548
(declare-var Flowchart3_Flowchart3.__Flowchart3_Flowchart3_1 Bool)
549
(declare-var Flowchart3_Flowchart3.idFlowchart3_A Int)
550
(declare-var Flowchart3_Flowchart3.idFlowchart3_A_1 Int)
551
(declare-var Flowchart3_Flowchart3.idFlowchart3_Flowchart3 Int)
552
(declare-var Flowchart3_Flowchart3.idFlowchart3_Flowchart3_1 Int)
553
(declare-var Flowchart3_Flowchart3.x_1 Int)
554
(declare-rel Flowchart3_Flowchart3_reset (Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool))
555
(declare-rel Flowchart3_Flowchart3_step (Bool Int Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool))
556

    
557
(rule (=> 
558
  (and 
559
       (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c)
560
       (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c)
561
       (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c)
562
       (= Flowchart3_Flowchart3.ni_4._arrow._first_m true)
563
       (Flowchart3_Flowchart3_node_reset Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
564
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
565
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
566
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
567
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
568
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c
569
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m
570
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m
571
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
572
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
573
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
574
                                         Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m)
575
  )
576
  (Flowchart3_Flowchart3_reset Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c
577
                               Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c
578
                               Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c
579
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
580
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
581
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
582
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
583
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
584
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c
585
                               Flowchart3_Flowchart3.ni_4._arrow._first_c
586
                               Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m
587
                               Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m
588
                               Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m
589
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m
590
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m
591
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
592
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
593
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
594
                               Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m
595
                               Flowchart3_Flowchart3.ni_4._arrow._first_m)
596
))
597

    
598
(rule (=> 
599
  (and (= Flowchart3_Flowchart3.ni_4._arrow._first_m Flowchart3_Flowchart3.ni_4._arrow._first_c)
600
       (and (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_1 (ite Flowchart3_Flowchart3.ni_4._arrow._first_m true false))
601
            (= Flowchart3_Flowchart3.ni_4._arrow._first_x false))
602
       (and (or (not (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_1 true))
603
               (= Flowchart3_Flowchart3.x_1 0))
604
            (or (not (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_1 false))
605
               (= Flowchart3_Flowchart3.x_1 Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c))
606
       )
607
       (= Flowchart3_Flowchart3.x 0)
608
       (and (or (not (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_1 false))
609
               (and (= Flowchart3_Flowchart3.idFlowchart3_Flowchart3_1 Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c)
610
                    (= Flowchart3_Flowchart3.idFlowchart3_A_1 Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c)
611
                    ))
612
            (or (not (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_1 true))
613
               (and (= Flowchart3_Flowchart3.idFlowchart3_Flowchart3_1 0)
614
                    (= Flowchart3_Flowchart3.idFlowchart3_A_1 0)
615
                    ))
616
       )
617
       (and (= Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c)
618
            (= Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c)
619
            (= Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c)
620
            (= Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c)
621
            (= Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c)
622
            (= Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c)
623
            )
624
       (Flowchart3_Flowchart3_node_step Flowchart3_Flowchart3.idFlowchart3_Flowchart3_1
625
                                        Flowchart3_Flowchart3.idFlowchart3_A_1
626
                                        Flowchart3_Flowchart3.idFlowchart3_Flowchart3
627
                                        Flowchart3_Flowchart3.idFlowchart3_A
628
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m
629
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m
630
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
631
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
632
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
633
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m
634
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x
635
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x
636
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
637
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
638
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x
639
                                        Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_x)
640
       (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_x Flowchart3_Flowchart3.x)
641
       (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_x Flowchart3_Flowchart3.idFlowchart3_Flowchart3)
642
       (= Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_x Flowchart3_Flowchart3.idFlowchart3_A)
643
       )
644
  (Flowchart3_Flowchart3_step Flowchart3_Flowchart3.noInput
645
                              Flowchart3_Flowchart3.x
646
                              Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c
647
                              Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c
648
                              Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c
649
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
650
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
651
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
652
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
653
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
654
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c
655
                              Flowchart3_Flowchart3.ni_4._arrow._first_c
656
                              Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_x
657
                              Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_x
658
                              Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_x
659
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x
660
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x
661
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
662
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
663
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x
664
                              Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_x
665
                              Flowchart3_Flowchart3.ni_4._arrow._first_x)
666
))
667

    
668
; flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until
669
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_1 Int)
670
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.flowchart3_a_INNER__restart_in Bool)
671
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.flowchart3_a_INNER__state_in flowchart3_a_INNER__type)
672
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_out Int)
673
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_2 Int)
674
(declare-rel flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until (Int Bool flowchart3_a_INNER__type Int))
675
(rule (=> 
676
  (and (Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action 
677
       flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_1
678
       flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_2)
679
       (= flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_out flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_2)
680
       (= flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.flowchart3_a_INNER__state_in POINTFlowchart3_A_INNER)
681
       (= flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.flowchart3_a_INNER__restart_in true)
682
       )
683
  (flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_1 flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.flowchart3_a_INNER__restart_in flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.flowchart3_a_INNER__state_in flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until.x_out)
684
))
685

    
686
; flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless
687
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__restart_in Bool)
688
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__state_in flowchart3_a_INNER__type)
689
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__restart_act Bool)
690
(declare-var flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__state_act flowchart3_a_INNER__type)
691
(declare-rel flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless (Bool flowchart3_a_INNER__type Bool flowchart3_a_INNER__type))
692
(rule (=> 
693
  (and (= flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__state_act flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__state_in)
694
       (= flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__restart_act flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__restart_in)
695
       )
696
  (flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__restart_in flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__state_in flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__restart_act flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless.flowchart3_a_INNER__state_act)
697
))
698

    
699
; flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until
700
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.x_1 Int)
701
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.flowchart3_a_INNER__restart_in Bool)
702
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.flowchart3_a_INNER__state_in flowchart3_a_INNER__type)
703
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.x_out Int)
704
(declare-rel flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until (Int Bool flowchart3_a_INNER__type Int))
705
(rule (=> 
706
  (and (= flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.x_out flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.x_1)
707
       (= flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.flowchart3_a_INNER__state_in POINTFlowchart3_A_INNER)
708
       (= flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.flowchart3_a_INNER__restart_in false)
709
       )
710
  (flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.x_1 flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.flowchart3_a_INNER__restart_in flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.flowchart3_a_INNER__state_in flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until.x_out)
711
))
712

    
713
; flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless
714
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__restart_in Bool)
715
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__state_in flowchart3_a_INNER__type)
716
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__restart_act Bool)
717
(declare-var flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__state_act flowchart3_a_INNER__type)
718
(declare-rel flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless (Bool flowchart3_a_INNER__type Bool flowchart3_a_INNER__type))
719
(rule (=> 
720
  (and (= flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__state_act FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1)
721
       (= flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__restart_act true)
722
       )
723
  (flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__restart_in flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__state_in flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__restart_act flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless.flowchart3_a_INNER__state_act)
724
))
725

    
726
; Flowchart3
727
(declare-var Flowchart3.i_virtual Real)
728
(declare-var Flowchart3.Out1_1_1 Int)
729
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c Int)
730
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c Int)
731
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c Int)
732
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c Bool)
733
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c flowchart3_flowchart3__type)
734
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c Bool)
735
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c flowchart3_a__type)
736
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c Bool)
737
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c Bool)
738
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_c Bool)
739
(declare-var Flowchart3.ni_2._arrow._first_c Bool)
740
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m Int)
741
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m Int)
742
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m Int)
743
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m Bool)
744
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m flowchart3_flowchart3__type)
745
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Bool)
746
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m flowchart3_a__type)
747
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Bool)
748
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m Bool)
749
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_m Bool)
750
(declare-var Flowchart3.ni_2._arrow._first_m Bool)
751
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_x Int)
752
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_x Int)
753
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_x Int)
754
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x Bool)
755
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x flowchart3_flowchart3__type)
756
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x Bool)
757
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x flowchart3_a__type)
758
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x Bool)
759
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_x Bool)
760
(declare-var Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_x Bool)
761
(declare-var Flowchart3.ni_2._arrow._first_x Bool)
762
(declare-var Flowchart3.Flowchart3_1_1 Int)
763
(declare-var Flowchart3.__Flowchart3_1 Bool)
764
(declare-var Flowchart3.i_virtual_local Real)
765
(declare-rel Flowchart3_reset (Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool Bool Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool Bool))
766
(declare-rel Flowchart3_step (Real Int Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool Bool Int Int Int Bool flowchart3_flowchart3__type Bool flowchart3_a__type Bool Bool Bool Bool))
767

    
768
(rule (=> 
769
  (and 
770
       
771
       (= Flowchart3.ni_2._arrow._first_m true)
772
       (Flowchart3_Flowchart3_reset Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c
773
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c
774
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c
775
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
776
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
777
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
778
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
779
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
780
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c
781
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_c
782
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m
783
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m
784
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m
785
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m
786
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m
787
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
788
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
789
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
790
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m
791
                                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_m)
792
  )
793
  (Flowchart3_reset Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c
794
                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c
795
                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c
796
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
797
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
798
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
799
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
800
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
801
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c
802
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_c
803
                    Flowchart3.ni_2._arrow._first_c
804
                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m
805
                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m
806
                    Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m
807
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m
808
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m
809
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
810
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
811
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
812
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m
813
                    Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_m
814
                    Flowchart3.ni_2._arrow._first_m)
815
))
816

    
817
(rule (=> 
818
  (and (= Flowchart3.ni_2._arrow._first_m Flowchart3.ni_2._arrow._first_c)
819
       (and (= Flowchart3.__Flowchart3_1 (ite Flowchart3.ni_2._arrow._first_m true false))
820
            (= Flowchart3.ni_2._arrow._first_x false))
821
       (and (or (not (= Flowchart3.__Flowchart3_1 true))
822
               (= Flowchart3.i_virtual_local 0.))
823
            (or (not (= Flowchart3.__Flowchart3_1 false))
824
               (= Flowchart3.i_virtual_local 1.))
825
       )
826
       (and (= Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c)
827
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c)
828
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c)
829
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c)
830
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c)
831
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c)
832
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c)
833
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c)
834
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c)
835
            (= Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_m Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_c)
836
            )
837
       (Flowchart3_Flowchart3_step true
838
                                   Flowchart3.Flowchart3_1_1
839
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_m
840
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_m
841
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_m
842
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_m
843
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_m
844
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_m
845
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_m
846
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_m
847
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_m
848
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_m
849
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_x
850
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_x
851
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_x
852
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x
853
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x
854
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
855
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
856
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x
857
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_x
858
                                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_x)
859
       (= Flowchart3.Out1_1_1 Flowchart3.Flowchart3_1_1)
860
       )
861
  (Flowchart3_step Flowchart3.i_virtual
862
                   Flowchart3.Out1_1_1
863
                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_c
864
                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_c
865
                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_c
866
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_c
867
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_c
868
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_c
869
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_c
870
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_c
871
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_c
872
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_c
873
                   Flowchart3.ni_2._arrow._first_c
874
                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_2_x
875
                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_3_x
876
                   Flowchart3.ni_1.Flowchart3_Flowchart3.__Flowchart3_Flowchart3_4_x
877
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_20_x
878
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.__Flowchart3_Flowchart3_node_21_x
879
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_7_x
880
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.__Flowchart3_A_node_8_x
881
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_5.flowchart3_flowchart3__FLOWCHART3_FLOWCHART3_PARALLEL_IDL_handler_until.ni_7.Flowchart3_A_node.ni_8._arrow._first_x
882
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_3.Flowchart3_Flowchart3_node.ni_6._arrow._first_x
883
                   Flowchart3.ni_1.Flowchart3_Flowchart3.ni_4._arrow._first_x
884
                   Flowchart3.ni_2._arrow._first_x)
885
))
886

    
887
; Flowchart3_A_ex
888
(declare-var Flowchart3_A_ex.idFlowchart3_Flowchart3_1 Int)
889
(declare-var Flowchart3_A_ex.isInner Bool)
890
(declare-var Flowchart3_A_ex.idFlowchart3_Flowchart3 Int)
891
(declare-var Flowchart3_A_ex.idFlowchart3_Flowchart3_2 Int)
892
(declare-rel Flowchart3_A_ex (Int Bool Int))
893
(rule (=> 
894
  (and (and (or (not (= (not Flowchart3_A_ex.isInner) true))
895
               (= Flowchart3_A_ex.idFlowchart3_Flowchart3_2 0))
896
            (or (not (= (not Flowchart3_A_ex.isInner) false))
897
               (= Flowchart3_A_ex.idFlowchart3_Flowchart3_2 Flowchart3_A_ex.idFlowchart3_Flowchart3_1))
898
       )
899
       (= Flowchart3_A_ex.idFlowchart3_Flowchart3 Flowchart3_A_ex.idFlowchart3_Flowchart3_1)
900
       )
901
  (Flowchart3_A_ex Flowchart3_A_ex.idFlowchart3_Flowchart3_1 Flowchart3_A_ex.isInner Flowchart3_A_ex.idFlowchart3_Flowchart3)
902
))
903

    
904
; Flowchart3_A_du
905
(declare-var Flowchart3_A_du.x_1 Int)
906
(declare-var Flowchart3_A_du.x Int)
907
(declare-var Flowchart3_A_du.__Flowchart3_A_du_12_c Bool)
908
(declare-var Flowchart3_A_du.__Flowchart3_A_du_13_c flowchart3_a_INNER__type)
909
(declare-var Flowchart3_A_du.ni_0._arrow._first_c Bool)
910
(declare-var Flowchart3_A_du.__Flowchart3_A_du_12_m Bool)
911
(declare-var Flowchart3_A_du.__Flowchart3_A_du_13_m flowchart3_a_INNER__type)
912
(declare-var Flowchart3_A_du.ni_0._arrow._first_m Bool)
913
(declare-var Flowchart3_A_du.__Flowchart3_A_du_12_x Bool)
914
(declare-var Flowchart3_A_du.__Flowchart3_A_du_13_x flowchart3_a_INNER__type)
915
(declare-var Flowchart3_A_du.ni_0._arrow._first_x Bool)
916
(declare-var Flowchart3_A_du.__Flowchart3_A_du_1 Bool)
917
(declare-var Flowchart3_A_du.__Flowchart3_A_du_10 Int)
918
(declare-var Flowchart3_A_du.__Flowchart3_A_du_11 Bool)
919
(declare-var Flowchart3_A_du.__Flowchart3_A_du_2 flowchart3_a_INNER__type)
920
(declare-var Flowchart3_A_du.__Flowchart3_A_du_3 Bool)
921
(declare-var Flowchart3_A_du.__Flowchart3_A_du_4 flowchart3_a_INNER__type)
922
(declare-var Flowchart3_A_du.__Flowchart3_A_du_5 Bool)
923
(declare-var Flowchart3_A_du.__Flowchart3_A_du_6 flowchart3_a_INNER__type)
924
(declare-var Flowchart3_A_du.__Flowchart3_A_du_7 Int)
925
(declare-var Flowchart3_A_du.__Flowchart3_A_du_8 Bool)
926
(declare-var Flowchart3_A_du.__Flowchart3_A_du_9 flowchart3_a_INNER__type)
927
(declare-var Flowchart3_A_du.flowchart3_a_INNER__next_restart_in Bool)
928
(declare-var Flowchart3_A_du.flowchart3_a_INNER__next_state_in flowchart3_a_INNER__type)
929
(declare-var Flowchart3_A_du.flowchart3_a_INNER__restart_act Bool)
930
(declare-var Flowchart3_A_du.flowchart3_a_INNER__restart_in Bool)
931
(declare-var Flowchart3_A_du.flowchart3_a_INNER__state_act flowchart3_a_INNER__type)
932
(declare-var Flowchart3_A_du.flowchart3_a_INNER__state_in flowchart3_a_INNER__type)
933
(declare-rel Flowchart3_A_du_reset (Bool flowchart3_a_INNER__type Bool Bool flowchart3_a_INNER__type Bool))
934
(declare-rel Flowchart3_A_du_step (Int Int Bool flowchart3_a_INNER__type Bool Bool flowchart3_a_INNER__type Bool))
935

    
936
(rule (=> 
937
  (and 
938
       (= Flowchart3_A_du.__Flowchart3_A_du_12_m Flowchart3_A_du.__Flowchart3_A_du_12_c)
939
       (= Flowchart3_A_du.__Flowchart3_A_du_13_m Flowchart3_A_du.__Flowchart3_A_du_13_c)
940
       (= Flowchart3_A_du.ni_0._arrow._first_m true)
941
  )
942
  (Flowchart3_A_du_reset Flowchart3_A_du.__Flowchart3_A_du_12_c
943
                         Flowchart3_A_du.__Flowchart3_A_du_13_c
944
                         Flowchart3_A_du.ni_0._arrow._first_c
945
                         Flowchart3_A_du.__Flowchart3_A_du_12_m
946
                         Flowchart3_A_du.__Flowchart3_A_du_13_m
947
                         Flowchart3_A_du.ni_0._arrow._first_m)
948
))
949

    
950
(rule (=> 
951
  (and (= Flowchart3_A_du.ni_0._arrow._first_m Flowchart3_A_du.ni_0._arrow._first_c)
952
       (and (= Flowchart3_A_du.__Flowchart3_A_du_11 (ite Flowchart3_A_du.ni_0._arrow._first_m true false))
953
            (= Flowchart3_A_du.ni_0._arrow._first_x false))
954
       (and (or (not (= Flowchart3_A_du.__Flowchart3_A_du_11 false))
955
               (and (= Flowchart3_A_du.flowchart3_a_INNER__state_in Flowchart3_A_du.__Flowchart3_A_du_13_c)
956
                    (= Flowchart3_A_du.flowchart3_a_INNER__restart_in Flowchart3_A_du.__Flowchart3_A_du_12_c)
957
                    ))
958
            (or (not (= Flowchart3_A_du.__Flowchart3_A_du_11 true))
959
               (and (= Flowchart3_A_du.flowchart3_a_INNER__state_in POINTFlowchart3_A_INNER)
960
                    (= Flowchart3_A_du.flowchart3_a_INNER__restart_in false)
961
                    ))
962
       )
963
       (and (or (not (= Flowchart3_A_du.flowchart3_a_INNER__state_in FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1))
964
               (and (flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_unless 
965
                    Flowchart3_A_du.flowchart3_a_INNER__restart_in
966
                    Flowchart3_A_du.flowchart3_a_INNER__state_in
967
                    Flowchart3_A_du.__Flowchart3_A_du_1
968
                    Flowchart3_A_du.__Flowchart3_A_du_2)
969
                    (= Flowchart3_A_du.flowchart3_a_INNER__state_act Flowchart3_A_du.__Flowchart3_A_du_2)
970
                    (= Flowchart3_A_du.flowchart3_a_INNER__restart_act Flowchart3_A_du.__Flowchart3_A_du_1)
971
                    ))
972
            (or (not (= Flowchart3_A_du.flowchart3_a_INNER__state_in POINTFlowchart3_A_INNER))
973
               (and (flowchart3_a_INNER__POINTFlowchart3_A_INNER_unless 
974
                    Flowchart3_A_du.flowchart3_a_INNER__restart_in
975
                    Flowchart3_A_du.flowchart3_a_INNER__state_in
976
                    Flowchart3_A_du.__Flowchart3_A_du_3
977
                    Flowchart3_A_du.__Flowchart3_A_du_4)
978
                    (= Flowchart3_A_du.flowchart3_a_INNER__state_act Flowchart3_A_du.__Flowchart3_A_du_4)
979
                    (= Flowchart3_A_du.flowchart3_a_INNER__restart_act Flowchart3_A_du.__Flowchart3_A_du_3)
980
                    ))
981
       )
982
       (and (or (not (= Flowchart3_A_du.flowchart3_a_INNER__state_act FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1))
983
               (and (flowchart3_a_INNER__FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1_handler_until 
984
                    Flowchart3_A_du.x_1
985
                    Flowchart3_A_du.__Flowchart3_A_du_5
986
                    Flowchart3_A_du.__Flowchart3_A_du_6
987
                    Flowchart3_A_du.__Flowchart3_A_du_7)
988
                    (= Flowchart3_A_du.x Flowchart3_A_du.__Flowchart3_A_du_7)
989
                    (= Flowchart3_A_du.flowchart3_a_INNER__next_state_in Flowchart3_A_du.__Flowchart3_A_du_6)
990
                    (= Flowchart3_A_du.flowchart3_a_INNER__next_restart_in Flowchart3_A_du.__Flowchart3_A_du_5)
991
                    ))
992
            (or (not (= Flowchart3_A_du.flowchart3_a_INNER__state_act POINTFlowchart3_A_INNER))
993
               (and (flowchart3_a_INNER__POINTFlowchart3_A_INNER_handler_until 
994
                    Flowchart3_A_du.x_1
995
                    Flowchart3_A_du.__Flowchart3_A_du_8
996
                    Flowchart3_A_du.__Flowchart3_A_du_9
997
                    Flowchart3_A_du.__Flowchart3_A_du_10)
998
                    (= Flowchart3_A_du.x Flowchart3_A_du.__Flowchart3_A_du_10)
999
                    (= Flowchart3_A_du.flowchart3_a_INNER__next_state_in Flowchart3_A_du.__Flowchart3_A_du_9)
1000
                    (= Flowchart3_A_du.flowchart3_a_INNER__next_restart_in Flowchart3_A_du.__Flowchart3_A_du_8)
1001
                    ))
1002
       )
1003
       (= Flowchart3_A_du.__Flowchart3_A_du_13_x Flowchart3_A_du.flowchart3_a_INNER__next_state_in)
1004
       (= Flowchart3_A_du.__Flowchart3_A_du_12_x Flowchart3_A_du.flowchart3_a_INNER__next_restart_in)
1005
       )
1006
  (Flowchart3_A_du_step Flowchart3_A_du.x_1
1007
                        Flowchart3_A_du.x
1008
                        Flowchart3_A_du.__Flowchart3_A_du_12_c
1009
                        Flowchart3_A_du.__Flowchart3_A_du_13_c
1010
                        Flowchart3_A_du.ni_0._arrow._first_c
1011
                        Flowchart3_A_du.__Flowchart3_A_du_12_x
1012
                        Flowchart3_A_du.__Flowchart3_A_du_13_x
1013
                        Flowchart3_A_du.ni_0._arrow._first_x)
1014
))
1015