Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / two_counters.smt2 @ 0c9457a0

History | View | Annotate | Download (6.45 KB)

1 b8dc00eb bourbouh
; greycounter
2
(declare-var greycounter.x Bool)
3
(declare-var greycounter.out Bool)
4
(declare-var greycounter.__greycounter_2_c Bool)
5
(declare-var greycounter.__greycounter_3_c Bool)
6
(declare-var greycounter.__greycounter_2_x Bool)
7
(declare-var greycounter.__greycounter_3_x Bool)
8
(declare-var greycounter.__greycounter_1 Bool)
9
(declare-var greycounter.a Bool)
10
(declare-var greycounter.b Bool)
11
(declare-rel greycounter_init (Bool Bool Bool Bool))
12
(declare-rel greycounter_step (Bool Bool Bool Bool Bool Bool))
13
14
(rule (=> 
15
  (and (= greycounter.__greycounter_1 true) (= greycounter.b (ite greycounter.__greycounter_1
16
                                                                false
17
                                                                greycounter.__greycounter_2_c)) (= greycounter.a (
18
       ite greycounter.__greycounter_1 false
19
         (not greycounter.__greycounter_3_c))) (= greycounter.out (and greycounter.a greycounter.b)) (= greycounter.__greycounter_3_x greycounter.b) (= greycounter.__greycounter_2_x greycounter.a)
20
  )
21
  (greycounter_init greycounter.x greycounter.out greycounter.__greycounter_2_x greycounter.__greycounter_3_x)
22
))
23
24
(rule (=> 
25
  (and (= greycounter.__greycounter_1 true) (= greycounter.b (ite greycounter.__greycounter_1
26
                                                                false
27
                                                                greycounter.__greycounter_2_c)) (= greycounter.a (
28
       ite greycounter.__greycounter_1 false
29
         (not greycounter.__greycounter_3_c))) (= greycounter.out (and greycounter.a greycounter.b)) (= greycounter.__greycounter_3_x greycounter.b) (= greycounter.__greycounter_2_x greycounter.a)
30
  )
31
  (greycounter_init greycounter.x greycounter.out greycounter.__greycounter_2_x greycounter.__greycounter_3_x)
32
))
33
34
(rule (=> 
35
  (and (= greycounter.__greycounter_1 false) (= greycounter.b (ite greycounter.__greycounter_1
36
                                                                 false
37
                                                                 greycounter.__greycounter_2_c)) (= greycounter.a (
38
       ite greycounter.__greycounter_1 false
39
         (not greycounter.__greycounter_3_c))) (= greycounter.out (and greycounter.a greycounter.b)) (= greycounter.__greycounter_3_x greycounter.b) (= greycounter.__greycounter_2_x greycounter.a)
40
  )
41
  (greycounter_step greycounter.x greycounter.out greycounter.__greycounter_2_c greycounter.__greycounter_3_c greycounter.__greycounter_2_x greycounter.__greycounter_3_x)
42
))
43
44
; intloopcounter
45
(declare-var intloopcounter.x Bool)
46
(declare-var intloopcounter.out Bool)
47
(declare-var intloopcounter.__intloopcounter_2_c Int)
48
(declare-var intloopcounter.__intloopcounter_2_x Int)
49
(declare-var intloopcounter.__intloopcounter_1 Bool)
50
(declare-var intloopcounter.__intloopcounter_3 Bool)
51
(declare-var intloopcounter.time Int)
52
(declare-rel intloopcounter_init (Bool Bool Int))
53
(declare-rel intloopcounter_step (Bool Bool Int Int))
54
55
(rule (=> 
56
  (and (= intloopcounter.__intloopcounter_3 (= intloopcounter.__intloopcounter_2_c 3)) (= intloopcounter.__intloopcounter_1 true) (= intloopcounter.time (
57
       ite intloopcounter.__intloopcounter_1 0
58
         (ite intloopcounter.__intloopcounter_3 0
59
            (+ intloopcounter.__intloopcounter_2_c 1)))) (= intloopcounter.out (= intloopcounter.time 2)) (= intloopcounter.__intloopcounter_2_x intloopcounter.time)
60
  )
61
  (intloopcounter_init intloopcounter.x intloopcounter.out intloopcounter.__intloopcounter_2_x)
62
))
63
64
(rule (=> 
65
  (and (= intloopcounter.__intloopcounter_3 (= intloopcounter.__intloopcounter_2_c 3)) (= intloopcounter.__intloopcounter_1 true) (= intloopcounter.time (
66
       ite intloopcounter.__intloopcounter_1 0
67
         (ite intloopcounter.__intloopcounter_3 0
68
            (+ intloopcounter.__intloopcounter_2_c 1)))) (= intloopcounter.out (= intloopcounter.time 2)) (= intloopcounter.__intloopcounter_2_x intloopcounter.time)
69
  )
70
  (intloopcounter_init intloopcounter.x intloopcounter.out intloopcounter.__intloopcounter_2_x)
71
))
72
73
(rule (=> 
74
  (and (= intloopcounter.__intloopcounter_3 (= intloopcounter.__intloopcounter_2_c 3)) (= intloopcounter.__intloopcounter_1 false) (= intloopcounter.time (
75
       ite intloopcounter.__intloopcounter_1 0
76
         (ite intloopcounter.__intloopcounter_3 0
77
            (+ intloopcounter.__intloopcounter_2_c 1)))) (= intloopcounter.out (= intloopcounter.time 2)) (= intloopcounter.__intloopcounter_2_x intloopcounter.time)
78
  )
79
  (intloopcounter_step intloopcounter.x intloopcounter.out intloopcounter.__intloopcounter_2_c intloopcounter.__intloopcounter_2_x)
80
))
81
82
; top
83
(declare-var top.x Bool)
84
(declare-var top.OK Bool)
85
(declare-var top.ni_0.greycounter.__greycounter_2_c Bool)
86
(declare-var top.ni_0.greycounter.__greycounter_3_c Bool)
87
(declare-var top.ni_1.intloopcounter.__intloopcounter_2_c Int)
88
(declare-var top.ni_0.greycounter.__greycounter_2_x Bool)
89
(declare-var top.ni_0.greycounter.__greycounter_3_x Bool)
90
(declare-var top.ni_1.intloopcounter.__intloopcounter_2_x Int)
91
(declare-var top.b Bool)
92
(declare-var top.d Bool)
93
(declare-rel top_init (Bool Bool Bool Bool Int))
94
(declare-rel top_step (Bool Bool Bool Bool Int Bool Bool Int))
95
96
(rule (=> 
97
  (and (intloopcounter_init top.x top.d top.ni_1.intloopcounter.__intloopcounter_2_x) (greycounter_init top.x top.b top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x) (= top.OK (= top.b top.d))
98
  )
99
  (top_init top.x top.OK top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_1.intloopcounter.__intloopcounter_2_x)
100
))
101
102
(rule (=> 
103
  (and (intloopcounter_init top.x top.d top.ni_1.intloopcounter.__intloopcounter_2_x) (greycounter_init top.x top.b top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x) (= top.OK (= top.b top.d))
104
  )
105
  (top_init top.x top.OK top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_1.intloopcounter.__intloopcounter_2_x)
106
))
107
108
(rule (=> 
109
  (and (intloopcounter_step top.x top.d top.ni_1.intloopcounter.__intloopcounter_2_c top.ni_1.intloopcounter.__intloopcounter_2_x) (greycounter_step top.x top.b top.ni_0.greycounter.__greycounter_2_c top.ni_0.greycounter.__greycounter_3_c top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x) (= top.OK (= top.b top.d))
110
  )
111
  (top_step top.x top.OK top.ni_0.greycounter.__greycounter_2_c top.ni_0.greycounter.__greycounter_3_c top.ni_1.intloopcounter.__intloopcounter_2_c top.ni_0.greycounter.__greycounter_2_x top.ni_0.greycounter.__greycounter_3_x top.ni_1.intloopcounter.__intloopcounter_2_x)
112
))