Project

General

Profile

Download (29.5 KB) Statistics
| Branch: | Tag: | Revision:
1
(declare-datatypes () ((four_states__type One Two Three Four)));
2

    
3
; four_states__Four_handler_until
4
(declare-var four_states__Four_handler_until.four_states__restart_act Bool)
5
(declare-var four_states__Four_handler_until.four_states__state_act four_states__type)
6
(declare-var four_states__Four_handler_until.four_states__restart_in Bool)
7
(declare-var four_states__Four_handler_until.four_states__state_in four_states__type)
8
(declare-var four_states__Four_handler_until._state_out Int)
9
(declare-rel four_states__Four_handler_until (Bool four_states__type Bool four_states__type Int))
10
(rule (=> 
11
  (and (= four_states__Four_handler_until.four_states__state_in One)
12
       (= four_states__Four_handler_until.four_states__restart_in true)
13
       (= four_states__Four_handler_until._state_out 4)
14
       )
15
  (four_states__Four_handler_until four_states__Four_handler_until.four_states__restart_act four_states__Four_handler_until.four_states__state_act four_states__Four_handler_until.four_states__restart_in four_states__Four_handler_until.four_states__state_in four_states__Four_handler_until._state_out)
16
))
17

    
18
; four_states__Four_unless
19
(declare-var four_states__Four_unless.four_states__restart_in Bool)
20
(declare-var four_states__Four_unless.four_states__state_in four_states__type)
21
(declare-var four_states__Four_unless.four_states__restart_act Bool)
22
(declare-var four_states__Four_unless.four_states__state_act four_states__type)
23
(declare-rel four_states__Four_unless (Bool four_states__type Bool four_states__type))
24
(rule (=> 
25
  (and (= four_states__Four_unless.four_states__state_act four_states__Four_unless.four_states__state_in)
26
       (= four_states__Four_unless.four_states__restart_act four_states__Four_unless.four_states__restart_in)
27
       )
28
  (four_states__Four_unless four_states__Four_unless.four_states__restart_in four_states__Four_unless.four_states__state_in four_states__Four_unless.four_states__restart_act four_states__Four_unless.four_states__state_act)
29
))
30

    
31
; four_states__One_handler_until
32
(declare-var four_states__One_handler_until.four_states__restart_act Bool)
33
(declare-var four_states__One_handler_until.four_states__state_act four_states__type)
34
(declare-var four_states__One_handler_until.four_states__restart_in Bool)
35
(declare-var four_states__One_handler_until.four_states__state_in four_states__type)
36
(declare-var four_states__One_handler_until._state_out Int)
37
(declare-rel four_states__One_handler_until (Bool four_states__type Bool four_states__type Int))
38
(rule (=> 
39
  (and (= four_states__One_handler_until.four_states__state_in Two)
40
       (= four_states__One_handler_until.four_states__restart_in true)
41
       (= four_states__One_handler_until._state_out 1)
42
       )
43
  (four_states__One_handler_until four_states__One_handler_until.four_states__restart_act four_states__One_handler_until.four_states__state_act four_states__One_handler_until.four_states__restart_in four_states__One_handler_until.four_states__state_in four_states__One_handler_until._state_out)
44
))
45

    
46
; four_states__One_unless
47
(declare-var four_states__One_unless.four_states__restart_in Bool)
48
(declare-var four_states__One_unless.four_states__state_in four_states__type)
49
(declare-var four_states__One_unless.four_states__restart_act Bool)
50
(declare-var four_states__One_unless.four_states__state_act four_states__type)
51
(declare-rel four_states__One_unless (Bool four_states__type Bool four_states__type))
52
(rule (=> 
53
  (and (= four_states__One_unless.four_states__state_act four_states__One_unless.four_states__state_in)
54
       (= four_states__One_unless.four_states__restart_act four_states__One_unless.four_states__restart_in)
55
       )
56
  (four_states__One_unless four_states__One_unless.four_states__restart_in four_states__One_unless.four_states__state_in four_states__One_unless.four_states__restart_act four_states__One_unless.four_states__state_act)
57
))
58

    
59
; four_states__Three_handler_until
60
(declare-var four_states__Three_handler_until.four_states__restart_act Bool)
61
(declare-var four_states__Three_handler_until.four_states__state_act four_states__type)
62
(declare-var four_states__Three_handler_until.four_states__restart_in Bool)
63
(declare-var four_states__Three_handler_until.four_states__state_in four_states__type)
64
(declare-var four_states__Three_handler_until._state_out Int)
65
(declare-rel four_states__Three_handler_until (Bool four_states__type Bool four_states__type Int))
66
(rule (=> 
67
  (and (= four_states__Three_handler_until.four_states__state_in Four)
68
       (= four_states__Three_handler_until.four_states__restart_in true)
69
       (= four_states__Three_handler_until._state_out 3)
70
       )
71
  (four_states__Three_handler_until four_states__Three_handler_until.four_states__restart_act four_states__Three_handler_until.four_states__state_act four_states__Three_handler_until.four_states__restart_in four_states__Three_handler_until.four_states__state_in four_states__Three_handler_until._state_out)
72
))
73

    
74
; four_states__Three_unless
75
(declare-var four_states__Three_unless.four_states__restart_in Bool)
76
(declare-var four_states__Three_unless.four_states__state_in four_states__type)
77
(declare-var four_states__Three_unless.four_states__restart_act Bool)
78
(declare-var four_states__Three_unless.four_states__state_act four_states__type)
79
(declare-rel four_states__Three_unless (Bool four_states__type Bool four_states__type))
80
(rule (=> 
81
  (and (= four_states__Three_unless.four_states__state_act four_states__Three_unless.four_states__state_in)
82
       (= four_states__Three_unless.four_states__restart_act four_states__Three_unless.four_states__restart_in)
83
       )
84
  (four_states__Three_unless four_states__Three_unless.four_states__restart_in four_states__Three_unless.four_states__state_in four_states__Three_unless.four_states__restart_act four_states__Three_unless.four_states__state_act)
85
))
86

    
87
; four_states__Two_handler_until
88
(declare-var four_states__Two_handler_until.four_states__restart_act Bool)
89
(declare-var four_states__Two_handler_until.four_states__state_act four_states__type)
90
(declare-var four_states__Two_handler_until.four_states__restart_in Bool)
91
(declare-var four_states__Two_handler_until.four_states__state_in four_states__type)
92
(declare-var four_states__Two_handler_until._state_out Int)
93
(declare-rel four_states__Two_handler_until (Bool four_states__type Bool four_states__type Int))
94
(rule (=> 
95
  (and (= four_states__Two_handler_until.four_states__state_in Three)
96
       (= four_states__Two_handler_until.four_states__restart_in true)
97
       (= four_states__Two_handler_until._state_out 2)
98
       )
99
  (four_states__Two_handler_until four_states__Two_handler_until.four_states__restart_act four_states__Two_handler_until.four_states__state_act four_states__Two_handler_until.four_states__restart_in four_states__Two_handler_until.four_states__state_in four_states__Two_handler_until._state_out)
100
))
101

    
102
; four_states__Two_unless
103
(declare-var four_states__Two_unless.four_states__restart_in Bool)
104
(declare-var four_states__Two_unless.four_states__state_in four_states__type)
105
(declare-var four_states__Two_unless.four_states__restart_act Bool)
106
(declare-var four_states__Two_unless.four_states__state_act four_states__type)
107
(declare-rel four_states__Two_unless (Bool four_states__type Bool four_states__type))
108
(rule (=> 
109
  (and (= four_states__Two_unless.four_states__state_act four_states__Two_unless.four_states__state_in)
110
       (= four_states__Two_unless.four_states__restart_act four_states__Two_unless.four_states__restart_in)
111
       )
112
  (four_states__Two_unless four_states__Two_unless.four_states__restart_in four_states__Two_unless.four_states__state_in four_states__Two_unless.four_states__restart_act four_states__Two_unless.four_states__state_act)
113
))
114

    
115
; auto
116
(declare-var auto.x Bool)
117
(declare-var auto._state Int)
118
(declare-var auto.__auto_22_c Bool)
119
(declare-var auto.__auto_23_c four_states__type)
120
(declare-var auto.ni_5._arrow._first_c Bool)
121
(declare-var auto.__auto_22_m Bool)
122
(declare-var auto.__auto_23_m four_states__type)
123
(declare-var auto.ni_5._arrow._first_m Bool)
124
(declare-var auto.__auto_22_x Bool)
125
(declare-var auto.__auto_23_x four_states__type)
126
(declare-var auto.ni_5._arrow._first_x Bool)
127
(declare-var auto.__auto_1 Bool)
128
(declare-var auto.__auto_10 four_states__type)
129
(declare-var auto.__auto_11 Int)
130
(declare-var auto.__auto_12 Bool)
131
(declare-var auto.__auto_13 four_states__type)
132
(declare-var auto.__auto_14 Int)
133
(declare-var auto.__auto_15 Bool)
134
(declare-var auto.__auto_16 four_states__type)
135
(declare-var auto.__auto_17 Int)
136
(declare-var auto.__auto_18 Bool)
137
(declare-var auto.__auto_19 four_states__type)
138
(declare-var auto.__auto_2 four_states__type)
139
(declare-var auto.__auto_20 Int)
140
(declare-var auto.__auto_21 Bool)
141
(declare-var auto.__auto_3 Bool)
142
(declare-var auto.__auto_4 four_states__type)
143
(declare-var auto.__auto_5 Bool)
144
(declare-var auto.__auto_6 four_states__type)
145
(declare-var auto.__auto_7 Bool)
146
(declare-var auto.__auto_8 four_states__type)
147
(declare-var auto.__auto_9 Bool)
148
(declare-var auto.four_states__next_restart_in Bool)
149
(declare-var auto.four_states__next_state_in four_states__type)
150
(declare-var auto.four_states__restart_act Bool)
151
(declare-var auto.four_states__restart_in Bool)
152
(declare-var auto.four_states__state_act four_states__type)
153
(declare-var auto.four_states__state_in four_states__type)
154
(declare-rel auto_reset (Bool four_states__type Bool Bool four_states__type Bool))
155
(declare-rel auto_step (Bool Int Bool four_states__type Bool Bool four_states__type Bool))
156

    
157
(rule (=> 
158
  (and 
159
       (= auto.__auto_22_m auto.__auto_22_c)
160
       (= auto.__auto_23_m auto.__auto_23_c)
161
       (= auto.ni_5._arrow._first_m true)
162
  )
163
  (auto_reset auto.__auto_22_c
164
              auto.__auto_23_c
165
              auto.ni_5._arrow._first_c
166
              auto.__auto_22_m
167
              auto.__auto_23_m
168
              auto.ni_5._arrow._first_m)
169
))
170

    
171
(rule (=> 
172
  (and (= auto.ni_5._arrow._first_m auto.ni_5._arrow._first_c)(and (= auto.__auto_21 (ite auto.ni_5._arrow._first_m true false))
173
                                                                   (= auto.ni_5._arrow._first_x false))
174
       (and (or (not (= auto.__auto_21 false))
175
               (and (= auto.four_states__state_in auto.__auto_23_c)
176
                    (= auto.four_states__restart_in auto.__auto_22_c)
177
                    ))
178
            (or (not (= auto.__auto_21 true))
179
               (and (= auto.four_states__state_in One)
180
                    (= auto.four_states__restart_in false)
181
                    ))
182
       )
183
       (and (or (not (= auto.four_states__state_in Four))
184
               (and (four_states__Four_unless auto.four_states__restart_in
185
                                              auto.four_states__state_in
186
                                              auto.__auto_1
187
                                              auto.__auto_2)
188
                    (= auto.four_states__state_act auto.__auto_2)
189
                    (= auto.four_states__restart_act auto.__auto_1)
190
                    ))
191
            (or (not (= auto.four_states__state_in One))
192
               (and (four_states__One_unless auto.four_states__restart_in
193
                                             auto.four_states__state_in
194
                                             auto.__auto_7
195
                                             auto.__auto_8)
196
                    (= auto.four_states__state_act auto.__auto_8)
197
                    (= auto.four_states__restart_act auto.__auto_7)
198
                    ))
199
            (or (not (= auto.four_states__state_in Three))
200
               (and (four_states__Three_unless auto.four_states__restart_in
201
                                               auto.four_states__state_in
202
                                               auto.__auto_3
203
                                               auto.__auto_4)
204
                    (= auto.four_states__state_act auto.__auto_4)
205
                    (= auto.four_states__restart_act auto.__auto_3)
206
                    ))
207
            (or (not (= auto.four_states__state_in Two))
208
               (and (four_states__Two_unless auto.four_states__restart_in
209
                                             auto.four_states__state_in
210
                                             auto.__auto_5
211
                                             auto.__auto_6)
212
                    (= auto.four_states__state_act auto.__auto_6)
213
                    (= auto.four_states__restart_act auto.__auto_5)
214
                    ))
215
       )
216
       (and (or (not (= auto.four_states__state_act Four))
217
               (and (four_states__Four_handler_until auto.four_states__restart_act
218
                                                     auto.four_states__state_act
219
                                                     auto.__auto_9
220
                                                     auto.__auto_10
221
                                                     auto.__auto_11)
222
                    (= auto.four_states__next_state_in auto.__auto_10)
223
                    (= auto.four_states__next_restart_in auto.__auto_9)
224
                    (= auto._state auto.__auto_11)
225
                    ))
226
            (or (not (= auto.four_states__state_act One))
227
               (and (four_states__One_handler_until auto.four_states__restart_act
228
                                                    auto.four_states__state_act
229
                                                    auto.__auto_18
230
                                                    auto.__auto_19
231
                                                    auto.__auto_20)
232
                    (= auto.four_states__next_state_in auto.__auto_19)
233
                    (= auto.four_states__next_restart_in auto.__auto_18)
234
                    (= auto._state auto.__auto_20)
235
                    ))
236
            (or (not (= auto.four_states__state_act Three))
237
               (and (four_states__Three_handler_until auto.four_states__restart_act
238
                                                      auto.four_states__state_act
239
                                                      auto.__auto_12
240
                                                      auto.__auto_13
241
                                                      auto.__auto_14)
242
                    (= auto.four_states__next_state_in auto.__auto_13)
243
                    (= auto.four_states__next_restart_in auto.__auto_12)
244
                    (= auto._state auto.__auto_14)
245
                    ))
246
            (or (not (= auto.four_states__state_act Two))
247
               (and (four_states__Two_handler_until auto.four_states__restart_act
248
                                                    auto.four_states__state_act
249
                                                    auto.__auto_15
250
                                                    auto.__auto_16
251
                                                    auto.__auto_17)
252
                    (= auto.four_states__next_state_in auto.__auto_16)
253
                    (= auto.four_states__next_restart_in auto.__auto_15)
254
                    (= auto._state auto.__auto_17)
255
                    ))
256
       )
257
       (= auto.__auto_23_x auto.four_states__next_state_in)
258
       (= auto.__auto_22_x auto.four_states__next_restart_in)
259
       )
260
  (auto_step auto.x
261
             auto._state
262
             auto.__auto_22_c
263
             auto.__auto_23_c
264
             auto.ni_5._arrow._first_c
265
             auto.__auto_22_x
266
             auto.__auto_23_x
267
             auto.ni_5._arrow._first_x)
268
))
269

    
270
; greycounter
271
(declare-var greycounter.x Bool)
272
(declare-var greycounter.out Bool)
273
(declare-var greycounter.__greycounter_2_c Bool)
274
(declare-var greycounter.__greycounter_3_c Bool)
275
(declare-var greycounter.ni_4._arrow._first_c Bool)
276
(declare-var greycounter.__greycounter_2_m Bool)
277
(declare-var greycounter.__greycounter_3_m Bool)
278
(declare-var greycounter.ni_4._arrow._first_m Bool)
279
(declare-var greycounter.__greycounter_2_x Bool)
280
(declare-var greycounter.__greycounter_3_x Bool)
281
(declare-var greycounter.ni_4._arrow._first_x Bool)
282
(declare-var greycounter.__greycounter_1 Bool)
283
(declare-var greycounter.a Bool)
284
(declare-var greycounter.b Bool)
285
(declare-rel greycounter_reset (Bool Bool Bool Bool Bool Bool))
286
(declare-rel greycounter_step (Bool Bool Bool Bool Bool Bool Bool Bool))
287

    
288
(rule (=> 
289
  (and 
290
       (= greycounter.__greycounter_2_m greycounter.__greycounter_2_c)
291
       (= greycounter.__greycounter_3_m greycounter.__greycounter_3_c)
292
       (= greycounter.ni_4._arrow._first_m true)
293
  )
294
  (greycounter_reset greycounter.__greycounter_2_c
295
                     greycounter.__greycounter_3_c
296
                     greycounter.ni_4._arrow._first_c
297
                     greycounter.__greycounter_2_m
298
                     greycounter.__greycounter_3_m
299
                     greycounter.ni_4._arrow._first_m)
300
))
301

    
302
(rule (=> 
303
  (and (= greycounter.ni_4._arrow._first_m greycounter.ni_4._arrow._first_c)
304
       (and (= greycounter.__greycounter_1 (ite greycounter.ni_4._arrow._first_m true false))
305
            (= greycounter.ni_4._arrow._first_x false))
306
       (and (or (not (= greycounter.__greycounter_1 false))
307
               (and (= greycounter.b greycounter.__greycounter_2_c)
308
                    (= greycounter.a (not greycounter.__greycounter_3_c))
309
                    ))
310
            (or (not (= greycounter.__greycounter_1 true))
311
               (and (= greycounter.b false)
312
                    (= greycounter.a false)
313
                    ))
314
       )
315
       (= greycounter.out (and greycounter.a greycounter.b))
316
       (= greycounter.__greycounter_3_x greycounter.b)
317
       (= greycounter.__greycounter_2_x greycounter.a)
318
       )
319
  (greycounter_step greycounter.x
320
                    greycounter.out
321
                    greycounter.__greycounter_2_c
322
                    greycounter.__greycounter_3_c
323
                    greycounter.ni_4._arrow._first_c
324
                    greycounter.__greycounter_2_x
325
                    greycounter.__greycounter_3_x
326
                    greycounter.ni_4._arrow._first_x)
327
))
328

    
329
; intloopcounter
330
(declare-var intloopcounter.x Bool)
331
(declare-var intloopcounter.out Bool)
332
(declare-var intloopcounter.__intloopcounter_2_c Int)
333
(declare-var intloopcounter.ni_3._arrow._first_c Bool)
334
(declare-var intloopcounter.__intloopcounter_2_m Int)
335
(declare-var intloopcounter.ni_3._arrow._first_m Bool)
336
(declare-var intloopcounter.__intloopcounter_2_x Int)
337
(declare-var intloopcounter.ni_3._arrow._first_x Bool)
338
(declare-var intloopcounter.__intloopcounter_1 Bool)
339
(declare-var intloopcounter.__intloopcounter_3 Bool)
340
(declare-var intloopcounter.time Int)
341
(declare-rel intloopcounter_reset (Int Bool Int Bool))
342
(declare-rel intloopcounter_step (Bool Bool Int Bool Int Bool))
343

    
344
(rule (=> 
345
  (and 
346
       (= intloopcounter.__intloopcounter_2_m intloopcounter.__intloopcounter_2_c)
347
       (= intloopcounter.ni_3._arrow._first_m true)
348
  )
349
  (intloopcounter_reset intloopcounter.__intloopcounter_2_c
350
                        intloopcounter.ni_3._arrow._first_c
351
                        intloopcounter.__intloopcounter_2_m
352
                        intloopcounter.ni_3._arrow._first_m)
353
))
354

    
355
(rule (=> 
356
  (and (= intloopcounter.__intloopcounter_3 (= intloopcounter.__intloopcounter_2_c 3))
357
       (= intloopcounter.ni_3._arrow._first_m intloopcounter.ni_3._arrow._first_c)
358
       (and (= intloopcounter.__intloopcounter_1 (ite intloopcounter.ni_3._arrow._first_m true false))
359
            (= intloopcounter.ni_3._arrow._first_x false))
360
       (and (or (not (= intloopcounter.__intloopcounter_1 true))
361
               (= intloopcounter.time 0))
362
            (or (not (= intloopcounter.__intloopcounter_1 false))
363
               (and (or (not (= intloopcounter.__intloopcounter_3 true))
364
                       (= intloopcounter.time 0))
365
                    (or (not (= intloopcounter.__intloopcounter_3 false))
366
                       (= intloopcounter.time (+ intloopcounter.__intloopcounter_2_c 1)))
367
               ))
368
       )
369
       (= intloopcounter.out (= intloopcounter.time 2))
370
       (= intloopcounter.__intloopcounter_2_x intloopcounter.time)
371
       )
372
  (intloopcounter_step intloopcounter.x
373
                       intloopcounter.out
374
                       intloopcounter.__intloopcounter_2_c
375
                       intloopcounter.ni_3._arrow._first_c
376
                       intloopcounter.__intloopcounter_2_x
377
                       intloopcounter.ni_3._arrow._first_x)
378
))
379

    
380
; top
381
(declare-var top.x Bool)
382
(declare-var top.OK Bool)
383
(declare-var top.ni_0.greycounter.__greycounter_2_c Bool)
384
(declare-var top.ni_0.greycounter.__greycounter_3_c Bool)
385
(declare-var top.ni_0.greycounter.ni_4._arrow._first_c Bool)
386
(declare-var top.ni_1.intloopcounter.__intloopcounter_2_c Int)
387
(declare-var top.ni_1.intloopcounter.ni_3._arrow._first_c Bool)
388
(declare-var top.ni_2.auto.__auto_22_c Bool)
389
(declare-var top.ni_2.auto.__auto_23_c four_states__type)
390
(declare-var top.ni_2.auto.ni_5._arrow._first_c Bool)
391
(declare-var top.ni_0.greycounter.__greycounter_2_m Bool)
392
(declare-var top.ni_0.greycounter.__greycounter_3_m Bool)
393
(declare-var top.ni_0.greycounter.ni_4._arrow._first_m Bool)
394
(declare-var top.ni_1.intloopcounter.__intloopcounter_2_m Int)
395
(declare-var top.ni_1.intloopcounter.ni_3._arrow._first_m Bool)
396
(declare-var top.ni_2.auto.__auto_22_m Bool)
397
(declare-var top.ni_2.auto.__auto_23_m four_states__type)
398
(declare-var top.ni_2.auto.ni_5._arrow._first_m Bool)
399
(declare-var top.ni_0.greycounter.__greycounter_2_x Bool)
400
(declare-var top.ni_0.greycounter.__greycounter_3_x Bool)
401
(declare-var top.ni_0.greycounter.ni_4._arrow._first_x Bool)
402
(declare-var top.ni_1.intloopcounter.__intloopcounter_2_x Int)
403
(declare-var top.ni_1.intloopcounter.ni_3._arrow._first_x Bool)
404
(declare-var top.ni_2.auto.__auto_22_x Bool)
405
(declare-var top.ni_2.auto.__auto_23_x four_states__type)
406
(declare-var top.ni_2.auto.ni_5._arrow._first_x Bool)
407
(declare-var top.a Bool)
408
(declare-var top.b Bool)
409
(declare-var top.d Bool)
410
(declare-var top.s Int)
411
(declare-rel top_reset (Bool Bool Bool Int Bool Bool four_states__type Bool Bool Bool Bool Int Bool Bool four_states__type Bool))
412
(declare-rel top_step (Bool Bool Bool Bool Bool Int Bool Bool four_states__type Bool Bool Bool Bool Int Bool Bool four_states__type Bool))
413

    
414
(rule (=> 
415
  (and 
416
       
417
       (auto_reset top.ni_2.auto.__auto_22_c top.ni_2.auto.__auto_23_c
418
                   top.ni_2.auto.ni_5._arrow._first_c
419
                   top.ni_2.auto.__auto_22_m top.ni_2.auto.__auto_23_m
420
                   top.ni_2.auto.ni_5._arrow._first_m)
421
       (intloopcounter_reset top.ni_1.intloopcounter.__intloopcounter_2_c
422
                             top.ni_1.intloopcounter.ni_3._arrow._first_c
423
                             top.ni_1.intloopcounter.__intloopcounter_2_m
424
                             top.ni_1.intloopcounter.ni_3._arrow._first_m)
425
       (greycounter_reset top.ni_0.greycounter.__greycounter_2_c
426
                          top.ni_0.greycounter.__greycounter_3_c
427
                          top.ni_0.greycounter.ni_4._arrow._first_c
428
                          top.ni_0.greycounter.__greycounter_2_m
429
                          top.ni_0.greycounter.__greycounter_3_m
430
                          top.ni_0.greycounter.ni_4._arrow._first_m)
431
  )
432
  (top_reset top.ni_0.greycounter.__greycounter_2_c
433
             top.ni_0.greycounter.__greycounter_3_c
434
             top.ni_0.greycounter.ni_4._arrow._first_c
435
             top.ni_1.intloopcounter.__intloopcounter_2_c
436
             top.ni_1.intloopcounter.ni_3._arrow._first_c
437
             top.ni_2.auto.__auto_22_c
438
             top.ni_2.auto.__auto_23_c
439
             top.ni_2.auto.ni_5._arrow._first_c
440
             top.ni_0.greycounter.__greycounter_2_m
441
             top.ni_0.greycounter.__greycounter_3_m
442
             top.ni_0.greycounter.ni_4._arrow._first_m
443
             top.ni_1.intloopcounter.__intloopcounter_2_m
444
             top.ni_1.intloopcounter.ni_3._arrow._first_m
445
             top.ni_2.auto.__auto_22_m
446
             top.ni_2.auto.__auto_23_m
447
             top.ni_2.auto.ni_5._arrow._first_m)
448
))
449

    
450
(rule (=> 
451
  (and (and (= top.ni_2.auto.__auto_22_m top.ni_2.auto.__auto_22_c)
452
            (= top.ni_2.auto.__auto_23_m top.ni_2.auto.__auto_23_c)
453
            (= top.ni_2.auto.ni_5._arrow._first_m top.ni_2.auto.ni_5._arrow._first_c)
454
            )
455
       (auto_step top.x
456
                  top.s
457
                  top.ni_2.auto.__auto_22_m
458
                  top.ni_2.auto.__auto_23_m
459
                  top.ni_2.auto.ni_5._arrow._first_m
460
                  top.ni_2.auto.__auto_22_x
461
                  top.ni_2.auto.__auto_23_x
462
                  top.ni_2.auto.ni_5._arrow._first_x)
463
       (and (= top.ni_1.intloopcounter.__intloopcounter_2_m top.ni_1.intloopcounter.__intloopcounter_2_c)
464
            (= top.ni_1.intloopcounter.ni_3._arrow._first_m top.ni_1.intloopcounter.ni_3._arrow._first_c)
465
            )
466
       (intloopcounter_step top.x
467
                            top.d
468
                            top.ni_1.intloopcounter.__intloopcounter_2_m
469
                            top.ni_1.intloopcounter.ni_3._arrow._first_m
470
                            top.ni_1.intloopcounter.__intloopcounter_2_x
471
                            top.ni_1.intloopcounter.ni_3._arrow._first_x)
472
       (and (= top.ni_0.greycounter.__greycounter_2_m top.ni_0.greycounter.__greycounter_2_c)
473
            (= top.ni_0.greycounter.__greycounter_3_m top.ni_0.greycounter.__greycounter_3_c)
474
            (= top.ni_0.greycounter.ni_4._arrow._first_m top.ni_0.greycounter.ni_4._arrow._first_c)
475
            )
476
       (greycounter_step top.x
477
                         top.b
478
                         top.ni_0.greycounter.__greycounter_2_m
479
                         top.ni_0.greycounter.__greycounter_3_m
480
                         top.ni_0.greycounter.ni_4._arrow._first_m
481
                         top.ni_0.greycounter.__greycounter_2_x
482
                         top.ni_0.greycounter.__greycounter_3_x
483
                         top.ni_0.greycounter.ni_4._arrow._first_x)
484
       (= top.a (= top.s 3))
485
       (= top.OK (= top.a top.d))
486
       )
487
  (top_step top.x
488
            top.OK
489
            top.ni_0.greycounter.__greycounter_2_c
490
            top.ni_0.greycounter.__greycounter_3_c
491
            top.ni_0.greycounter.ni_4._arrow._first_c
492
            top.ni_1.intloopcounter.__intloopcounter_2_c
493
            top.ni_1.intloopcounter.ni_3._arrow._first_c
494
            top.ni_2.auto.__auto_22_c
495
            top.ni_2.auto.__auto_23_c
496
            top.ni_2.auto.ni_5._arrow._first_c
497
            top.ni_0.greycounter.__greycounter_2_x
498
            top.ni_0.greycounter.__greycounter_3_x
499
            top.ni_0.greycounter.ni_4._arrow._first_x
500
            top.ni_1.intloopcounter.__intloopcounter_2_x
501
            top.ni_1.intloopcounter.ni_3._arrow._first_x
502
            top.ni_2.auto.__auto_22_x
503
            top.ni_2.auto.__auto_23_x
504
            top.ni_2.auto.ni_5._arrow._first_x)
505
))
506

    
507
; Collecting semantics for node top
508

    
509
(declare-rel MAIN (Bool Bool Bool Int Bool Bool four_states__type Bool Bool))
510
; Initial set: Reset(c,m) + One Step(m,x) 
511
(declare-rel INIT_STATE ())
512
(rule INIT_STATE)
513
(rule (=> 
514
  (and INIT_STATE
515
       (top_reset top.ni_0.greycounter.__greycounter_2_c top.ni_0.greycounter.__greycounter_3_c top.ni_0.greycounter.ni_4._arrow._first_c top.ni_1.intloopcounter.__intloopcounter_2_c top.ni_1.intloopcounter.ni_3._arrow._first_c top.ni_2.auto.__auto_22_c top.ni_2.auto.__auto_23_c top.ni_2.auto.ni_5._arrow._first_c top.ni_0.greycounter.__greycounter_2_m top.ni_0.greycounter.__greycounter_3_m top.ni_0.greycounter.ni_4._arrow._first_m top.ni_1.intloopcounter.__intloopcounter_2_m top.ni_1.intloopcounter.ni_3._arrow._first_m top.ni_2.auto.__auto_22_m top.ni_2.auto.__auto_23_m top.ni_2.auto.ni_5._arrow._first_m)
516
       (top_step top.x top.OK top.ni_0.greycounter.__greycounter_2_m top.ni_0.greycounter.__greycounter_3_m top.ni_0.greycounter.ni_4._arrow._first_m top.ni_1.intloopcounter.__intloopcounter_2_m top.ni_1.intloopcounter.ni_3._arrow._first_m top.ni_2.auto.__auto_22_m top.ni_2.auto.__auto_23_m top.ni_2.auto.ni_5._arrow._first_m top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_0.greycounter.ni_4._arrow._first_x top.ni_1.intloopcounter.__intloopcounter_2_x top.ni_1.intloopcounter.ni_3._arrow._first_x top.ni_2.auto.__auto_22_x top.ni_2.auto.__auto_23_x top.ni_2.auto.ni_5._arrow._first_x)
517
  )
518
  (MAIN top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_0.greycounter.ni_4._arrow._first_x top.ni_1.intloopcounter.__intloopcounter_2_x top.ni_1.intloopcounter.ni_3._arrow._first_x top.ni_2.auto.__auto_22_x top.ni_2.auto.__auto_23_x top.ni_2.auto.ni_5._arrow._first_x top.OK)
519
))
520

    
521
; Inductive def
522
(declare-var dummytop.OK Bool)
523
(rule (=> 
524
  (and (MAIN top.ni_0.greycounter.__greycounter_2_c top.ni_0.greycounter.__greycounter_3_c top.ni_0.greycounter.ni_4._arrow._first_c top.ni_1.intloopcounter.__intloopcounter_2_c top.ni_1.intloopcounter.ni_3._arrow._first_c top.ni_2.auto.__auto_22_c top.ni_2.auto.__auto_23_c top.ni_2.auto.ni_5._arrow._first_c dummytop.OK)
525
       (top_step top.x top.OK top.ni_0.greycounter.__greycounter_2_c top.ni_0.greycounter.__greycounter_3_c top.ni_0.greycounter.ni_4._arrow._first_c top.ni_1.intloopcounter.__intloopcounter_2_c top.ni_1.intloopcounter.ni_3._arrow._first_c top.ni_2.auto.__auto_22_c top.ni_2.auto.__auto_23_c top.ni_2.auto.ni_5._arrow._first_c top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_0.greycounter.ni_4._arrow._first_x top.ni_1.intloopcounter.__intloopcounter_2_x top.ni_1.intloopcounter.ni_3._arrow._first_x top.ni_2.auto.__auto_22_x top.ni_2.auto.__auto_23_x top.ni_2.auto.ni_5._arrow._first_x)
526
  )
527
  (MAIN top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_0.greycounter.ni_4._arrow._first_x top.ni_1.intloopcounter.__intloopcounter_2_x top.ni_1.intloopcounter.ni_3._arrow._first_x top.ni_2.auto.__auto_22_x top.ni_2.auto.__auto_23_x top.ni_2.auto.ni_5._arrow._first_x top.OK)
528
))
529

    
530
; Property def
531
(declare-rel ERR ())
532
(rule (=> 
533
  (and (not top.OK)
534
       (MAIN top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_0.greycounter.ni_4._arrow._first_x top.ni_1.intloopcounter.__intloopcounter_2_x top.ni_1.intloopcounter.ni_3._arrow._first_x top.ni_2.auto.__auto_22_x top.ni_2.auto.__auto_23_x top.ni_2.auto.ni_5._arrow._first_x top.OK))
535
  ERR))
536
(query ERR)
(4-4/11)