Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Super2 / Super2.smt2 @ eb639349

History | View | Annotate | Download (188 KB)

1
(declare-datatypes () ((super2_super2__type POINTSuper2_Super2 POINT__TO__SUPER2_A_1 SUPER2_A__TO__SUPER2_C_1 SUPER2_A__TO__C_C1_2 SUPER2_B__TO__SUPER2_A_1 SUPER2_C__TO__SUPER2_B_1 SUPER2_A_IDL SUPER2_B_IDL SUPER2_C_IDL)));
2

    
3
(declare-datatypes () ((super2_c__type POINTSuper2_C POINT__TO__C_C1_1 C_C1__TO__SUPER2_B_1 C_C1_IDL)));
4

    
5
; C_C1_ex
6
(declare-var C_C1_ex.idSuper2_C_1 Int)
7
(declare-var C_C1_ex.isInner Bool)
8
(declare-var C_C1_ex.idSuper2_C Int)
9
(declare-var C_C1_ex.idSuper2_C_2 Int)
10
(declare-rel C_C1_ex (Int Bool Int))
11
(rule (=> 
12
  (and (and (or (not (= (not C_C1_ex.isInner) true))
13
               (= C_C1_ex.idSuper2_C_2 0))
14
            (or (not (= (not C_C1_ex.isInner) false))
15
               (= C_C1_ex.idSuper2_C_2 C_C1_ex.idSuper2_C_1))
16
       )
17
       (= C_C1_ex.idSuper2_C C_C1_ex.idSuper2_C_1)
18
       )
19
  (C_C1_ex C_C1_ex.idSuper2_C_1 C_C1_ex.isInner C_C1_ex.idSuper2_C)
20
))
21

    
22
; Super2_B_en
23
(declare-var Super2_B_en.idSuper2_Super2_1 Int)
24
(declare-var Super2_B_en.s_1 Real)
25
(declare-var Super2_B_en.isInner Bool)
26
(declare-var Super2_B_en.idSuper2_Super2 Int)
27
(declare-var Super2_B_en.s Real)
28
(declare-var Super2_B_en.s_2 Real)
29
(declare-rel Super2_B_en (Int Real Bool Int Real))
30
(rule (=> 
31
  (and (and (or (not (= (not Super2_B_en.isInner) true))
32
               (= Super2_B_en.s_2 3.))
33
            (or (not (= (not Super2_B_en.isInner) false))
34
               (= Super2_B_en.s_2 Super2_B_en.s_1))
35
       )
36
       (= Super2_B_en.s Super2_B_en.s_2)
37
       (= Super2_B_en.idSuper2_Super2 1951)
38
       )
39
  (Super2_B_en Super2_B_en.idSuper2_Super2_1 Super2_B_en.s_1 Super2_B_en.isInner Super2_B_en.idSuper2_Super2 Super2_B_en.s)
40
))
41

    
42
; Super2_C_ex
43
(declare-var Super2_C_ex.idSuper2_C_1 Int)
44
(declare-var Super2_C_ex.idSuper2_Super2_1 Int)
45
(declare-var Super2_C_ex.isInner Bool)
46
(declare-var Super2_C_ex.idSuper2_C Int)
47
(declare-var Super2_C_ex.idSuper2_Super2 Int)
48
(declare-var Super2_C_ex.__Super2_C_ex_2 Bool)
49
(declare-var Super2_C_ex.__Super2_C_ex_3 Int)
50
(declare-var Super2_C_ex.idSuper2_C_2 Int)
51
(declare-var Super2_C_ex.idSuper2_C_3 Int)
52
(declare-var Super2_C_ex.idSuper2_Super2_2 Int)
53
(declare-rel Super2_C_ex (Int Int Bool Int Int))
54
(rule (=> 
55
  (and (and (or (not (= (not Super2_C_ex.isInner) true))
56
               (= Super2_C_ex.idSuper2_Super2_2 0))
57
            (or (not (= (not Super2_C_ex.isInner) false))
58
               (= Super2_C_ex.idSuper2_Super2_2 Super2_C_ex.idSuper2_Super2_1))
59
       )
60
       (C_C1_ex Super2_C_ex.idSuper2_C_1
61
                false
62
                Super2_C_ex.__Super2_C_ex_3)
63
       (= Super2_C_ex.__Super2_C_ex_2 (= Super2_C_ex.idSuper2_C_1 1952))
64
       (and (or (not (= Super2_C_ex.__Super2_C_ex_2 false))
65
               (and (= Super2_C_ex.idSuper2_C_2 Super2_C_ex.idSuper2_C_1)
66
                    (= Super2_C_ex.idSuper2_C_3 Super2_C_ex.idSuper2_C_1)
67
                    ))
68
            (or (not (= Super2_C_ex.__Super2_C_ex_2 true))
69
               (and (= Super2_C_ex.idSuper2_C_2 Super2_C_ex.__Super2_C_ex_3)
70
                    (= Super2_C_ex.idSuper2_C_3 Super2_C_ex.idSuper2_C_2)
71
                    ))
72
       )
73
       (= Super2_C_ex.idSuper2_Super2 Super2_C_ex.idSuper2_Super2_1)
74
       (= Super2_C_ex.idSuper2_C 0)
75
       )
76
  (Super2_C_ex Super2_C_ex.idSuper2_C_1 Super2_C_ex.idSuper2_Super2_1 Super2_C_ex.isInner Super2_C_ex.idSuper2_C Super2_C_ex.idSuper2_Super2)
77
))
78

    
79
; C_C1_en
80
(declare-var C_C1_en.idSuper2_C_1 Int)
81
(declare-var C_C1_en.s_1 Real)
82
(declare-var C_C1_en.isInner Bool)
83
(declare-var C_C1_en.idSuper2_C Int)
84
(declare-var C_C1_en.s Real)
85
(declare-var C_C1_en.s_2 Real)
86
(declare-rel C_C1_en (Int Real Bool Int Real))
87
(rule (=> 
88
  (and (and (or (not (= (not C_C1_en.isInner) true))
89
               (= C_C1_en.s_2 2.))
90
            (or (not (= (not C_C1_en.isInner) false))
91
               (= C_C1_en.s_2 C_C1_en.s_1))
92
       )
93
       (= C_C1_en.s C_C1_en.s_2)
94
       (= C_C1_en.idSuper2_C 1952)
95
       )
96
  (C_C1_en C_C1_en.idSuper2_C_1 C_C1_en.s_1 C_C1_en.isInner C_C1_en.idSuper2_C C_C1_en.s)
97
))
98

    
99
; super2_c__C_C1_IDL_handler_until
100
(declare-var super2_c__C_C1_IDL_handler_until.idSuper2_C_1 Int)
101
(declare-var super2_c__C_C1_IDL_handler_until.s_1 Real)
102
(declare-var super2_c__C_C1_IDL_handler_until.idSuper2_Super2_1 Int)
103
(declare-var super2_c__C_C1_IDL_handler_until.super2_c__restart_in Bool)
104
(declare-var super2_c__C_C1_IDL_handler_until.super2_c__state_in super2_c__type)
105
(declare-var super2_c__C_C1_IDL_handler_until.idSuper2_C_out Int)
106
(declare-var super2_c__C_C1_IDL_handler_until.idSuper2_Super2_out Int)
107
(declare-var super2_c__C_C1_IDL_handler_until.s_out Real)
108
(declare-rel super2_c__C_C1_IDL_handler_until (Int Real Int Bool super2_c__type Int Int Real))
109
(rule (=> 
110
  (and (= super2_c__C_C1_IDL_handler_until.super2_c__state_in POINTSuper2_C)
111
       (= super2_c__C_C1_IDL_handler_until.super2_c__restart_in true)
112
       (= super2_c__C_C1_IDL_handler_until.s_out super2_c__C_C1_IDL_handler_until.s_1)
113
       (= super2_c__C_C1_IDL_handler_until.idSuper2_Super2_out super2_c__C_C1_IDL_handler_until.idSuper2_Super2_1)
114
       (= super2_c__C_C1_IDL_handler_until.idSuper2_C_out super2_c__C_C1_IDL_handler_until.idSuper2_C_1)
115
       )
116
  (super2_c__C_C1_IDL_handler_until super2_c__C_C1_IDL_handler_until.idSuper2_C_1 super2_c__C_C1_IDL_handler_until.s_1 super2_c__C_C1_IDL_handler_until.idSuper2_Super2_1 super2_c__C_C1_IDL_handler_until.super2_c__restart_in super2_c__C_C1_IDL_handler_until.super2_c__state_in super2_c__C_C1_IDL_handler_until.idSuper2_C_out super2_c__C_C1_IDL_handler_until.idSuper2_Super2_out super2_c__C_C1_IDL_handler_until.s_out)
117
))
118

    
119
; super2_c__C_C1_IDL_unless
120
(declare-var super2_c__C_C1_IDL_unless.super2_c__restart_in Bool)
121
(declare-var super2_c__C_C1_IDL_unless.super2_c__state_in super2_c__type)
122
(declare-var super2_c__C_C1_IDL_unless.super2_c__restart_act Bool)
123
(declare-var super2_c__C_C1_IDL_unless.super2_c__state_act super2_c__type)
124
(declare-rel super2_c__C_C1_IDL_unless (Bool super2_c__type Bool super2_c__type))
125
(rule (=> 
126
  (and (= super2_c__C_C1_IDL_unless.super2_c__state_act super2_c__C_C1_IDL_unless.super2_c__state_in)
127
       (= super2_c__C_C1_IDL_unless.super2_c__restart_act super2_c__C_C1_IDL_unless.super2_c__restart_in)
128
       )
129
  (super2_c__C_C1_IDL_unless super2_c__C_C1_IDL_unless.super2_c__restart_in super2_c__C_C1_IDL_unless.super2_c__state_in super2_c__C_C1_IDL_unless.super2_c__restart_act super2_c__C_C1_IDL_unless.super2_c__state_act)
130
))
131

    
132
; super2_c__C_C1__TO__SUPER2_B_1_handler_until
133
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_1 Int)
134
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_1 Real)
135
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_1 Int)
136
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.super2_c__restart_in Bool)
137
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.super2_c__state_in super2_c__type)
138
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_out Int)
139
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_out Int)
140
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_out Real)
141
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_2 Int)
142
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_2 Int)
143
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_3 Int)
144
(declare-var super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_2 Real)
145
(declare-rel super2_c__C_C1__TO__SUPER2_B_1_handler_until (Int Real Int Bool super2_c__type Int Int Real))
146
(rule (=> 
147
  (and (= super2_c__C_C1__TO__SUPER2_B_1_handler_until.super2_c__state_in POINTSuper2_C)
148
       (= super2_c__C_C1__TO__SUPER2_B_1_handler_until.super2_c__restart_in true)
149
       (Super2_C_ex super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_1
150
                    super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_1
151
                    false
152
                    super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_2
153
                    super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_2)
154
       (Super2_B_en super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_2
155
                    super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_1
156
                    false
157
                    super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_3
158
                    super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_2)
159
       (= super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_out super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_2)
160
       (= super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_out super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_3)
161
       (= super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_out super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_2)
162
       )
163
  (super2_c__C_C1__TO__SUPER2_B_1_handler_until super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_1 super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_1 super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_1 super2_c__C_C1__TO__SUPER2_B_1_handler_until.super2_c__restart_in super2_c__C_C1__TO__SUPER2_B_1_handler_until.super2_c__state_in super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_C_out super2_c__C_C1__TO__SUPER2_B_1_handler_until.idSuper2_Super2_out super2_c__C_C1__TO__SUPER2_B_1_handler_until.s_out)
164
))
165

    
166
; super2_c__C_C1__TO__SUPER2_B_1_unless
167
(declare-var super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__restart_in Bool)
168
(declare-var super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__state_in super2_c__type)
169
(declare-var super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__restart_act Bool)
170
(declare-var super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__state_act super2_c__type)
171
(declare-rel super2_c__C_C1__TO__SUPER2_B_1_unless (Bool super2_c__type Bool super2_c__type))
172
(rule (=> 
173
  (and (= super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__state_act super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__state_in)
174
       (= super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__restart_act super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__restart_in)
175
       )
176
  (super2_c__C_C1__TO__SUPER2_B_1_unless super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__restart_in super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__state_in super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__restart_act super2_c__C_C1__TO__SUPER2_B_1_unless.super2_c__state_act)
177
))
178

    
179
; super2_c__POINTSuper2_C_handler_until
180
(declare-var super2_c__POINTSuper2_C_handler_until.idSuper2_C_1 Int)
181
(declare-var super2_c__POINTSuper2_C_handler_until.s_1 Real)
182
(declare-var super2_c__POINTSuper2_C_handler_until.idSuper2_Super2_1 Int)
183
(declare-var super2_c__POINTSuper2_C_handler_until.super2_c__restart_in Bool)
184
(declare-var super2_c__POINTSuper2_C_handler_until.super2_c__state_in super2_c__type)
185
(declare-var super2_c__POINTSuper2_C_handler_until.idSuper2_C_out Int)
186
(declare-var super2_c__POINTSuper2_C_handler_until.idSuper2_Super2_out Int)
187
(declare-var super2_c__POINTSuper2_C_handler_until.s_out Real)
188
(declare-rel super2_c__POINTSuper2_C_handler_until (Int Real Int Bool super2_c__type Int Int Real))
189
(rule (=> 
190
  (and (= super2_c__POINTSuper2_C_handler_until.super2_c__state_in POINTSuper2_C)
191
       (= super2_c__POINTSuper2_C_handler_until.super2_c__restart_in false)
192
       (= super2_c__POINTSuper2_C_handler_until.s_out super2_c__POINTSuper2_C_handler_until.s_1)
193
       (= super2_c__POINTSuper2_C_handler_until.idSuper2_Super2_out super2_c__POINTSuper2_C_handler_until.idSuper2_Super2_1)
194
       (= super2_c__POINTSuper2_C_handler_until.idSuper2_C_out super2_c__POINTSuper2_C_handler_until.idSuper2_C_1)
195
       )
196
  (super2_c__POINTSuper2_C_handler_until super2_c__POINTSuper2_C_handler_until.idSuper2_C_1 super2_c__POINTSuper2_C_handler_until.s_1 super2_c__POINTSuper2_C_handler_until.idSuper2_Super2_1 super2_c__POINTSuper2_C_handler_until.super2_c__restart_in super2_c__POINTSuper2_C_handler_until.super2_c__state_in super2_c__POINTSuper2_C_handler_until.idSuper2_C_out super2_c__POINTSuper2_C_handler_until.idSuper2_Super2_out super2_c__POINTSuper2_C_handler_until.s_out)
197
))
198

    
199
; super2_c__POINTSuper2_C_unless
200
(declare-var super2_c__POINTSuper2_C_unless.super2_c__restart_in Bool)
201
(declare-var super2_c__POINTSuper2_C_unless.super2_c__state_in super2_c__type)
202
(declare-var super2_c__POINTSuper2_C_unless.idSuper2_C_1 Int)
203
(declare-var super2_c__POINTSuper2_C_unless.E Bool)
204
(declare-var super2_c__POINTSuper2_C_unless.super2_c__restart_act Bool)
205
(declare-var super2_c__POINTSuper2_C_unless.super2_c__state_act super2_c__type)
206
(declare-var super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_1 Bool)
207
(declare-var super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_2 Bool)
208
(declare-var super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_3 Bool)
209
(declare-rel super2_c__POINTSuper2_C_unless (Bool super2_c__type Int Bool Bool super2_c__type))
210
(rule (=> 
211
  (and (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_3 (= super2_c__POINTSuper2_C_unless.idSuper2_C_1 1952))
212
       (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_2 (and (= super2_c__POINTSuper2_C_unless.idSuper2_C_1 1952) super2_c__POINTSuper2_C_unless.E))
213
       (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_1 (= super2_c__POINTSuper2_C_unless.idSuper2_C_1 0))
214
       (and (or (not (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_1 false))
215
               (and (or (not (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_2 false))
216
                       (and (or (not (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_3 false))
217
                               (and (= super2_c__POINTSuper2_C_unless.super2_c__state_act super2_c__POINTSuper2_C_unless.super2_c__state_in)
218
                                    (= super2_c__POINTSuper2_C_unless.super2_c__restart_act super2_c__POINTSuper2_C_unless.super2_c__restart_in)
219
                                    ))
220
                            (or (not (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_3 true))
221
                               (and (= super2_c__POINTSuper2_C_unless.super2_c__state_act C_C1_IDL)
222
                                    (= super2_c__POINTSuper2_C_unless.super2_c__restart_act true)
223
                                    ))
224
                       ))
225
                    (or (not (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_2 true))
226
                       (and (= super2_c__POINTSuper2_C_unless.super2_c__state_act C_C1__TO__SUPER2_B_1)
227
                            (= super2_c__POINTSuper2_C_unless.super2_c__restart_act true)
228
                            ))
229
               ))
230
            (or (not (= super2_c__POINTSuper2_C_unless.__super2_c__POINTSuper2_C_unless_1 true))
231
               (and (= super2_c__POINTSuper2_C_unless.super2_c__state_act POINT__TO__C_C1_1)
232
                    (= super2_c__POINTSuper2_C_unless.super2_c__restart_act true)
233
                    ))
234
       )
235
       )
236
  (super2_c__POINTSuper2_C_unless super2_c__POINTSuper2_C_unless.super2_c__restart_in super2_c__POINTSuper2_C_unless.super2_c__state_in super2_c__POINTSuper2_C_unless.idSuper2_C_1 super2_c__POINTSuper2_C_unless.E super2_c__POINTSuper2_C_unless.super2_c__restart_act super2_c__POINTSuper2_C_unless.super2_c__state_act)
237
))
238

    
239
; super2_c__POINT__TO__C_C1_1_handler_until
240
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_1 Int)
241
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.s_1 Real)
242
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_Super2_1 Int)
243
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.super2_c__restart_in Bool)
244
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.super2_c__state_in super2_c__type)
245
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_out Int)
246
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_Super2_out Int)
247
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.s_out Real)
248
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_2 Int)
249
(declare-var super2_c__POINT__TO__C_C1_1_handler_until.s_2 Real)
250
(declare-rel super2_c__POINT__TO__C_C1_1_handler_until (Int Real Int Bool super2_c__type Int Int Real))
251
(rule (=> 
252
  (and (= super2_c__POINT__TO__C_C1_1_handler_until.super2_c__state_in POINTSuper2_C)
253
       (= super2_c__POINT__TO__C_C1_1_handler_until.super2_c__restart_in true)
254
       (C_C1_en super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_1
255
                super2_c__POINT__TO__C_C1_1_handler_until.s_1
256
                false
257
                super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_2
258
                super2_c__POINT__TO__C_C1_1_handler_until.s_2)
259
       (= super2_c__POINT__TO__C_C1_1_handler_until.s_out super2_c__POINT__TO__C_C1_1_handler_until.s_2)
260
       (= super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_Super2_out super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_Super2_1)
261
       (= super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_out super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_2)
262
       )
263
  (super2_c__POINT__TO__C_C1_1_handler_until super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_1 super2_c__POINT__TO__C_C1_1_handler_until.s_1 super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_Super2_1 super2_c__POINT__TO__C_C1_1_handler_until.super2_c__restart_in super2_c__POINT__TO__C_C1_1_handler_until.super2_c__state_in super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_C_out super2_c__POINT__TO__C_C1_1_handler_until.idSuper2_Super2_out super2_c__POINT__TO__C_C1_1_handler_until.s_out)
264
))
265

    
266
; super2_c__POINT__TO__C_C1_1_unless
267
(declare-var super2_c__POINT__TO__C_C1_1_unless.super2_c__restart_in Bool)
268
(declare-var super2_c__POINT__TO__C_C1_1_unless.super2_c__state_in super2_c__type)
269
(declare-var super2_c__POINT__TO__C_C1_1_unless.super2_c__restart_act Bool)
270
(declare-var super2_c__POINT__TO__C_C1_1_unless.super2_c__state_act super2_c__type)
271
(declare-rel super2_c__POINT__TO__C_C1_1_unless (Bool super2_c__type Bool super2_c__type))
272
(rule (=> 
273
  (and (= super2_c__POINT__TO__C_C1_1_unless.super2_c__state_act super2_c__POINT__TO__C_C1_1_unless.super2_c__state_in)
274
       (= super2_c__POINT__TO__C_C1_1_unless.super2_c__restart_act super2_c__POINT__TO__C_C1_1_unless.super2_c__restart_in)
275
       )
276
  (super2_c__POINT__TO__C_C1_1_unless super2_c__POINT__TO__C_C1_1_unless.super2_c__restart_in super2_c__POINT__TO__C_C1_1_unless.super2_c__state_in super2_c__POINT__TO__C_C1_1_unless.super2_c__restart_act super2_c__POINT__TO__C_C1_1_unless.super2_c__state_act)
277
))
278

    
279
; Super2_A_en
280
(declare-var Super2_A_en.idSuper2_Super2_1 Int)
281
(declare-var Super2_A_en.s_1 Real)
282
(declare-var Super2_A_en.isInner Bool)
283
(declare-var Super2_A_en.idSuper2_Super2 Int)
284
(declare-var Super2_A_en.s Real)
285
(declare-var Super2_A_en.s_2 Real)
286
(declare-rel Super2_A_en (Int Real Bool Int Real))
287
(rule (=> 
288
  (and (and (or (not (= (not Super2_A_en.isInner) true))
289
               (= Super2_A_en.s_2 1.))
290
            (or (not (= (not Super2_A_en.isInner) false))
291
               (= Super2_A_en.s_2 Super2_A_en.s_1))
292
       )
293
       (= Super2_A_en.s Super2_A_en.s_2)
294
       (= Super2_A_en.idSuper2_Super2 1950)
295
       )
296
  (Super2_A_en Super2_A_en.idSuper2_Super2_1 Super2_A_en.s_1 Super2_A_en.isInner Super2_A_en.idSuper2_Super2 Super2_A_en.s)
297
))
298

    
299
; Super2_A_ex
300
(declare-var Super2_A_ex.idSuper2_Super2_1 Int)
301
(declare-var Super2_A_ex.isInner Bool)
302
(declare-var Super2_A_ex.idSuper2_Super2 Int)
303
(declare-var Super2_A_ex.idSuper2_Super2_2 Int)
304
(declare-rel Super2_A_ex (Int Bool Int))
305
(rule (=> 
306
  (and (and (or (not (= (not Super2_A_ex.isInner) true))
307
               (= Super2_A_ex.idSuper2_Super2_2 0))
308
            (or (not (= (not Super2_A_ex.isInner) false))
309
               (= Super2_A_ex.idSuper2_Super2_2 Super2_A_ex.idSuper2_Super2_1))
310
       )
311
       (= Super2_A_ex.idSuper2_Super2 Super2_A_ex.idSuper2_Super2_1)
312
       )
313
  (Super2_A_ex Super2_A_ex.idSuper2_Super2_1 Super2_A_ex.isInner Super2_A_ex.idSuper2_Super2)
314
))
315

    
316
; Super2_C_en
317
(declare-var Super2_C_en.idSuper2_C_1 Int)
318
(declare-var Super2_C_en.idSuper2_Super2_1 Int)
319
(declare-var Super2_C_en.s_1 Real)
320
(declare-var Super2_C_en.isInner Bool)
321
(declare-var Super2_C_en.idSuper2_C Int)
322
(declare-var Super2_C_en.idSuper2_Super2 Int)
323
(declare-var Super2_C_en.s Real)
324
(declare-var Super2_C_en.__Super2_C_en_1 Bool)
325
(declare-var Super2_C_en.__Super2_C_en_2 Bool)
326
(declare-var Super2_C_en.__Super2_C_en_3 Int)
327
(declare-var Super2_C_en.__Super2_C_en_4 Real)
328
(declare-var Super2_C_en.idSuper2_C_2 Int)
329
(declare-var Super2_C_en.idSuper2_C_3 Int)
330
(declare-var Super2_C_en.idSuper2_C_4 Int)
331
(declare-var Super2_C_en.idSuper2_C_5 Int)
332
(declare-var Super2_C_en.idSuper2_Super2_3 Int)
333
(declare-var Super2_C_en.idSuper2_Super2_4 Int)
334
(declare-var Super2_C_en.s_2 Real)
335
(declare-var Super2_C_en.s_3 Real)
336
(declare-var Super2_C_en.s_4 Real)
337
(declare-var Super2_C_en.s_5 Real)
338
(declare-rel Super2_C_en (Int Int Real Bool Int Int Real))
339
(rule (=> 
340
  (and (C_C1_en Super2_C_en.idSuper2_C_1
341
                Super2_C_en.s_1
342
                false
343
                Super2_C_en.__Super2_C_en_3
344
                Super2_C_en.__Super2_C_en_4)
345
       (= Super2_C_en.__Super2_C_en_2 (= Super2_C_en.idSuper2_C_1 1952))
346
       (and (or (not (= Super2_C_en.__Super2_C_en_2 false))
347
               (and (= Super2_C_en.s_4 Super2_C_en.s_1)
348
                    (= Super2_C_en.idSuper2_C_4 Super2_C_en.idSuper2_C_1)
349
                    ))
350
            (or (not (= Super2_C_en.__Super2_C_en_2 true))
351
               (and (= Super2_C_en.s_4 Super2_C_en.__Super2_C_en_4)
352
                    (= Super2_C_en.idSuper2_C_4 Super2_C_en.__Super2_C_en_3)
353
                    ))
354
       )
355
       (C_C1_en Super2_C_en.idSuper2_C_1
356
                Super2_C_en.s_1
357
                false
358
                Super2_C_en.idSuper2_C_2
359
                Super2_C_en.s_2)
360
       (= Super2_C_en.__Super2_C_en_1 (= Super2_C_en.idSuper2_C_1 0))
361
       (and (or (not (= Super2_C_en.__Super2_C_en_1 false))
362
               (and (= Super2_C_en.s_3 Super2_C_en.s_1)
363
                    (= Super2_C_en.idSuper2_Super2_3 1953)
364
                    (= Super2_C_en.idSuper2_C_3 Super2_C_en.idSuper2_C_1)
365
                    (and (or (not (= Super2_C_en.__Super2_C_en_2 false))
366
                            (and (= Super2_C_en.s_5 Super2_C_en.s_1)
367
                                 (= Super2_C_en.idSuper2_Super2_4 1953)
368
                                 (= Super2_C_en.idSuper2_C_5 Super2_C_en.idSuper2_C_1)
369
                                 ))
370
                         (or (not (= Super2_C_en.__Super2_C_en_2 true))
371
                            (and (= Super2_C_en.s_5 Super2_C_en.s_4)
372
                                 (= Super2_C_en.idSuper2_Super2_4 Super2_C_en.idSuper2_Super2_3)
373
                                 (= Super2_C_en.idSuper2_C_5 Super2_C_en.idSuper2_C_4)
374
                                 ))
375
                    )
376
                    ))
377
            (or (not (= Super2_C_en.__Super2_C_en_1 true))
378
               (and (= Super2_C_en.s_3 Super2_C_en.s_2)
379
                    (= Super2_C_en.idSuper2_Super2_3 1953)
380
                    (= Super2_C_en.idSuper2_C_3 Super2_C_en.idSuper2_C_2)
381
                    (= Super2_C_en.s_5 Super2_C_en.s_3)
382
                    (= Super2_C_en.idSuper2_Super2_4 Super2_C_en.idSuper2_Super2_3)
383
                    (= Super2_C_en.idSuper2_C_5 Super2_C_en.idSuper2_C_3)
384
                    ))
385
       )
386
       (= Super2_C_en.s Super2_C_en.s_5)
387
       (= Super2_C_en.idSuper2_Super2 Super2_C_en.idSuper2_Super2_4)
388
       (= Super2_C_en.idSuper2_C Super2_C_en.idSuper2_C_5)
389
       )
390
  (Super2_C_en Super2_C_en.idSuper2_C_1 Super2_C_en.idSuper2_Super2_1 Super2_C_en.s_1 Super2_C_en.isInner Super2_C_en.idSuper2_C Super2_C_en.idSuper2_Super2 Super2_C_en.s)
391
))
392

    
393
; Super2_B_ex
394
(declare-var Super2_B_ex.idSuper2_Super2_1 Int)
395
(declare-var Super2_B_ex.isInner Bool)
396
(declare-var Super2_B_ex.idSuper2_Super2 Int)
397
(declare-var Super2_B_ex.idSuper2_Super2_2 Int)
398
(declare-rel Super2_B_ex (Int Bool Int))
399
(rule (=> 
400
  (and (and (or (not (= (not Super2_B_ex.isInner) true))
401
               (= Super2_B_ex.idSuper2_Super2_2 0))
402
            (or (not (= (not Super2_B_ex.isInner) false))
403
               (= Super2_B_ex.idSuper2_Super2_2 Super2_B_ex.idSuper2_Super2_1))
404
       )
405
       (= Super2_B_ex.idSuper2_Super2 Super2_B_ex.idSuper2_Super2_1)
406
       )
407
  (Super2_B_ex Super2_B_ex.idSuper2_Super2_1 Super2_B_ex.isInner Super2_B_ex.idSuper2_Super2)
408
))
409

    
410
; Super2_C_node
411
(declare-var Super2_C_node.idSuper2_C_1 Int)
412
(declare-var Super2_C_node.s_1 Real)
413
(declare-var Super2_C_node.E Bool)
414
(declare-var Super2_C_node.idSuper2_Super2_1 Int)
415
(declare-var Super2_C_node.idSuper2_C Int)
416
(declare-var Super2_C_node.s Real)
417
(declare-var Super2_C_node.idSuper2_Super2 Int)
418
(declare-var Super2_C_node.__Super2_C_node_30_c Bool)
419
(declare-var Super2_C_node.__Super2_C_node_31_c super2_c__type)
420
(declare-var Super2_C_node.ni_9._arrow._first_c Bool)
421
(declare-var Super2_C_node.__Super2_C_node_30_m Bool)
422
(declare-var Super2_C_node.__Super2_C_node_31_m super2_c__type)
423
(declare-var Super2_C_node.ni_9._arrow._first_m Bool)
424
(declare-var Super2_C_node.__Super2_C_node_30_x Bool)
425
(declare-var Super2_C_node.__Super2_C_node_31_x super2_c__type)
426
(declare-var Super2_C_node.ni_9._arrow._first_x Bool)
427
(declare-var Super2_C_node.__Super2_C_node_1 Bool)
428
(declare-var Super2_C_node.__Super2_C_node_10 super2_c__type)
429
(declare-var Super2_C_node.__Super2_C_node_11 Int)
430
(declare-var Super2_C_node.__Super2_C_node_12 Int)
431
(declare-var Super2_C_node.__Super2_C_node_13 Real)
432
(declare-var Super2_C_node.__Super2_C_node_14 Bool)
433
(declare-var Super2_C_node.__Super2_C_node_15 super2_c__type)
434
(declare-var Super2_C_node.__Super2_C_node_16 Int)
435
(declare-var Super2_C_node.__Super2_C_node_17 Int)
436
(declare-var Super2_C_node.__Super2_C_node_18 Real)
437
(declare-var Super2_C_node.__Super2_C_node_19 Bool)
438
(declare-var Super2_C_node.__Super2_C_node_2 super2_c__type)
439
(declare-var Super2_C_node.__Super2_C_node_20 super2_c__type)
440
(declare-var Super2_C_node.__Super2_C_node_21 Int)
441
(declare-var Super2_C_node.__Super2_C_node_22 Int)
442
(declare-var Super2_C_node.__Super2_C_node_23 Real)
443
(declare-var Super2_C_node.__Super2_C_node_24 Bool)
444
(declare-var Super2_C_node.__Super2_C_node_25 super2_c__type)
445
(declare-var Super2_C_node.__Super2_C_node_26 Int)
446
(declare-var Super2_C_node.__Super2_C_node_27 Int)
447
(declare-var Super2_C_node.__Super2_C_node_28 Real)
448
(declare-var Super2_C_node.__Super2_C_node_29 Bool)
449
(declare-var Super2_C_node.__Super2_C_node_3 Bool)
450
(declare-var Super2_C_node.__Super2_C_node_4 super2_c__type)
451
(declare-var Super2_C_node.__Super2_C_node_5 Bool)
452
(declare-var Super2_C_node.__Super2_C_node_6 super2_c__type)
453
(declare-var Super2_C_node.__Super2_C_node_7 Bool)
454
(declare-var Super2_C_node.__Super2_C_node_8 super2_c__type)
455
(declare-var Super2_C_node.__Super2_C_node_9 Bool)
456
(declare-var Super2_C_node.super2_c__next_restart_in Bool)
457
(declare-var Super2_C_node.super2_c__next_state_in super2_c__type)
458
(declare-var Super2_C_node.super2_c__restart_act Bool)
459
(declare-var Super2_C_node.super2_c__restart_in Bool)
460
(declare-var Super2_C_node.super2_c__state_act super2_c__type)
461
(declare-var Super2_C_node.super2_c__state_in super2_c__type)
462
(declare-rel Super2_C_node_reset (Bool super2_c__type Bool Bool super2_c__type Bool))
463
(declare-rel Super2_C_node_step (Int Real Bool Int Int Real Int Bool super2_c__type Bool Bool super2_c__type Bool))
464

    
465
(rule (=> 
466
  (and 
467
       (= Super2_C_node.__Super2_C_node_30_m Super2_C_node.__Super2_C_node_30_c)
468
       (= Super2_C_node.__Super2_C_node_31_m Super2_C_node.__Super2_C_node_31_c)
469
       (= Super2_C_node.ni_9._arrow._first_m true)
470
  )
471
  (Super2_C_node_reset Super2_C_node.__Super2_C_node_30_c
472
                       Super2_C_node.__Super2_C_node_31_c
473
                       Super2_C_node.ni_9._arrow._first_c
474
                       Super2_C_node.__Super2_C_node_30_m
475
                       Super2_C_node.__Super2_C_node_31_m
476
                       Super2_C_node.ni_9._arrow._first_m)
477
))
478

    
479
(rule (=> 
480
  (and (= Super2_C_node.ni_9._arrow._first_m Super2_C_node.ni_9._arrow._first_c)
481
       (and (= Super2_C_node.__Super2_C_node_29 (ite Super2_C_node.ni_9._arrow._first_m true false))
482
            (= Super2_C_node.ni_9._arrow._first_x false))
483
       (and (or (not (= Super2_C_node.__Super2_C_node_29 false))
484
               (and (= Super2_C_node.super2_c__state_in Super2_C_node.__Super2_C_node_31_c)
485
                    (= Super2_C_node.super2_c__restart_in Super2_C_node.__Super2_C_node_30_c)
486
                    ))
487
            (or (not (= Super2_C_node.__Super2_C_node_29 true))
488
               (and (= Super2_C_node.super2_c__state_in POINTSuper2_C)
489
                    (= Super2_C_node.super2_c__restart_in false)
490
                    ))
491
       )
492
       (and (or (not (= Super2_C_node.super2_c__state_in C_C1_IDL))
493
               (and (super2_c__C_C1_IDL_unless Super2_C_node.super2_c__restart_in
494
                                               Super2_C_node.super2_c__state_in
495
                                               Super2_C_node.__Super2_C_node_1
496
                                               Super2_C_node.__Super2_C_node_2)
497
                    (= Super2_C_node.super2_c__state_act Super2_C_node.__Super2_C_node_2)
498
                    (= Super2_C_node.super2_c__restart_act Super2_C_node.__Super2_C_node_1)
499
                    ))
500
            (or (not (= Super2_C_node.super2_c__state_in C_C1__TO__SUPER2_B_1))
501
               (and (super2_c__C_C1__TO__SUPER2_B_1_unless Super2_C_node.super2_c__restart_in
502
                                                           Super2_C_node.super2_c__state_in
503
                                                           Super2_C_node.__Super2_C_node_3
504
                                                           Super2_C_node.__Super2_C_node_4)
505
                    (= Super2_C_node.super2_c__state_act Super2_C_node.__Super2_C_node_4)
506
                    (= Super2_C_node.super2_c__restart_act Super2_C_node.__Super2_C_node_3)
507
                    ))
508
            (or (not (= Super2_C_node.super2_c__state_in POINTSuper2_C))
509
               (and (super2_c__POINTSuper2_C_unless Super2_C_node.super2_c__restart_in
510
                                                    Super2_C_node.super2_c__state_in
511
                                                    Super2_C_node.idSuper2_C_1
512
                                                    Super2_C_node.E
513
                                                    Super2_C_node.__Super2_C_node_7
514
                                                    Super2_C_node.__Super2_C_node_8)
515
                    (= Super2_C_node.super2_c__state_act Super2_C_node.__Super2_C_node_8)
516
                    (= Super2_C_node.super2_c__restart_act Super2_C_node.__Super2_C_node_7)
517
                    ))
518
            (or (not (= Super2_C_node.super2_c__state_in POINT__TO__C_C1_1))
519
               (and (super2_c__POINT__TO__C_C1_1_unless Super2_C_node.super2_c__restart_in
520
                                                        Super2_C_node.super2_c__state_in
521
                                                        Super2_C_node.__Super2_C_node_5
522
                                                        Super2_C_node.__Super2_C_node_6)
523
                    (= Super2_C_node.super2_c__state_act Super2_C_node.__Super2_C_node_6)
524
                    (= Super2_C_node.super2_c__restart_act Super2_C_node.__Super2_C_node_5)
525
                    ))
526
       )
527
       (and (or (not (= Super2_C_node.super2_c__state_act C_C1_IDL))
528
               (and (super2_c__C_C1_IDL_handler_until Super2_C_node.idSuper2_C_1
529
                                                      Super2_C_node.s_1
530
                                                      Super2_C_node.idSuper2_Super2_1
531
                                                      Super2_C_node.__Super2_C_node_9
532
                                                      Super2_C_node.__Super2_C_node_10
533
                                                      Super2_C_node.__Super2_C_node_11
534
                                                      Super2_C_node.__Super2_C_node_12
535
                                                      Super2_C_node.__Super2_C_node_13)
536
                    (= Super2_C_node.super2_c__next_state_in Super2_C_node.__Super2_C_node_10)
537
                    (= Super2_C_node.super2_c__next_restart_in Super2_C_node.__Super2_C_node_9)
538
                    (= Super2_C_node.s Super2_C_node.__Super2_C_node_13)
539
                    (= Super2_C_node.idSuper2_Super2 Super2_C_node.__Super2_C_node_12)
540
                    (= Super2_C_node.idSuper2_C Super2_C_node.__Super2_C_node_11)
541
                    ))
542
            (or (not (= Super2_C_node.super2_c__state_act C_C1__TO__SUPER2_B_1))
543
               (and (super2_c__C_C1__TO__SUPER2_B_1_handler_until Super2_C_node.idSuper2_C_1
544
                                                                  Super2_C_node.s_1
545
                                                                  Super2_C_node.idSuper2_Super2_1
546
                                                                  Super2_C_node.__Super2_C_node_14
547
                                                                  Super2_C_node.__Super2_C_node_15
548
                                                                  Super2_C_node.__Super2_C_node_16
549
                                                                  Super2_C_node.__Super2_C_node_17
550
                                                                  Super2_C_node.__Super2_C_node_18)
551
                    (= Super2_C_node.super2_c__next_state_in Super2_C_node.__Super2_C_node_15)
552
                    (= Super2_C_node.super2_c__next_restart_in Super2_C_node.__Super2_C_node_14)
553
                    (= Super2_C_node.s Super2_C_node.__Super2_C_node_18)
554
                    (= Super2_C_node.idSuper2_Super2 Super2_C_node.__Super2_C_node_17)
555
                    (= Super2_C_node.idSuper2_C Super2_C_node.__Super2_C_node_16)
556
                    ))
557
            (or (not (= Super2_C_node.super2_c__state_act POINTSuper2_C))
558
               (and (super2_c__POINTSuper2_C_handler_until Super2_C_node.idSuper2_C_1
559
                                                           Super2_C_node.s_1
560
                                                           Super2_C_node.idSuper2_Super2_1
561
                                                           Super2_C_node.__Super2_C_node_24
562
                                                           Super2_C_node.__Super2_C_node_25
563
                                                           Super2_C_node.__Super2_C_node_26
564
                                                           Super2_C_node.__Super2_C_node_27
565
                                                           Super2_C_node.__Super2_C_node_28)
566
                    (= Super2_C_node.super2_c__next_state_in Super2_C_node.__Super2_C_node_25)
567
                    (= Super2_C_node.super2_c__next_restart_in Super2_C_node.__Super2_C_node_24)
568
                    (= Super2_C_node.s Super2_C_node.__Super2_C_node_28)
569
                    (= Super2_C_node.idSuper2_Super2 Super2_C_node.__Super2_C_node_27)
570
                    (= Super2_C_node.idSuper2_C Super2_C_node.__Super2_C_node_26)
571
                    ))
572
            (or (not (= Super2_C_node.super2_c__state_act POINT__TO__C_C1_1))
573
               (and (super2_c__POINT__TO__C_C1_1_handler_until Super2_C_node.idSuper2_C_1
574
                                                               Super2_C_node.s_1
575
                                                               Super2_C_node.idSuper2_Super2_1
576
                                                               Super2_C_node.__Super2_C_node_19
577
                                                               Super2_C_node.__Super2_C_node_20
578
                                                               Super2_C_node.__Super2_C_node_21
579
                                                               Super2_C_node.__Super2_C_node_22
580
                                                               Super2_C_node.__Super2_C_node_23)
581
                    (= Super2_C_node.super2_c__next_state_in Super2_C_node.__Super2_C_node_20)
582
                    (= Super2_C_node.super2_c__next_restart_in Super2_C_node.__Super2_C_node_19)
583
                    (= Super2_C_node.s Super2_C_node.__Super2_C_node_23)
584
                    (= Super2_C_node.idSuper2_Super2 Super2_C_node.__Super2_C_node_22)
585
                    (= Super2_C_node.idSuper2_C Super2_C_node.__Super2_C_node_21)
586
                    ))
587
       )
588
       (= Super2_C_node.__Super2_C_node_31_x Super2_C_node.super2_c__next_state_in)
589
       (= Super2_C_node.__Super2_C_node_30_x Super2_C_node.super2_c__next_restart_in)
590
       )
591
  (Super2_C_node_step Super2_C_node.idSuper2_C_1
592
                      Super2_C_node.s_1
593
                      Super2_C_node.E
594
                      Super2_C_node.idSuper2_Super2_1
595
                      Super2_C_node.idSuper2_C
596
                      Super2_C_node.s
597
                      Super2_C_node.idSuper2_Super2
598
                      Super2_C_node.__Super2_C_node_30_c
599
                      Super2_C_node.__Super2_C_node_31_c
600
                      Super2_C_node.ni_9._arrow._first_c
601
                      Super2_C_node.__Super2_C_node_30_x
602
                      Super2_C_node.__Super2_C_node_31_x
603
                      Super2_C_node.ni_9._arrow._first_x)
604
))
605

    
606
; super2_super2__POINTSuper2_Super2_handler_until
607
(declare-var super2_super2__POINTSuper2_Super2_handler_until.idSuper2_Super2_1 Int)
608
(declare-var super2_super2__POINTSuper2_Super2_handler_until.s_1 Real)
609
(declare-var super2_super2__POINTSuper2_Super2_handler_until.idSuper2_C_1 Int)
610
(declare-var super2_super2__POINTSuper2_Super2_handler_until.super2_super2__restart_in Bool)
611
(declare-var super2_super2__POINTSuper2_Super2_handler_until.super2_super2__state_in super2_super2__type)
612
(declare-var super2_super2__POINTSuper2_Super2_handler_until.idSuper2_C_out Int)
613
(declare-var super2_super2__POINTSuper2_Super2_handler_until.idSuper2_Super2_out Int)
614
(declare-var super2_super2__POINTSuper2_Super2_handler_until.s_out Real)
615
(declare-rel super2_super2__POINTSuper2_Super2_handler_until (Int Real Int Bool super2_super2__type Int Int Real))
616
(rule (=> 
617
  (and (= super2_super2__POINTSuper2_Super2_handler_until.super2_super2__state_in POINTSuper2_Super2)
618
       (= super2_super2__POINTSuper2_Super2_handler_until.super2_super2__restart_in false)
619
       (= super2_super2__POINTSuper2_Super2_handler_until.s_out super2_super2__POINTSuper2_Super2_handler_until.s_1)
620
       (= super2_super2__POINTSuper2_Super2_handler_until.idSuper2_Super2_out super2_super2__POINTSuper2_Super2_handler_until.idSuper2_Super2_1)
621
       (= super2_super2__POINTSuper2_Super2_handler_until.idSuper2_C_out super2_super2__POINTSuper2_Super2_handler_until.idSuper2_C_1)
622
       )
623
  (super2_super2__POINTSuper2_Super2_handler_until super2_super2__POINTSuper2_Super2_handler_until.idSuper2_Super2_1 super2_super2__POINTSuper2_Super2_handler_until.s_1 super2_super2__POINTSuper2_Super2_handler_until.idSuper2_C_1 super2_super2__POINTSuper2_Super2_handler_until.super2_super2__restart_in super2_super2__POINTSuper2_Super2_handler_until.super2_super2__state_in super2_super2__POINTSuper2_Super2_handler_until.idSuper2_C_out super2_super2__POINTSuper2_Super2_handler_until.idSuper2_Super2_out super2_super2__POINTSuper2_Super2_handler_until.s_out)
624
))
625

    
626
; super2_super2__POINTSuper2_Super2_unless
627
(declare-var super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_in Bool)
628
(declare-var super2_super2__POINTSuper2_Super2_unless.super2_super2__state_in super2_super2__type)
629
(declare-var super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 Int)
630
(declare-var super2_super2__POINTSuper2_Super2_unless.F Bool)
631
(declare-var super2_super2__POINTSuper2_Super2_unless.E Bool)
632
(declare-var super2_super2__POINTSuper2_Super2_unless.G Bool)
633
(declare-var super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act Bool)
634
(declare-var super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act super2_super2__type)
635
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_1 Bool)
636
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_2 Bool)
637
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_3 Bool)
638
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_4 Bool)
639
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_5 Bool)
640
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_6 Bool)
641
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_7 Bool)
642
(declare-var super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_8 Bool)
643
(declare-rel super2_super2__POINTSuper2_Super2_unless (Bool super2_super2__type Int Bool Bool Bool Bool super2_super2__type))
644
(rule (=> 
645
  (and (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_8 (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 1953))
646
       (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_7 (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 1951))
647
       (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_6 (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 1950))
648
       (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_5 (and (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 1953) super2_super2__POINTSuper2_Super2_unless.F))
649
       (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_4 (and (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 1951) super2_super2__POINTSuper2_Super2_unless.G))
650
       (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_3 (and (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 1950) super2_super2__POINTSuper2_Super2_unless.E))
651
       (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_2 (and (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 1950) super2_super2__POINTSuper2_Super2_unless.F))
652
       (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_1 (= super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 0))
653
       (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_1 false))
654
               (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_2 false))
655
                       (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_3 false))
656
                               (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_4 false))
657
                                       (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_5 false))
658
                                               (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_6 false))
659
                                                       (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_7 false))
660
                                                               (and (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_8 false))
661
                                                                    (and 
662
                                                                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act super2_super2__POINTSuper2_Super2_unless.super2_super2__state_in)
663
                                                                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_in)
664
                                                                    ))
665
                                                                    (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_8 true))
666
                                                                    (and 
667
                                                                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act SUPER2_C_IDL)
668
                                                                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
669
                                                                    ))
670
                                                               ))
671
                                                            (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_7 true))
672
                                                               (and (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act SUPER2_B_IDL)
673
                                                                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
674
                                                                    ))
675
                                                       ))
676
                                                    (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_6 true))
677
                                                       (and (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act SUPER2_A_IDL)
678
                                                            (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
679
                                                            ))
680
                                               ))
681
                                            (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_5 true))
682
                                               (and (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act SUPER2_C__TO__SUPER2_B_1)
683
                                                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
684
                                                    ))
685
                                       ))
686
                                    (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_4 true))
687
                                       (and (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act SUPER2_B__TO__SUPER2_A_1)
688
                                            (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
689
                                            ))
690
                               ))
691
                            (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_3 true))
692
                               (and (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act SUPER2_A__TO__C_C1_2)
693
                                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
694
                                    ))
695
                       ))
696
                    (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_2 true))
697
                       (and (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act SUPER2_A__TO__SUPER2_C_1)
698
                            (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
699
                            ))
700
               ))
701
            (or (not (= super2_super2__POINTSuper2_Super2_unless.__super2_super2__POINTSuper2_Super2_unless_1 true))
702
               (and (= super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act POINT__TO__SUPER2_A_1)
703
                    (= super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act true)
704
                    ))
705
       )
706
       )
707
  (super2_super2__POINTSuper2_Super2_unless super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_in super2_super2__POINTSuper2_Super2_unless.super2_super2__state_in super2_super2__POINTSuper2_Super2_unless.idSuper2_Super2_1 super2_super2__POINTSuper2_Super2_unless.F super2_super2__POINTSuper2_Super2_unless.E super2_super2__POINTSuper2_Super2_unless.G super2_super2__POINTSuper2_Super2_unless.super2_super2__restart_act super2_super2__POINTSuper2_Super2_unless.super2_super2__state_act)
708
))
709

    
710
; super2_super2__POINT__TO__SUPER2_A_1_handler_until
711
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_1 Int)
712
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_1 Real)
713
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_C_1 Int)
714
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.super2_super2__restart_in Bool)
715
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.super2_super2__state_in super2_super2__type)
716
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_C_out Int)
717
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_out Int)
718
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_out Real)
719
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_2 Int)
720
(declare-var super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_2 Real)
721
(declare-rel super2_super2__POINT__TO__SUPER2_A_1_handler_until (Int Real Int Bool super2_super2__type Int Int Real))
722
(rule (=> 
723
  (and (= super2_super2__POINT__TO__SUPER2_A_1_handler_until.super2_super2__state_in POINTSuper2_Super2)
724
       (= super2_super2__POINT__TO__SUPER2_A_1_handler_until.super2_super2__restart_in true)
725
       (Super2_A_en super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_1
726
                    super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_1
727
                    false
728
                    super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_2
729
                    super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_2)
730
       (= super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_out super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_2)
731
       (= super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_out super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_2)
732
       (= super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_C_out super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_C_1)
733
       )
734
  (super2_super2__POINT__TO__SUPER2_A_1_handler_until super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_1 super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_1 super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_C_1 super2_super2__POINT__TO__SUPER2_A_1_handler_until.super2_super2__restart_in super2_super2__POINT__TO__SUPER2_A_1_handler_until.super2_super2__state_in super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_C_out super2_super2__POINT__TO__SUPER2_A_1_handler_until.idSuper2_Super2_out super2_super2__POINT__TO__SUPER2_A_1_handler_until.s_out)
735
))
736

    
737
; super2_super2__POINT__TO__SUPER2_A_1_unless
738
(declare-var super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__restart_in Bool)
739
(declare-var super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__state_in super2_super2__type)
740
(declare-var super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__restart_act Bool)
741
(declare-var super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__state_act super2_super2__type)
742
(declare-rel super2_super2__POINT__TO__SUPER2_A_1_unless (Bool super2_super2__type Bool super2_super2__type))
743
(rule (=> 
744
  (and (= super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__state_act super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__state_in)
745
       (= super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__restart_act super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__restart_in)
746
       )
747
  (super2_super2__POINT__TO__SUPER2_A_1_unless super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__restart_in super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__state_in super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__restart_act super2_super2__POINT__TO__SUPER2_A_1_unless.super2_super2__state_act)
748
))
749

    
750
; super2_super2__SUPER2_A_IDL_handler_until
751
(declare-var super2_super2__SUPER2_A_IDL_handler_until.idSuper2_Super2_1 Int)
752
(declare-var super2_super2__SUPER2_A_IDL_handler_until.s_1 Real)
753
(declare-var super2_super2__SUPER2_A_IDL_handler_until.idSuper2_C_1 Int)
754
(declare-var super2_super2__SUPER2_A_IDL_handler_until.super2_super2__restart_in Bool)
755
(declare-var super2_super2__SUPER2_A_IDL_handler_until.super2_super2__state_in super2_super2__type)
756
(declare-var super2_super2__SUPER2_A_IDL_handler_until.idSuper2_C_out Int)
757
(declare-var super2_super2__SUPER2_A_IDL_handler_until.idSuper2_Super2_out Int)
758
(declare-var super2_super2__SUPER2_A_IDL_handler_until.s_out Real)
759
(declare-rel super2_super2__SUPER2_A_IDL_handler_until (Int Real Int Bool super2_super2__type Int Int Real))
760
(rule (=> 
761
  (and (= super2_super2__SUPER2_A_IDL_handler_until.super2_super2__state_in POINTSuper2_Super2)
762
       (= super2_super2__SUPER2_A_IDL_handler_until.super2_super2__restart_in true)
763
       (= super2_super2__SUPER2_A_IDL_handler_until.s_out super2_super2__SUPER2_A_IDL_handler_until.s_1)
764
       (= super2_super2__SUPER2_A_IDL_handler_until.idSuper2_Super2_out super2_super2__SUPER2_A_IDL_handler_until.idSuper2_Super2_1)
765
       (= super2_super2__SUPER2_A_IDL_handler_until.idSuper2_C_out super2_super2__SUPER2_A_IDL_handler_until.idSuper2_C_1)
766
       )
767
  (super2_super2__SUPER2_A_IDL_handler_until super2_super2__SUPER2_A_IDL_handler_until.idSuper2_Super2_1 super2_super2__SUPER2_A_IDL_handler_until.s_1 super2_super2__SUPER2_A_IDL_handler_until.idSuper2_C_1 super2_super2__SUPER2_A_IDL_handler_until.super2_super2__restart_in super2_super2__SUPER2_A_IDL_handler_until.super2_super2__state_in super2_super2__SUPER2_A_IDL_handler_until.idSuper2_C_out super2_super2__SUPER2_A_IDL_handler_until.idSuper2_Super2_out super2_super2__SUPER2_A_IDL_handler_until.s_out)
768
))
769

    
770
; super2_super2__SUPER2_A_IDL_unless
771
(declare-var super2_super2__SUPER2_A_IDL_unless.super2_super2__restart_in Bool)
772
(declare-var super2_super2__SUPER2_A_IDL_unless.super2_super2__state_in super2_super2__type)
773
(declare-var super2_super2__SUPER2_A_IDL_unless.super2_super2__restart_act Bool)
774
(declare-var super2_super2__SUPER2_A_IDL_unless.super2_super2__state_act super2_super2__type)
775
(declare-rel super2_super2__SUPER2_A_IDL_unless (Bool super2_super2__type Bool super2_super2__type))
776
(rule (=> 
777
  (and (= super2_super2__SUPER2_A_IDL_unless.super2_super2__state_act super2_super2__SUPER2_A_IDL_unless.super2_super2__state_in)
778
       (= super2_super2__SUPER2_A_IDL_unless.super2_super2__restart_act super2_super2__SUPER2_A_IDL_unless.super2_super2__restart_in)
779
       )
780
  (super2_super2__SUPER2_A_IDL_unless super2_super2__SUPER2_A_IDL_unless.super2_super2__restart_in super2_super2__SUPER2_A_IDL_unless.super2_super2__state_in super2_super2__SUPER2_A_IDL_unless.super2_super2__restart_act super2_super2__SUPER2_A_IDL_unless.super2_super2__state_act)
781
))
782

    
783
; super2_super2__SUPER2_A__TO__C_C1_2_handler_until
784
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_1 Int)
785
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_1 Real)
786
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.super2_super2__restart_in Bool)
787
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.super2_super2__state_in super2_super2__type)
788
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_C_out Int)
789
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_out Int)
790
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_out Real)
791
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_C_3 Int)
792
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_2 Int)
793
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_3 Int)
794
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_2 Real)
795
(declare-rel super2_super2__SUPER2_A__TO__C_C1_2_handler_until (Int Real Bool super2_super2__type Int Int Real))
796
(rule (=> 
797
  (and (= super2_super2__SUPER2_A__TO__C_C1_2_handler_until.super2_super2__state_in POINTSuper2_Super2)
798
       (= super2_super2__SUPER2_A__TO__C_C1_2_handler_until.super2_super2__restart_in true)
799
       (Super2_A_ex super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_1
800
                    false
801
                    super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_2)
802
       (Super2_C_en 1952
803
                    super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_2
804
                    super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_1
805
                    false
806
                    super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_C_3
807
                    super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_3
808
                    super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_2)
809
       (= super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_out super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_2)
810
       (= super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_out super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_3)
811
       (= super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_C_out super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_C_3)
812
       )
813
  (super2_super2__SUPER2_A__TO__C_C1_2_handler_until super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_1 super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_1 super2_super2__SUPER2_A__TO__C_C1_2_handler_until.super2_super2__restart_in super2_super2__SUPER2_A__TO__C_C1_2_handler_until.super2_super2__state_in super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_C_out super2_super2__SUPER2_A__TO__C_C1_2_handler_until.idSuper2_Super2_out super2_super2__SUPER2_A__TO__C_C1_2_handler_until.s_out)
814
))
815

    
816
; super2_super2__SUPER2_A__TO__C_C1_2_unless
817
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__restart_in Bool)
818
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__state_in super2_super2__type)
819
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__restart_act Bool)
820
(declare-var super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__state_act super2_super2__type)
821
(declare-rel super2_super2__SUPER2_A__TO__C_C1_2_unless (Bool super2_super2__type Bool super2_super2__type))
822
(rule (=> 
823
  (and (= super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__state_act super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__state_in)
824
       (= super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__restart_act super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__restart_in)
825
       )
826
  (super2_super2__SUPER2_A__TO__C_C1_2_unless super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__restart_in super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__state_in super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__restart_act super2_super2__SUPER2_A__TO__C_C1_2_unless.super2_super2__state_act)
827
))
828

    
829
; super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until
830
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_1 Int)
831
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_1 Real)
832
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_1 Int)
833
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.super2_super2__restart_in Bool)
834
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.super2_super2__state_in super2_super2__type)
835
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_out Int)
836
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_out Int)
837
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_out Real)
838
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_2 Int)
839
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_2 Int)
840
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_3 Int)
841
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_2 Real)
842
(declare-rel super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until (Int Real Int Bool super2_super2__type Int Int Real))
843
(rule (=> 
844
  (and (= super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.super2_super2__state_in POINTSuper2_Super2)
845
       (= super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.super2_super2__restart_in true)
846
       (Super2_A_ex super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_1
847
                    false
848
                    super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_2)
849
       (Super2_C_en super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_1
850
                    super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_2
851
                    super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_1
852
                    false
853
                    super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_2
854
                    super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_3
855
                    super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_2)
856
       (= super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_out super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_2)
857
       (= super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_out super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_3)
858
       (= super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_out super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_2)
859
       )
860
  (super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_1 super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_1 super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_1 super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.super2_super2__restart_in super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.super2_super2__state_in super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_C_out super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.idSuper2_Super2_out super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until.s_out)
861
))
862

    
863
; super2_super2__SUPER2_A__TO__SUPER2_C_1_unless
864
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__restart_in Bool)
865
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__state_in super2_super2__type)
866
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__restart_act Bool)
867
(declare-var super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__state_act super2_super2__type)
868
(declare-rel super2_super2__SUPER2_A__TO__SUPER2_C_1_unless (Bool super2_super2__type Bool super2_super2__type))
869
(rule (=> 
870
  (and (= super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__state_act super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__state_in)
871
       (= super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__restart_act super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__restart_in)
872
       )
873
  (super2_super2__SUPER2_A__TO__SUPER2_C_1_unless super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__restart_in super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__state_in super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__restart_act super2_super2__SUPER2_A__TO__SUPER2_C_1_unless.super2_super2__state_act)
874
))
875

    
876
; super2_super2__SUPER2_B_IDL_handler_until
877
(declare-var super2_super2__SUPER2_B_IDL_handler_until.idSuper2_Super2_1 Int)
878
(declare-var super2_super2__SUPER2_B_IDL_handler_until.s_1 Real)
879
(declare-var super2_super2__SUPER2_B_IDL_handler_until.idSuper2_C_1 Int)
880
(declare-var super2_super2__SUPER2_B_IDL_handler_until.super2_super2__restart_in Bool)
881
(declare-var super2_super2__SUPER2_B_IDL_handler_until.super2_super2__state_in super2_super2__type)
882
(declare-var super2_super2__SUPER2_B_IDL_handler_until.idSuper2_C_out Int)
883
(declare-var super2_super2__SUPER2_B_IDL_handler_until.idSuper2_Super2_out Int)
884
(declare-var super2_super2__SUPER2_B_IDL_handler_until.s_out Real)
885
(declare-rel super2_super2__SUPER2_B_IDL_handler_until (Int Real Int Bool super2_super2__type Int Int Real))
886
(rule (=> 
887
  (and (= super2_super2__SUPER2_B_IDL_handler_until.super2_super2__state_in POINTSuper2_Super2)
888
       (= super2_super2__SUPER2_B_IDL_handler_until.super2_super2__restart_in true)
889
       (= super2_super2__SUPER2_B_IDL_handler_until.s_out super2_super2__SUPER2_B_IDL_handler_until.s_1)
890
       (= super2_super2__SUPER2_B_IDL_handler_until.idSuper2_Super2_out super2_super2__SUPER2_B_IDL_handler_until.idSuper2_Super2_1)
891
       (= super2_super2__SUPER2_B_IDL_handler_until.idSuper2_C_out super2_super2__SUPER2_B_IDL_handler_until.idSuper2_C_1)
892
       )
893
  (super2_super2__SUPER2_B_IDL_handler_until super2_super2__SUPER2_B_IDL_handler_until.idSuper2_Super2_1 super2_super2__SUPER2_B_IDL_handler_until.s_1 super2_super2__SUPER2_B_IDL_handler_until.idSuper2_C_1 super2_super2__SUPER2_B_IDL_handler_until.super2_super2__restart_in super2_super2__SUPER2_B_IDL_handler_until.super2_super2__state_in super2_super2__SUPER2_B_IDL_handler_until.idSuper2_C_out super2_super2__SUPER2_B_IDL_handler_until.idSuper2_Super2_out super2_super2__SUPER2_B_IDL_handler_until.s_out)
894
))
895

    
896
; super2_super2__SUPER2_B_IDL_unless
897
(declare-var super2_super2__SUPER2_B_IDL_unless.super2_super2__restart_in Bool)
898
(declare-var super2_super2__SUPER2_B_IDL_unless.super2_super2__state_in super2_super2__type)
899
(declare-var super2_super2__SUPER2_B_IDL_unless.super2_super2__restart_act Bool)
900
(declare-var super2_super2__SUPER2_B_IDL_unless.super2_super2__state_act super2_super2__type)
901
(declare-rel super2_super2__SUPER2_B_IDL_unless (Bool super2_super2__type Bool super2_super2__type))
902
(rule (=> 
903
  (and (= super2_super2__SUPER2_B_IDL_unless.super2_super2__state_act super2_super2__SUPER2_B_IDL_unless.super2_super2__state_in)
904
       (= super2_super2__SUPER2_B_IDL_unless.super2_super2__restart_act super2_super2__SUPER2_B_IDL_unless.super2_super2__restart_in)
905
       )
906
  (super2_super2__SUPER2_B_IDL_unless super2_super2__SUPER2_B_IDL_unless.super2_super2__restart_in super2_super2__SUPER2_B_IDL_unless.super2_super2__state_in super2_super2__SUPER2_B_IDL_unless.super2_super2__restart_act super2_super2__SUPER2_B_IDL_unless.super2_super2__state_act)
907
))
908

    
909
; super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until
910
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_1 Int)
911
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_1 Real)
912
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_C_1 Int)
913
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.super2_super2__restart_in Bool)
914
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.super2_super2__state_in super2_super2__type)
915
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_C_out Int)
916
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_out Int)
917
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_out Real)
918
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_2 Int)
919
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_3 Int)
920
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_2 Real)
921
(declare-rel super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until (Int Real Int Bool super2_super2__type Int Int Real))
922
(rule (=> 
923
  (and (= super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.super2_super2__state_in POINTSuper2_Super2)
924
       (= super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.super2_super2__restart_in true)
925
       (Super2_B_ex super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_1
926
                    false
927
                    super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_2)
928
       (Super2_A_en super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_2
929
                    super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_1
930
                    false
931
                    super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_3
932
                    super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_2)
933
       (= super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_out super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_2)
934
       (= super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_out super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_3)
935
       (= super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_C_out super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_C_1)
936
       )
937
  (super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_1 super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_1 super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_C_1 super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.super2_super2__restart_in super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.super2_super2__state_in super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_C_out super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.idSuper2_Super2_out super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until.s_out)
938
))
939

    
940
; super2_super2__SUPER2_B__TO__SUPER2_A_1_unless
941
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__restart_in Bool)
942
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__state_in super2_super2__type)
943
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__restart_act Bool)
944
(declare-var super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__state_act super2_super2__type)
945
(declare-rel super2_super2__SUPER2_B__TO__SUPER2_A_1_unless (Bool super2_super2__type Bool super2_super2__type))
946
(rule (=> 
947
  (and (= super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__state_act super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__state_in)
948
       (= super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__restart_act super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__restart_in)
949
       )
950
  (super2_super2__SUPER2_B__TO__SUPER2_A_1_unless super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__restart_in super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__state_in super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__restart_act super2_super2__SUPER2_B__TO__SUPER2_A_1_unless.super2_super2__state_act)
951
))
952

    
953
; super2_super2__SUPER2_C_IDL_handler_until
954
(declare-var super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_1 Int)
955
(declare-var super2_super2__SUPER2_C_IDL_handler_until.s_1 Real)
956
(declare-var super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_1 Int)
957
(declare-var super2_super2__SUPER2_C_IDL_handler_until.E Bool)
958
(declare-var super2_super2__SUPER2_C_IDL_handler_until.super2_super2__restart_in Bool)
959
(declare-var super2_super2__SUPER2_C_IDL_handler_until.super2_super2__state_in super2_super2__type)
960
(declare-var super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_out Int)
961
(declare-var super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_out Int)
962
(declare-var super2_super2__SUPER2_C_IDL_handler_until.s_out Real)
963
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
964
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
965
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
966
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
967
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
968
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
969
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
970
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
971
(declare-var super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
972
(declare-var super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_2 Int)
973
(declare-var super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_2 Int)
974
(declare-var super2_super2__SUPER2_C_IDL_handler_until.s_2 Real)
975
(declare-rel super2_super2__SUPER2_C_IDL_handler_until_reset (Bool super2_c__type Bool Bool super2_c__type Bool))
976
(declare-rel super2_super2__SUPER2_C_IDL_handler_until_step (Int Real Int Bool Bool super2_super2__type Int Int Real Bool super2_c__type Bool Bool super2_c__type Bool))
977

    
978
(rule (=> 
979
  (and 
980
       
981
       (Super2_C_node_reset super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
982
                            super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
983
                            super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
984
                            super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
985
                            super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
986
                            super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m)
987
  )
988
  (super2_super2__SUPER2_C_IDL_handler_until_reset super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
989
                                                   super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
990
                                                   super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
991
                                                   super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
992
                                                   super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
993
                                                   super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m)
994
))
995

    
996
(rule (=> 
997
  (and (= super2_super2__SUPER2_C_IDL_handler_until.super2_super2__state_in POINTSuper2_Super2)
998
       (= super2_super2__SUPER2_C_IDL_handler_until.super2_super2__restart_in true)
999
       (and (= super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
1000
            (= super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
1001
            (= super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
1002
            )
1003
       (Super2_C_node_step super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_1
1004
                           super2_super2__SUPER2_C_IDL_handler_until.s_1
1005
                           super2_super2__SUPER2_C_IDL_handler_until.E
1006
                           super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_1
1007
                           super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_2
1008
                           super2_super2__SUPER2_C_IDL_handler_until.s_2
1009
                           super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_2
1010
                           super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1011
                           super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1012
                           super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1013
                           super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1014
                           super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1015
                           super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x)
1016
       (= super2_super2__SUPER2_C_IDL_handler_until.s_out super2_super2__SUPER2_C_IDL_handler_until.s_2)
1017
       (= super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_out super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_2)
1018
       (= super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_out super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_2)
1019
       )
1020
  (super2_super2__SUPER2_C_IDL_handler_until_step super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_1
1021
                                                  super2_super2__SUPER2_C_IDL_handler_until.s_1
1022
                                                  super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_1
1023
                                                  super2_super2__SUPER2_C_IDL_handler_until.E
1024
                                                  super2_super2__SUPER2_C_IDL_handler_until.super2_super2__restart_in
1025
                                                  super2_super2__SUPER2_C_IDL_handler_until.super2_super2__state_in
1026
                                                  super2_super2__SUPER2_C_IDL_handler_until.idSuper2_C_out
1027
                                                  super2_super2__SUPER2_C_IDL_handler_until.idSuper2_Super2_out
1028
                                                  super2_super2__SUPER2_C_IDL_handler_until.s_out
1029
                                                  super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1030
                                                  super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1031
                                                  super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1032
                                                  super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1033
                                                  super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1034
                                                  super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x)
1035
))
1036

    
1037
; super2_super2__SUPER2_C_IDL_unless
1038
(declare-var super2_super2__SUPER2_C_IDL_unless.super2_super2__restart_in Bool)
1039
(declare-var super2_super2__SUPER2_C_IDL_unless.super2_super2__state_in super2_super2__type)
1040
(declare-var super2_super2__SUPER2_C_IDL_unless.super2_super2__restart_act Bool)
1041
(declare-var super2_super2__SUPER2_C_IDL_unless.super2_super2__state_act super2_super2__type)
1042
(declare-rel super2_super2__SUPER2_C_IDL_unless (Bool super2_super2__type Bool super2_super2__type))
1043
(rule (=> 
1044
  (and (= super2_super2__SUPER2_C_IDL_unless.super2_super2__state_act super2_super2__SUPER2_C_IDL_unless.super2_super2__state_in)
1045
       (= super2_super2__SUPER2_C_IDL_unless.super2_super2__restart_act super2_super2__SUPER2_C_IDL_unless.super2_super2__restart_in)
1046
       )
1047
  (super2_super2__SUPER2_C_IDL_unless super2_super2__SUPER2_C_IDL_unless.super2_super2__restart_in super2_super2__SUPER2_C_IDL_unless.super2_super2__state_in super2_super2__SUPER2_C_IDL_unless.super2_super2__restart_act super2_super2__SUPER2_C_IDL_unless.super2_super2__state_act)
1048
))
1049

    
1050
; super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until
1051
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_1 Int)
1052
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_1 Real)
1053
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_1 Int)
1054
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.super2_super2__restart_in Bool)
1055
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.super2_super2__state_in super2_super2__type)
1056
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_out Int)
1057
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_out Int)
1058
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_out Real)
1059
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_2 Int)
1060
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_2 Int)
1061
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_3 Int)
1062
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_2 Real)
1063
(declare-rel super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until (Int Real Int Bool super2_super2__type Int Int Real))
1064
(rule (=> 
1065
  (and (= super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.super2_super2__state_in POINTSuper2_Super2)
1066
       (= super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.super2_super2__restart_in true)
1067
       (Super2_C_ex super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_1
1068
                    super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_1
1069
                    false
1070
                    super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_2
1071
                    super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_2)
1072
       (Super2_B_en super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_2
1073
                    super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_1
1074
                    false
1075
                    super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_3
1076
                    super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_2)
1077
       (= super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_out super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_2)
1078
       (= super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_out super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_3)
1079
       (= super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_out super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_2)
1080
       )
1081
  (super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_1 super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_1 super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_1 super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.super2_super2__restart_in super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.super2_super2__state_in super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_C_out super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.idSuper2_Super2_out super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until.s_out)
1082
))
1083

    
1084
; super2_super2__SUPER2_C__TO__SUPER2_B_1_unless
1085
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__restart_in Bool)
1086
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__state_in super2_super2__type)
1087
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__restart_act Bool)
1088
(declare-var super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__state_act super2_super2__type)
1089
(declare-rel super2_super2__SUPER2_C__TO__SUPER2_B_1_unless (Bool super2_super2__type Bool super2_super2__type))
1090
(rule (=> 
1091
  (and (= super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__state_act super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__state_in)
1092
       (= super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__restart_act super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__restart_in)
1093
       )
1094
  (super2_super2__SUPER2_C__TO__SUPER2_B_1_unless super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__restart_in super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__state_in super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__restart_act super2_super2__SUPER2_C__TO__SUPER2_B_1_unless.super2_super2__state_act)
1095
))
1096

    
1097
; Super2_Super2_node
1098
(declare-var Super2_Super2_node.idSuper2_Super2_1 Int)
1099
(declare-var Super2_Super2_node.s_1 Real)
1100
(declare-var Super2_Super2_node.F Bool)
1101
(declare-var Super2_Super2_node.idSuper2_C_1 Int)
1102
(declare-var Super2_Super2_node.E Bool)
1103
(declare-var Super2_Super2_node.G Bool)
1104
(declare-var Super2_Super2_node.idSuper2_Super2 Int)
1105
(declare-var Super2_Super2_node.s Real)
1106
(declare-var Super2_Super2_node.idSuper2_C Int)
1107
(declare-var Super2_Super2_node.__Super2_Super2_node_65_c Bool)
1108
(declare-var Super2_Super2_node.__Super2_Super2_node_66_c super2_super2__type)
1109
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
1110
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
1111
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
1112
(declare-var Super2_Super2_node.ni_7._arrow._first_c Bool)
1113
(declare-var Super2_Super2_node.__Super2_Super2_node_65_m Bool)
1114
(declare-var Super2_Super2_node.__Super2_Super2_node_66_m super2_super2__type)
1115
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
1116
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
1117
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
1118
(declare-var Super2_Super2_node.ni_7._arrow._first_m Bool)
1119
(declare-var Super2_Super2_node.__Super2_Super2_node_65_x Bool)
1120
(declare-var Super2_Super2_node.__Super2_Super2_node_66_x super2_super2__type)
1121
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
1122
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
1123
(declare-var Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
1124
(declare-var Super2_Super2_node.ni_7._arrow._first_x Bool)
1125
(declare-var Super2_Super2_node.__Super2_Super2_node_1 Bool)
1126
(declare-var Super2_Super2_node.__Super2_Super2_node_10 super2_super2__type)
1127
(declare-var Super2_Super2_node.__Super2_Super2_node_11 Bool)
1128
(declare-var Super2_Super2_node.__Super2_Super2_node_12 super2_super2__type)
1129
(declare-var Super2_Super2_node.__Super2_Super2_node_13 Bool)
1130
(declare-var Super2_Super2_node.__Super2_Super2_node_14 super2_super2__type)
1131
(declare-var Super2_Super2_node.__Super2_Super2_node_15 Bool)
1132
(declare-var Super2_Super2_node.__Super2_Super2_node_16 super2_super2__type)
1133
(declare-var Super2_Super2_node.__Super2_Super2_node_17 Bool)
1134
(declare-var Super2_Super2_node.__Super2_Super2_node_18 super2_super2__type)
1135
(declare-var Super2_Super2_node.__Super2_Super2_node_19 Bool)
1136
(declare-var Super2_Super2_node.__Super2_Super2_node_2 super2_super2__type)
1137
(declare-var Super2_Super2_node.__Super2_Super2_node_20 super2_super2__type)
1138
(declare-var Super2_Super2_node.__Super2_Super2_node_21 Int)
1139
(declare-var Super2_Super2_node.__Super2_Super2_node_22 Int)
1140
(declare-var Super2_Super2_node.__Super2_Super2_node_23 Real)
1141
(declare-var Super2_Super2_node.__Super2_Super2_node_24 Bool)
1142
(declare-var Super2_Super2_node.__Super2_Super2_node_25 super2_super2__type)
1143
(declare-var Super2_Super2_node.__Super2_Super2_node_26 Int)
1144
(declare-var Super2_Super2_node.__Super2_Super2_node_27 Int)
1145
(declare-var Super2_Super2_node.__Super2_Super2_node_28 Real)
1146
(declare-var Super2_Super2_node.__Super2_Super2_node_29 Bool)
1147
(declare-var Super2_Super2_node.__Super2_Super2_node_3 Bool)
1148
(declare-var Super2_Super2_node.__Super2_Super2_node_30 super2_super2__type)
1149
(declare-var Super2_Super2_node.__Super2_Super2_node_31 Int)
1150
(declare-var Super2_Super2_node.__Super2_Super2_node_32 Int)
1151
(declare-var Super2_Super2_node.__Super2_Super2_node_33 Real)
1152
(declare-var Super2_Super2_node.__Super2_Super2_node_34 Bool)
1153
(declare-var Super2_Super2_node.__Super2_Super2_node_35 super2_super2__type)
1154
(declare-var Super2_Super2_node.__Super2_Super2_node_36 Int)
1155
(declare-var Super2_Super2_node.__Super2_Super2_node_37 Int)
1156
(declare-var Super2_Super2_node.__Super2_Super2_node_38 Real)
1157
(declare-var Super2_Super2_node.__Super2_Super2_node_39 Bool)
1158
(declare-var Super2_Super2_node.__Super2_Super2_node_4 super2_super2__type)
1159
(declare-var Super2_Super2_node.__Super2_Super2_node_40 super2_super2__type)
1160
(declare-var Super2_Super2_node.__Super2_Super2_node_41 Int)
1161
(declare-var Super2_Super2_node.__Super2_Super2_node_42 Int)
1162
(declare-var Super2_Super2_node.__Super2_Super2_node_43 Real)
1163
(declare-var Super2_Super2_node.__Super2_Super2_node_44 Bool)
1164
(declare-var Super2_Super2_node.__Super2_Super2_node_45 super2_super2__type)
1165
(declare-var Super2_Super2_node.__Super2_Super2_node_46 Int)
1166
(declare-var Super2_Super2_node.__Super2_Super2_node_47 Int)
1167
(declare-var Super2_Super2_node.__Super2_Super2_node_48 Real)
1168
(declare-var Super2_Super2_node.__Super2_Super2_node_49 Bool)
1169
(declare-var Super2_Super2_node.__Super2_Super2_node_5 Bool)
1170
(declare-var Super2_Super2_node.__Super2_Super2_node_50 super2_super2__type)
1171
(declare-var Super2_Super2_node.__Super2_Super2_node_51 Int)
1172
(declare-var Super2_Super2_node.__Super2_Super2_node_52 Int)
1173
(declare-var Super2_Super2_node.__Super2_Super2_node_53 Real)
1174
(declare-var Super2_Super2_node.__Super2_Super2_node_54 Bool)
1175
(declare-var Super2_Super2_node.__Super2_Super2_node_55 super2_super2__type)
1176
(declare-var Super2_Super2_node.__Super2_Super2_node_56 Int)
1177
(declare-var Super2_Super2_node.__Super2_Super2_node_57 Int)
1178
(declare-var Super2_Super2_node.__Super2_Super2_node_58 Real)
1179
(declare-var Super2_Super2_node.__Super2_Super2_node_59 Bool)
1180
(declare-var Super2_Super2_node.__Super2_Super2_node_6 super2_super2__type)
1181
(declare-var Super2_Super2_node.__Super2_Super2_node_60 super2_super2__type)
1182
(declare-var Super2_Super2_node.__Super2_Super2_node_61 Int)
1183
(declare-var Super2_Super2_node.__Super2_Super2_node_62 Int)
1184
(declare-var Super2_Super2_node.__Super2_Super2_node_63 Real)
1185
(declare-var Super2_Super2_node.__Super2_Super2_node_64 Bool)
1186
(declare-var Super2_Super2_node.__Super2_Super2_node_7 Bool)
1187
(declare-var Super2_Super2_node.__Super2_Super2_node_8 super2_super2__type)
1188
(declare-var Super2_Super2_node.__Super2_Super2_node_9 Bool)
1189
(declare-var Super2_Super2_node.super2_super2__next_restart_in Bool)
1190
(declare-var Super2_Super2_node.super2_super2__next_state_in super2_super2__type)
1191
(declare-var Super2_Super2_node.super2_super2__restart_act Bool)
1192
(declare-var Super2_Super2_node.super2_super2__restart_in Bool)
1193
(declare-var Super2_Super2_node.super2_super2__state_act super2_super2__type)
1194
(declare-var Super2_Super2_node.super2_super2__state_in super2_super2__type)
1195
(declare-rel Super2_Super2_node_reset (Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool))
1196
(declare-rel Super2_Super2_node_step (Int Real Bool Int Bool Bool Int Real Int Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool))
1197

    
1198
(rule (=> 
1199
  (and 
1200
       (= Super2_Super2_node.__Super2_Super2_node_65_m Super2_Super2_node.__Super2_Super2_node_65_c)
1201
       (= Super2_Super2_node.__Super2_Super2_node_66_m Super2_Super2_node.__Super2_Super2_node_66_c)
1202
       (= Super2_Super2_node.ni_7._arrow._first_m true)
1203
       (super2_super2__SUPER2_C_IDL_handler_until_reset Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1204
                                                        Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1205
                                                        Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1206
                                                        Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1207
                                                        Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1208
                                                        Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m)
1209
  )
1210
  (Super2_Super2_node_reset Super2_Super2_node.__Super2_Super2_node_65_c
1211
                            Super2_Super2_node.__Super2_Super2_node_66_c
1212
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1213
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1214
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1215
                            Super2_Super2_node.ni_7._arrow._first_c
1216
                            Super2_Super2_node.__Super2_Super2_node_65_m
1217
                            Super2_Super2_node.__Super2_Super2_node_66_m
1218
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1219
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1220
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1221
                            Super2_Super2_node.ni_7._arrow._first_m)
1222
))
1223

    
1224
(rule (=> 
1225
  (and (= Super2_Super2_node.ni_7._arrow._first_m Super2_Super2_node.ni_7._arrow._first_c)
1226
       (and (= Super2_Super2_node.__Super2_Super2_node_64 (ite Super2_Super2_node.ni_7._arrow._first_m true false))
1227
            (= Super2_Super2_node.ni_7._arrow._first_x false))
1228
       (and (or (not (= Super2_Super2_node.__Super2_Super2_node_64 false))
1229
               (and (= Super2_Super2_node.super2_super2__state_in Super2_Super2_node.__Super2_Super2_node_66_c)
1230
                    (= Super2_Super2_node.super2_super2__restart_in Super2_Super2_node.__Super2_Super2_node_65_c)
1231
                    ))
1232
            (or (not (= Super2_Super2_node.__Super2_Super2_node_64 true))
1233
               (and (= Super2_Super2_node.super2_super2__state_in POINTSuper2_Super2)
1234
                    (= Super2_Super2_node.super2_super2__restart_in false)
1235
                    ))
1236
       )
1237
       (and (or (not (= Super2_Super2_node.super2_super2__state_in POINTSuper2_Super2))
1238
               (and (super2_super2__POINTSuper2_Super2_unless Super2_Super2_node.super2_super2__restart_in
1239
                                                              Super2_Super2_node.super2_super2__state_in
1240
                                                              Super2_Super2_node.idSuper2_Super2_1
1241
                                                              Super2_Super2_node.F
1242
                                                              Super2_Super2_node.E
1243
                                                              Super2_Super2_node.G
1244
                                                              Super2_Super2_node.__Super2_Super2_node_17
1245
                                                              Super2_Super2_node.__Super2_Super2_node_18)
1246
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_18)
1247
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_17)
1248
                    ))
1249
            (or (not (= Super2_Super2_node.super2_super2__state_in POINT__TO__SUPER2_A_1))
1250
               (and (super2_super2__POINT__TO__SUPER2_A_1_unless Super2_Super2_node.super2_super2__restart_in
1251
                                                                 Super2_Super2_node.super2_super2__state_in
1252
                                                                 Super2_Super2_node.__Super2_Super2_node_15
1253
                                                                 Super2_Super2_node.__Super2_Super2_node_16)
1254
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_16)
1255
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_15)
1256
                    ))
1257
            (or (not (= Super2_Super2_node.super2_super2__state_in SUPER2_A_IDL))
1258
               (and (super2_super2__SUPER2_A_IDL_unless Super2_Super2_node.super2_super2__restart_in
1259
                                                        Super2_Super2_node.super2_super2__state_in
1260
                                                        Super2_Super2_node.__Super2_Super2_node_5
1261
                                                        Super2_Super2_node.__Super2_Super2_node_6)
1262
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_6)
1263
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_5)
1264
                    ))
1265
            (or (not (= Super2_Super2_node.super2_super2__state_in SUPER2_A__TO__C_C1_2))
1266
               (and (super2_super2__SUPER2_A__TO__C_C1_2_unless Super2_Super2_node.super2_super2__restart_in
1267
                                                                Super2_Super2_node.super2_super2__state_in
1268
                                                                Super2_Super2_node.__Super2_Super2_node_11
1269
                                                                Super2_Super2_node.__Super2_Super2_node_12)
1270
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_12)
1271
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_11)
1272
                    ))
1273
            (or (not (= Super2_Super2_node.super2_super2__state_in SUPER2_A__TO__SUPER2_C_1))
1274
               (and (super2_super2__SUPER2_A__TO__SUPER2_C_1_unless Super2_Super2_node.super2_super2__restart_in
1275
                                                                    Super2_Super2_node.super2_super2__state_in
1276
                                                                    Super2_Super2_node.__Super2_Super2_node_13
1277
                                                                    Super2_Super2_node.__Super2_Super2_node_14)
1278
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_14)
1279
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_13)
1280
                    ))
1281
            (or (not (= Super2_Super2_node.super2_super2__state_in SUPER2_B_IDL))
1282
               (and (super2_super2__SUPER2_B_IDL_unless Super2_Super2_node.super2_super2__restart_in
1283
                                                        Super2_Super2_node.super2_super2__state_in
1284
                                                        Super2_Super2_node.__Super2_Super2_node_3
1285
                                                        Super2_Super2_node.__Super2_Super2_node_4)
1286
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_4)
1287
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_3)
1288
                    ))
1289
            (or (not (= Super2_Super2_node.super2_super2__state_in SUPER2_B__TO__SUPER2_A_1))
1290
               (and (super2_super2__SUPER2_B__TO__SUPER2_A_1_unless Super2_Super2_node.super2_super2__restart_in
1291
                                                                    Super2_Super2_node.super2_super2__state_in
1292
                                                                    Super2_Super2_node.__Super2_Super2_node_9
1293
                                                                    Super2_Super2_node.__Super2_Super2_node_10)
1294
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_10)
1295
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_9)
1296
                    ))
1297
            (or (not (= Super2_Super2_node.super2_super2__state_in SUPER2_C_IDL))
1298
               (and (super2_super2__SUPER2_C_IDL_unless Super2_Super2_node.super2_super2__restart_in
1299
                                                        Super2_Super2_node.super2_super2__state_in
1300
                                                        Super2_Super2_node.__Super2_Super2_node_1
1301
                                                        Super2_Super2_node.__Super2_Super2_node_2)
1302
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_2)
1303
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_1)
1304
                    ))
1305
            (or (not (= Super2_Super2_node.super2_super2__state_in SUPER2_C__TO__SUPER2_B_1))
1306
               (and (super2_super2__SUPER2_C__TO__SUPER2_B_1_unless Super2_Super2_node.super2_super2__restart_in
1307
                                                                    Super2_Super2_node.super2_super2__state_in
1308
                                                                    Super2_Super2_node.__Super2_Super2_node_7
1309
                                                                    Super2_Super2_node.__Super2_Super2_node_8)
1310
                    (= Super2_Super2_node.super2_super2__state_act Super2_Super2_node.__Super2_Super2_node_8)
1311
                    (= Super2_Super2_node.super2_super2__restart_act Super2_Super2_node.__Super2_Super2_node_7)
1312
                    ))
1313
       )
1314
       (and (or (not (= Super2_Super2_node.super2_super2__state_act POINTSuper2_Super2))
1315
               (and (super2_super2__POINTSuper2_Super2_handler_until 
1316
                    Super2_Super2_node.idSuper2_Super2_1
1317
                    Super2_Super2_node.s_1
1318
                    Super2_Super2_node.idSuper2_C_1
1319
                    Super2_Super2_node.__Super2_Super2_node_59
1320
                    Super2_Super2_node.__Super2_Super2_node_60
1321
                    Super2_Super2_node.__Super2_Super2_node_61
1322
                    Super2_Super2_node.__Super2_Super2_node_62
1323
                    Super2_Super2_node.__Super2_Super2_node_63)
1324
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_60)
1325
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_59)
1326
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_63)
1327
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_62)
1328
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_61)
1329
                    ))
1330
            (or (not (= Super2_Super2_node.super2_super2__state_act POINT__TO__SUPER2_A_1))
1331
               (and (super2_super2__POINT__TO__SUPER2_A_1_handler_until 
1332
                    Super2_Super2_node.idSuper2_Super2_1
1333
                    Super2_Super2_node.s_1
1334
                    Super2_Super2_node.idSuper2_C_1
1335
                    Super2_Super2_node.__Super2_Super2_node_54
1336
                    Super2_Super2_node.__Super2_Super2_node_55
1337
                    Super2_Super2_node.__Super2_Super2_node_56
1338
                    Super2_Super2_node.__Super2_Super2_node_57
1339
                    Super2_Super2_node.__Super2_Super2_node_58)
1340
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_55)
1341
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_54)
1342
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_58)
1343
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_57)
1344
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_56)
1345
                    ))
1346
            (or (not (= Super2_Super2_node.super2_super2__state_act SUPER2_A_IDL))
1347
               (and (super2_super2__SUPER2_A_IDL_handler_until Super2_Super2_node.idSuper2_Super2_1
1348
                                                               Super2_Super2_node.s_1
1349
                                                               Super2_Super2_node.idSuper2_C_1
1350
                                                               Super2_Super2_node.__Super2_Super2_node_29
1351
                                                               Super2_Super2_node.__Super2_Super2_node_30
1352
                                                               Super2_Super2_node.__Super2_Super2_node_31
1353
                                                               Super2_Super2_node.__Super2_Super2_node_32
1354
                                                               Super2_Super2_node.__Super2_Super2_node_33)
1355
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_30)
1356
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_29)
1357
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_33)
1358
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_32)
1359
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_31)
1360
                    ))
1361
            (or (not (= Super2_Super2_node.super2_super2__state_act SUPER2_A__TO__C_C1_2))
1362
               (and (super2_super2__SUPER2_A__TO__C_C1_2_handler_until 
1363
                    Super2_Super2_node.idSuper2_Super2_1
1364
                    Super2_Super2_node.s_1
1365
                    Super2_Super2_node.__Super2_Super2_node_44
1366
                    Super2_Super2_node.__Super2_Super2_node_45
1367
                    Super2_Super2_node.__Super2_Super2_node_46
1368
                    Super2_Super2_node.__Super2_Super2_node_47
1369
                    Super2_Super2_node.__Super2_Super2_node_48)
1370
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_45)
1371
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_44)
1372
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_48)
1373
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_47)
1374
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_46)
1375
                    ))
1376
            (or (not (= Super2_Super2_node.super2_super2__state_act SUPER2_A__TO__SUPER2_C_1))
1377
               (and (super2_super2__SUPER2_A__TO__SUPER2_C_1_handler_until 
1378
                    Super2_Super2_node.idSuper2_Super2_1
1379
                    Super2_Super2_node.s_1
1380
                    Super2_Super2_node.idSuper2_C_1
1381
                    Super2_Super2_node.__Super2_Super2_node_49
1382
                    Super2_Super2_node.__Super2_Super2_node_50
1383
                    Super2_Super2_node.__Super2_Super2_node_51
1384
                    Super2_Super2_node.__Super2_Super2_node_52
1385
                    Super2_Super2_node.__Super2_Super2_node_53)
1386
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_50)
1387
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_49)
1388
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_53)
1389
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_52)
1390
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_51)
1391
                    ))
1392
            (or (not (= Super2_Super2_node.super2_super2__state_act SUPER2_B_IDL))
1393
               (and (super2_super2__SUPER2_B_IDL_handler_until Super2_Super2_node.idSuper2_Super2_1
1394
                                                               Super2_Super2_node.s_1
1395
                                                               Super2_Super2_node.idSuper2_C_1
1396
                                                               Super2_Super2_node.__Super2_Super2_node_24
1397
                                                               Super2_Super2_node.__Super2_Super2_node_25
1398
                                                               Super2_Super2_node.__Super2_Super2_node_26
1399
                                                               Super2_Super2_node.__Super2_Super2_node_27
1400
                                                               Super2_Super2_node.__Super2_Super2_node_28)
1401
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_25)
1402
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_24)
1403
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_28)
1404
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_27)
1405
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_26)
1406
                    ))
1407
            (or (not (= Super2_Super2_node.super2_super2__state_act SUPER2_B__TO__SUPER2_A_1))
1408
               (and (super2_super2__SUPER2_B__TO__SUPER2_A_1_handler_until 
1409
                    Super2_Super2_node.idSuper2_Super2_1
1410
                    Super2_Super2_node.s_1
1411
                    Super2_Super2_node.idSuper2_C_1
1412
                    Super2_Super2_node.__Super2_Super2_node_39
1413
                    Super2_Super2_node.__Super2_Super2_node_40
1414
                    Super2_Super2_node.__Super2_Super2_node_41
1415
                    Super2_Super2_node.__Super2_Super2_node_42
1416
                    Super2_Super2_node.__Super2_Super2_node_43)
1417
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_40)
1418
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_39)
1419
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_43)
1420
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_42)
1421
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_41)
1422
                    ))
1423
            (or (not (= Super2_Super2_node.super2_super2__state_act SUPER2_C_IDL))
1424
               (and (and (or (not (= Super2_Super2_node.super2_super2__restart_act true))
1425
                            (super2_super2__SUPER2_C_IDL_handler_until_reset 
1426
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1427
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1428
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1429
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1430
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1431
                            Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m))
1432
                         (or (not (= Super2_Super2_node.super2_super2__restart_act false))
1433
                            (and (= Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
1434
                                 (= Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
1435
                                 (= Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
1436
                                 )
1437
                            )
1438
                    )
1439
                    (and (= Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
1440
                         (= Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
1441
                         (= Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
1442
                         )
1443
                    (super2_super2__SUPER2_C_IDL_handler_until_step Super2_Super2_node.idSuper2_Super2_1
1444
                                                                    Super2_Super2_node.s_1
1445
                                                                    Super2_Super2_node.idSuper2_C_1
1446
                                                                    Super2_Super2_node.E
1447
                                                                    Super2_Super2_node.__Super2_Super2_node_19
1448
                                                                    Super2_Super2_node.__Super2_Super2_node_20
1449
                                                                    Super2_Super2_node.__Super2_Super2_node_21
1450
                                                                    Super2_Super2_node.__Super2_Super2_node_22
1451
                                                                    Super2_Super2_node.__Super2_Super2_node_23
1452
                                                                    Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1453
                                                                    Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1454
                                                                    Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1455
                                                                    Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1456
                                                                    Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1457
                                                                    Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x)
1458
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_20)
1459
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_19)
1460
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_23)
1461
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_22)
1462
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_21)
1463
                    ))
1464
            (or (not (= Super2_Super2_node.super2_super2__state_act SUPER2_C__TO__SUPER2_B_1))
1465
               (and (super2_super2__SUPER2_C__TO__SUPER2_B_1_handler_until 
1466
                    Super2_Super2_node.idSuper2_Super2_1
1467
                    Super2_Super2_node.s_1
1468
                    Super2_Super2_node.idSuper2_C_1
1469
                    Super2_Super2_node.__Super2_Super2_node_34
1470
                    Super2_Super2_node.__Super2_Super2_node_35
1471
                    Super2_Super2_node.__Super2_Super2_node_36
1472
                    Super2_Super2_node.__Super2_Super2_node_37
1473
                    Super2_Super2_node.__Super2_Super2_node_38)
1474
                    (= Super2_Super2_node.super2_super2__next_state_in Super2_Super2_node.__Super2_Super2_node_35)
1475
                    (= Super2_Super2_node.super2_super2__next_restart_in Super2_Super2_node.__Super2_Super2_node_34)
1476
                    (= Super2_Super2_node.s Super2_Super2_node.__Super2_Super2_node_38)
1477
                    (= Super2_Super2_node.idSuper2_Super2 Super2_Super2_node.__Super2_Super2_node_37)
1478
                    (= Super2_Super2_node.idSuper2_C Super2_Super2_node.__Super2_Super2_node_36)
1479
                    ))
1480
       )
1481
       (= Super2_Super2_node.__Super2_Super2_node_66_x Super2_Super2_node.super2_super2__next_state_in)
1482
       (= Super2_Super2_node.__Super2_Super2_node_65_x Super2_Super2_node.super2_super2__next_restart_in)
1483
       )
1484
  (Super2_Super2_node_step Super2_Super2_node.idSuper2_Super2_1
1485
                           Super2_Super2_node.s_1
1486
                           Super2_Super2_node.F
1487
                           Super2_Super2_node.idSuper2_C_1
1488
                           Super2_Super2_node.E
1489
                           Super2_Super2_node.G
1490
                           Super2_Super2_node.idSuper2_Super2
1491
                           Super2_Super2_node.s
1492
                           Super2_Super2_node.idSuper2_C
1493
                           Super2_Super2_node.__Super2_Super2_node_65_c
1494
                           Super2_Super2_node.__Super2_Super2_node_66_c
1495
                           Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1496
                           Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1497
                           Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1498
                           Super2_Super2_node.ni_7._arrow._first_c
1499
                           Super2_Super2_node.__Super2_Super2_node_65_x
1500
                           Super2_Super2_node.__Super2_Super2_node_66_x
1501
                           Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1502
                           Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1503
                           Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
1504
                           Super2_Super2_node.ni_7._arrow._first_x)
1505
))
1506

    
1507
; Super2_Super2
1508
(declare-var Super2_Super2.x Int)
1509
(declare-var Super2_Super2.E Bool)
1510
(declare-var Super2_Super2.F Bool)
1511
(declare-var Super2_Super2.G Bool)
1512
(declare-var Super2_Super2.s Real)
1513
(declare-var Super2_Super2.__Super2_Super2_11_c Int)
1514
(declare-var Super2_Super2.__Super2_Super2_12_c Int)
1515
(declare-var Super2_Super2.__Super2_Super2_13_c Real)
1516
(declare-var Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c Bool)
1517
(declare-var Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c super2_super2__type)
1518
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
1519
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
1520
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
1521
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c Bool)
1522
(declare-var Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c Bool)
1523
(declare-var Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c super2_super2__type)
1524
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
1525
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
1526
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
1527
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c Bool)
1528
(declare-var Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c Bool)
1529
(declare-var Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c super2_super2__type)
1530
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
1531
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
1532
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
1533
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c Bool)
1534
(declare-var Super2_Super2.ni_5._arrow._first_c Bool)
1535
(declare-var Super2_Super2.__Super2_Super2_11_m Int)
1536
(declare-var Super2_Super2.__Super2_Super2_12_m Int)
1537
(declare-var Super2_Super2.__Super2_Super2_13_m Real)
1538
(declare-var Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m Bool)
1539
(declare-var Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m super2_super2__type)
1540
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
1541
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
1542
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
1543
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m Bool)
1544
(declare-var Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m Bool)
1545
(declare-var Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m super2_super2__type)
1546
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
1547
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
1548
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
1549
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m Bool)
1550
(declare-var Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m Bool)
1551
(declare-var Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m super2_super2__type)
1552
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
1553
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
1554
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
1555
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m Bool)
1556
(declare-var Super2_Super2.ni_5._arrow._first_m Bool)
1557
(declare-var Super2_Super2.__Super2_Super2_11_x Int)
1558
(declare-var Super2_Super2.__Super2_Super2_12_x Int)
1559
(declare-var Super2_Super2.__Super2_Super2_13_x Real)
1560
(declare-var Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_x Bool)
1561
(declare-var Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_x super2_super2__type)
1562
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
1563
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
1564
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
1565
(declare-var Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_x Bool)
1566
(declare-var Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_x Bool)
1567
(declare-var Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_x super2_super2__type)
1568
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
1569
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
1570
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
1571
(declare-var Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_x Bool)
1572
(declare-var Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_x Bool)
1573
(declare-var Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_x super2_super2__type)
1574
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
1575
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
1576
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
1577
(declare-var Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_x Bool)
1578
(declare-var Super2_Super2.ni_5._arrow._first_x Bool)
1579
(declare-var Super2_Super2.__Super2_Super2_1 Int)
1580
(declare-var Super2_Super2.__Super2_Super2_10 Bool)
1581
(declare-var Super2_Super2.__Super2_Super2_2 Real)
1582
(declare-var Super2_Super2.__Super2_Super2_3 Int)
1583
(declare-var Super2_Super2.__Super2_Super2_4 Int)
1584
(declare-var Super2_Super2.__Super2_Super2_5 Real)
1585
(declare-var Super2_Super2.__Super2_Super2_6 Int)
1586
(declare-var Super2_Super2.__Super2_Super2_7 Int)
1587
(declare-var Super2_Super2.__Super2_Super2_8 Real)
1588
(declare-var Super2_Super2.__Super2_Super2_9 Int)
1589
(declare-var Super2_Super2.idSuper2_C Int)
1590
(declare-var Super2_Super2.idSuper2_C_1 Int)
1591
(declare-var Super2_Super2.idSuper2_C_2 Int)
1592
(declare-var Super2_Super2.idSuper2_C_3 Int)
1593
(declare-var Super2_Super2.idSuper2_Super2 Int)
1594
(declare-var Super2_Super2.idSuper2_Super2_1 Int)
1595
(declare-var Super2_Super2.idSuper2_Super2_2 Int)
1596
(declare-var Super2_Super2.idSuper2_Super2_3 Int)
1597
(declare-var Super2_Super2.s_1 Real)
1598
(declare-var Super2_Super2.s_2 Real)
1599
(declare-var Super2_Super2.s_3 Real)
1600
(declare-rel Super2_Super2_reset (Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool))
1601
(declare-rel Super2_Super2_step (Int Bool Bool Bool Real Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool))
1602

    
1603
(rule (=> 
1604
  (and 
1605
       (= Super2_Super2.__Super2_Super2_11_m Super2_Super2.__Super2_Super2_11_c)
1606
       (= Super2_Super2.__Super2_Super2_12_m Super2_Super2.__Super2_Super2_12_c)
1607
       (= Super2_Super2.__Super2_Super2_13_m Super2_Super2.__Super2_Super2_13_c)
1608
       (= Super2_Super2.ni_5._arrow._first_m true)
1609
       (Super2_Super2_node_reset Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c
1610
                                 Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c
1611
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1612
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1613
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1614
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c
1615
                                 Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m
1616
                                 Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m
1617
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1618
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1619
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1620
                                 Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m)
1621
       (Super2_Super2_node_reset Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c
1622
                                 Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c
1623
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1624
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1625
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1626
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c
1627
                                 Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m
1628
                                 Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m
1629
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1630
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1631
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1632
                                 Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m)
1633
       (Super2_Super2_node_reset Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c
1634
                                 Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c
1635
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1636
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1637
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1638
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c
1639
                                 Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m
1640
                                 Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m
1641
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1642
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1643
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1644
                                 Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m)
1645
  )
1646
  (Super2_Super2_reset Super2_Super2.__Super2_Super2_11_c
1647
                       Super2_Super2.__Super2_Super2_12_c
1648
                       Super2_Super2.__Super2_Super2_13_c
1649
                       Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c
1650
                       Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c
1651
                       Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1652
                       Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1653
                       Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1654
                       Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c
1655
                       Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c
1656
                       Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c
1657
                       Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1658
                       Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1659
                       Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1660
                       Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c
1661
                       Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c
1662
                       Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c
1663
                       Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1664
                       Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1665
                       Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1666
                       Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c
1667
                       Super2_Super2.ni_5._arrow._first_c
1668
                       Super2_Super2.__Super2_Super2_11_m
1669
                       Super2_Super2.__Super2_Super2_12_m
1670
                       Super2_Super2.__Super2_Super2_13_m
1671
                       Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m
1672
                       Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m
1673
                       Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1674
                       Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1675
                       Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1676
                       Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m
1677
                       Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m
1678
                       Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m
1679
                       Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1680
                       Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1681
                       Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1682
                       Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m
1683
                       Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m
1684
                       Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m
1685
                       Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1686
                       Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1687
                       Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1688
                       Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m
1689
                       Super2_Super2.ni_5._arrow._first_m)
1690
))
1691

    
1692
(rule (=> 
1693
  (and (= Super2_Super2.ni_5._arrow._first_m Super2_Super2.ni_5._arrow._first_c)
1694
       (and (= Super2_Super2.__Super2_Super2_10 (ite Super2_Super2.ni_5._arrow._first_m true false))
1695
            (= Super2_Super2.ni_5._arrow._first_x false))
1696
       (and (or (not (= Super2_Super2.__Super2_Super2_10 false))
1697
               (and (= Super2_Super2.s_1 Super2_Super2.__Super2_Super2_13_c)
1698
                    (= Super2_Super2.idSuper2_Super2_1 Super2_Super2.__Super2_Super2_12_c)
1699
                    (= Super2_Super2.idSuper2_C_1 Super2_Super2.__Super2_Super2_11_c)
1700
                    ))
1701
            (or (not (= Super2_Super2.__Super2_Super2_10 true))
1702
               (and (= Super2_Super2.s_1 0.)
1703
                    (= Super2_Super2.idSuper2_Super2_1 0)
1704
                    (= Super2_Super2.idSuper2_C_1 0)
1705
                    ))
1706
       )
1707
       (and (= Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c)
1708
            (= Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c)
1709
            (= Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
1710
            (= Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
1711
            (= Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
1712
            (= Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c)
1713
            )
1714
       (Super2_Super2_node_step Super2_Super2.idSuper2_Super2_1
1715
                                Super2_Super2.s_1
1716
                                false
1717
                                Super2_Super2.idSuper2_C_1
1718
                                Super2_Super2.E
1719
                                false
1720
                                Super2_Super2.__Super2_Super2_7
1721
                                Super2_Super2.__Super2_Super2_8
1722
                                Super2_Super2.__Super2_Super2_9
1723
                                Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m
1724
                                Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m
1725
                                Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1726
                                Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1727
                                Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1728
                                Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m
1729
                                Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_x
1730
                                Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_x
1731
                                Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1732
                                Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1733
                                Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
1734
                                Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_x)
1735
       (and (or (not (= Super2_Super2.E false))
1736
               (and (= Super2_Super2.s_2 Super2_Super2.s_1)
1737
                    (= Super2_Super2.idSuper2_Super2_2 Super2_Super2.idSuper2_Super2_1)
1738
                    (= Super2_Super2.idSuper2_C_2 Super2_Super2.idSuper2_C_1)
1739
                    ))
1740
            (or (not (= Super2_Super2.E true))
1741
               (and (= Super2_Super2.s_2 Super2_Super2.__Super2_Super2_8)
1742
                    (= Super2_Super2.idSuper2_Super2_2 Super2_Super2.__Super2_Super2_7)
1743
                    (= Super2_Super2.idSuper2_C_2 Super2_Super2.__Super2_Super2_9)
1744
                    ))
1745
       )
1746
       (and (= Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c)
1747
            (= Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c)
1748
            (= Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
1749
            (= Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
1750
            (= Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
1751
            (= Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c)
1752
            )
1753
       (Super2_Super2_node_step Super2_Super2.idSuper2_Super2_2
1754
                                Super2_Super2.s_2
1755
                                Super2_Super2.F
1756
                                Super2_Super2.idSuper2_C_2
1757
                                false
1758
                                false
1759
                                Super2_Super2.__Super2_Super2_4
1760
                                Super2_Super2.__Super2_Super2_5
1761
                                Super2_Super2.__Super2_Super2_6
1762
                                Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m
1763
                                Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m
1764
                                Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1765
                                Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1766
                                Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1767
                                Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m
1768
                                Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_x
1769
                                Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_x
1770
                                Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1771
                                Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1772
                                Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
1773
                                Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_x)
1774
       (and (or (not (= Super2_Super2.F false))
1775
               (and (= Super2_Super2.s_3 Super2_Super2.s_2)
1776
                    (= Super2_Super2.idSuper2_Super2_3 Super2_Super2.idSuper2_Super2_2)
1777
                    (= Super2_Super2.idSuper2_C_3 Super2_Super2.idSuper2_C_2)
1778
                    ))
1779
            (or (not (= Super2_Super2.F true))
1780
               (and (= Super2_Super2.s_3 Super2_Super2.__Super2_Super2_5)
1781
                    (= Super2_Super2.idSuper2_Super2_3 Super2_Super2.__Super2_Super2_4)
1782
                    (= Super2_Super2.idSuper2_C_3 Super2_Super2.__Super2_Super2_6)
1783
                    ))
1784
       )
1785
       (and (= Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c)
1786
            (= Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c)
1787
            (= Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
1788
            (= Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
1789
            (= Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
1790
            (= Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c)
1791
            )
1792
       (Super2_Super2_node_step Super2_Super2.idSuper2_Super2_3
1793
                                Super2_Super2.s_3
1794
                                false
1795
                                Super2_Super2.idSuper2_C_3
1796
                                false
1797
                                Super2_Super2.G
1798
                                Super2_Super2.__Super2_Super2_1
1799
                                Super2_Super2.__Super2_Super2_2
1800
                                Super2_Super2.__Super2_Super2_3
1801
                                Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m
1802
                                Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m
1803
                                Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
1804
                                Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
1805
                                Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
1806
                                Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m
1807
                                Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_x
1808
                                Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_x
1809
                                Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1810
                                Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1811
                                Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
1812
                                Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_x)
1813
       (and (or (not (= Super2_Super2.G false))
1814
               (and (= Super2_Super2.s Super2_Super2.s_3)
1815
                    (= Super2_Super2.idSuper2_Super2 Super2_Super2.idSuper2_Super2_3)
1816
                    (= Super2_Super2.idSuper2_C Super2_Super2.idSuper2_C_3)
1817
                    ))
1818
            (or (not (= Super2_Super2.G true))
1819
               (and (= Super2_Super2.s Super2_Super2.__Super2_Super2_2)
1820
                    (= Super2_Super2.idSuper2_Super2 Super2_Super2.__Super2_Super2_1)
1821
                    (= Super2_Super2.idSuper2_C Super2_Super2.__Super2_Super2_3)
1822
                    ))
1823
       )
1824
       (= Super2_Super2.__Super2_Super2_13_x Super2_Super2.s)
1825
       (= Super2_Super2.__Super2_Super2_12_x Super2_Super2.idSuper2_Super2)
1826
       (= Super2_Super2.__Super2_Super2_11_x Super2_Super2.idSuper2_C)
1827
       )
1828
  (Super2_Super2_step Super2_Super2.x
1829
                      Super2_Super2.E
1830
                      Super2_Super2.F
1831
                      Super2_Super2.G
1832
                      Super2_Super2.s
1833
                      Super2_Super2.__Super2_Super2_11_c
1834
                      Super2_Super2.__Super2_Super2_12_c
1835
                      Super2_Super2.__Super2_Super2_13_c
1836
                      Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c
1837
                      Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c
1838
                      Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1839
                      Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1840
                      Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1841
                      Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c
1842
                      Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c
1843
                      Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c
1844
                      Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1845
                      Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1846
                      Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1847
                      Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c
1848
                      Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c
1849
                      Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c
1850
                      Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1851
                      Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1852
                      Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1853
                      Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c
1854
                      Super2_Super2.ni_5._arrow._first_c
1855
                      Super2_Super2.__Super2_Super2_11_x
1856
                      Super2_Super2.__Super2_Super2_12_x
1857
                      Super2_Super2.__Super2_Super2_13_x
1858
                      Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_x
1859
                      Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_x
1860
                      Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1861
                      Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1862
                      Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
1863
                      Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_x
1864
                      Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_x
1865
                      Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_x
1866
                      Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1867
                      Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1868
                      Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
1869
                      Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_x
1870
                      Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_x
1871
                      Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_x
1872
                      Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
1873
                      Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
1874
                      Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
1875
                      Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_x
1876
                      Super2_Super2.ni_5._arrow._first_x)
1877
))
1878

    
1879
; Super2
1880
(declare-var Super2.x_1_1 Int)
1881
(declare-var Super2.E_1_1 Real)
1882
(declare-var Super2.F_1_1 Real)
1883
(declare-var Super2.G_1_1 Real)
1884
(declare-var Super2.state_1_1 Real)
1885
(declare-var Super2.__Super2_2_c Real)
1886
(declare-var Super2.__Super2_3_c Real)
1887
(declare-var Super2.__Super2_4_c Real)
1888
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_11_c Int)
1889
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_12_c Int)
1890
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_13_c Real)
1891
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c Bool)
1892
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c super2_super2__type)
1893
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
1894
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
1895
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
1896
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c Bool)
1897
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c Bool)
1898
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c super2_super2__type)
1899
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
1900
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
1901
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
1902
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c Bool)
1903
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c Bool)
1904
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c super2_super2__type)
1905
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c Bool)
1906
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c super2_c__type)
1907
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c Bool)
1908
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c Bool)
1909
(declare-var Super2.ni_0.Super2_Super2.ni_5._arrow._first_c Bool)
1910
(declare-var Super2.ni_1._arrow._first_c Bool)
1911
(declare-var Super2.__Super2_2_m Real)
1912
(declare-var Super2.__Super2_3_m Real)
1913
(declare-var Super2.__Super2_4_m Real)
1914
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_11_m Int)
1915
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_12_m Int)
1916
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_13_m Real)
1917
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m Bool)
1918
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m super2_super2__type)
1919
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
1920
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
1921
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
1922
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m Bool)
1923
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m Bool)
1924
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m super2_super2__type)
1925
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
1926
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
1927
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
1928
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m Bool)
1929
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m Bool)
1930
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m super2_super2__type)
1931
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Bool)
1932
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m super2_c__type)
1933
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Bool)
1934
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m Bool)
1935
(declare-var Super2.ni_0.Super2_Super2.ni_5._arrow._first_m Bool)
1936
(declare-var Super2.ni_1._arrow._first_m Bool)
1937
(declare-var Super2.__Super2_2_x Real)
1938
(declare-var Super2.__Super2_3_x Real)
1939
(declare-var Super2.__Super2_4_x Real)
1940
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_11_x Int)
1941
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_12_x Int)
1942
(declare-var Super2.ni_0.Super2_Super2.__Super2_Super2_13_x Real)
1943
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_x Bool)
1944
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_x super2_super2__type)
1945
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
1946
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
1947
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
1948
(declare-var Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_x Bool)
1949
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_x Bool)
1950
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_x super2_super2__type)
1951
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
1952
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
1953
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
1954
(declare-var Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_x Bool)
1955
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_x Bool)
1956
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_x super2_super2__type)
1957
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x Bool)
1958
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x super2_c__type)
1959
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x Bool)
1960
(declare-var Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_x Bool)
1961
(declare-var Super2.ni_0.Super2_Super2.ni_5._arrow._first_x Bool)
1962
(declare-var Super2.ni_1._arrow._first_x Bool)
1963
(declare-var Super2.Super2Mux_1_1_event Bool)
1964
(declare-var Super2.Super2Mux_1_2_event Bool)
1965
(declare-var Super2.Super2Mux_1_3_event Bool)
1966
(declare-var Super2.Super2_1_1 Real)
1967
(declare-var Super2.__Super2_1 Bool)
1968
(declare-var Super2.i_virtual_local Real)
1969
(declare-rel Super2_reset (Real Real Real Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool Bool Real Real Real Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool Bool))
1970
(declare-rel Super2_step (Int Real Real Real Real Real Real Real Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool Bool Real Real Real Int Int Real Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool super2_super2__type Bool super2_c__type Bool Bool Bool Bool))
1971

    
1972
(rule (=> 
1973
  (and 
1974
       (= Super2.__Super2_2_m Super2.__Super2_2_c)
1975
       (= Super2.__Super2_3_m Super2.__Super2_3_c)
1976
       (= Super2.__Super2_4_m Super2.__Super2_4_c)
1977
       (= Super2.ni_1._arrow._first_m true)
1978
       (Super2_Super2_reset Super2.ni_0.Super2_Super2.__Super2_Super2_11_c
1979
                            Super2.ni_0.Super2_Super2.__Super2_Super2_12_c
1980
                            Super2.ni_0.Super2_Super2.__Super2_Super2_13_c
1981
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c
1982
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c
1983
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1984
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1985
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1986
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c
1987
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c
1988
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c
1989
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1990
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1991
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1992
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c
1993
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c
1994
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c
1995
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
1996
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
1997
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
1998
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c
1999
                            Super2.ni_0.Super2_Super2.ni_5._arrow._first_c
2000
                            Super2.ni_0.Super2_Super2.__Super2_Super2_11_m
2001
                            Super2.ni_0.Super2_Super2.__Super2_Super2_12_m
2002
                            Super2.ni_0.Super2_Super2.__Super2_Super2_13_m
2003
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m
2004
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m
2005
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2006
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2007
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2008
                            Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m
2009
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m
2010
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m
2011
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2012
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2013
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2014
                            Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m
2015
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m
2016
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m
2017
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2018
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2019
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2020
                            Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m
2021
                            Super2.ni_0.Super2_Super2.ni_5._arrow._first_m)
2022
  )
2023
  (Super2_reset Super2.__Super2_2_c
2024
                Super2.__Super2_3_c
2025
                Super2.__Super2_4_c
2026
                Super2.ni_0.Super2_Super2.__Super2_Super2_11_c
2027
                Super2.ni_0.Super2_Super2.__Super2_Super2_12_c
2028
                Super2.ni_0.Super2_Super2.__Super2_Super2_13_c
2029
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c
2030
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c
2031
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
2032
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
2033
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
2034
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c
2035
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c
2036
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c
2037
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
2038
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
2039
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
2040
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c
2041
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c
2042
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c
2043
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
2044
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
2045
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
2046
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c
2047
                Super2.ni_0.Super2_Super2.ni_5._arrow._first_c
2048
                Super2.ni_1._arrow._first_c
2049
                Super2.__Super2_2_m
2050
                Super2.__Super2_3_m
2051
                Super2.__Super2_4_m
2052
                Super2.ni_0.Super2_Super2.__Super2_Super2_11_m
2053
                Super2.ni_0.Super2_Super2.__Super2_Super2_12_m
2054
                Super2.ni_0.Super2_Super2.__Super2_Super2_13_m
2055
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m
2056
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m
2057
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2058
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2059
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2060
                Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m
2061
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m
2062
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m
2063
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2064
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2065
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2066
                Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m
2067
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m
2068
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m
2069
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2070
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2071
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2072
                Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m
2073
                Super2.ni_0.Super2_Super2.ni_5._arrow._first_m
2074
                Super2.ni_1._arrow._first_m)
2075
))
2076

    
2077
(rule (=> 
2078
  (and (= Super2.ni_1._arrow._first_m Super2.ni_1._arrow._first_c)(and (= Super2.__Super2_1 (ite Super2.ni_1._arrow._first_m true false))
2079
                                                                    (= Super2.ni_1._arrow._first_x false))
2080
       (and (or (not (= Super2.__Super2_1 true))
2081
               (= Super2.Super2Mux_1_3_event false))
2082
            (or (not (= Super2.__Super2_1 false))
2083
               (= Super2.Super2Mux_1_3_event (or (and (> Super2.__Super2_2_c 0.) (<= Super2.G_1_1 0.)) (and (<= Super2.__Super2_2_c 0.) (> Super2.G_1_1 0.)))))
2084
       )
2085
       (and (or (not (= Super2.__Super2_1 true))
2086
               (= Super2.Super2Mux_1_2_event false))
2087
            (or (not (= Super2.__Super2_1 false))
2088
               (= Super2.Super2Mux_1_2_event (or (and (> Super2.__Super2_3_c 0.) (<= Super2.F_1_1 0.)) (and (<= Super2.__Super2_3_c 0.) (> Super2.F_1_1 0.)))))
2089
       )
2090
       (and (or (not (= Super2.__Super2_1 true))
2091
               (= Super2.Super2Mux_1_1_event false))
2092
            (or (not (= Super2.__Super2_1 false))
2093
               (= Super2.Super2Mux_1_1_event (or (and (> Super2.__Super2_4_c 0.) (<= Super2.E_1_1 0.)) (and (<= Super2.__Super2_4_c 0.) (> Super2.E_1_1 0.)))))
2094
       )
2095
       (and (= Super2.ni_0.Super2_Super2.__Super2_Super2_11_m Super2.ni_0.Super2_Super2.__Super2_Super2_11_c)
2096
            (= Super2.ni_0.Super2_Super2.__Super2_Super2_12_m Super2.ni_0.Super2_Super2.__Super2_Super2_12_c)
2097
            (= Super2.ni_0.Super2_Super2.__Super2_Super2_13_m Super2.ni_0.Super2_Super2.__Super2_Super2_13_c)
2098
            (= Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c)
2099
            (= Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c)
2100
            (= Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
2101
            (= Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
2102
            (= Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
2103
            (= Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c)
2104
            (= Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c)
2105
            (= Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c)
2106
            (= Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
2107
            (= Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
2108
            (= Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
2109
            (= Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c)
2110
            (= Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c)
2111
            (= Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c)
2112
            (= Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c)
2113
            (= Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c)
2114
            (= Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c)
2115
            (= Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c)
2116
            (= Super2.ni_0.Super2_Super2.ni_5._arrow._first_m Super2.ni_0.Super2_Super2.ni_5._arrow._first_c)
2117
            )
2118
       (Super2_Super2_step Super2.x_1_1
2119
                           Super2.Super2Mux_1_1_event
2120
                           Super2.Super2Mux_1_2_event
2121
                           Super2.Super2Mux_1_3_event
2122
                           Super2.Super2_1_1
2123
                           Super2.ni_0.Super2_Super2.__Super2_Super2_11_m
2124
                           Super2.ni_0.Super2_Super2.__Super2_Super2_12_m
2125
                           Super2.ni_0.Super2_Super2.__Super2_Super2_13_m
2126
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_m
2127
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_m
2128
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2129
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2130
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2131
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_m
2132
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_m
2133
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_m
2134
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2135
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2136
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2137
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_m
2138
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_m
2139
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_m
2140
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_m
2141
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_m
2142
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_m
2143
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_m
2144
                           Super2.ni_0.Super2_Super2.ni_5._arrow._first_m
2145
                           Super2.ni_0.Super2_Super2.__Super2_Super2_11_x
2146
                           Super2.ni_0.Super2_Super2.__Super2_Super2_12_x
2147
                           Super2.ni_0.Super2_Super2.__Super2_Super2_13_x
2148
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_x
2149
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_x
2150
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
2151
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
2152
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
2153
                           Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_x
2154
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_x
2155
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_x
2156
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
2157
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
2158
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
2159
                           Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_x
2160
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_x
2161
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_x
2162
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
2163
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
2164
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
2165
                           Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_x
2166
                           Super2.ni_0.Super2_Super2.ni_5._arrow._first_x)
2167
       (= Super2.state_1_1 Super2.Super2_1_1)
2168
       (and (or (not (= Super2.__Super2_1 true))
2169
               (= Super2.i_virtual_local 0.))
2170
            (or (not (= Super2.__Super2_1 false))
2171
               (= Super2.i_virtual_local 1.))
2172
       )
2173
       (= Super2.__Super2_4_x Super2.E_1_1)
2174
       (= Super2.__Super2_3_x Super2.F_1_1)
2175
       (= Super2.__Super2_2_x Super2.G_1_1)
2176
       )
2177
  (Super2_step Super2.x_1_1
2178
               Super2.E_1_1
2179
               Super2.F_1_1
2180
               Super2.G_1_1
2181
               Super2.state_1_1
2182
               Super2.__Super2_2_c
2183
               Super2.__Super2_3_c
2184
               Super2.__Super2_4_c
2185
               Super2.ni_0.Super2_Super2.__Super2_Super2_11_c
2186
               Super2.ni_0.Super2_Super2.__Super2_Super2_12_c
2187
               Super2.ni_0.Super2_Super2.__Super2_Super2_13_c
2188
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_c
2189
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_c
2190
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
2191
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
2192
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
2193
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_c
2194
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_c
2195
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_c
2196
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
2197
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
2198
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
2199
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_c
2200
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_c
2201
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_c
2202
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_c
2203
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_c
2204
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_c
2205
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_c
2206
               Super2.ni_0.Super2_Super2.ni_5._arrow._first_c
2207
               Super2.ni_1._arrow._first_c
2208
               Super2.__Super2_2_x
2209
               Super2.__Super2_3_x
2210
               Super2.__Super2_4_x
2211
               Super2.ni_0.Super2_Super2.__Super2_Super2_11_x
2212
               Super2.ni_0.Super2_Super2.__Super2_Super2_12_x
2213
               Super2.ni_0.Super2_Super2.__Super2_Super2_13_x
2214
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_65_x
2215
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.__Super2_Super2_node_66_x
2216
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
2217
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
2218
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
2219
               Super2.ni_0.Super2_Super2.ni_2.Super2_Super2_node.ni_7._arrow._first_x
2220
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_65_x
2221
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.__Super2_Super2_node_66_x
2222
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
2223
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
2224
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
2225
               Super2.ni_0.Super2_Super2.ni_3.Super2_Super2_node.ni_7._arrow._first_x
2226
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_65_x
2227
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.__Super2_Super2_node_66_x
2228
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_30_x
2229
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.__Super2_C_node_31_x
2230
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_6.super2_super2__SUPER2_C_IDL_handler_until.ni_8.Super2_C_node.ni_9._arrow._first_x
2231
               Super2.ni_0.Super2_Super2.ni_4.Super2_Super2_node.ni_7._arrow._first_x
2232
               Super2.ni_0.Super2_Super2.ni_5._arrow._first_x
2233
               Super2.ni_1._arrow._first_x)
2234
))
2235