Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_SetReset / SetReset.smt2 @ eb639349

History | View | Annotate | Download (75.8 KB)

1
(declare-datatypes () ((setreset_setreset__type POINTSetReset_SetReset POINT__TO__SETRESET_OFF_1 SETRESET_OFF__TO__SETRESET_ON_1 SETRESET_ON__TO__SETRESET_OFF_1 SETRESET_OFF_IDL SETRESET_ON_IDL)));
2

    
3
; SetReset_Off_en
4
(declare-var SetReset_Off_en.idSetReset_SetReset_1 Int)
5
(declare-var SetReset_Off_en.x_1 Int)
6
(declare-var SetReset_Off_en.isInner Bool)
7
(declare-var SetReset_Off_en.idSetReset_SetReset Int)
8
(declare-var SetReset_Off_en.x Int)
9
(declare-var SetReset_Off_en.x_2 Int)
10
(declare-rel SetReset_Off_en (Int Int Bool Int Int))
11
(rule (=> 
12
  (and (and (or (not (= (not SetReset_Off_en.isInner) true))
13
               (= SetReset_Off_en.x_2 0))
14
            (or (not (= (not SetReset_Off_en.isInner) false))
15
               (= SetReset_Off_en.x_2 SetReset_Off_en.x_1))
16
       )
17
       (= SetReset_Off_en.x SetReset_Off_en.x_2)
18
       (= SetReset_Off_en.idSetReset_SetReset 1724)
19
       )
20
  (SetReset_Off_en SetReset_Off_en.idSetReset_SetReset_1 SetReset_Off_en.x_1 SetReset_Off_en.isInner SetReset_Off_en.idSetReset_SetReset SetReset_Off_en.x)
21
))
22

    
23
; SetReset_Off_ex
24
(declare-var SetReset_Off_ex.idSetReset_SetReset_1 Int)
25
(declare-var SetReset_Off_ex.isInner Bool)
26
(declare-var SetReset_Off_ex.idSetReset_SetReset Int)
27
(declare-var SetReset_Off_ex.idSetReset_SetReset_2 Int)
28
(declare-rel SetReset_Off_ex (Int Bool Int))
29
(rule (=> 
30
  (and (and (or (not (= (not SetReset_Off_ex.isInner) true))
31
               (= SetReset_Off_ex.idSetReset_SetReset_2 0))
32
            (or (not (= (not SetReset_Off_ex.isInner) false))
33
               (= SetReset_Off_ex.idSetReset_SetReset_2 SetReset_Off_ex.idSetReset_SetReset_1))
34
       )
35
       (= SetReset_Off_ex.idSetReset_SetReset SetReset_Off_ex.idSetReset_SetReset_1)
36
       )
37
  (SetReset_Off_ex SetReset_Off_ex.idSetReset_SetReset_1 SetReset_Off_ex.isInner SetReset_Off_ex.idSetReset_SetReset)
38
))
39

    
40
; SetReset_On_en
41
(declare-var SetReset_On_en.idSetReset_SetReset_1 Int)
42
(declare-var SetReset_On_en.x_1 Int)
43
(declare-var SetReset_On_en.isInner Bool)
44
(declare-var SetReset_On_en.idSetReset_SetReset Int)
45
(declare-var SetReset_On_en.x Int)
46
(declare-var SetReset_On_en.x_2 Int)
47
(declare-rel SetReset_On_en (Int Int Bool Int Int))
48
(rule (=> 
49
  (and (and (or (not (= (not SetReset_On_en.isInner) true))
50
               (= SetReset_On_en.x_2 1))
51
            (or (not (= (not SetReset_On_en.isInner) false))
52
               (= SetReset_On_en.x_2 SetReset_On_en.x_1))
53
       )
54
       (= SetReset_On_en.x SetReset_On_en.x_2)
55
       (= SetReset_On_en.idSetReset_SetReset 1725)
56
       )
57
  (SetReset_On_en SetReset_On_en.idSetReset_SetReset_1 SetReset_On_en.x_1 SetReset_On_en.isInner SetReset_On_en.idSetReset_SetReset SetReset_On_en.x)
58
))
59

    
60
; SetReset_On_ex
61
(declare-var SetReset_On_ex.idSetReset_SetReset_1 Int)
62
(declare-var SetReset_On_ex.isInner Bool)
63
(declare-var SetReset_On_ex.idSetReset_SetReset Int)
64
(declare-var SetReset_On_ex.idSetReset_SetReset_2 Int)
65
(declare-rel SetReset_On_ex (Int Bool Int))
66
(rule (=> 
67
  (and (and (or (not (= (not SetReset_On_ex.isInner) true))
68
               (= SetReset_On_ex.idSetReset_SetReset_2 0))
69
            (or (not (= (not SetReset_On_ex.isInner) false))
70
               (= SetReset_On_ex.idSetReset_SetReset_2 SetReset_On_ex.idSetReset_SetReset_1))
71
       )
72
       (= SetReset_On_ex.idSetReset_SetReset SetReset_On_ex.idSetReset_SetReset_1)
73
       )
74
  (SetReset_On_ex SetReset_On_ex.idSetReset_SetReset_1 SetReset_On_ex.isInner SetReset_On_ex.idSetReset_SetReset)
75
))
76

    
77
; setreset_setreset__POINTSetReset_SetReset_handler_until
78
(declare-var setreset_setreset__POINTSetReset_SetReset_handler_until.idSetReset_SetReset_1 Int)
79
(declare-var setreset_setreset__POINTSetReset_SetReset_handler_until.x_1 Int)
80
(declare-var setreset_setreset__POINTSetReset_SetReset_handler_until.setreset_setreset__restart_in Bool)
81
(declare-var setreset_setreset__POINTSetReset_SetReset_handler_until.setreset_setreset__state_in setreset_setreset__type)
82
(declare-var setreset_setreset__POINTSetReset_SetReset_handler_until.idSetReset_SetReset_out Int)
83
(declare-var setreset_setreset__POINTSetReset_SetReset_handler_until.x_out Int)
84
(declare-rel setreset_setreset__POINTSetReset_SetReset_handler_until (Int Int Bool setreset_setreset__type Int Int))
85
(rule (=> 
86
  (and (= setreset_setreset__POINTSetReset_SetReset_handler_until.x_out setreset_setreset__POINTSetReset_SetReset_handler_until.x_1)
87
       (= setreset_setreset__POINTSetReset_SetReset_handler_until.setreset_setreset__state_in POINTSetReset_SetReset)
88
       (= setreset_setreset__POINTSetReset_SetReset_handler_until.setreset_setreset__restart_in false)
89
       (= setreset_setreset__POINTSetReset_SetReset_handler_until.idSetReset_SetReset_out setreset_setreset__POINTSetReset_SetReset_handler_until.idSetReset_SetReset_1)
90
       )
91
  (setreset_setreset__POINTSetReset_SetReset_handler_until setreset_setreset__POINTSetReset_SetReset_handler_until.idSetReset_SetReset_1 setreset_setreset__POINTSetReset_SetReset_handler_until.x_1 setreset_setreset__POINTSetReset_SetReset_handler_until.setreset_setreset__restart_in setreset_setreset__POINTSetReset_SetReset_handler_until.setreset_setreset__state_in setreset_setreset__POINTSetReset_SetReset_handler_until.idSetReset_SetReset_out setreset_setreset__POINTSetReset_SetReset_handler_until.x_out)
92
))
93

    
94
; setreset_setreset__POINTSetReset_SetReset_unless
95
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_in Bool)
96
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_in setreset_setreset__type)
97
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.idSetReset_SetReset_1 Int)
98
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.Set Bool)
99
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.Reset Bool)
100
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act Bool)
101
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act setreset_setreset__type)
102
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_1 Bool)
103
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_2 Bool)
104
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_3 Bool)
105
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_4 Bool)
106
(declare-var setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_5 Bool)
107
(declare-rel setreset_setreset__POINTSetReset_SetReset_unless (Bool setreset_setreset__type Int Bool Bool Bool setreset_setreset__type))
108
(rule (=> 
109
  (and (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_5 (= setreset_setreset__POINTSetReset_SetReset_unless.idSetReset_SetReset_1 1725))
110
       (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_4 (= setreset_setreset__POINTSetReset_SetReset_unless.idSetReset_SetReset_1 1724))
111
       (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_3 (and (= setreset_setreset__POINTSetReset_SetReset_unless.idSetReset_SetReset_1 1725) setreset_setreset__POINTSetReset_SetReset_unless.Reset))
112
       (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_2 (and (= setreset_setreset__POINTSetReset_SetReset_unless.idSetReset_SetReset_1 1724) setreset_setreset__POINTSetReset_SetReset_unless.Set))
113
       (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_1 (= setreset_setreset__POINTSetReset_SetReset_unless.idSetReset_SetReset_1 0))
114
       (and (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_1 false))
115
               (and (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_2 false))
116
                       (and (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_3 false))
117
                               (and (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_4 false))
118
                                       (and (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_5 false))
119
                                               (and (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_in)
120
                                                    (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_in)
121
                                                    ))
122
                                            (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_5 true))
123
                                               (and (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act SETRESET_ON_IDL)
124
                                                    (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act true)
125
                                                    ))
126
                                       ))
127
                                    (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_4 true))
128
                                       (and (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act SETRESET_OFF_IDL)
129
                                            (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act true)
130
                                            ))
131
                               ))
132
                            (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_3 true))
133
                               (and (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act SETRESET_ON__TO__SETRESET_OFF_1)
134
                                    (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act true)
135
                                    ))
136
                       ))
137
                    (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_2 true))
138
                       (and (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act SETRESET_OFF__TO__SETRESET_ON_1)
139
                            (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act true)
140
                            ))
141
               ))
142
            (or (not (= setreset_setreset__POINTSetReset_SetReset_unless.__setreset_setreset__POINTSetReset_SetReset_unless_1 true))
143
               (and (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act POINT__TO__SETRESET_OFF_1)
144
                    (= setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act true)
145
                    ))
146
       )
147
       )
148
  (setreset_setreset__POINTSetReset_SetReset_unless setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_in setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_in setreset_setreset__POINTSetReset_SetReset_unless.idSetReset_SetReset_1 setreset_setreset__POINTSetReset_SetReset_unless.Set setreset_setreset__POINTSetReset_SetReset_unless.Reset setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__restart_act setreset_setreset__POINTSetReset_SetReset_unless.setreset_setreset__state_act)
149
))
150

    
151
; setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until
152
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_1 Int)
153
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_1 Int)
154
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.setreset_setreset__restart_in Bool)
155
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.setreset_setreset__state_in setreset_setreset__type)
156
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_out Int)
157
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_out Int)
158
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_2 Int)
159
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_2 Int)
160
(declare-rel setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until (Int Int Bool setreset_setreset__type Int Int))
161
(rule (=> 
162
  (and (SetReset_Off_en setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_1
163
                        setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_1
164
                        false
165
                        setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_2
166
                        setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_2)
167
       (= setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_out setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_2)
168
       (= setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.setreset_setreset__state_in POINTSetReset_SetReset)
169
       (= setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.setreset_setreset__restart_in true)
170
       (= setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_out setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_2)
171
       )
172
  (setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_1 setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_1 setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.setreset_setreset__restart_in setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.setreset_setreset__state_in setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_out setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until.x_out)
173
))
174

    
175
; setreset_setreset__POINT__TO__SETRESET_OFF_1_unless
176
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_in Bool)
177
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__state_in setreset_setreset__type)
178
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_act Bool)
179
(declare-var setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__state_act setreset_setreset__type)
180
(declare-rel setreset_setreset__POINT__TO__SETRESET_OFF_1_unless (Bool setreset_setreset__type Bool setreset_setreset__type))
181
(rule (=> 
182
  (and (= setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__state_act setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__state_in)
183
       (= setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_act setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_in)
184
       )
185
  (setreset_setreset__POINT__TO__SETRESET_OFF_1_unless setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_in setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__state_in setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_act setreset_setreset__POINT__TO__SETRESET_OFF_1_unless.setreset_setreset__state_act)
186
))
187

    
188
; setreset_setreset__SETRESET_OFF_IDL_handler_until
189
(declare-var setreset_setreset__SETRESET_OFF_IDL_handler_until.idSetReset_SetReset_1 Int)
190
(declare-var setreset_setreset__SETRESET_OFF_IDL_handler_until.x_1 Int)
191
(declare-var setreset_setreset__SETRESET_OFF_IDL_handler_until.setreset_setreset__restart_in Bool)
192
(declare-var setreset_setreset__SETRESET_OFF_IDL_handler_until.setreset_setreset__state_in setreset_setreset__type)
193
(declare-var setreset_setreset__SETRESET_OFF_IDL_handler_until.idSetReset_SetReset_out Int)
194
(declare-var setreset_setreset__SETRESET_OFF_IDL_handler_until.x_out Int)
195
(declare-rel setreset_setreset__SETRESET_OFF_IDL_handler_until (Int Int Bool setreset_setreset__type Int Int))
196
(rule (=> 
197
  (and (= setreset_setreset__SETRESET_OFF_IDL_handler_until.x_out setreset_setreset__SETRESET_OFF_IDL_handler_until.x_1)
198
       (= setreset_setreset__SETRESET_OFF_IDL_handler_until.setreset_setreset__state_in POINTSetReset_SetReset)
199
       (= setreset_setreset__SETRESET_OFF_IDL_handler_until.setreset_setreset__restart_in true)
200
       (= setreset_setreset__SETRESET_OFF_IDL_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_OFF_IDL_handler_until.idSetReset_SetReset_1)
201
       )
202
  (setreset_setreset__SETRESET_OFF_IDL_handler_until setreset_setreset__SETRESET_OFF_IDL_handler_until.idSetReset_SetReset_1 setreset_setreset__SETRESET_OFF_IDL_handler_until.x_1 setreset_setreset__SETRESET_OFF_IDL_handler_until.setreset_setreset__restart_in setreset_setreset__SETRESET_OFF_IDL_handler_until.setreset_setreset__state_in setreset_setreset__SETRESET_OFF_IDL_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_OFF_IDL_handler_until.x_out)
203
))
204

    
205
; setreset_setreset__SETRESET_OFF_IDL_unless
206
(declare-var setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__restart_in Bool)
207
(declare-var setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__state_in setreset_setreset__type)
208
(declare-var setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__restart_act Bool)
209
(declare-var setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__state_act setreset_setreset__type)
210
(declare-rel setreset_setreset__SETRESET_OFF_IDL_unless (Bool setreset_setreset__type Bool setreset_setreset__type))
211
(rule (=> 
212
  (and (= setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__state_act setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__state_in)
213
       (= setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__restart_in)
214
       )
215
  (setreset_setreset__SETRESET_OFF_IDL_unless setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__restart_in setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__state_in setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_OFF_IDL_unless.setreset_setreset__state_act)
216
))
217

    
218
; setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until
219
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_1 Int)
220
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_1 Int)
221
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.setreset_setreset__restart_in Bool)
222
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.setreset_setreset__state_in setreset_setreset__type)
223
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_out Int)
224
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_out Int)
225
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_2 Int)
226
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_3 Int)
227
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_2 Int)
228
(declare-rel setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until (Int Int Bool setreset_setreset__type Int Int))
229
(rule (=> 
230
  (and (SetReset_Off_ex setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_1
231
                        false
232
                        setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_2)
233
       (SetReset_On_en setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_2
234
                       setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_1
235
                       false
236
                       setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_3
237
                       setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_2)
238
       (= setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_out setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_2)
239
       (= setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.setreset_setreset__state_in POINTSetReset_SetReset)
240
       (= setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.setreset_setreset__restart_in true)
241
       (= setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_3)
242
       )
243
  (setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_1 setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_1 setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.setreset_setreset__restart_in setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.setreset_setreset__state_in setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until.x_out)
244
))
245

    
246
; setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless
247
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__restart_in Bool)
248
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__state_in setreset_setreset__type)
249
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__restart_act Bool)
250
(declare-var setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__state_act setreset_setreset__type)
251
(declare-rel setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless (Bool setreset_setreset__type Bool setreset_setreset__type))
252
(rule (=> 
253
  (and (= setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__state_act setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__state_in)
254
       (= setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__restart_in)
255
       )
256
  (setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__restart_in setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__state_in setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless.setreset_setreset__state_act)
257
))
258

    
259
; setreset_setreset__SETRESET_ON_IDL_handler_until
260
(declare-var setreset_setreset__SETRESET_ON_IDL_handler_until.idSetReset_SetReset_1 Int)
261
(declare-var setreset_setreset__SETRESET_ON_IDL_handler_until.x_1 Int)
262
(declare-var setreset_setreset__SETRESET_ON_IDL_handler_until.setreset_setreset__restart_in Bool)
263
(declare-var setreset_setreset__SETRESET_ON_IDL_handler_until.setreset_setreset__state_in setreset_setreset__type)
264
(declare-var setreset_setreset__SETRESET_ON_IDL_handler_until.idSetReset_SetReset_out Int)
265
(declare-var setreset_setreset__SETRESET_ON_IDL_handler_until.x_out Int)
266
(declare-rel setreset_setreset__SETRESET_ON_IDL_handler_until (Int Int Bool setreset_setreset__type Int Int))
267
(rule (=> 
268
  (and (= setreset_setreset__SETRESET_ON_IDL_handler_until.x_out setreset_setreset__SETRESET_ON_IDL_handler_until.x_1)
269
       (= setreset_setreset__SETRESET_ON_IDL_handler_until.setreset_setreset__state_in POINTSetReset_SetReset)
270
       (= setreset_setreset__SETRESET_ON_IDL_handler_until.setreset_setreset__restart_in true)
271
       (= setreset_setreset__SETRESET_ON_IDL_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_ON_IDL_handler_until.idSetReset_SetReset_1)
272
       )
273
  (setreset_setreset__SETRESET_ON_IDL_handler_until setreset_setreset__SETRESET_ON_IDL_handler_until.idSetReset_SetReset_1 setreset_setreset__SETRESET_ON_IDL_handler_until.x_1 setreset_setreset__SETRESET_ON_IDL_handler_until.setreset_setreset__restart_in setreset_setreset__SETRESET_ON_IDL_handler_until.setreset_setreset__state_in setreset_setreset__SETRESET_ON_IDL_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_ON_IDL_handler_until.x_out)
274
))
275

    
276
; setreset_setreset__SETRESET_ON_IDL_unless
277
(declare-var setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__restart_in Bool)
278
(declare-var setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__state_in setreset_setreset__type)
279
(declare-var setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__restart_act Bool)
280
(declare-var setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__state_act setreset_setreset__type)
281
(declare-rel setreset_setreset__SETRESET_ON_IDL_unless (Bool setreset_setreset__type Bool setreset_setreset__type))
282
(rule (=> 
283
  (and (= setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__state_act setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__state_in)
284
       (= setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__restart_in)
285
       )
286
  (setreset_setreset__SETRESET_ON_IDL_unless setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__restart_in setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__state_in setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_ON_IDL_unless.setreset_setreset__state_act)
287
))
288

    
289
; setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until
290
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_1 Int)
291
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_1 Int)
292
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.setreset_setreset__restart_in Bool)
293
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.setreset_setreset__state_in setreset_setreset__type)
294
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_out Int)
295
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_out Int)
296
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_2 Int)
297
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_3 Int)
298
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_2 Int)
299
(declare-rel setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until (Int Int Bool setreset_setreset__type Int Int))
300
(rule (=> 
301
  (and (SetReset_On_ex setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_1
302
                       false
303
                       setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_2)
304
       (SetReset_Off_en setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_2
305
                        setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_1
306
                        false
307
                        setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_3
308
                        setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_2)
309
       (= setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_out setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_2)
310
       (= setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.setreset_setreset__state_in POINTSetReset_SetReset)
311
       (= setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.setreset_setreset__restart_in true)
312
       (= setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_3)
313
       )
314
  (setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_1 setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_1 setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.setreset_setreset__restart_in setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.setreset_setreset__state_in setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.idSetReset_SetReset_out setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until.x_out)
315
))
316

    
317
; setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless
318
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_in Bool)
319
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__state_in setreset_setreset__type)
320
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_act Bool)
321
(declare-var setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__state_act setreset_setreset__type)
322
(declare-rel setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless (Bool setreset_setreset__type Bool setreset_setreset__type))
323
(rule (=> 
324
  (and (= setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__state_act setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__state_in)
325
       (= setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_in)
326
       )
327
  (setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_in setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__state_in setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__restart_act setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless.setreset_setreset__state_act)
328
))
329

    
330
; SetReset_SetReset_node
331
(declare-var SetReset_SetReset_node.idSetReset_SetReset_1 Int)
332
(declare-var SetReset_SetReset_node.x_1 Int)
333
(declare-var SetReset_SetReset_node.Set Bool)
334
(declare-var SetReset_SetReset_node.Reset Bool)
335
(declare-var SetReset_SetReset_node.idSetReset_SetReset Int)
336
(declare-var SetReset_SetReset_node.x Int)
337
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_38_c Bool)
338
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_39_c setreset_setreset__type)
339
(declare-var SetReset_SetReset_node.ni_5._arrow._first_c Bool)
340
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_38_m Bool)
341
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_39_m setreset_setreset__type)
342
(declare-var SetReset_SetReset_node.ni_5._arrow._first_m Bool)
343
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_38_x Bool)
344
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_39_x setreset_setreset__type)
345
(declare-var SetReset_SetReset_node.ni_5._arrow._first_x Bool)
346
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_1 Bool)
347
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_10 setreset_setreset__type)
348
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_11 Bool)
349
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_12 setreset_setreset__type)
350
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_13 Bool)
351
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_14 setreset_setreset__type)
352
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_15 Int)
353
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_16 Int)
354
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_17 Bool)
355
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_18 setreset_setreset__type)
356
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_19 Int)
357
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_2 setreset_setreset__type)
358
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_20 Int)
359
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_21 Bool)
360
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_22 setreset_setreset__type)
361
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_23 Int)
362
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_24 Int)
363
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_25 Bool)
364
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_26 setreset_setreset__type)
365
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_27 Int)
366
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_28 Int)
367
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_29 Bool)
368
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_3 Bool)
369
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_30 setreset_setreset__type)
370
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_31 Int)
371
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_32 Int)
372
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_33 Bool)
373
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_34 setreset_setreset__type)
374
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_35 Int)
375
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_36 Int)
376
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_37 Bool)
377
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_4 setreset_setreset__type)
378
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_5 Bool)
379
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_6 setreset_setreset__type)
380
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_7 Bool)
381
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_8 setreset_setreset__type)
382
(declare-var SetReset_SetReset_node.__SetReset_SetReset_node_9 Bool)
383
(declare-var SetReset_SetReset_node.setreset_setreset__next_restart_in Bool)
384
(declare-var SetReset_SetReset_node.setreset_setreset__next_state_in setreset_setreset__type)
385
(declare-var SetReset_SetReset_node.setreset_setreset__restart_act Bool)
386
(declare-var SetReset_SetReset_node.setreset_setreset__restart_in Bool)
387
(declare-var SetReset_SetReset_node.setreset_setreset__state_act setreset_setreset__type)
388
(declare-var SetReset_SetReset_node.setreset_setreset__state_in setreset_setreset__type)
389
(declare-rel SetReset_SetReset_node_reset (Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool))
390
(declare-rel SetReset_SetReset_node_step (Int Int Bool Bool Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool))
391

    
392
(rule (=> 
393
  (and 
394
       (= SetReset_SetReset_node.__SetReset_SetReset_node_38_m SetReset_SetReset_node.__SetReset_SetReset_node_38_c)
395
       (= SetReset_SetReset_node.__SetReset_SetReset_node_39_m SetReset_SetReset_node.__SetReset_SetReset_node_39_c)
396
       (= SetReset_SetReset_node.ni_5._arrow._first_m true)
397
  )
398
  (SetReset_SetReset_node_reset SetReset_SetReset_node.__SetReset_SetReset_node_38_c
399
                                SetReset_SetReset_node.__SetReset_SetReset_node_39_c
400
                                SetReset_SetReset_node.ni_5._arrow._first_c
401
                                SetReset_SetReset_node.__SetReset_SetReset_node_38_m
402
                                SetReset_SetReset_node.__SetReset_SetReset_node_39_m
403
                                SetReset_SetReset_node.ni_5._arrow._first_m)
404
))
405

    
406
(rule (=> 
407
  (and (= SetReset_SetReset_node.ni_5._arrow._first_m SetReset_SetReset_node.ni_5._arrow._first_c)
408
       (and (= SetReset_SetReset_node.__SetReset_SetReset_node_37 (ite SetReset_SetReset_node.ni_5._arrow._first_m true false))
409
            (= SetReset_SetReset_node.ni_5._arrow._first_x false))
410
       (and (or (not (= SetReset_SetReset_node.__SetReset_SetReset_node_37 false))
411
               (and (= SetReset_SetReset_node.setreset_setreset__state_in SetReset_SetReset_node.__SetReset_SetReset_node_39_c)
412
                    (= SetReset_SetReset_node.setreset_setreset__restart_in SetReset_SetReset_node.__SetReset_SetReset_node_38_c)
413
                    ))
414
            (or (not (= SetReset_SetReset_node.__SetReset_SetReset_node_37 true))
415
               (and (= SetReset_SetReset_node.setreset_setreset__state_in POINTSetReset_SetReset)
416
                    (= SetReset_SetReset_node.setreset_setreset__restart_in false)
417
                    ))
418
       )
419
       (and (or (not (= SetReset_SetReset_node.setreset_setreset__state_in POINTSetReset_SetReset))
420
               (and (setreset_setreset__POINTSetReset_SetReset_unless 
421
                    SetReset_SetReset_node.setreset_setreset__restart_in
422
                    SetReset_SetReset_node.setreset_setreset__state_in
423
                    SetReset_SetReset_node.idSetReset_SetReset_1
424
                    SetReset_SetReset_node.Set
425
                    SetReset_SetReset_node.Reset
426
                    SetReset_SetReset_node.__SetReset_SetReset_node_11
427
                    SetReset_SetReset_node.__SetReset_SetReset_node_12)
428
                    (= SetReset_SetReset_node.setreset_setreset__state_act SetReset_SetReset_node.__SetReset_SetReset_node_12)
429
                    (= SetReset_SetReset_node.setreset_setreset__restart_act SetReset_SetReset_node.__SetReset_SetReset_node_11)
430
                    ))
431
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_in POINT__TO__SETRESET_OFF_1))
432
               (and (setreset_setreset__POINT__TO__SETRESET_OFF_1_unless 
433
                    SetReset_SetReset_node.setreset_setreset__restart_in
434
                    SetReset_SetReset_node.setreset_setreset__state_in
435
                    SetReset_SetReset_node.__SetReset_SetReset_node_9
436
                    SetReset_SetReset_node.__SetReset_SetReset_node_10)
437
                    (= SetReset_SetReset_node.setreset_setreset__state_act SetReset_SetReset_node.__SetReset_SetReset_node_10)
438
                    (= SetReset_SetReset_node.setreset_setreset__restart_act SetReset_SetReset_node.__SetReset_SetReset_node_9)
439
                    ))
440
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_in SETRESET_OFF_IDL))
441
               (and (setreset_setreset__SETRESET_OFF_IDL_unless SetReset_SetReset_node.setreset_setreset__restart_in
442
                                                                SetReset_SetReset_node.setreset_setreset__state_in
443
                                                                SetReset_SetReset_node.__SetReset_SetReset_node_3
444
                                                                SetReset_SetReset_node.__SetReset_SetReset_node_4)
445
                    (= SetReset_SetReset_node.setreset_setreset__state_act SetReset_SetReset_node.__SetReset_SetReset_node_4)
446
                    (= SetReset_SetReset_node.setreset_setreset__restart_act SetReset_SetReset_node.__SetReset_SetReset_node_3)
447
                    ))
448
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_in SETRESET_OFF__TO__SETRESET_ON_1))
449
               (and (setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_unless 
450
                    SetReset_SetReset_node.setreset_setreset__restart_in
451
                    SetReset_SetReset_node.setreset_setreset__state_in
452
                    SetReset_SetReset_node.__SetReset_SetReset_node_7
453
                    SetReset_SetReset_node.__SetReset_SetReset_node_8)
454
                    (= SetReset_SetReset_node.setreset_setreset__state_act SetReset_SetReset_node.__SetReset_SetReset_node_8)
455
                    (= SetReset_SetReset_node.setreset_setreset__restart_act SetReset_SetReset_node.__SetReset_SetReset_node_7)
456
                    ))
457
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_in SETRESET_ON_IDL))
458
               (and (setreset_setreset__SETRESET_ON_IDL_unless SetReset_SetReset_node.setreset_setreset__restart_in
459
                                                               SetReset_SetReset_node.setreset_setreset__state_in
460
                                                               SetReset_SetReset_node.__SetReset_SetReset_node_1
461
                                                               SetReset_SetReset_node.__SetReset_SetReset_node_2)
462
                    (= SetReset_SetReset_node.setreset_setreset__state_act SetReset_SetReset_node.__SetReset_SetReset_node_2)
463
                    (= SetReset_SetReset_node.setreset_setreset__restart_act SetReset_SetReset_node.__SetReset_SetReset_node_1)
464
                    ))
465
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_in SETRESET_ON__TO__SETRESET_OFF_1))
466
               (and (setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_unless 
467
                    SetReset_SetReset_node.setreset_setreset__restart_in
468
                    SetReset_SetReset_node.setreset_setreset__state_in
469
                    SetReset_SetReset_node.__SetReset_SetReset_node_5
470
                    SetReset_SetReset_node.__SetReset_SetReset_node_6)
471
                    (= SetReset_SetReset_node.setreset_setreset__state_act SetReset_SetReset_node.__SetReset_SetReset_node_6)
472
                    (= SetReset_SetReset_node.setreset_setreset__restart_act SetReset_SetReset_node.__SetReset_SetReset_node_5)
473
                    ))
474
       )
475
       (and (or (not (= SetReset_SetReset_node.setreset_setreset__state_act POINTSetReset_SetReset))
476
               (and (setreset_setreset__POINTSetReset_SetReset_handler_until 
477
                    SetReset_SetReset_node.idSetReset_SetReset_1
478
                    SetReset_SetReset_node.x_1
479
                    SetReset_SetReset_node.__SetReset_SetReset_node_33
480
                    SetReset_SetReset_node.__SetReset_SetReset_node_34
481
                    SetReset_SetReset_node.__SetReset_SetReset_node_35
482
                    SetReset_SetReset_node.__SetReset_SetReset_node_36)
483
                    (= SetReset_SetReset_node.x SetReset_SetReset_node.__SetReset_SetReset_node_36)
484
                    (= SetReset_SetReset_node.setreset_setreset__next_state_in SetReset_SetReset_node.__SetReset_SetReset_node_34)
485
                    (= SetReset_SetReset_node.setreset_setreset__next_restart_in SetReset_SetReset_node.__SetReset_SetReset_node_33)
486
                    (= SetReset_SetReset_node.idSetReset_SetReset SetReset_SetReset_node.__SetReset_SetReset_node_35)
487
                    ))
488
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_act POINT__TO__SETRESET_OFF_1))
489
               (and (setreset_setreset__POINT__TO__SETRESET_OFF_1_handler_until 
490
                    SetReset_SetReset_node.idSetReset_SetReset_1
491
                    SetReset_SetReset_node.x_1
492
                    SetReset_SetReset_node.__SetReset_SetReset_node_29
493
                    SetReset_SetReset_node.__SetReset_SetReset_node_30
494
                    SetReset_SetReset_node.__SetReset_SetReset_node_31
495
                    SetReset_SetReset_node.__SetReset_SetReset_node_32)
496
                    (= SetReset_SetReset_node.x SetReset_SetReset_node.__SetReset_SetReset_node_32)
497
                    (= SetReset_SetReset_node.setreset_setreset__next_state_in SetReset_SetReset_node.__SetReset_SetReset_node_30)
498
                    (= SetReset_SetReset_node.setreset_setreset__next_restart_in SetReset_SetReset_node.__SetReset_SetReset_node_29)
499
                    (= SetReset_SetReset_node.idSetReset_SetReset SetReset_SetReset_node.__SetReset_SetReset_node_31)
500
                    ))
501
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_act SETRESET_OFF_IDL))
502
               (and (setreset_setreset__SETRESET_OFF_IDL_handler_until 
503
                    SetReset_SetReset_node.idSetReset_SetReset_1
504
                    SetReset_SetReset_node.x_1
505
                    SetReset_SetReset_node.__SetReset_SetReset_node_17
506
                    SetReset_SetReset_node.__SetReset_SetReset_node_18
507
                    SetReset_SetReset_node.__SetReset_SetReset_node_19
508
                    SetReset_SetReset_node.__SetReset_SetReset_node_20)
509
                    (= SetReset_SetReset_node.x SetReset_SetReset_node.__SetReset_SetReset_node_20)
510
                    (= SetReset_SetReset_node.setreset_setreset__next_state_in SetReset_SetReset_node.__SetReset_SetReset_node_18)
511
                    (= SetReset_SetReset_node.setreset_setreset__next_restart_in SetReset_SetReset_node.__SetReset_SetReset_node_17)
512
                    (= SetReset_SetReset_node.idSetReset_SetReset SetReset_SetReset_node.__SetReset_SetReset_node_19)
513
                    ))
514
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_act SETRESET_OFF__TO__SETRESET_ON_1))
515
               (and (setreset_setreset__SETRESET_OFF__TO__SETRESET_ON_1_handler_until 
516
                    SetReset_SetReset_node.idSetReset_SetReset_1
517
                    SetReset_SetReset_node.x_1
518
                    SetReset_SetReset_node.__SetReset_SetReset_node_25
519
                    SetReset_SetReset_node.__SetReset_SetReset_node_26
520
                    SetReset_SetReset_node.__SetReset_SetReset_node_27
521
                    SetReset_SetReset_node.__SetReset_SetReset_node_28)
522
                    (= SetReset_SetReset_node.x SetReset_SetReset_node.__SetReset_SetReset_node_28)
523
                    (= SetReset_SetReset_node.setreset_setreset__next_state_in SetReset_SetReset_node.__SetReset_SetReset_node_26)
524
                    (= SetReset_SetReset_node.setreset_setreset__next_restart_in SetReset_SetReset_node.__SetReset_SetReset_node_25)
525
                    (= SetReset_SetReset_node.idSetReset_SetReset SetReset_SetReset_node.__SetReset_SetReset_node_27)
526
                    ))
527
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_act SETRESET_ON_IDL))
528
               (and (setreset_setreset__SETRESET_ON_IDL_handler_until 
529
                    SetReset_SetReset_node.idSetReset_SetReset_1
530
                    SetReset_SetReset_node.x_1
531
                    SetReset_SetReset_node.__SetReset_SetReset_node_13
532
                    SetReset_SetReset_node.__SetReset_SetReset_node_14
533
                    SetReset_SetReset_node.__SetReset_SetReset_node_15
534
                    SetReset_SetReset_node.__SetReset_SetReset_node_16)
535
                    (= SetReset_SetReset_node.x SetReset_SetReset_node.__SetReset_SetReset_node_16)
536
                    (= SetReset_SetReset_node.setreset_setreset__next_state_in SetReset_SetReset_node.__SetReset_SetReset_node_14)
537
                    (= SetReset_SetReset_node.setreset_setreset__next_restart_in SetReset_SetReset_node.__SetReset_SetReset_node_13)
538
                    (= SetReset_SetReset_node.idSetReset_SetReset SetReset_SetReset_node.__SetReset_SetReset_node_15)
539
                    ))
540
            (or (not (= SetReset_SetReset_node.setreset_setreset__state_act SETRESET_ON__TO__SETRESET_OFF_1))
541
               (and (setreset_setreset__SETRESET_ON__TO__SETRESET_OFF_1_handler_until 
542
                    SetReset_SetReset_node.idSetReset_SetReset_1
543
                    SetReset_SetReset_node.x_1
544
                    SetReset_SetReset_node.__SetReset_SetReset_node_21
545
                    SetReset_SetReset_node.__SetReset_SetReset_node_22
546
                    SetReset_SetReset_node.__SetReset_SetReset_node_23
547
                    SetReset_SetReset_node.__SetReset_SetReset_node_24)
548
                    (= SetReset_SetReset_node.x SetReset_SetReset_node.__SetReset_SetReset_node_24)
549
                    (= SetReset_SetReset_node.setreset_setreset__next_state_in SetReset_SetReset_node.__SetReset_SetReset_node_22)
550
                    (= SetReset_SetReset_node.setreset_setreset__next_restart_in SetReset_SetReset_node.__SetReset_SetReset_node_21)
551
                    (= SetReset_SetReset_node.idSetReset_SetReset SetReset_SetReset_node.__SetReset_SetReset_node_23)
552
                    ))
553
       )
554
       (= SetReset_SetReset_node.__SetReset_SetReset_node_39_x SetReset_SetReset_node.setreset_setreset__next_state_in)
555
       (= SetReset_SetReset_node.__SetReset_SetReset_node_38_x SetReset_SetReset_node.setreset_setreset__next_restart_in)
556
       )
557
  (SetReset_SetReset_node_step SetReset_SetReset_node.idSetReset_SetReset_1
558
                               SetReset_SetReset_node.x_1
559
                               SetReset_SetReset_node.Set
560
                               SetReset_SetReset_node.Reset
561
                               SetReset_SetReset_node.idSetReset_SetReset
562
                               SetReset_SetReset_node.x
563
                               SetReset_SetReset_node.__SetReset_SetReset_node_38_c
564
                               SetReset_SetReset_node.__SetReset_SetReset_node_39_c
565
                               SetReset_SetReset_node.ni_5._arrow._first_c
566
                               SetReset_SetReset_node.__SetReset_SetReset_node_38_x
567
                               SetReset_SetReset_node.__SetReset_SetReset_node_39_x
568
                               SetReset_SetReset_node.ni_5._arrow._first_x)
569
))
570

    
571
; SetReset_SetReset
572
(declare-var SetReset_SetReset.Set Bool)
573
(declare-var SetReset_SetReset.Reset Bool)
574
(declare-var SetReset_SetReset.x Int)
575
(declare-var SetReset_SetReset.__SetReset_SetReset_6_c Int)
576
(declare-var SetReset_SetReset.__SetReset_SetReset_7_c Int)
577
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c Bool)
578
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c setreset_setreset__type)
579
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c Bool)
580
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c Bool)
581
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c setreset_setreset__type)
582
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c Bool)
583
(declare-var SetReset_SetReset.ni_4._arrow._first_c Bool)
584
(declare-var SetReset_SetReset.__SetReset_SetReset_6_m Int)
585
(declare-var SetReset_SetReset.__SetReset_SetReset_7_m Int)
586
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m Bool)
587
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m setreset_setreset__type)
588
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m Bool)
589
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m Bool)
590
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m setreset_setreset__type)
591
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m Bool)
592
(declare-var SetReset_SetReset.ni_4._arrow._first_m Bool)
593
(declare-var SetReset_SetReset.__SetReset_SetReset_6_x Int)
594
(declare-var SetReset_SetReset.__SetReset_SetReset_7_x Int)
595
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_x Bool)
596
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_x setreset_setreset__type)
597
(declare-var SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_x Bool)
598
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_x Bool)
599
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_x setreset_setreset__type)
600
(declare-var SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_x Bool)
601
(declare-var SetReset_SetReset.ni_4._arrow._first_x Bool)
602
(declare-var SetReset_SetReset.__SetReset_SetReset_1 Int)
603
(declare-var SetReset_SetReset.__SetReset_SetReset_2 Int)
604
(declare-var SetReset_SetReset.__SetReset_SetReset_3 Int)
605
(declare-var SetReset_SetReset.__SetReset_SetReset_4 Int)
606
(declare-var SetReset_SetReset.__SetReset_SetReset_5 Bool)
607
(declare-var SetReset_SetReset.idSetReset_SetReset Int)
608
(declare-var SetReset_SetReset.idSetReset_SetReset_1 Int)
609
(declare-var SetReset_SetReset.idSetReset_SetReset_2 Int)
610
(declare-var SetReset_SetReset.x_1 Int)
611
(declare-var SetReset_SetReset.x_2 Int)
612
(declare-rel SetReset_SetReset_reset (Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool))
613
(declare-rel SetReset_SetReset_step (Bool Bool Int Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool))
614

    
615
(rule (=> 
616
  (and 
617
       (= SetReset_SetReset.__SetReset_SetReset_6_m SetReset_SetReset.__SetReset_SetReset_6_c)
618
       (= SetReset_SetReset.__SetReset_SetReset_7_m SetReset_SetReset.__SetReset_SetReset_7_c)
619
       (= SetReset_SetReset.ni_4._arrow._first_m true)
620
       (SetReset_SetReset_node_reset SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
621
                                     SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
622
                                     SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c
623
                                     SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
624
                                     SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
625
                                     SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m)
626
       (SetReset_SetReset_node_reset SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
627
                                     SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
628
                                     SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c
629
                                     SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
630
                                     SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
631
                                     SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m)
632
  )
633
  (SetReset_SetReset_reset SetReset_SetReset.__SetReset_SetReset_6_c
634
                           SetReset_SetReset.__SetReset_SetReset_7_c
635
                           SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
636
                           SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
637
                           SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c
638
                           SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
639
                           SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
640
                           SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c
641
                           SetReset_SetReset.ni_4._arrow._first_c
642
                           SetReset_SetReset.__SetReset_SetReset_6_m
643
                           SetReset_SetReset.__SetReset_SetReset_7_m
644
                           SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
645
                           SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
646
                           SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m
647
                           SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
648
                           SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
649
                           SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m
650
                           SetReset_SetReset.ni_4._arrow._first_m)
651
))
652

    
653
(rule (=> 
654
  (and (= SetReset_SetReset.ni_4._arrow._first_m SetReset_SetReset.ni_4._arrow._first_c)
655
       (and (= SetReset_SetReset.__SetReset_SetReset_5 (ite SetReset_SetReset.ni_4._arrow._first_m true false))
656
            (= SetReset_SetReset.ni_4._arrow._first_x false))
657
       (and (or (not (= SetReset_SetReset.__SetReset_SetReset_5 false))
658
               (and (= SetReset_SetReset.x_1 SetReset_SetReset.__SetReset_SetReset_7_c)
659
                    (= SetReset_SetReset.idSetReset_SetReset_1 SetReset_SetReset.__SetReset_SetReset_6_c)
660
                    ))
661
            (or (not (= SetReset_SetReset.__SetReset_SetReset_5 true))
662
               (and (= SetReset_SetReset.x_1 0)
663
                    (= SetReset_SetReset.idSetReset_SetReset_1 0)
664
                    ))
665
       )
666
       (and (= SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c)
667
            (= SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c)
668
            (= SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c)
669
            )
670
       (SetReset_SetReset_node_step SetReset_SetReset.idSetReset_SetReset_1
671
                                    SetReset_SetReset.x_1
672
                                    SetReset_SetReset.Set
673
                                    false
674
                                    SetReset_SetReset.__SetReset_SetReset_3
675
                                    SetReset_SetReset.__SetReset_SetReset_4
676
                                    SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
677
                                    SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
678
                                    SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m
679
                                    SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
680
                                    SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
681
                                    SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_x)
682
       (and (or (not (= SetReset_SetReset.Set false))
683
               (and (= SetReset_SetReset.x_2 SetReset_SetReset.x_1)
684
                    (= SetReset_SetReset.idSetReset_SetReset_2 SetReset_SetReset.idSetReset_SetReset_1)
685
                    ))
686
            (or (not (= SetReset_SetReset.Set true))
687
               (and (= SetReset_SetReset.x_2 SetReset_SetReset.__SetReset_SetReset_4)
688
                    (= SetReset_SetReset.idSetReset_SetReset_2 SetReset_SetReset.__SetReset_SetReset_3)
689
                    ))
690
       )
691
       (and (= SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c)
692
            (= SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c)
693
            (= SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c)
694
            )
695
       (SetReset_SetReset_node_step SetReset_SetReset.idSetReset_SetReset_2
696
                                    SetReset_SetReset.x_2
697
                                    false
698
                                    SetReset_SetReset.Reset
699
                                    SetReset_SetReset.__SetReset_SetReset_1
700
                                    SetReset_SetReset.__SetReset_SetReset_2
701
                                    SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
702
                                    SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
703
                                    SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m
704
                                    SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
705
                                    SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
706
                                    SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_x)
707
       (and (or (not (= SetReset_SetReset.Reset false))
708
               (and (= SetReset_SetReset.x SetReset_SetReset.x_2)
709
                    (= SetReset_SetReset.idSetReset_SetReset SetReset_SetReset.idSetReset_SetReset_2)
710
                    ))
711
            (or (not (= SetReset_SetReset.Reset true))
712
               (and (= SetReset_SetReset.x SetReset_SetReset.__SetReset_SetReset_2)
713
                    (= SetReset_SetReset.idSetReset_SetReset SetReset_SetReset.__SetReset_SetReset_1)
714
                    ))
715
       )
716
       (= SetReset_SetReset.__SetReset_SetReset_7_x SetReset_SetReset.x)
717
       (= SetReset_SetReset.__SetReset_SetReset_6_x SetReset_SetReset.idSetReset_SetReset)
718
       )
719
  (SetReset_SetReset_step SetReset_SetReset.Set
720
                          SetReset_SetReset.Reset
721
                          SetReset_SetReset.x
722
                          SetReset_SetReset.__SetReset_SetReset_6_c
723
                          SetReset_SetReset.__SetReset_SetReset_7_c
724
                          SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
725
                          SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
726
                          SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c
727
                          SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
728
                          SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
729
                          SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c
730
                          SetReset_SetReset.ni_4._arrow._first_c
731
                          SetReset_SetReset.__SetReset_SetReset_6_x
732
                          SetReset_SetReset.__SetReset_SetReset_7_x
733
                          SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
734
                          SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
735
                          SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_x
736
                          SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
737
                          SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
738
                          SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_x
739
                          SetReset_SetReset.ni_4._arrow._first_x)
740
))
741

    
742
; SetReset
743
(declare-var SetReset.Set_1_1 Real)
744
(declare-var SetReset.Reset_1_1 Real)
745
(declare-var SetReset.output_1_1 Int)
746
(declare-var SetReset.__SetReset_2_c Real)
747
(declare-var SetReset.__SetReset_3_c Real)
748
(declare-var SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_c Int)
749
(declare-var SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_c Int)
750
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c Bool)
751
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c setreset_setreset__type)
752
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c Bool)
753
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c Bool)
754
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c setreset_setreset__type)
755
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c Bool)
756
(declare-var SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_c Bool)
757
(declare-var SetReset.ni_1._arrow._first_c Bool)
758
(declare-var SetReset.__SetReset_2_m Real)
759
(declare-var SetReset.__SetReset_3_m Real)
760
(declare-var SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_m Int)
761
(declare-var SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_m Int)
762
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m Bool)
763
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m setreset_setreset__type)
764
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m Bool)
765
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m Bool)
766
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m setreset_setreset__type)
767
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m Bool)
768
(declare-var SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_m Bool)
769
(declare-var SetReset.ni_1._arrow._first_m Bool)
770
(declare-var SetReset.__SetReset_2_x Real)
771
(declare-var SetReset.__SetReset_3_x Real)
772
(declare-var SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_x Int)
773
(declare-var SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_x Int)
774
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_x Bool)
775
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_x setreset_setreset__type)
776
(declare-var SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_x Bool)
777
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_x Bool)
778
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_x setreset_setreset__type)
779
(declare-var SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_x Bool)
780
(declare-var SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_x Bool)
781
(declare-var SetReset.ni_1._arrow._first_x Bool)
782
(declare-var SetReset.SetResetMux_1_1_event Bool)
783
(declare-var SetReset.SetResetMux_1_2_event Bool)
784
(declare-var SetReset.SetReset_1_1 Int)
785
(declare-var SetReset.__SetReset_1 Bool)
786
(declare-var SetReset.i_virtual_local Real)
787
(declare-rel SetReset_reset (Real Real Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool Bool Real Real Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool Bool))
788
(declare-rel SetReset_step (Real Real Int Real Real Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool Bool Real Real Int Int Bool setreset_setreset__type Bool Bool setreset_setreset__type Bool Bool Bool))
789

    
790
(rule (=> 
791
  (and 
792
       (= SetReset.__SetReset_2_m SetReset.__SetReset_2_c)
793
       (= SetReset.__SetReset_3_m SetReset.__SetReset_3_c)
794
       (= SetReset.ni_1._arrow._first_m true)
795
       (SetReset_SetReset_reset SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_c
796
                                SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_c
797
                                SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
798
                                SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
799
                                SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c
800
                                SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
801
                                SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
802
                                SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c
803
                                SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_c
804
                                SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_m
805
                                SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_m
806
                                SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
807
                                SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
808
                                SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m
809
                                SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
810
                                SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
811
                                SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m
812
                                SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_m)
813
  )
814
  (SetReset_reset SetReset.__SetReset_2_c
815
                  SetReset.__SetReset_3_c
816
                  SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_c
817
                  SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_c
818
                  SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
819
                  SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
820
                  SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c
821
                  SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
822
                  SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
823
                  SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c
824
                  SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_c
825
                  SetReset.ni_1._arrow._first_c
826
                  SetReset.__SetReset_2_m
827
                  SetReset.__SetReset_3_m
828
                  SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_m
829
                  SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_m
830
                  SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
831
                  SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
832
                  SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m
833
                  SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
834
                  SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
835
                  SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m
836
                  SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_m
837
                  SetReset.ni_1._arrow._first_m)
838
))
839

    
840
(rule (=> 
841
  (and (= SetReset.ni_1._arrow._first_m SetReset.ni_1._arrow._first_c)
842
       (and (= SetReset.__SetReset_1 (ite SetReset.ni_1._arrow._first_m true false))
843
            (= SetReset.ni_1._arrow._first_x false))
844
       (and (or (not (= SetReset.__SetReset_1 true))
845
               (= SetReset.SetResetMux_1_2_event false))
846
            (or (not (= SetReset.__SetReset_1 false))
847
               (= SetReset.SetResetMux_1_2_event (and (<= SetReset.__SetReset_2_c 0.) (> SetReset.Reset_1_1 0.))))
848
       )
849
       (and (or (not (= SetReset.__SetReset_1 true))
850
               (= SetReset.SetResetMux_1_1_event false))
851
            (or (not (= SetReset.__SetReset_1 false))
852
               (= SetReset.SetResetMux_1_1_event (and (<= SetReset.__SetReset_3_c 0.) (> SetReset.Set_1_1 0.))))
853
       )
854
       (and (= SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_m SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_c)
855
            (= SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_m SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_c)
856
            (= SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c)
857
            (= SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c)
858
            (= SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c)
859
            (= SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c)
860
            (= SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c)
861
            (= SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c)
862
            (= SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_m SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_c)
863
            )
864
       (SetReset_SetReset_step SetReset.SetResetMux_1_1_event
865
                               SetReset.SetResetMux_1_2_event
866
                               SetReset.SetReset_1_1
867
                               SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_m
868
                               SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_m
869
                               SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
870
                               SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
871
                               SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_m
872
                               SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_m
873
                               SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_m
874
                               SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_m
875
                               SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_m
876
                               SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_x
877
                               SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_x
878
                               SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
879
                               SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
880
                               SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_x
881
                               SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
882
                               SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
883
                               SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_x
884
                               SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_x)
885
       (= SetReset.output_1_1 SetReset.SetReset_1_1)
886
       (and (or (not (= SetReset.__SetReset_1 true))
887
               (= SetReset.i_virtual_local 0.))
888
            (or (not (= SetReset.__SetReset_1 false))
889
               (= SetReset.i_virtual_local 1.))
890
       )
891
       (= SetReset.__SetReset_3_x SetReset.Set_1_1)
892
       (= SetReset.__SetReset_2_x SetReset.Reset_1_1)
893
       )
894
  (SetReset_step SetReset.Set_1_1
895
                 SetReset.Reset_1_1
896
                 SetReset.output_1_1
897
                 SetReset.__SetReset_2_c
898
                 SetReset.__SetReset_3_c
899
                 SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_c
900
                 SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_c
901
                 SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
902
                 SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
903
                 SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_c
904
                 SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_c
905
                 SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_c
906
                 SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_c
907
                 SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_c
908
                 SetReset.ni_1._arrow._first_c
909
                 SetReset.__SetReset_2_x
910
                 SetReset.__SetReset_3_x
911
                 SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_6_x
912
                 SetReset.ni_0.SetReset_SetReset.__SetReset_SetReset_7_x
913
                 SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
914
                 SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
915
                 SetReset.ni_0.SetReset_SetReset.ni_2.SetReset_SetReset_node.ni_5._arrow._first_x
916
                 SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_38_x
917
                 SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.__SetReset_SetReset_node_39_x
918
                 SetReset.ni_0.SetReset_SetReset.ni_3.SetReset_SetReset_node.ni_5._arrow._first_x
919
                 SetReset.ni_0.SetReset_SetReset.ni_4._arrow._first_x
920
                 SetReset.ni_1._arrow._first_x)
921
))
922