Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart6 / Flowchart6.smt2 @ eb639349

History | View | Annotate | Download (140 KB)

1
(declare-datatypes () ((flowchart6_a__type POINTFlowchart6_A POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1)));
2

    
3
(declare-datatypes () ((flowchart6_flowchart6__type POINTFlowchart6_Flowchart6 POINT__TO__FLOWCHART6_A_1 FLOWCHART6_A_IDL)));
4

    
5
(declare-datatypes () ((flowchart6_a_INNER__type POINTFlowchart6_A_INNER FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1)));
6

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

    
16
; flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until
17
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_1 Int)
18
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a_INNER__restart_in Bool)
19
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a_INNER__state_in flowchart6_a_INNER__type)
20
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_out Int)
21
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_2 Int)
22
(declare-rel flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until (Int Bool flowchart6_a_INNER__type Int))
23
(rule (=> 
24
  (and (Flowchart6_Flowchart6Junction818__To__Flowchart6_Flowchart6Junction819_1_Condition_Action 
25
       flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_1
26
       flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_2)
27
       (= flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_out flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_2)
28
       (= flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a_INNER__state_in POINTFlowchart6_A_INNER)
29
       (= flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a_INNER__restart_in true)
30
       )
31
  (flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_1 flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a_INNER__restart_in flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a_INNER__state_in flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_out)
32
))
33

    
34
; flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless
35
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__restart_in Bool)
36
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__state_in flowchart6_a_INNER__type)
37
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__restart_act Bool)
38
(declare-var flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__state_act flowchart6_a_INNER__type)
39
(declare-rel flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless (Bool flowchart6_a_INNER__type Bool flowchart6_a_INNER__type))
40
(rule (=> 
41
  (and (= flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__state_act flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__state_in)
42
       (= flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__restart_act flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__restart_in)
43
       )
44
  (flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__restart_in flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__state_in flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__restart_act flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a_INNER__state_act)
45
))
46

    
47
; flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until
48
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.x_1 Int)
49
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.flowchart6_a_INNER__restart_in Bool)
50
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.flowchart6_a_INNER__state_in flowchart6_a_INNER__type)
51
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.x_out Int)
52
(declare-rel flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until (Int Bool flowchart6_a_INNER__type Int))
53
(rule (=> 
54
  (and (= flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.x_out flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.x_1)
55
       (= flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.flowchart6_a_INNER__state_in POINTFlowchart6_A_INNER)
56
       (= flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.flowchart6_a_INNER__restart_in false)
57
       )
58
  (flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.x_1 flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.flowchart6_a_INNER__restart_in flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.flowchart6_a_INNER__state_in flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until.x_out)
59
))
60

    
61
; flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless
62
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__restart_in Bool)
63
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__state_in flowchart6_a_INNER__type)
64
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__restart_act Bool)
65
(declare-var flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__state_act flowchart6_a_INNER__type)
66
(declare-rel flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless (Bool flowchart6_a_INNER__type Bool flowchart6_a_INNER__type))
67
(rule (=> 
68
  (and (= flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__state_act FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1)
69
       (= flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__restart_act true)
70
       )
71
  (flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__restart_in flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__state_in flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__restart_act flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless.flowchart6_a_INNER__state_act)
72
))
73

    
74
; flowchart6_a__POINTFlowchart6_A_handler_until
75
(declare-var flowchart6_a__POINTFlowchart6_A_handler_until.idFlowchart6_A_1 Int)
76
(declare-var flowchart6_a__POINTFlowchart6_A_handler_until.x_1 Int)
77
(declare-var flowchart6_a__POINTFlowchart6_A_handler_until.flowchart6_a__restart_in Bool)
78
(declare-var flowchart6_a__POINTFlowchart6_A_handler_until.flowchart6_a__state_in flowchart6_a__type)
79
(declare-var flowchart6_a__POINTFlowchart6_A_handler_until.idFlowchart6_A_out Int)
80
(declare-var flowchart6_a__POINTFlowchart6_A_handler_until.x_out Int)
81
(declare-rel flowchart6_a__POINTFlowchart6_A_handler_until (Int Int Bool flowchart6_a__type Int Int))
82
(rule (=> 
83
  (and (= flowchart6_a__POINTFlowchart6_A_handler_until.x_out flowchart6_a__POINTFlowchart6_A_handler_until.x_1)
84
       (= flowchart6_a__POINTFlowchart6_A_handler_until.idFlowchart6_A_out flowchart6_a__POINTFlowchart6_A_handler_until.idFlowchart6_A_1)
85
       (= flowchart6_a__POINTFlowchart6_A_handler_until.flowchart6_a__state_in POINTFlowchart6_A)
86
       (= flowchart6_a__POINTFlowchart6_A_handler_until.flowchart6_a__restart_in false)
87
       )
88
  (flowchart6_a__POINTFlowchart6_A_handler_until flowchart6_a__POINTFlowchart6_A_handler_until.idFlowchart6_A_1 flowchart6_a__POINTFlowchart6_A_handler_until.x_1 flowchart6_a__POINTFlowchart6_A_handler_until.flowchart6_a__restart_in flowchart6_a__POINTFlowchart6_A_handler_until.flowchart6_a__state_in flowchart6_a__POINTFlowchart6_A_handler_until.idFlowchart6_A_out flowchart6_a__POINTFlowchart6_A_handler_until.x_out)
89
))
90

    
91
; flowchart6_a__POINTFlowchart6_A_unless
92
(declare-var flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__restart_in Bool)
93
(declare-var flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__state_in flowchart6_a__type)
94
(declare-var flowchart6_a__POINTFlowchart6_A_unless.idFlowchart6_A_1 Int)
95
(declare-var flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__restart_act Bool)
96
(declare-var flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__state_act flowchart6_a__type)
97
(declare-var flowchart6_a__POINTFlowchart6_A_unless.__flowchart6_a__POINTFlowchart6_A_unless_1 Bool)
98
(declare-rel flowchart6_a__POINTFlowchart6_A_unless (Bool flowchart6_a__type Int Bool flowchart6_a__type))
99
(rule (=> 
100
  (and (= flowchart6_a__POINTFlowchart6_A_unless.__flowchart6_a__POINTFlowchart6_A_unless_1 (= flowchart6_a__POINTFlowchart6_A_unless.idFlowchart6_A_1 0))
101
       (and (or (not (= flowchart6_a__POINTFlowchart6_A_unless.__flowchart6_a__POINTFlowchart6_A_unless_1 false))
102
               (and (= flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__state_act flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__state_in)
103
                    (= flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__restart_act flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__restart_in)
104
                    ))
105
            (or (not (= flowchart6_a__POINTFlowchart6_A_unless.__flowchart6_a__POINTFlowchart6_A_unless_1 true))
106
               (and (= flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__state_act POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1)
107
                    (= flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__restart_act true)
108
                    ))
109
       )
110
       )
111
  (flowchart6_a__POINTFlowchart6_A_unless flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__restart_in flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__state_in flowchart6_a__POINTFlowchart6_A_unless.idFlowchart6_A_1 flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__restart_act flowchart6_a__POINTFlowchart6_A_unless.flowchart6_a__state_act)
112
))
113

    
114
; flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until
115
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.idFlowchart6_A_1 Int)
116
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_1 Int)
117
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a__restart_in Bool)
118
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a__state_in flowchart6_a__type)
119
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.idFlowchart6_A_out Int)
120
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_out Int)
121
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_2 Int)
122
(declare-rel flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until (Int Int Bool flowchart6_a__type Int Int))
123
(rule (=> 
124
  (and (Flowchart6_Flowchart6Junction818__To__Flowchart6_Flowchart6Junction819_1_Condition_Action 
125
       flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_1
126
       flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_2)
127
       (= flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_out flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_2)
128
       (= flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.idFlowchart6_A_out flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.idFlowchart6_A_1)
129
       (= flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a__state_in POINTFlowchart6_A)
130
       (= flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a__restart_in true)
131
       )
132
  (flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.idFlowchart6_A_1 flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_1 flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a__restart_in flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.flowchart6_a__state_in flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.idFlowchart6_A_out flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until.x_out)
133
))
134

    
135
; flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless
136
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__restart_in Bool)
137
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__state_in flowchart6_a__type)
138
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__restart_act Bool)
139
(declare-var flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__state_act flowchart6_a__type)
140
(declare-rel flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless (Bool flowchart6_a__type Bool flowchart6_a__type))
141
(rule (=> 
142
  (and (= flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__state_act flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__state_in)
143
       (= flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__restart_act flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__restart_in)
144
       )
145
  (flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__restart_in flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__state_in flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__restart_act flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless.flowchart6_a__state_act)
146
))
147

    
148
; Flowchart6_A_du
149
(declare-var Flowchart6_A_du.x_1 Int)
150
(declare-var Flowchart6_A_du.x Int)
151
(declare-var Flowchart6_A_du.__Flowchart6_A_du_12_c Bool)
152
(declare-var Flowchart6_A_du.__Flowchart6_A_du_13_c flowchart6_a_INNER__type)
153
(declare-var Flowchart6_A_du.ni_9._arrow._first_c Bool)
154
(declare-var Flowchart6_A_du.__Flowchart6_A_du_12_m Bool)
155
(declare-var Flowchart6_A_du.__Flowchart6_A_du_13_m flowchart6_a_INNER__type)
156
(declare-var Flowchart6_A_du.ni_9._arrow._first_m Bool)
157
(declare-var Flowchart6_A_du.__Flowchart6_A_du_12_x Bool)
158
(declare-var Flowchart6_A_du.__Flowchart6_A_du_13_x flowchart6_a_INNER__type)
159
(declare-var Flowchart6_A_du.ni_9._arrow._first_x Bool)
160
(declare-var Flowchart6_A_du.__Flowchart6_A_du_1 Bool)
161
(declare-var Flowchart6_A_du.__Flowchart6_A_du_10 Int)
162
(declare-var Flowchart6_A_du.__Flowchart6_A_du_11 Bool)
163
(declare-var Flowchart6_A_du.__Flowchart6_A_du_2 flowchart6_a_INNER__type)
164
(declare-var Flowchart6_A_du.__Flowchart6_A_du_3 Bool)
165
(declare-var Flowchart6_A_du.__Flowchart6_A_du_4 flowchart6_a_INNER__type)
166
(declare-var Flowchart6_A_du.__Flowchart6_A_du_5 Bool)
167
(declare-var Flowchart6_A_du.__Flowchart6_A_du_6 flowchart6_a_INNER__type)
168
(declare-var Flowchart6_A_du.__Flowchart6_A_du_7 Int)
169
(declare-var Flowchart6_A_du.__Flowchart6_A_du_8 Bool)
170
(declare-var Flowchart6_A_du.__Flowchart6_A_du_9 flowchart6_a_INNER__type)
171
(declare-var Flowchart6_A_du.flowchart6_a_INNER__next_restart_in Bool)
172
(declare-var Flowchart6_A_du.flowchart6_a_INNER__next_state_in flowchart6_a_INNER__type)
173
(declare-var Flowchart6_A_du.flowchart6_a_INNER__restart_act Bool)
174
(declare-var Flowchart6_A_du.flowchart6_a_INNER__restart_in Bool)
175
(declare-var Flowchart6_A_du.flowchart6_a_INNER__state_act flowchart6_a_INNER__type)
176
(declare-var Flowchart6_A_du.flowchart6_a_INNER__state_in flowchart6_a_INNER__type)
177
(declare-rel Flowchart6_A_du_reset (Bool flowchart6_a_INNER__type Bool Bool flowchart6_a_INNER__type Bool))
178
(declare-rel Flowchart6_A_du_step (Int Int Bool flowchart6_a_INNER__type Bool Bool flowchart6_a_INNER__type Bool))
179

    
180
(rule (=> 
181
  (and 
182
       (= Flowchart6_A_du.__Flowchart6_A_du_12_m Flowchart6_A_du.__Flowchart6_A_du_12_c)
183
       (= Flowchart6_A_du.__Flowchart6_A_du_13_m Flowchart6_A_du.__Flowchart6_A_du_13_c)
184
       (= Flowchart6_A_du.ni_9._arrow._first_m true)
185
  )
186
  (Flowchart6_A_du_reset Flowchart6_A_du.__Flowchart6_A_du_12_c
187
                         Flowchart6_A_du.__Flowchart6_A_du_13_c
188
                         Flowchart6_A_du.ni_9._arrow._first_c
189
                         Flowchart6_A_du.__Flowchart6_A_du_12_m
190
                         Flowchart6_A_du.__Flowchart6_A_du_13_m
191
                         Flowchart6_A_du.ni_9._arrow._first_m)
192
))
193

    
194
(rule (=> 
195
  (and (= Flowchart6_A_du.ni_9._arrow._first_m Flowchart6_A_du.ni_9._arrow._first_c)
196
       (and (= Flowchart6_A_du.__Flowchart6_A_du_11 (ite Flowchart6_A_du.ni_9._arrow._first_m true false))
197
            (= Flowchart6_A_du.ni_9._arrow._first_x false))
198
       (and (or (not (= Flowchart6_A_du.__Flowchart6_A_du_11 false))
199
               (and (= Flowchart6_A_du.flowchart6_a_INNER__state_in Flowchart6_A_du.__Flowchart6_A_du_13_c)
200
                    (= Flowchart6_A_du.flowchart6_a_INNER__restart_in Flowchart6_A_du.__Flowchart6_A_du_12_c)
201
                    ))
202
            (or (not (= Flowchart6_A_du.__Flowchart6_A_du_11 true))
203
               (and (= Flowchart6_A_du.flowchart6_a_INNER__state_in POINTFlowchart6_A_INNER)
204
                    (= Flowchart6_A_du.flowchart6_a_INNER__restart_in false)
205
                    ))
206
       )
207
       (and (or (not (= Flowchart6_A_du.flowchart6_a_INNER__state_in FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1))
208
               (and (flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless 
209
                    Flowchart6_A_du.flowchart6_a_INNER__restart_in
210
                    Flowchart6_A_du.flowchart6_a_INNER__state_in
211
                    Flowchart6_A_du.__Flowchart6_A_du_1
212
                    Flowchart6_A_du.__Flowchart6_A_du_2)
213
                    (= Flowchart6_A_du.flowchart6_a_INNER__state_act Flowchart6_A_du.__Flowchart6_A_du_2)
214
                    (= Flowchart6_A_du.flowchart6_a_INNER__restart_act Flowchart6_A_du.__Flowchart6_A_du_1)
215
                    ))
216
            (or (not (= Flowchart6_A_du.flowchart6_a_INNER__state_in POINTFlowchart6_A_INNER))
217
               (and (flowchart6_a_INNER__POINTFlowchart6_A_INNER_unless 
218
                    Flowchart6_A_du.flowchart6_a_INNER__restart_in
219
                    Flowchart6_A_du.flowchart6_a_INNER__state_in
220
                    Flowchart6_A_du.__Flowchart6_A_du_3
221
                    Flowchart6_A_du.__Flowchart6_A_du_4)
222
                    (= Flowchart6_A_du.flowchart6_a_INNER__state_act Flowchart6_A_du.__Flowchart6_A_du_4)
223
                    (= Flowchart6_A_du.flowchart6_a_INNER__restart_act Flowchart6_A_du.__Flowchart6_A_du_3)
224
                    ))
225
       )
226
       (and (or (not (= Flowchart6_A_du.flowchart6_a_INNER__state_act FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1))
227
               (and (flowchart6_a_INNER__FLOWCHART6_A__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until 
228
                    Flowchart6_A_du.x_1
229
                    Flowchart6_A_du.__Flowchart6_A_du_5
230
                    Flowchart6_A_du.__Flowchart6_A_du_6
231
                    Flowchart6_A_du.__Flowchart6_A_du_7)
232
                    (= Flowchart6_A_du.x Flowchart6_A_du.__Flowchart6_A_du_7)
233
                    (= Flowchart6_A_du.flowchart6_a_INNER__next_state_in Flowchart6_A_du.__Flowchart6_A_du_6)
234
                    (= Flowchart6_A_du.flowchart6_a_INNER__next_restart_in Flowchart6_A_du.__Flowchart6_A_du_5)
235
                    ))
236
            (or (not (= Flowchart6_A_du.flowchart6_a_INNER__state_act POINTFlowchart6_A_INNER))
237
               (and (flowchart6_a_INNER__POINTFlowchart6_A_INNER_handler_until 
238
                    Flowchart6_A_du.x_1
239
                    Flowchart6_A_du.__Flowchart6_A_du_8
240
                    Flowchart6_A_du.__Flowchart6_A_du_9
241
                    Flowchart6_A_du.__Flowchart6_A_du_10)
242
                    (= Flowchart6_A_du.x Flowchart6_A_du.__Flowchart6_A_du_10)
243
                    (= Flowchart6_A_du.flowchart6_a_INNER__next_state_in Flowchart6_A_du.__Flowchart6_A_du_9)
244
                    (= Flowchart6_A_du.flowchart6_a_INNER__next_restart_in Flowchart6_A_du.__Flowchart6_A_du_8)
245
                    ))
246
       )
247
       (= Flowchart6_A_du.__Flowchart6_A_du_13_x Flowchart6_A_du.flowchart6_a_INNER__next_state_in)
248
       (= Flowchart6_A_du.__Flowchart6_A_du_12_x Flowchart6_A_du.flowchart6_a_INNER__next_restart_in)
249
       )
250
  (Flowchart6_A_du_step Flowchart6_A_du.x_1
251
                        Flowchart6_A_du.x
252
                        Flowchart6_A_du.__Flowchart6_A_du_12_c
253
                        Flowchart6_A_du.__Flowchart6_A_du_13_c
254
                        Flowchart6_A_du.ni_9._arrow._first_c
255
                        Flowchart6_A_du.__Flowchart6_A_du_12_x
256
                        Flowchart6_A_du.__Flowchart6_A_du_13_x
257
                        Flowchart6_A_du.ni_9._arrow._first_x)
258
))
259

    
260
; Flowchart6_A_node
261
(declare-var Flowchart6_A_node.idFlowchart6_A_1 Int)
262
(declare-var Flowchart6_A_node.x_1 Int)
263
(declare-var Flowchart6_A_node.idFlowchart6_A Int)
264
(declare-var Flowchart6_A_node.x Int)
265
(declare-var Flowchart6_A_node.__Flowchart6_A_node_14_c Bool)
266
(declare-var Flowchart6_A_node.__Flowchart6_A_node_15_c flowchart6_a__type)
267
(declare-var Flowchart6_A_node.ni_8._arrow._first_c Bool)
268
(declare-var Flowchart6_A_node.__Flowchart6_A_node_14_m Bool)
269
(declare-var Flowchart6_A_node.__Flowchart6_A_node_15_m flowchart6_a__type)
270
(declare-var Flowchart6_A_node.ni_8._arrow._first_m Bool)
271
(declare-var Flowchart6_A_node.__Flowchart6_A_node_14_x Bool)
272
(declare-var Flowchart6_A_node.__Flowchart6_A_node_15_x flowchart6_a__type)
273
(declare-var Flowchart6_A_node.ni_8._arrow._first_x Bool)
274
(declare-var Flowchart6_A_node.__Flowchart6_A_node_1 Bool)
275
(declare-var Flowchart6_A_node.__Flowchart6_A_node_10 flowchart6_a__type)
276
(declare-var Flowchart6_A_node.__Flowchart6_A_node_11 Int)
277
(declare-var Flowchart6_A_node.__Flowchart6_A_node_12 Int)
278
(declare-var Flowchart6_A_node.__Flowchart6_A_node_13 Bool)
279
(declare-var Flowchart6_A_node.__Flowchart6_A_node_2 flowchart6_a__type)
280
(declare-var Flowchart6_A_node.__Flowchart6_A_node_3 Bool)
281
(declare-var Flowchart6_A_node.__Flowchart6_A_node_4 flowchart6_a__type)
282
(declare-var Flowchart6_A_node.__Flowchart6_A_node_5 Bool)
283
(declare-var Flowchart6_A_node.__Flowchart6_A_node_6 flowchart6_a__type)
284
(declare-var Flowchart6_A_node.__Flowchart6_A_node_7 Int)
285
(declare-var Flowchart6_A_node.__Flowchart6_A_node_8 Int)
286
(declare-var Flowchart6_A_node.__Flowchart6_A_node_9 Bool)
287
(declare-var Flowchart6_A_node.flowchart6_a__next_restart_in Bool)
288
(declare-var Flowchart6_A_node.flowchart6_a__next_state_in flowchart6_a__type)
289
(declare-var Flowchart6_A_node.flowchart6_a__restart_act Bool)
290
(declare-var Flowchart6_A_node.flowchart6_a__restart_in Bool)
291
(declare-var Flowchart6_A_node.flowchart6_a__state_act flowchart6_a__type)
292
(declare-var Flowchart6_A_node.flowchart6_a__state_in flowchart6_a__type)
293
(declare-rel Flowchart6_A_node_reset (Bool flowchart6_a__type Bool Bool flowchart6_a__type Bool))
294
(declare-rel Flowchart6_A_node_step (Int Int Int Int Bool flowchart6_a__type Bool Bool flowchart6_a__type Bool))
295

    
296
(rule (=> 
297
  (and 
298
       (= Flowchart6_A_node.__Flowchart6_A_node_14_m Flowchart6_A_node.__Flowchart6_A_node_14_c)
299
       (= Flowchart6_A_node.__Flowchart6_A_node_15_m Flowchart6_A_node.__Flowchart6_A_node_15_c)
300
       (= Flowchart6_A_node.ni_8._arrow._first_m true)
301
  )
302
  (Flowchart6_A_node_reset Flowchart6_A_node.__Flowchart6_A_node_14_c
303
                           Flowchart6_A_node.__Flowchart6_A_node_15_c
304
                           Flowchart6_A_node.ni_8._arrow._first_c
305
                           Flowchart6_A_node.__Flowchart6_A_node_14_m
306
                           Flowchart6_A_node.__Flowchart6_A_node_15_m
307
                           Flowchart6_A_node.ni_8._arrow._first_m)
308
))
309

    
310
(rule (=> 
311
  (and (= Flowchart6_A_node.ni_8._arrow._first_m Flowchart6_A_node.ni_8._arrow._first_c)
312
       (and (= Flowchart6_A_node.__Flowchart6_A_node_13 (ite Flowchart6_A_node.ni_8._arrow._first_m true false))
313
            (= Flowchart6_A_node.ni_8._arrow._first_x false))
314
       (and (or (not (= Flowchart6_A_node.__Flowchart6_A_node_13 false))
315
               (and (= Flowchart6_A_node.flowchart6_a__state_in Flowchart6_A_node.__Flowchart6_A_node_15_c)
316
                    (= Flowchart6_A_node.flowchart6_a__restart_in Flowchart6_A_node.__Flowchart6_A_node_14_c)
317
                    ))
318
            (or (not (= Flowchart6_A_node.__Flowchart6_A_node_13 true))
319
               (and (= Flowchart6_A_node.flowchart6_a__state_in POINTFlowchart6_A)
320
                    (= Flowchart6_A_node.flowchart6_a__restart_in false)
321
                    ))
322
       )
323
       (and (or (not (= Flowchart6_A_node.flowchart6_a__state_in POINTFlowchart6_A))
324
               (and (flowchart6_a__POINTFlowchart6_A_unless Flowchart6_A_node.flowchart6_a__restart_in
325
                                                            Flowchart6_A_node.flowchart6_a__state_in
326
                                                            Flowchart6_A_node.idFlowchart6_A_1
327
                                                            Flowchart6_A_node.__Flowchart6_A_node_3
328
                                                            Flowchart6_A_node.__Flowchart6_A_node_4)
329
                    (= Flowchart6_A_node.flowchart6_a__state_act Flowchart6_A_node.__Flowchart6_A_node_4)
330
                    (= Flowchart6_A_node.flowchart6_a__restart_act Flowchart6_A_node.__Flowchart6_A_node_3)
331
                    ))
332
            (or (not (= Flowchart6_A_node.flowchart6_a__state_in POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1))
333
               (and (flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_unless 
334
                    Flowchart6_A_node.flowchart6_a__restart_in
335
                    Flowchart6_A_node.flowchart6_a__state_in
336
                    Flowchart6_A_node.__Flowchart6_A_node_1
337
                    Flowchart6_A_node.__Flowchart6_A_node_2)
338
                    (= Flowchart6_A_node.flowchart6_a__state_act Flowchart6_A_node.__Flowchart6_A_node_2)
339
                    (= Flowchart6_A_node.flowchart6_a__restart_act Flowchart6_A_node.__Flowchart6_A_node_1)
340
                    ))
341
       )
342
       (and (or (not (= Flowchart6_A_node.flowchart6_a__state_act POINTFlowchart6_A))
343
               (and (flowchart6_a__POINTFlowchart6_A_handler_until Flowchart6_A_node.idFlowchart6_A_1
344
                                                                   Flowchart6_A_node.x_1
345
                                                                   Flowchart6_A_node.__Flowchart6_A_node_9
346
                                                                   Flowchart6_A_node.__Flowchart6_A_node_10
347
                                                                   Flowchart6_A_node.__Flowchart6_A_node_11
348
                                                                   Flowchart6_A_node.__Flowchart6_A_node_12)
349
                    (= Flowchart6_A_node.x Flowchart6_A_node.__Flowchart6_A_node_12)
350
                    (= Flowchart6_A_node.idFlowchart6_A Flowchart6_A_node.__Flowchart6_A_node_11)
351
                    (= Flowchart6_A_node.flowchart6_a__next_state_in Flowchart6_A_node.__Flowchart6_A_node_10)
352
                    (= Flowchart6_A_node.flowchart6_a__next_restart_in Flowchart6_A_node.__Flowchart6_A_node_9)
353
                    ))
354
            (or (not (= Flowchart6_A_node.flowchart6_a__state_act POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1))
355
               (and (flowchart6_a__POINT__TO__FLOWCHART6_FLOWCHART6JUNCTION818_1_handler_until 
356
                    Flowchart6_A_node.idFlowchart6_A_1
357
                    Flowchart6_A_node.x_1
358
                    Flowchart6_A_node.__Flowchart6_A_node_5
359
                    Flowchart6_A_node.__Flowchart6_A_node_6
360
                    Flowchart6_A_node.__Flowchart6_A_node_7
361
                    Flowchart6_A_node.__Flowchart6_A_node_8)
362
                    (= Flowchart6_A_node.x Flowchart6_A_node.__Flowchart6_A_node_8)
363
                    (= Flowchart6_A_node.idFlowchart6_A Flowchart6_A_node.__Flowchart6_A_node_7)
364
                    (= Flowchart6_A_node.flowchart6_a__next_state_in Flowchart6_A_node.__Flowchart6_A_node_6)
365
                    (= Flowchart6_A_node.flowchart6_a__next_restart_in Flowchart6_A_node.__Flowchart6_A_node_5)
366
                    ))
367
       )
368
       (= Flowchart6_A_node.__Flowchart6_A_node_15_x Flowchart6_A_node.flowchart6_a__next_state_in)
369
       (= Flowchart6_A_node.__Flowchart6_A_node_14_x Flowchart6_A_node.flowchart6_a__next_restart_in)
370
       )
371
  (Flowchart6_A_node_step Flowchart6_A_node.idFlowchart6_A_1
372
                          Flowchart6_A_node.x_1
373
                          Flowchart6_A_node.idFlowchart6_A
374
                          Flowchart6_A_node.x
375
                          Flowchart6_A_node.__Flowchart6_A_node_14_c
376
                          Flowchart6_A_node.__Flowchart6_A_node_15_c
377
                          Flowchart6_A_node.ni_8._arrow._first_c
378
                          Flowchart6_A_node.__Flowchart6_A_node_14_x
379
                          Flowchart6_A_node.__Flowchart6_A_node_15_x
380
                          Flowchart6_A_node.ni_8._arrow._first_x)
381
))
382

    
383
; Flowchart6_A_en
384
(declare-var Flowchart6_A_en.idFlowchart6_A_1 Int)
385
(declare-var Flowchart6_A_en.idFlowchart6_Flowchart6_1 Int)
386
(declare-var Flowchart6_A_en.x_1 Int)
387
(declare-var Flowchart6_A_en.isInner Bool)
388
(declare-var Flowchart6_A_en.idFlowchart6_A Int)
389
(declare-var Flowchart6_A_en.idFlowchart6_Flowchart6 Int)
390
(declare-var Flowchart6_A_en.x Int)
391
(declare-var Flowchart6_A_en.__Flowchart6_A_en_1 Bool)
392
(declare-var Flowchart6_A_en.idFlowchart6_A_2 Int)
393
(declare-var Flowchart6_A_en.idFlowchart6_A_3 Int)
394
(declare-var Flowchart6_A_en.idFlowchart6_Flowchart6_3 Int)
395
(declare-var Flowchart6_A_en.idFlowchart6_Flowchart6_4 Int)
396
(declare-var Flowchart6_A_en.x_2 Int)
397
(declare-var Flowchart6_A_en.x_3 Int)
398
(declare-var Flowchart6_A_en.x_4 Int)
399
(declare-rel Flowchart6_A_en (Int Int Int Bool Int Int Int))
400
(rule (=> 
401
  (and (Flowchart6_Flowchart6Junction818__To__Flowchart6_Flowchart6Junction819_1_Condition_Action 
402
       Flowchart6_A_en.x_1
403
       Flowchart6_A_en.x_2)
404
       (= Flowchart6_A_en.__Flowchart6_A_en_1 (= Flowchart6_A_en.idFlowchart6_A_1 0))
405
       (and (or (not (= Flowchart6_A_en.__Flowchart6_A_en_1 false))
406
               (and (= Flowchart6_A_en.x_3 Flowchart6_A_en.x_1)
407
                    (= Flowchart6_A_en.idFlowchart6_Flowchart6_3 817)
408
                    (= Flowchart6_A_en.idFlowchart6_A_2 Flowchart6_A_en.idFlowchart6_A_1)
409
                    (= Flowchart6_A_en.x_4 Flowchart6_A_en.x_1)
410
                    (= Flowchart6_A_en.idFlowchart6_Flowchart6_4 817)
411
                    (= Flowchart6_A_en.idFlowchart6_A_3 Flowchart6_A_en.idFlowchart6_A_1)
412
                    ))
413
            (or (not (= Flowchart6_A_en.__Flowchart6_A_en_1 true))
414
               (and (= Flowchart6_A_en.x_3 Flowchart6_A_en.x_2)
415
                    (= Flowchart6_A_en.idFlowchart6_Flowchart6_3 817)
416
                    (= Flowchart6_A_en.idFlowchart6_A_2 Flowchart6_A_en.idFlowchart6_A_1)
417
                    (= Flowchart6_A_en.x_4 Flowchart6_A_en.x_3)
418
                    (= Flowchart6_A_en.idFlowchart6_Flowchart6_4 Flowchart6_A_en.idFlowchart6_Flowchart6_3)
419
                    (= Flowchart6_A_en.idFlowchart6_A_3 Flowchart6_A_en.idFlowchart6_A_2)
420
                    ))
421
       )
422
       (= Flowchart6_A_en.x Flowchart6_A_en.x_4)
423
       (= Flowchart6_A_en.idFlowchart6_Flowchart6 Flowchart6_A_en.idFlowchart6_Flowchart6_4)
424
       (= Flowchart6_A_en.idFlowchart6_A (- 1))
425
       )
426
  (Flowchart6_A_en Flowchart6_A_en.idFlowchart6_A_1 Flowchart6_A_en.idFlowchart6_Flowchart6_1 Flowchart6_A_en.x_1 Flowchart6_A_en.isInner Flowchart6_A_en.idFlowchart6_A Flowchart6_A_en.idFlowchart6_Flowchart6 Flowchart6_A_en.x)
427
))
428

    
429
; flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until
430
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_Flowchart6_1 Int)
431
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_1 Int)
432
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_1 Int)
433
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.flowchart6_flowchart6__restart_in Bool)
434
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.flowchart6_flowchart6__state_in flowchart6_flowchart6__type)
435
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_out Int)
436
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_Flowchart6_out Int)
437
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_out Int)
438
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c Bool)
439
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c flowchart6_a__type)
440
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c Bool)
441
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c Bool)
442
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c flowchart6_a_INNER__type)
443
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c Bool)
444
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Bool)
445
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m flowchart6_a__type)
446
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Bool)
447
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Bool)
448
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m flowchart6_a_INNER__type)
449
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Bool)
450
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x Bool)
451
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x flowchart6_a__type)
452
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x Bool)
453
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x Bool)
454
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x flowchart6_a_INNER__type)
455
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x Bool)
456
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_2 Int)
457
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_2 Int)
458
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_3 Int)
459
(declare-rel flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until_reset (Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool))
460
(declare-rel flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until_step (Int Int Int Bool flowchart6_flowchart6__type Int Int Int Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool))
461

    
462
(rule (=> 
463
  (and 
464
       
465
       (Flowchart6_A_du_reset flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
466
                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
467
                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
468
                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
469
                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
470
                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m)
471
       (Flowchart6_A_node_reset flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
472
                                flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
473
                                flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
474
                                flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
475
                                flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
476
                                flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m)
477
  )
478
  (flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until_reset flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
479
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
480
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
481
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
482
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
483
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
484
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
485
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
486
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
487
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
488
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
489
                                                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m)
490
))
491

    
492
(rule (=> 
493
  (and (and (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c)
494
            (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c)
495
            (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c)
496
            )
497
       (Flowchart6_A_du_step flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_1
498
                             flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_2
499
                             flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
500
                             flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
501
                             flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
502
                             flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
503
                             flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
504
                             flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x)
505
       (and (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c)
506
            (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c)
507
            (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c)
508
            )
509
       (Flowchart6_A_node_step flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_1
510
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_2
511
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_2
512
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_3
513
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
514
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
515
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
516
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
517
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
518
                               flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x)
519
       (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_out flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_3)
520
       (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_Flowchart6_out flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_Flowchart6_1)
521
       (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_out flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_2)
522
       (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.flowchart6_flowchart6__state_in POINTFlowchart6_Flowchart6)
523
       (= flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.flowchart6_flowchart6__restart_in true)
524
       )
525
  (flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until_step flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_Flowchart6_1
526
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_1
527
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_1
528
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.flowchart6_flowchart6__restart_in
529
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.flowchart6_flowchart6__state_in
530
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_A_out
531
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.idFlowchart6_Flowchart6_out
532
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.x_out
533
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
534
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
535
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
536
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
537
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
538
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
539
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
540
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
541
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x
542
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
543
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
544
                                                              flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x)
545
))
546

    
547
; flowchart6_flowchart6__FLOWCHART6_A_IDL_unless
548
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__restart_in Bool)
549
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__state_in flowchart6_flowchart6__type)
550
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__restart_act Bool)
551
(declare-var flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__state_act flowchart6_flowchart6__type)
552
(declare-rel flowchart6_flowchart6__FLOWCHART6_A_IDL_unless (Bool flowchart6_flowchart6__type Bool flowchart6_flowchart6__type))
553
(rule (=> 
554
  (and (= flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__state_act flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__state_in)
555
       (= flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__restart_act flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__restart_in)
556
       )
557
  (flowchart6_flowchart6__FLOWCHART6_A_IDL_unless flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__restart_in flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__state_in flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__restart_act flowchart6_flowchart6__FLOWCHART6_A_IDL_unless.flowchart6_flowchart6__state_act)
558
))
559

    
560
; flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until
561
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_Flowchart6_1 Int)
562
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_A_1 Int)
563
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.x_1 Int)
564
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.flowchart6_flowchart6__restart_in Bool)
565
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.flowchart6_flowchart6__state_in flowchart6_flowchart6__type)
566
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_A_out Int)
567
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_Flowchart6_out Int)
568
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.x_out Int)
569
(declare-rel flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until (Int Int Int Bool flowchart6_flowchart6__type Int Int Int))
570
(rule (=> 
571
  (and (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.x_out flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.x_1)
572
       (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_Flowchart6_out flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_Flowchart6_1)
573
       (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_A_out flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_A_1)
574
       (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.flowchart6_flowchart6__state_in POINTFlowchart6_Flowchart6)
575
       (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.flowchart6_flowchart6__restart_in false)
576
       )
577
  (flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_Flowchart6_1 flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_A_1 flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.x_1 flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.flowchart6_flowchart6__restart_in flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.flowchart6_flowchart6__state_in flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_A_out flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.idFlowchart6_Flowchart6_out flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until.x_out)
578
))
579

    
580
; flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless
581
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_in Bool)
582
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_in flowchart6_flowchart6__type)
583
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.idFlowchart6_Flowchart6_1 Int)
584
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_act Bool)
585
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_act flowchart6_flowchart6__type)
586
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_1 Bool)
587
(declare-var flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_2 Bool)
588
(declare-rel flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless (Bool flowchart6_flowchart6__type Int Bool flowchart6_flowchart6__type))
589
(rule (=> 
590
  (and (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_2 (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.idFlowchart6_Flowchart6_1 817))
591
       (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_1 (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.idFlowchart6_Flowchart6_1 0))
592
       (and (or (not (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_1 false))
593
               (and (or (not (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_2 false))
594
                       (and (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_act flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_in)
595
                            (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_act flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_in)
596
                            ))
597
                    (or (not (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_2 true))
598
                       (and (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_act FLOWCHART6_A_IDL)
599
                            (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_act true)
600
                            ))
601
               ))
602
            (or (not (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.__flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless_1 true))
603
               (and (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_act POINT__TO__FLOWCHART6_A_1)
604
                    (= flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_act true)
605
                    ))
606
       )
607
       )
608
  (flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_in flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_in flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.idFlowchart6_Flowchart6_1 flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__restart_act flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless.flowchart6_flowchart6__state_act)
609
))
610

    
611
; flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until
612
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_1 Int)
613
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_1 Int)
614
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_1 Int)
615
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.flowchart6_flowchart6__restart_in Bool)
616
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.flowchart6_flowchart6__state_in flowchart6_flowchart6__type)
617
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_out Int)
618
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_out Int)
619
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_out Int)
620
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_2 Int)
621
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_2 Int)
622
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_2 Int)
623
(declare-rel flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until (Int Int Int Bool flowchart6_flowchart6__type Int Int Int))
624
(rule (=> 
625
  (and (Flowchart6_A_en flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_1
626
                        flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_1
627
                        flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_1
628
                        false
629
                        flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_2
630
                        flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_2
631
                        flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_2)
632
       (= flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_out flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_2)
633
       (= flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_out flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_2)
634
       (= flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_out flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_2)
635
       (= flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.flowchart6_flowchart6__state_in POINTFlowchart6_Flowchart6)
636
       (= flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.flowchart6_flowchart6__restart_in true)
637
       )
638
  (flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_1 flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_1 flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_1 flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.flowchart6_flowchart6__restart_in flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.flowchart6_flowchart6__state_in flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_A_out flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.idFlowchart6_Flowchart6_out flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until.x_out)
639
))
640

    
641
; flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless
642
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__restart_in Bool)
643
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__state_in flowchart6_flowchart6__type)
644
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__restart_act Bool)
645
(declare-var flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__state_act flowchart6_flowchart6__type)
646
(declare-rel flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless (Bool flowchart6_flowchart6__type Bool flowchart6_flowchart6__type))
647
(rule (=> 
648
  (and (= flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__state_act flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__state_in)
649
       (= flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__restart_act flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__restart_in)
650
       )
651
  (flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__restart_in flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__state_in flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__restart_act flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless.flowchart6_flowchart6__state_act)
652
))
653

    
654
; Flowchart6_Flowchart6_node
655
(declare-var Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6_1 Int)
656
(declare-var Flowchart6_Flowchart6_node.idFlowchart6_A_1 Int)
657
(declare-var Flowchart6_Flowchart6_node.x_1 Int)
658
(declare-var Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6 Int)
659
(declare-var Flowchart6_Flowchart6_node.idFlowchart6_A Int)
660
(declare-var Flowchart6_Flowchart6_node.x Int)
661
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c Bool)
662
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c flowchart6_flowchart6__type)
663
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c Bool)
664
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c flowchart6_a__type)
665
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c Bool)
666
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c Bool)
667
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c flowchart6_a_INNER__type)
668
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c Bool)
669
(declare-var Flowchart6_Flowchart6_node.ni_5._arrow._first_c Bool)
670
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m Bool)
671
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m flowchart6_flowchart6__type)
672
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Bool)
673
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m flowchart6_a__type)
674
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Bool)
675
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Bool)
676
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m flowchart6_a_INNER__type)
677
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Bool)
678
(declare-var Flowchart6_Flowchart6_node.ni_5._arrow._first_m Bool)
679
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x Bool)
680
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x flowchart6_flowchart6__type)
681
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x Bool)
682
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x flowchart6_a__type)
683
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x Bool)
684
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x Bool)
685
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x flowchart6_a_INNER__type)
686
(declare-var Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x Bool)
687
(declare-var Flowchart6_Flowchart6_node.ni_5._arrow._first_x Bool)
688
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_1 Bool)
689
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_10 Int)
690
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_11 Int)
691
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_12 Bool)
692
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_13 flowchart6_flowchart6__type)
693
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_14 Int)
694
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_15 Int)
695
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_16 Int)
696
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_17 Bool)
697
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_18 flowchart6_flowchart6__type)
698
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_19 Int)
699
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_2 flowchart6_flowchart6__type)
700
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_20 Int)
701
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_21 Int)
702
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_22 Bool)
703
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_3 Bool)
704
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_4 flowchart6_flowchart6__type)
705
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_5 Bool)
706
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_6 flowchart6_flowchart6__type)
707
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_7 Bool)
708
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_8 flowchart6_flowchart6__type)
709
(declare-var Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_9 Int)
710
(declare-var Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_restart_in Bool)
711
(declare-var Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_state_in flowchart6_flowchart6__type)
712
(declare-var Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_act Bool)
713
(declare-var Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_in Bool)
714
(declare-var Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_act flowchart6_flowchart6__type)
715
(declare-var Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in flowchart6_flowchart6__type)
716
(declare-rel Flowchart6_Flowchart6_node_reset (Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool))
717
(declare-rel Flowchart6_Flowchart6_node_step (Int Int Int Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool))
718

    
719
(rule (=> 
720
  (and 
721
       (= Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c)
722
       (= Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c)
723
       (= Flowchart6_Flowchart6_node.ni_5._arrow._first_m true)
724
       (flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until_reset Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
725
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
726
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
727
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
728
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
729
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
730
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
731
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
732
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
733
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
734
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
735
                                                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m)
736
  )
737
  (Flowchart6_Flowchart6_node_reset Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
738
                                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
739
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
740
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
741
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
742
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
743
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
744
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
745
                                    Flowchart6_Flowchart6_node.ni_5._arrow._first_c
746
                                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m
747
                                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m
748
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
749
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
750
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
751
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
752
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
753
                                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
754
                                    Flowchart6_Flowchart6_node.ni_5._arrow._first_m)
755
))
756

    
757
(rule (=> 
758
  (and (= Flowchart6_Flowchart6_node.ni_5._arrow._first_m Flowchart6_Flowchart6_node.ni_5._arrow._first_c)
759
       (and (= Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_22 (ite Flowchart6_Flowchart6_node.ni_5._arrow._first_m true false))
760
            (= Flowchart6_Flowchart6_node.ni_5._arrow._first_x false))
761
       (and (or (not (= Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_22 false))
762
               (and (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c)
763
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c)
764
                    ))
765
            (or (not (= Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_22 true))
766
               (and (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in POINTFlowchart6_Flowchart6)
767
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_in false)
768
                    ))
769
       )
770
       (and (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in FLOWCHART6_A_IDL))
771
               (and (flowchart6_flowchart6__FLOWCHART6_A_IDL_unless Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_in
772
                                                                    Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in
773
                                                                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_1
774
                                                                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_2)
775
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_act Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_2)
776
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_act Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_1)
777
                    ))
778
            (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in POINTFlowchart6_Flowchart6))
779
               (and (flowchart6_flowchart6__POINTFlowchart6_Flowchart6_unless 
780
                    Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_in
781
                    Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in
782
                    Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6_1
783
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_5
784
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_6)
785
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_act Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_6)
786
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_act Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_5)
787
                    ))
788
            (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in POINT__TO__FLOWCHART6_A_1))
789
               (and (flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_unless 
790
                    Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_in
791
                    Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_in
792
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_3
793
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_4)
794
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_act Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_4)
795
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_act Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_3)
796
                    ))
797
       )
798
       (and (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_act FLOWCHART6_A_IDL))
799
               (and (and (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_act true))
800
                            (flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until_reset 
801
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
802
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
803
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
804
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
805
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
806
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
807
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
808
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
809
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
810
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
811
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
812
                            Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m))
813
                         (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__restart_act false))
814
                            (and (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c)
815
                                 (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c)
816
                                 (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c)
817
                                 (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c)
818
                                 (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c)
819
                                 (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c)
820
                                 )
821
                            )
822
                    )
823
                    (and (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c)
824
                         (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c)
825
                         (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c)
826
                         (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c)
827
                         (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c)
828
                         (= Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c)
829
                         )
830
                    (flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until_step 
831
                    Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6_1
832
                    Flowchart6_Flowchart6_node.idFlowchart6_A_1
833
                    Flowchart6_Flowchart6_node.x_1
834
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_7
835
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_8
836
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_9
837
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_10
838
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_11
839
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
840
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
841
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
842
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
843
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
844
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
845
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
846
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
847
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x
848
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
849
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
850
                    Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x)
851
                    (= Flowchart6_Flowchart6_node.x Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_11)
852
                    (= Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6 Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_10)
853
                    (= Flowchart6_Flowchart6_node.idFlowchart6_A Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_9)
854
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_state_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_8)
855
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_restart_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_7)
856
                    ))
857
            (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_act POINTFlowchart6_Flowchart6))
858
               (and (flowchart6_flowchart6__POINTFlowchart6_Flowchart6_handler_until 
859
                    Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6_1
860
                    Flowchart6_Flowchart6_node.idFlowchart6_A_1
861
                    Flowchart6_Flowchart6_node.x_1
862
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_17
863
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_18
864
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_19
865
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_20
866
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_21)
867
                    (= Flowchart6_Flowchart6_node.x Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_21)
868
                    (= Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6 Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_20)
869
                    (= Flowchart6_Flowchart6_node.idFlowchart6_A Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_19)
870
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_state_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_18)
871
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_restart_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_17)
872
                    ))
873
            (or (not (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__state_act POINT__TO__FLOWCHART6_A_1))
874
               (and (flowchart6_flowchart6__POINT__TO__FLOWCHART6_A_1_handler_until 
875
                    Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6_1
876
                    Flowchart6_Flowchart6_node.idFlowchart6_A_1
877
                    Flowchart6_Flowchart6_node.x_1
878
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_12
879
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_13
880
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_14
881
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_15
882
                    Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_16)
883
                    (= Flowchart6_Flowchart6_node.x Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_16)
884
                    (= Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6 Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_15)
885
                    (= Flowchart6_Flowchart6_node.idFlowchart6_A Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_14)
886
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_state_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_13)
887
                    (= Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_restart_in Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_12)
888
                    ))
889
       )
890
       (= Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_state_in)
891
       (= Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x Flowchart6_Flowchart6_node.flowchart6_flowchart6__next_restart_in)
892
       )
893
  (Flowchart6_Flowchart6_node_step Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6_1
894
                                   Flowchart6_Flowchart6_node.idFlowchart6_A_1
895
                                   Flowchart6_Flowchart6_node.x_1
896
                                   Flowchart6_Flowchart6_node.idFlowchart6_Flowchart6
897
                                   Flowchart6_Flowchart6_node.idFlowchart6_A
898
                                   Flowchart6_Flowchart6_node.x
899
                                   Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
900
                                   Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
901
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
902
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
903
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
904
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
905
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
906
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
907
                                   Flowchart6_Flowchart6_node.ni_5._arrow._first_c
908
                                   Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x
909
                                   Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x
910
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
911
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
912
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x
913
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
914
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
915
                                   Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x
916
                                   Flowchart6_Flowchart6_node.ni_5._arrow._first_x)
917
))
918

    
919
; Flowchart6_Flowchart6
920
(declare-var Flowchart6_Flowchart6.noInput Bool)
921
(declare-var Flowchart6_Flowchart6.x Int)
922
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c Int)
923
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c Int)
924
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c Int)
925
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c Bool)
926
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c flowchart6_flowchart6__type)
927
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c Bool)
928
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c flowchart6_a__type)
929
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c Bool)
930
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c Bool)
931
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c flowchart6_a_INNER__type)
932
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c Bool)
933
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c Bool)
934
(declare-var Flowchart6_Flowchart6.ni_3._arrow._first_c Bool)
935
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m Int)
936
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m Int)
937
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m Int)
938
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m Bool)
939
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m flowchart6_flowchart6__type)
940
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Bool)
941
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m flowchart6_a__type)
942
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Bool)
943
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Bool)
944
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m flowchart6_a_INNER__type)
945
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Bool)
946
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m Bool)
947
(declare-var Flowchart6_Flowchart6.ni_3._arrow._first_m Bool)
948
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_x Int)
949
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_x Int)
950
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_x Int)
951
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x Bool)
952
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x flowchart6_flowchart6__type)
953
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x Bool)
954
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x flowchart6_a__type)
955
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x Bool)
956
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x Bool)
957
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x flowchart6_a_INNER__type)
958
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x Bool)
959
(declare-var Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_x Bool)
960
(declare-var Flowchart6_Flowchart6.ni_3._arrow._first_x Bool)
961
(declare-var Flowchart6_Flowchart6.__Flowchart6_Flowchart6_1 Bool)
962
(declare-var Flowchart6_Flowchart6.idFlowchart6_A Int)
963
(declare-var Flowchart6_Flowchart6.idFlowchart6_A_1 Int)
964
(declare-var Flowchart6_Flowchart6.idFlowchart6_Flowchart6 Int)
965
(declare-var Flowchart6_Flowchart6.idFlowchart6_Flowchart6_1 Int)
966
(declare-var Flowchart6_Flowchart6.x_1 Int)
967
(declare-rel Flowchart6_Flowchart6_reset (Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool))
968
(declare-rel Flowchart6_Flowchart6_step (Bool Int Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool))
969

    
970
(rule (=> 
971
  (and 
972
       (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c)
973
       (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c)
974
       (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c)
975
       (= Flowchart6_Flowchart6.ni_3._arrow._first_m true)
976
       (Flowchart6_Flowchart6_node_reset Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
977
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
978
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
979
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
980
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
981
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
982
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
983
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
984
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c
985
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m
986
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m
987
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
988
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
989
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
990
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
991
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
992
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
993
                                         Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m)
994
  )
995
  (Flowchart6_Flowchart6_reset Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c
996
                               Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c
997
                               Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c
998
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
999
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
1000
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
1001
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
1002
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
1003
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
1004
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
1005
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
1006
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c
1007
                               Flowchart6_Flowchart6.ni_3._arrow._first_c
1008
                               Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m
1009
                               Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m
1010
                               Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m
1011
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m
1012
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m
1013
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
1014
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
1015
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
1016
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
1017
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
1018
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
1019
                               Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m
1020
                               Flowchart6_Flowchart6.ni_3._arrow._first_m)
1021
))
1022

    
1023
(rule (=> 
1024
  (and (= Flowchart6_Flowchart6.ni_3._arrow._first_m Flowchart6_Flowchart6.ni_3._arrow._first_c)
1025
       (and (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_1 (ite Flowchart6_Flowchart6.ni_3._arrow._first_m true false))
1026
            (= Flowchart6_Flowchart6.ni_3._arrow._first_x false))
1027
       (and (or (not (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_1 false))
1028
               (and (= Flowchart6_Flowchart6.x_1 Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c)
1029
                    (= Flowchart6_Flowchart6.idFlowchart6_Flowchart6_1 Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c)
1030
                    (= Flowchart6_Flowchart6.idFlowchart6_A_1 Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c)
1031
                    ))
1032
            (or (not (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_1 true))
1033
               (and (= Flowchart6_Flowchart6.x_1 0)
1034
                    (= Flowchart6_Flowchart6.idFlowchart6_Flowchart6_1 0)
1035
                    (= Flowchart6_Flowchart6.idFlowchart6_A_1 0)
1036
                    ))
1037
       )
1038
       (and (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c)
1039
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c)
1040
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c)
1041
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c)
1042
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c)
1043
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c)
1044
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c)
1045
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c)
1046
            (= Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c)
1047
            )
1048
       (Flowchart6_Flowchart6_node_step Flowchart6_Flowchart6.idFlowchart6_Flowchart6_1
1049
                                        Flowchart6_Flowchart6.idFlowchart6_A_1
1050
                                        Flowchart6_Flowchart6.x_1
1051
                                        Flowchart6_Flowchart6.idFlowchart6_Flowchart6
1052
                                        Flowchart6_Flowchart6.idFlowchart6_A
1053
                                        Flowchart6_Flowchart6.x
1054
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m
1055
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m
1056
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
1057
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
1058
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
1059
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
1060
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
1061
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
1062
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m
1063
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x
1064
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x
1065
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
1066
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
1067
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x
1068
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
1069
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
1070
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x
1071
                                        Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_x)
1072
       (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_x Flowchart6_Flowchart6.x)
1073
       (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_x Flowchart6_Flowchart6.idFlowchart6_Flowchart6)
1074
       (= Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_x Flowchart6_Flowchart6.idFlowchart6_A)
1075
       )
1076
  (Flowchart6_Flowchart6_step Flowchart6_Flowchart6.noInput
1077
                              Flowchart6_Flowchart6.x
1078
                              Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c
1079
                              Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c
1080
                              Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c
1081
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
1082
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
1083
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
1084
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
1085
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
1086
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
1087
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
1088
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
1089
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c
1090
                              Flowchart6_Flowchart6.ni_3._arrow._first_c
1091
                              Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_x
1092
                              Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_x
1093
                              Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_x
1094
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x
1095
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x
1096
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
1097
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
1098
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x
1099
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
1100
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
1101
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x
1102
                              Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_x
1103
                              Flowchart6_Flowchart6.ni_3._arrow._first_x)
1104
))
1105

    
1106
; Flowchart6_A_ex
1107
(declare-var Flowchart6_A_ex.idFlowchart6_Flowchart6_1 Int)
1108
(declare-var Flowchart6_A_ex.isInner Bool)
1109
(declare-var Flowchart6_A_ex.idFlowchart6_Flowchart6 Int)
1110
(declare-var Flowchart6_A_ex.idFlowchart6_Flowchart6_2 Int)
1111
(declare-rel Flowchart6_A_ex (Int Bool Int))
1112
(rule (=> 
1113
  (and (and (or (not (= (not Flowchart6_A_ex.isInner) true))
1114
               (= Flowchart6_A_ex.idFlowchart6_Flowchart6_2 0))
1115
            (or (not (= (not Flowchart6_A_ex.isInner) false))
1116
               (= Flowchart6_A_ex.idFlowchart6_Flowchart6_2 Flowchart6_A_ex.idFlowchart6_Flowchart6_1))
1117
       )
1118
       (= Flowchart6_A_ex.idFlowchart6_Flowchart6 Flowchart6_A_ex.idFlowchart6_Flowchart6_1)
1119
       )
1120
  (Flowchart6_A_ex Flowchart6_A_ex.idFlowchart6_Flowchart6_1 Flowchart6_A_ex.isInner Flowchart6_A_ex.idFlowchart6_Flowchart6)
1121
))
1122

    
1123
; Flowchart6
1124
(declare-var Flowchart6.i_virtual Real)
1125
(declare-var Flowchart6.Out1_1_1 Int)
1126
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c Int)
1127
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c Int)
1128
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c Int)
1129
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c Bool)
1130
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c flowchart6_flowchart6__type)
1131
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c Bool)
1132
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c flowchart6_a__type)
1133
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c Bool)
1134
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c Bool)
1135
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c flowchart6_a_INNER__type)
1136
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c Bool)
1137
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c Bool)
1138
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_c Bool)
1139
(declare-var Flowchart6.ni_1._arrow._first_c Bool)
1140
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m Int)
1141
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m Int)
1142
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m Int)
1143
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m Bool)
1144
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m flowchart6_flowchart6__type)
1145
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Bool)
1146
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m flowchart6_a__type)
1147
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Bool)
1148
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Bool)
1149
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m flowchart6_a_INNER__type)
1150
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Bool)
1151
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m Bool)
1152
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_m Bool)
1153
(declare-var Flowchart6.ni_1._arrow._first_m Bool)
1154
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_x Int)
1155
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_x Int)
1156
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_x Int)
1157
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x Bool)
1158
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x flowchart6_flowchart6__type)
1159
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x Bool)
1160
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x flowchart6_a__type)
1161
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x Bool)
1162
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x Bool)
1163
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x flowchart6_a_INNER__type)
1164
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x Bool)
1165
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_x Bool)
1166
(declare-var Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_x Bool)
1167
(declare-var Flowchart6.ni_1._arrow._first_x Bool)
1168
(declare-var Flowchart6.Flowchart6_1_1 Int)
1169
(declare-var Flowchart6.__Flowchart6_1 Bool)
1170
(declare-var Flowchart6.i_virtual_local Real)
1171
(declare-rel Flowchart6_reset (Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool Bool Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool Bool))
1172
(declare-rel Flowchart6_step (Real Int Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool Bool Int Int Int Bool flowchart6_flowchart6__type Bool flowchart6_a__type Bool Bool flowchart6_a_INNER__type Bool Bool Bool Bool))
1173

    
1174
(rule (=> 
1175
  (and 
1176
       
1177
       (= Flowchart6.ni_1._arrow._first_m true)
1178
       (Flowchart6_Flowchart6_reset Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c
1179
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c
1180
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c
1181
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
1182
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
1183
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
1184
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
1185
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
1186
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
1187
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
1188
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
1189
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c
1190
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_c
1191
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m
1192
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m
1193
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m
1194
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m
1195
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m
1196
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
1197
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
1198
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
1199
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
1200
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
1201
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
1202
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m
1203
                                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_m)
1204
  )
1205
  (Flowchart6_reset Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c
1206
                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c
1207
                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c
1208
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
1209
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
1210
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
1211
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
1212
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
1213
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
1214
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
1215
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
1216
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c
1217
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_c
1218
                    Flowchart6.ni_1._arrow._first_c
1219
                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m
1220
                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m
1221
                    Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m
1222
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m
1223
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m
1224
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
1225
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
1226
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
1227
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
1228
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
1229
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
1230
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m
1231
                    Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_m
1232
                    Flowchart6.ni_1._arrow._first_m)
1233
))
1234

    
1235
(rule (=> 
1236
  (and (= Flowchart6.ni_1._arrow._first_m Flowchart6.ni_1._arrow._first_c)
1237
       (and (= Flowchart6.__Flowchart6_1 (ite Flowchart6.ni_1._arrow._first_m true false))
1238
            (= Flowchart6.ni_1._arrow._first_x false))
1239
       (and (or (not (= Flowchart6.__Flowchart6_1 true))
1240
               (= Flowchart6.i_virtual_local 0.))
1241
            (or (not (= Flowchart6.__Flowchart6_1 false))
1242
               (= Flowchart6.i_virtual_local 1.))
1243
       )
1244
       (and (= Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c)
1245
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c)
1246
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c)
1247
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c)
1248
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c)
1249
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c)
1250
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c)
1251
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c)
1252
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c)
1253
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c)
1254
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c)
1255
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c)
1256
            (= Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_m Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_c)
1257
            )
1258
       (Flowchart6_Flowchart6_step true
1259
                                   Flowchart6.Flowchart6_1_1
1260
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_m
1261
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_m
1262
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_m
1263
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_m
1264
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_m
1265
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_m
1266
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_m
1267
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_m
1268
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_m
1269
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_m
1270
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_m
1271
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_m
1272
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_m
1273
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_x
1274
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_x
1275
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_x
1276
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x
1277
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x
1278
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
1279
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
1280
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x
1281
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
1282
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
1283
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x
1284
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_x
1285
                                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_x)
1286
       (= Flowchart6.Out1_1_1 Flowchart6.Flowchart6_1_1)
1287
       )
1288
  (Flowchart6_step Flowchart6.i_virtual
1289
                   Flowchart6.Out1_1_1
1290
                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_c
1291
                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_c
1292
                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_c
1293
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_c
1294
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_c
1295
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_c
1296
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_c
1297
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_c
1298
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_c
1299
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_c
1300
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_c
1301
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_c
1302
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_c
1303
                   Flowchart6.ni_1._arrow._first_c
1304
                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_2_x
1305
                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_3_x
1306
                   Flowchart6.ni_0.Flowchart6_Flowchart6.__Flowchart6_Flowchart6_4_x
1307
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_23_x
1308
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.__Flowchart6_Flowchart6_node_24_x
1309
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_14_x
1310
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.__Flowchart6_A_node_15_x
1311
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_6.Flowchart6_A_node.ni_8._arrow._first_x
1312
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_12_x
1313
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.__Flowchart6_A_du_13_x
1314
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_4.flowchart6_flowchart6__FLOWCHART6_A_IDL_handler_until.ni_7.Flowchart6_A_du.ni_9._arrow._first_x
1315
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_2.Flowchart6_Flowchart6_node.ni_5._arrow._first_x
1316
                   Flowchart6.ni_0.Flowchart6_Flowchart6.ni_3._arrow._first_x
1317
                   Flowchart6.ni_1._arrow._first_x)
1318
))
1319