|
1
|
; COUNTER
|
|
2
|
(declare-var COUNTER.init Int)
|
|
3
|
(declare-var COUNTER.incr Int)
|
|
4
|
(declare-var COUNTER.X Bool)
|
|
5
|
(declare-var COUNTER.reset Bool)
|
|
6
|
(declare-var COUNTER.C Int)
|
|
7
|
(declare-var COUNTER.__COUNTER_1_c Int)
|
|
8
|
(declare-var COUNTER.__COUNTER_1_x Int)
|
|
9
|
(declare-var COUNTER.PC Int)
|
|
10
|
(declare-rel COUNTER_init (Int Int Bool Bool Int Int))
|
|
11
|
(declare-rel COUNTER_step (Int Int Bool Bool Int Int Int))
|
|
12
|
|
|
13
|
(rule (=>
|
|
14
|
(and (= COUNTER.PC COUNTER.init)
|
|
15
|
(= COUNTER.C (ite COUNTER.reset COUNTER.init
|
|
16
|
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC)))
|
|
17
|
(= COUNTER.__COUNTER_1_x COUNTER.C)
|
|
18
|
)
|
|
19
|
(COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.__COUNTER_1_x)
|
|
20
|
))
|
|
21
|
|
|
22
|
(rule (=>
|
|
23
|
(and (= COUNTER.PC COUNTER.__COUNTER_1_c)
|
|
24
|
(= COUNTER.C (ite COUNTER.reset COUNTER.init
|
|
25
|
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC)))
|
|
26
|
(= COUNTER.__COUNTER_1_x COUNTER.C)
|
|
27
|
)
|
|
28
|
(COUNTER_step COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.__COUNTER_1_c COUNTER.__COUNTER_1_x)
|
|
29
|
))
|
|
30
|
|
|
31
|
; speed
|
|
32
|
(declare-var speed.beacon Bool)
|
|
33
|
(declare-var speed.second Bool)
|
|
34
|
(declare-var speed.late Bool)
|
|
35
|
(declare-var speed.early Bool)
|
|
36
|
(declare-var speed.__speed_3_c Bool)
|
|
37
|
(declare-var speed.__speed_6_c Bool)
|
|
38
|
(declare-var speed.ni_4.COUNTER.__COUNTER_1_c Int)
|
|
39
|
(declare-var speed.__speed_3_x Bool)
|
|
40
|
(declare-var speed.__speed_6_x Bool)
|
|
41
|
(declare-var speed.ni_4.COUNTER.__COUNTER_1_x Int)
|
|
42
|
(declare-var speed.__speed_1 Bool)
|
|
43
|
(declare-var speed.__speed_2 Bool)
|
|
44
|
(declare-var speed.__speed_4 Bool)
|
|
45
|
(declare-var speed.__speed_5 Bool)
|
|
46
|
(declare-var speed.__speed_7 Bool)
|
|
47
|
(declare-var speed.__speed_8 Bool)
|
|
48
|
(declare-var speed.diff Int)
|
|
49
|
(declare-var speed.incr Int)
|
|
50
|
(declare-rel speed_init (Bool Bool Bool Bool Bool Bool Int))
|
|
51
|
(declare-rel speed_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Int))
|
|
52
|
|
|
53
|
(rule (=>
|
|
54
|
(and (= speed.__speed_2 (and speed.second (not speed.beacon)))
|
|
55
|
(= speed.__speed_1 (and speed.beacon (not speed.second)))
|
|
56
|
(= speed.incr (ite speed.__speed_1 1 (ite speed.__speed_2 2 0)))
|
|
57
|
(COUNTER_init 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
58
|
(= speed.__speed_7 speed.__speed_6_c)
|
|
59
|
(= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
|
|
60
|
(<= speed.diff (- 10))))
|
|
61
|
(= speed.late false)
|
|
62
|
(= speed.__speed_4 speed.__speed_3_c)
|
|
63
|
(= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
|
|
64
|
(>= speed.diff 10)))
|
|
65
|
(= speed.early false)
|
|
66
|
(= speed.__speed_6_x speed.late)
|
|
67
|
(= speed.__speed_3_x speed.early)
|
|
68
|
)
|
|
69
|
(speed_init speed.beacon speed.second speed.late speed.early speed.__speed_3_x speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
70
|
))
|
|
71
|
|
|
72
|
(rule (=>
|
|
73
|
(and (= speed.__speed_2 (and speed.second (not speed.beacon)))
|
|
74
|
(= speed.__speed_1 (and speed.beacon (not speed.second)))
|
|
75
|
(= speed.incr (ite speed.__speed_1 1 (ite speed.__speed_2 2 0)))
|
|
76
|
(COUNTER_step 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_c speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
77
|
(= speed.__speed_7 speed.__speed_6_c)
|
|
78
|
(= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
|
|
79
|
(<= speed.diff (- 10))))
|
|
80
|
(= speed.late speed.__speed_8)
|
|
81
|
(= speed.__speed_4 speed.__speed_3_c)
|
|
82
|
(= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
|
|
83
|
(>= speed.diff 10)))
|
|
84
|
(= speed.early speed.__speed_5)
|
|
85
|
(= speed.__speed_6_x speed.late)
|
|
86
|
(= speed.__speed_3_x speed.early)
|
|
87
|
)
|
|
88
|
(speed_step speed.beacon speed.second speed.late speed.early speed.__speed_3_c speed.__speed_6_c speed.ni_4.COUNTER.__COUNTER_1_c speed.__speed_3_x speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
89
|
))
|
|
90
|
|
|
91
|
; top
|
|
92
|
(declare-var top.beacon Bool)
|
|
93
|
(declare-var top.second Bool)
|
|
94
|
(declare-var top.OK Bool)
|
|
95
|
(declare-var top.__top_1_c Bool)
|
|
96
|
(declare-var top.ni_1.speed.__speed_3_c Bool)
|
|
97
|
(declare-var top.ni_1.speed.__speed_6_c Bool)
|
|
98
|
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c Int)
|
|
99
|
(declare-var top.__top_1_x Bool)
|
|
100
|
(declare-var top.ni_1.speed.__speed_3_x Bool)
|
|
101
|
(declare-var top.ni_1.speed.__speed_6_x Bool)
|
|
102
|
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x Int)
|
|
103
|
(declare-var top.early Bool)
|
|
104
|
(declare-var top.late Bool)
|
|
105
|
(declare-rel top_init (Bool Bool Bool Bool Bool Bool Int))
|
|
106
|
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int))
|
|
107
|
|
|
108
|
(rule (=>
|
|
109
|
(and (speed_init top.beacon top.second top.late top.early top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
110
|
(= top.OK true)
|
|
111
|
(= top.__top_1_x top.early)
|
|
112
|
)
|
|
113
|
(top_init top.beacon top.second top.OK top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
114
|
))
|
|
115
|
|
|
116
|
(rule (=>
|
|
117
|
(and (speed_step top.beacon top.second top.late top.early top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
118
|
(= top.OK (or (not top.__top_1_c) (not top.late)))
|
|
119
|
(= top.__top_1_x top.early)
|
|
120
|
)
|
|
121
|
(top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
122
|
))
|
|
123
|
|
|
124
|
; Collecting semantics with main node top
|
|
125
|
|
|
126
|
(declare-rel MAIN (Bool Bool Bool Int Bool))
|
|
127
|
; Initial set
|
|
128
|
(declare-rel INIT_STATE ())
|
|
129
|
(rule INIT_STATE)
|
|
130
|
(rule (=>
|
|
131
|
(and INIT_STATE
|
|
132
|
(top_init top.beacon top.second top.OK top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
133
|
)
|
|
134
|
(MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x top.OK)
|
|
135
|
))
|
|
136
|
|
|
137
|
; Inductive def
|
|
138
|
(declare-var dummy Bool)
|
|
139
|
(rule (=>
|
|
140
|
(and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c dummy)
|
|
141
|
(top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
142
|
)
|
|
143
|
(MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x top.OK)
|
|
144
|
))
|
|
145
|
|
|
146
|
; Property def
|
|
147
|
(declare-rel ERR ())
|
|
148
|
(rule (=>
|
|
149
|
(and (not (= top.OK true))
|
|
150
|
(MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c))
|
|
151
|
ERR))
|
|
152
|
(query ERR)
|