Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / ex3.smt2 @ 4f3cc9f3

History | View | Annotate | Download (6.63 KB)

1 faa5e5c5 ploc
; COUNTER
2 40f8d0f9 ploc
(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 c0003810 ploc
(declare-var COUNTER.__COUNTER_1_c Int)
8
(declare-var COUNTER.__COUNTER_1_x Int)
9 40f8d0f9 ploc
(declare-var COUNTER.PC Int)
10
(declare-rel COUNTER_init (Int Int Bool Bool Int Int))
11 faa5e5c5 ploc
(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 c0003810 ploc
  (COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.__COUNTER_1_x)
20 faa5e5c5 ploc
))
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 c0003810 ploc
  (COUNTER_step COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.__COUNTER_1_c COUNTER.__COUNTER_1_x)
29 faa5e5c5 ploc
))
30
31
; speed
32 40f8d0f9 ploc
(declare-var speed.beacon Bool)
33
(declare-var speed.second Bool)
34
(declare-var speed.late Bool)
35
(declare-var speed.early Bool)
36 c0003810 ploc
(declare-var speed.__speed_3_c Bool)
37
(declare-var speed.__speed_6_c Bool)
38 40f8d0f9 ploc
(declare-var speed.ni_4.COUNTER.__COUNTER_1_c Int)
39 c0003810 ploc
(declare-var speed.__speed_3_x Bool)
40
(declare-var speed.__speed_6_x Bool)
41 40f8d0f9 ploc
(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 faa5e5c5 ploc
(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 4f3cc9f3 ploc
       (COUNTER_init 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_x)
58 faa5e5c5 ploc
       (= speed.__speed_7 speed.__speed_6_c)
59
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
60
                             (<= speed.diff (- 10))))
61 4f3cc9f3 ploc
       (= speed.late false)
62 faa5e5c5 ploc
       (= speed.__speed_4 speed.__speed_3_c)
63
       (= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
64
                             (>= speed.diff 10)))
65 4f3cc9f3 ploc
       (= speed.early false)
66 faa5e5c5 ploc
       (= speed.__speed_6_x speed.late)
67
       (= speed.__speed_3_x speed.early)
68
  )
69 c0003810 ploc
  (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 faa5e5c5 ploc
))
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 4f3cc9f3 ploc
       (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 faa5e5c5 ploc
       (= 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 c0003810 ploc
  (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 faa5e5c5 ploc
))
90
91
; top
92 40f8d0f9 ploc
(declare-var top.beacon Bool)
93
(declare-var top.second Bool)
94
(declare-var top.OK Bool)
95 c0003810 ploc
(declare-var top.__top_1_c Bool)
96 40f8d0f9 ploc
(declare-var top.ni_1.speed.__speed_3_c Bool)
97
(declare-var top.ni_1.speed.__speed_6_c Bool)
98 4f3cc9f3 ploc
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c Int)
99 c0003810 ploc
(declare-var top.__top_1_x Bool)
100 40f8d0f9 ploc
(declare-var top.ni_1.speed.__speed_3_x Bool)
101
(declare-var top.ni_1.speed.__speed_6_x Bool)
102 4f3cc9f3 ploc
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x Int)
103 40f8d0f9 ploc
(declare-var top.early Bool)
104
(declare-var top.late Bool)
105
(declare-rel top_init (Bool Bool Bool Bool Bool Bool Int))
106 faa5e5c5 ploc
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int))
107
108
(rule (=> 
109 4f3cc9f3 ploc
  (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 faa5e5c5 ploc
       (= top.__top_1_x top.early)
112
  )
113 4f3cc9f3 ploc
  (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 faa5e5c5 ploc
))
115
116
(rule (=> 
117 4f3cc9f3 ploc
  (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 faa5e5c5 ploc
       (= top.OK (or (not top.__top_1_c) (not top.late)))
119
       (= top.__top_1_x top.early)
120
  )
121 4f3cc9f3 ploc
  (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 faa5e5c5 ploc
))
123
124 4f3cc9f3 ploc
; 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)