Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Hierarchy4 / Hierarchy4.smt2 @ eb639349

History | View | Annotate | Download (61.4 KB)

1
(declare-datatypes () ((hierarchy4_hierarchy4__type POINTHierarchy4_Hierarchy4 POINT__TO__HIERARCHY4_A_1 POINT__TO__HIERARCHY4_B_2 HIERARCHY4_A_IDL HIERARCHY4_B_IDL)));
2

    
3
; Hierarchy4_A_en
4
(declare-var Hierarchy4_A_en.idHierarchy4_Hierarchy4_1 Int)
5
(declare-var Hierarchy4_A_en.y_1 Int)
6
(declare-var Hierarchy4_A_en.isInner Bool)
7
(declare-var Hierarchy4_A_en.idHierarchy4_Hierarchy4 Int)
8
(declare-var Hierarchy4_A_en.y Int)
9
(declare-var Hierarchy4_A_en.y_2 Int)
10
(declare-rel Hierarchy4_A_en (Int Int Bool Int Int))
11
(rule (=> 
12
  (and (and (or (not (= (not Hierarchy4_A_en.isInner) true))
13
               (= Hierarchy4_A_en.y_2 1))
14
            (or (not (= (not Hierarchy4_A_en.isInner) false))
15
               (= Hierarchy4_A_en.y_2 Hierarchy4_A_en.y_1))
16
       )
17
       (= Hierarchy4_A_en.y Hierarchy4_A_en.y_2)
18
       (= Hierarchy4_A_en.idHierarchy4_Hierarchy4 1021)
19
       )
20
  (Hierarchy4_A_en Hierarchy4_A_en.idHierarchy4_Hierarchy4_1 Hierarchy4_A_en.y_1 Hierarchy4_A_en.isInner Hierarchy4_A_en.idHierarchy4_Hierarchy4 Hierarchy4_A_en.y)
21
))
22

    
23
; Hierarchy4_B_en
24
(declare-var Hierarchy4_B_en.idHierarchy4_Hierarchy4_1 Int)
25
(declare-var Hierarchy4_B_en.y_1 Int)
26
(declare-var Hierarchy4_B_en.isInner Bool)
27
(declare-var Hierarchy4_B_en.idHierarchy4_Hierarchy4 Int)
28
(declare-var Hierarchy4_B_en.y Int)
29
(declare-var Hierarchy4_B_en.y_2 Int)
30
(declare-rel Hierarchy4_B_en (Int Int Bool Int Int))
31
(rule (=> 
32
  (and (and (or (not (= (not Hierarchy4_B_en.isInner) true))
33
               (= Hierarchy4_B_en.y_2 2))
34
            (or (not (= (not Hierarchy4_B_en.isInner) false))
35
               (= Hierarchy4_B_en.y_2 Hierarchy4_B_en.y_1))
36
       )
37
       (= Hierarchy4_B_en.y Hierarchy4_B_en.y_2)
38
       (= Hierarchy4_B_en.idHierarchy4_Hierarchy4 1022)
39
       )
40
  (Hierarchy4_B_en Hierarchy4_B_en.idHierarchy4_Hierarchy4_1 Hierarchy4_B_en.y_1 Hierarchy4_B_en.isInner Hierarchy4_B_en.idHierarchy4_Hierarchy4 Hierarchy4_B_en.y)
41
))
42

    
43
; hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until
44
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.idHierarchy4_Hierarchy4_1 Int)
45
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.y_1 Int)
46
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.hierarchy4_hierarchy4__restart_in Bool)
47
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
48
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.idHierarchy4_Hierarchy4_out Int)
49
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.y_out Int)
50
(declare-rel hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until (Int Int Bool hierarchy4_hierarchy4__type Int Int))
51
(rule (=> 
52
  (and (= hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.y_out hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.y_1)
53
       (= hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.idHierarchy4_Hierarchy4_1)
54
       (= hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.hierarchy4_hierarchy4__state_in POINTHierarchy4_Hierarchy4)
55
       (= hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.hierarchy4_hierarchy4__restart_in true)
56
       )
57
  (hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.idHierarchy4_Hierarchy4_1 hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.y_1 hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until.y_out)
58
))
59

    
60
; hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless
61
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__restart_in Bool)
62
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
63
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__restart_act Bool)
64
(declare-var hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__type)
65
(declare-rel hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless (Bool hierarchy4_hierarchy4__type Bool hierarchy4_hierarchy4__type))
66
(rule (=> 
67
  (and (= hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__state_in)
68
       (= hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__restart_in)
69
       )
70
  (hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless.hierarchy4_hierarchy4__state_act)
71
))
72

    
73
; hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until
74
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.idHierarchy4_Hierarchy4_1 Int)
75
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.y_1 Int)
76
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.hierarchy4_hierarchy4__restart_in Bool)
77
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
78
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.idHierarchy4_Hierarchy4_out Int)
79
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.y_out Int)
80
(declare-rel hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until (Int Int Bool hierarchy4_hierarchy4__type Int Int))
81
(rule (=> 
82
  (and (= hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.y_out hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.y_1)
83
       (= hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.idHierarchy4_Hierarchy4_1)
84
       (= hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.hierarchy4_hierarchy4__state_in POINTHierarchy4_Hierarchy4)
85
       (= hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.hierarchy4_hierarchy4__restart_in true)
86
       )
87
  (hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.idHierarchy4_Hierarchy4_1 hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.y_1 hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until.y_out)
88
))
89

    
90
; hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless
91
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__restart_in Bool)
92
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
93
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__restart_act Bool)
94
(declare-var hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__type)
95
(declare-rel hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless (Bool hierarchy4_hierarchy4__type Bool hierarchy4_hierarchy4__type))
96
(rule (=> 
97
  (and (= hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__state_in)
98
       (= hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__restart_in)
99
       )
100
  (hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless.hierarchy4_hierarchy4__state_act)
101
))
102

    
103
; hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until
104
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.idHierarchy4_Hierarchy4_1 Int)
105
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.y_1 Int)
106
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.hierarchy4_hierarchy4__restart_in Bool)
107
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
108
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.idHierarchy4_Hierarchy4_out Int)
109
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.y_out Int)
110
(declare-rel hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until (Int Int Bool hierarchy4_hierarchy4__type Int Int))
111
(rule (=> 
112
  (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.y_out hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.y_1)
113
       (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.idHierarchy4_Hierarchy4_1)
114
       (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.hierarchy4_hierarchy4__state_in POINTHierarchy4_Hierarchy4)
115
       (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.hierarchy4_hierarchy4__restart_in false)
116
       )
117
  (hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.idHierarchy4_Hierarchy4_1 hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.y_1 hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until.y_out)
118
))
119

    
120
; hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless
121
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_in Bool)
122
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
123
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.idHierarchy4_Hierarchy4_1 Int)
124
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.x Int)
125
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_act Bool)
126
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__type)
127
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_1 Bool)
128
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_2 Bool)
129
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_3 Bool)
130
(declare-var hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_4 Bool)
131
(declare-rel hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless (Bool hierarchy4_hierarchy4__type Int Int Bool hierarchy4_hierarchy4__type))
132
(rule (=> 
133
  (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_4 (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.idHierarchy4_Hierarchy4_1 1022))
134
       (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_3 (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.idHierarchy4_Hierarchy4_1 1021))
135
       (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_2 (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.idHierarchy4_Hierarchy4_1 0) (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.x 0))))
136
       (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_1 (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.idHierarchy4_Hierarchy4_1 0) (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.x 0)))
137
       (and (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_1 false))
138
               (and (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_2 false))
139
                       (and (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_3 false))
140
                               (and (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_4 false))
141
                                       (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_in)
142
                                            (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_in)
143
                                            ))
144
                                    (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_4 true))
145
                                       (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_act HIERARCHY4_B_IDL)
146
                                            (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_act true)
147
                                            ))
148
                               ))
149
                            (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_3 true))
150
                               (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_act HIERARCHY4_A_IDL)
151
                                    (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_act true)
152
                                    ))
153
                       ))
154
                    (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_2 true))
155
                       (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_act POINT__TO__HIERARCHY4_B_2)
156
                            (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_act true)
157
                            ))
158
               ))
159
            (or (not (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.__hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless_1 true))
160
               (and (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_act POINT__TO__HIERARCHY4_A_1)
161
                    (= hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_act true)
162
                    ))
163
       )
164
       )
165
  (hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.idHierarchy4_Hierarchy4_1 hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.x hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless.hierarchy4_hierarchy4__state_act)
166
))
167

    
168
; hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until
169
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_1 Int)
170
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_1 Int)
171
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.hierarchy4_hierarchy4__restart_in Bool)
172
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
173
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_out Int)
174
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_out Int)
175
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_2 Int)
176
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_2 Int)
177
(declare-rel hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until (Int Int Bool hierarchy4_hierarchy4__type Int Int))
178
(rule (=> 
179
  (and (Hierarchy4_A_en hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_1
180
                        hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_1
181
                        false
182
                        hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_2
183
                        hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_2)
184
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_out hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_2)
185
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_2)
186
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.hierarchy4_hierarchy4__state_in POINTHierarchy4_Hierarchy4)
187
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.hierarchy4_hierarchy4__restart_in true)
188
       )
189
  (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_1 hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_1 hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until.y_out)
190
))
191

    
192
; hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless
193
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__restart_in Bool)
194
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
195
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__restart_act Bool)
196
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__type)
197
(declare-rel hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless (Bool hierarchy4_hierarchy4__type Bool hierarchy4_hierarchy4__type))
198
(rule (=> 
199
  (and (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__state_in)
200
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__restart_in)
201
       )
202
  (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless.hierarchy4_hierarchy4__state_act)
203
))
204

    
205
; hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until
206
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_1 Int)
207
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_1 Int)
208
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.hierarchy4_hierarchy4__restart_in Bool)
209
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
210
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_out Int)
211
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_out Int)
212
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_2 Int)
213
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_2 Int)
214
(declare-rel hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until (Int Int Bool hierarchy4_hierarchy4__type Int Int))
215
(rule (=> 
216
  (and (Hierarchy4_B_en hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_1
217
                        hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_1
218
                        false
219
                        hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_2
220
                        hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_2)
221
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_out hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_2)
222
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_2)
223
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.hierarchy4_hierarchy4__state_in POINTHierarchy4_Hierarchy4)
224
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.hierarchy4_hierarchy4__restart_in true)
225
       )
226
  (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_1 hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_1 hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.idHierarchy4_Hierarchy4_out hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until.y_out)
227
))
228

    
229
; hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless
230
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__restart_in Bool)
231
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
232
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__restart_act Bool)
233
(declare-var hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__type)
234
(declare-rel hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless (Bool hierarchy4_hierarchy4__type Bool hierarchy4_hierarchy4__type))
235
(rule (=> 
236
  (and (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__state_in)
237
       (= hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__restart_in)
238
       )
239
  (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__restart_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__restart_act hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless.hierarchy4_hierarchy4__state_act)
240
))
241

    
242
; Hierarchy4_Hierarchy4_node
243
(declare-var Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1 Int)
244
(declare-var Hierarchy4_Hierarchy4_node.x Int)
245
(declare-var Hierarchy4_Hierarchy4_node.y_1 Int)
246
(declare-var Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4 Int)
247
(declare-var Hierarchy4_Hierarchy4_node.y Int)
248
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c Bool)
249
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c hierarchy4_hierarchy4__type)
250
(declare-var Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c Bool)
251
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m Bool)
252
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m hierarchy4_hierarchy4__type)
253
(declare-var Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m Bool)
254
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x Bool)
255
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x hierarchy4_hierarchy4__type)
256
(declare-var Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x Bool)
257
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_1 Bool)
258
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_10 hierarchy4_hierarchy4__type)
259
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_11 Bool)
260
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_12 hierarchy4_hierarchy4__type)
261
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_13 Int)
262
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_14 Int)
263
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_15 Bool)
264
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_16 hierarchy4_hierarchy4__type)
265
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_17 Int)
266
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_18 Int)
267
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_19 Bool)
268
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_2 hierarchy4_hierarchy4__type)
269
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_20 hierarchy4_hierarchy4__type)
270
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_21 Int)
271
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_22 Int)
272
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_23 Bool)
273
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_24 hierarchy4_hierarchy4__type)
274
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_25 Int)
275
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_26 Int)
276
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_27 Bool)
277
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_28 hierarchy4_hierarchy4__type)
278
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_29 Int)
279
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_3 Bool)
280
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_30 Int)
281
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_31 Bool)
282
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_4 hierarchy4_hierarchy4__type)
283
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_5 Bool)
284
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_6 hierarchy4_hierarchy4__type)
285
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_7 Bool)
286
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_8 hierarchy4_hierarchy4__type)
287
(declare-var Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_9 Bool)
288
(declare-var Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_restart_in Bool)
289
(declare-var Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_state_in hierarchy4_hierarchy4__type)
290
(declare-var Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_act Bool)
291
(declare-var Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in Bool)
292
(declare-var Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act hierarchy4_hierarchy4__type)
293
(declare-var Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in hierarchy4_hierarchy4__type)
294
(declare-rel Hierarchy4_Hierarchy4_node_reset (Bool hierarchy4_hierarchy4__type Bool Bool hierarchy4_hierarchy4__type Bool))
295
(declare-rel Hierarchy4_Hierarchy4_node_step (Int Int Int Int Int Bool hierarchy4_hierarchy4__type Bool Bool hierarchy4_hierarchy4__type Bool))
296

    
297
(rule (=> 
298
  (and 
299
       (= Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c)
300
       (= Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c)
301
       (= Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m true)
302
  )
303
  (Hierarchy4_Hierarchy4_node_reset Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
304
                                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
305
                                    Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
306
                                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m
307
                                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m
308
                                    Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m)
309
))
310

    
311
(rule (=> 
312
  (and (= Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c)
313
       (and (= Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_31 (ite Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m true false))
314
            (= Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x false))
315
       (and (or (not (= Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_31 false))
316
               (and (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c)
317
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c)
318
                    ))
319
            (or (not (= Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_31 true))
320
               (and (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in POINTHierarchy4_Hierarchy4)
321
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in false)
322
                    ))
323
       )
324
       (and (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in HIERARCHY4_A_IDL))
325
               (and (hierarchy4_hierarchy4__HIERARCHY4_A_IDL_unless Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in
326
                                                                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in
327
                                                                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_3
328
                                                                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_4)
329
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_4)
330
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_3)
331
                    ))
332
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in HIERARCHY4_B_IDL))
333
               (and (hierarchy4_hierarchy4__HIERARCHY4_B_IDL_unless Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in
334
                                                                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in
335
                                                                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_1
336
                                                                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_2)
337
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_2)
338
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_1)
339
                    ))
340
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in POINTHierarchy4_Hierarchy4))
341
               (and (hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_unless 
342
                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in
343
                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in
344
                    Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1
345
                    Hierarchy4_Hierarchy4_node.x
346
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_9
347
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_10)
348
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_10)
349
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_9)
350
                    ))
351
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in POINT__TO__HIERARCHY4_A_1))
352
               (and (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_unless 
353
                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in
354
                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in
355
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_7
356
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_8)
357
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_8)
358
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_7)
359
                    ))
360
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in POINT__TO__HIERARCHY4_B_2))
361
               (and (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_unless 
362
                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_in
363
                    Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_in
364
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_5
365
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_6)
366
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_6)
367
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__restart_act Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_5)
368
                    ))
369
       )
370
       (and (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act HIERARCHY4_A_IDL))
371
               (and (hierarchy4_hierarchy4__HIERARCHY4_A_IDL_handler_until 
372
                    Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1
373
                    Hierarchy4_Hierarchy4_node.y_1
374
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_15
375
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_16
376
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_17
377
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_18)
378
                    (= Hierarchy4_Hierarchy4_node.y Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_18)
379
                    (= Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4 Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_17)
380
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_state_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_16)
381
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_restart_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_15)
382
                    ))
383
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act HIERARCHY4_B_IDL))
384
               (and (hierarchy4_hierarchy4__HIERARCHY4_B_IDL_handler_until 
385
                    Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1
386
                    Hierarchy4_Hierarchy4_node.y_1
387
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_11
388
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_12
389
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_13
390
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_14)
391
                    (= Hierarchy4_Hierarchy4_node.y Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_14)
392
                    (= Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4 Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_13)
393
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_state_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_12)
394
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_restart_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_11)
395
                    ))
396
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act POINTHierarchy4_Hierarchy4))
397
               (and (hierarchy4_hierarchy4__POINTHierarchy4_Hierarchy4_handler_until 
398
                    Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1
399
                    Hierarchy4_Hierarchy4_node.y_1
400
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_27
401
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_28
402
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_29
403
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_30)
404
                    (= Hierarchy4_Hierarchy4_node.y Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_30)
405
                    (= Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4 Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_29)
406
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_state_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_28)
407
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_restart_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_27)
408
                    ))
409
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act POINT__TO__HIERARCHY4_A_1))
410
               (and (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_A_1_handler_until 
411
                    Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1
412
                    Hierarchy4_Hierarchy4_node.y_1
413
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_23
414
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_24
415
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_25
416
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_26)
417
                    (= Hierarchy4_Hierarchy4_node.y Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_26)
418
                    (= Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4 Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_25)
419
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_state_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_24)
420
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_restart_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_23)
421
                    ))
422
            (or (not (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__state_act POINT__TO__HIERARCHY4_B_2))
423
               (and (hierarchy4_hierarchy4__POINT__TO__HIERARCHY4_B_2_handler_until 
424
                    Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1
425
                    Hierarchy4_Hierarchy4_node.y_1
426
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_19
427
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_20
428
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_21
429
                    Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_22)
430
                    (= Hierarchy4_Hierarchy4_node.y Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_22)
431
                    (= Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4 Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_21)
432
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_state_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_20)
433
                    (= Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_restart_in Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_19)
434
                    ))
435
       )
436
       (= Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_state_in)
437
       (= Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x Hierarchy4_Hierarchy4_node.hierarchy4_hierarchy4__next_restart_in)
438
       )
439
  (Hierarchy4_Hierarchy4_node_step Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4_1
440
                                   Hierarchy4_Hierarchy4_node.x
441
                                   Hierarchy4_Hierarchy4_node.y_1
442
                                   Hierarchy4_Hierarchy4_node.idHierarchy4_Hierarchy4
443
                                   Hierarchy4_Hierarchy4_node.y
444
                                   Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
445
                                   Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
446
                                   Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
447
                                   Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x
448
                                   Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x
449
                                   Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x)
450
))
451

    
452
; Hierarchy4_Hierarchy4
453
(declare-var Hierarchy4_Hierarchy4.x Int)
454
(declare-var Hierarchy4_Hierarchy4.y Int)
455
(declare-var Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c Int)
456
(declare-var Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c Int)
457
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c Bool)
458
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c hierarchy4_hierarchy4__type)
459
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c Bool)
460
(declare-var Hierarchy4_Hierarchy4.ni_3._arrow._first_c Bool)
461
(declare-var Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m Int)
462
(declare-var Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m Int)
463
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m Bool)
464
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m hierarchy4_hierarchy4__type)
465
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m Bool)
466
(declare-var Hierarchy4_Hierarchy4.ni_3._arrow._first_m Bool)
467
(declare-var Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_x Int)
468
(declare-var Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_x Int)
469
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x Bool)
470
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x hierarchy4_hierarchy4__type)
471
(declare-var Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x Bool)
472
(declare-var Hierarchy4_Hierarchy4.ni_3._arrow._first_x Bool)
473
(declare-var Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_1 Bool)
474
(declare-var Hierarchy4_Hierarchy4.idHierarchy4_Hierarchy4 Int)
475
(declare-var Hierarchy4_Hierarchy4.idHierarchy4_Hierarchy4_1 Int)
476
(declare-var Hierarchy4_Hierarchy4.y_1 Int)
477
(declare-rel Hierarchy4_Hierarchy4_reset (Int Int Bool hierarchy4_hierarchy4__type Bool Bool Int Int Bool hierarchy4_hierarchy4__type Bool Bool))
478
(declare-rel Hierarchy4_Hierarchy4_step (Int Int Int Int Bool hierarchy4_hierarchy4__type Bool Bool Int Int Bool hierarchy4_hierarchy4__type Bool Bool))
479

    
480
(rule (=> 
481
  (and 
482
       (= Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c)
483
       (= Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c)
484
       (= Hierarchy4_Hierarchy4.ni_3._arrow._first_m true)
485
       (Hierarchy4_Hierarchy4_node_reset Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
486
                                         Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
487
                                         Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
488
                                         Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m
489
                                         Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m
490
                                         Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m)
491
  )
492
  (Hierarchy4_Hierarchy4_reset Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c
493
                               Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c
494
                               Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
495
                               Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
496
                               Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
497
                               Hierarchy4_Hierarchy4.ni_3._arrow._first_c
498
                               Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m
499
                               Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m
500
                               Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m
501
                               Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m
502
                               Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m
503
                               Hierarchy4_Hierarchy4.ni_3._arrow._first_m)
504
))
505

    
506
(rule (=> 
507
  (and (= Hierarchy4_Hierarchy4.ni_3._arrow._first_m Hierarchy4_Hierarchy4.ni_3._arrow._first_c)
508
       (and (= Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_1 (ite Hierarchy4_Hierarchy4.ni_3._arrow._first_m true false))
509
            (= Hierarchy4_Hierarchy4.ni_3._arrow._first_x false))
510
       (and (or (not (= Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_1 false))
511
               (and (= Hierarchy4_Hierarchy4.y_1 Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c)
512
                    (= Hierarchy4_Hierarchy4.idHierarchy4_Hierarchy4_1 Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c)
513
                    ))
514
            (or (not (= Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_1 true))
515
               (and (= Hierarchy4_Hierarchy4.y_1 0)
516
                    (= Hierarchy4_Hierarchy4.idHierarchy4_Hierarchy4_1 0)
517
                    ))
518
       )
519
       (and (= Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c)
520
            (= Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c)
521
            (= Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c)
522
            )
523
       (Hierarchy4_Hierarchy4_node_step Hierarchy4_Hierarchy4.idHierarchy4_Hierarchy4_1
524
                                        Hierarchy4_Hierarchy4.x
525
                                        Hierarchy4_Hierarchy4.y_1
526
                                        Hierarchy4_Hierarchy4.idHierarchy4_Hierarchy4
527
                                        Hierarchy4_Hierarchy4.y
528
                                        Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m
529
                                        Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m
530
                                        Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m
531
                                        Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x
532
                                        Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x
533
                                        Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x)
534
       (= Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_x Hierarchy4_Hierarchy4.y)
535
       (= Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_x Hierarchy4_Hierarchy4.idHierarchy4_Hierarchy4)
536
       )
537
  (Hierarchy4_Hierarchy4_step Hierarchy4_Hierarchy4.x
538
                              Hierarchy4_Hierarchy4.y
539
                              Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c
540
                              Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c
541
                              Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
542
                              Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
543
                              Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
544
                              Hierarchy4_Hierarchy4.ni_3._arrow._first_c
545
                              Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_x
546
                              Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_x
547
                              Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x
548
                              Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x
549
                              Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x
550
                              Hierarchy4_Hierarchy4.ni_3._arrow._first_x)
551
))
552

    
553
; Hierarchy4
554
(declare-var Hierarchy4.In1_1_1 Int)
555
(declare-var Hierarchy4.Out1_1_1 Int)
556
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c Int)
557
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c Int)
558
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c Bool)
559
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c hierarchy4_hierarchy4__type)
560
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c Bool)
561
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_c Bool)
562
(declare-var Hierarchy4.ni_1._arrow._first_c Bool)
563
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m Int)
564
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m Int)
565
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m Bool)
566
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m hierarchy4_hierarchy4__type)
567
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m Bool)
568
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_m Bool)
569
(declare-var Hierarchy4.ni_1._arrow._first_m Bool)
570
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_x Int)
571
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_x Int)
572
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x Bool)
573
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x hierarchy4_hierarchy4__type)
574
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x Bool)
575
(declare-var Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_x Bool)
576
(declare-var Hierarchy4.ni_1._arrow._first_x Bool)
577
(declare-var Hierarchy4.Hierarchy4_1_1 Int)
578
(declare-var Hierarchy4.__Hierarchy4_1 Bool)
579
(declare-var Hierarchy4.i_virtual_local Real)
580
(declare-rel Hierarchy4_reset (Int Int Bool hierarchy4_hierarchy4__type Bool Bool Bool Int Int Bool hierarchy4_hierarchy4__type Bool Bool Bool))
581
(declare-rel Hierarchy4_step (Int Int Int Int Bool hierarchy4_hierarchy4__type Bool Bool Bool Int Int Bool hierarchy4_hierarchy4__type Bool Bool Bool))
582

    
583
(rule (=> 
584
  (and 
585
       
586
       (= Hierarchy4.ni_1._arrow._first_m true)
587
       (Hierarchy4_Hierarchy4_reset Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c
588
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c
589
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
590
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
591
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
592
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_c
593
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m
594
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m
595
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m
596
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m
597
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m
598
                                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_m)
599
  )
600
  (Hierarchy4_reset Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c
601
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c
602
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
603
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
604
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
605
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_c
606
                    Hierarchy4.ni_1._arrow._first_c
607
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m
608
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m
609
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m
610
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m
611
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m
612
                    Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_m
613
                    Hierarchy4.ni_1._arrow._first_m)
614
))
615

    
616
(rule (=> 
617
  (and (= Hierarchy4.ni_1._arrow._first_m Hierarchy4.ni_1._arrow._first_c)
618
       (and (= Hierarchy4.__Hierarchy4_1 (ite Hierarchy4.ni_1._arrow._first_m true false))
619
            (= Hierarchy4.ni_1._arrow._first_x false))
620
       (and (or (not (= Hierarchy4.__Hierarchy4_1 true))
621
               (= Hierarchy4.i_virtual_local 0.))
622
            (or (not (= Hierarchy4.__Hierarchy4_1 false))
623
               (= Hierarchy4.i_virtual_local 1.))
624
       )
625
       (and (= Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c)
626
            (= Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c)
627
            (= Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c)
628
            (= Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c)
629
            (= Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c)
630
            (= Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_m Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_c)
631
            )
632
       (Hierarchy4_Hierarchy4_step Hierarchy4.In1_1_1
633
                                   Hierarchy4.Hierarchy4_1_1
634
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_m
635
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_m
636
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_m
637
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_m
638
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_m
639
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_m
640
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_x
641
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_x
642
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x
643
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x
644
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x
645
                                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_x)
646
       (= Hierarchy4.Out1_1_1 Hierarchy4.Hierarchy4_1_1)
647
       )
648
  (Hierarchy4_step Hierarchy4.In1_1_1
649
                   Hierarchy4.Out1_1_1
650
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_c
651
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_c
652
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_c
653
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_c
654
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_c
655
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_c
656
                   Hierarchy4.ni_1._arrow._first_c
657
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_2_x
658
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.__Hierarchy4_Hierarchy4_3_x
659
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_32_x
660
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.__Hierarchy4_Hierarchy4_node_33_x
661
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_2.Hierarchy4_Hierarchy4_node.ni_4._arrow._first_x
662
                   Hierarchy4.ni_0.Hierarchy4_Hierarchy4.ni_3._arrow._first_x
663
                   Hierarchy4.ni_1._arrow._first_x)
664
))
665

    
666
; Hierarchy4_A_ex
667
(declare-var Hierarchy4_A_ex.idHierarchy4_Hierarchy4_1 Int)
668
(declare-var Hierarchy4_A_ex.isInner Bool)
669
(declare-var Hierarchy4_A_ex.idHierarchy4_Hierarchy4 Int)
670
(declare-var Hierarchy4_A_ex.idHierarchy4_Hierarchy4_2 Int)
671
(declare-rel Hierarchy4_A_ex (Int Bool Int))
672
(rule (=> 
673
  (and (and (or (not (= (not Hierarchy4_A_ex.isInner) true))
674
               (= Hierarchy4_A_ex.idHierarchy4_Hierarchy4_2 0))
675
            (or (not (= (not Hierarchy4_A_ex.isInner) false))
676
               (= Hierarchy4_A_ex.idHierarchy4_Hierarchy4_2 Hierarchy4_A_ex.idHierarchy4_Hierarchy4_1))
677
       )
678
       (= Hierarchy4_A_ex.idHierarchy4_Hierarchy4 Hierarchy4_A_ex.idHierarchy4_Hierarchy4_1)
679
       )
680
  (Hierarchy4_A_ex Hierarchy4_A_ex.idHierarchy4_Hierarchy4_1 Hierarchy4_A_ex.isInner Hierarchy4_A_ex.idHierarchy4_Hierarchy4)
681
))
682

    
683
; Hierarchy4_B_ex
684
(declare-var Hierarchy4_B_ex.idHierarchy4_Hierarchy4_1 Int)
685
(declare-var Hierarchy4_B_ex.isInner Bool)
686
(declare-var Hierarchy4_B_ex.idHierarchy4_Hierarchy4 Int)
687
(declare-var Hierarchy4_B_ex.idHierarchy4_Hierarchy4_2 Int)
688
(declare-rel Hierarchy4_B_ex (Int Bool Int))
689
(rule (=> 
690
  (and (and (or (not (= (not Hierarchy4_B_ex.isInner) true))
691
               (= Hierarchy4_B_ex.idHierarchy4_Hierarchy4_2 0))
692
            (or (not (= (not Hierarchy4_B_ex.isInner) false))
693
               (= Hierarchy4_B_ex.idHierarchy4_Hierarchy4_2 Hierarchy4_B_ex.idHierarchy4_Hierarchy4_1))
694
       )
695
       (= Hierarchy4_B_ex.idHierarchy4_Hierarchy4 Hierarchy4_B_ex.idHierarchy4_Hierarchy4_1)
696
       )
697
  (Hierarchy4_B_ex Hierarchy4_B_ex.idHierarchy4_Hierarchy4_1 Hierarchy4_B_ex.isInner Hierarchy4_B_ex.idHierarchy4_Hierarchy4)
698
))
699