Project

General

Profile

Revision 4f3cc9f3 ex3.smt2

View differences:

ex3.smt2
54 54
  (and (= speed.__speed_2 (and speed.second (not speed.beacon)))
55 55
       (= speed.__speed_1 (and speed.beacon (not speed.second)))
56 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) 0 speed.diff speed.__COUNTER_1_x)
57
       (COUNTER_init 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_x)
58 58
       (= speed.__speed_7 speed.__speed_6_c)
59 59
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
60 60
                             (<= speed.diff (- 10))))
61
       (= speed.late 0)
61
       (= speed.late false)
62 62
       (= speed.__speed_4 speed.__speed_3_c)
63 63
       (= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0)
64 64
                             (>= speed.diff 10)))
65
       (= speed.early 0)
65
       (= speed.early false)
66 66
       (= speed.__speed_6_x speed.late)
67 67
       (= speed.__speed_3_x speed.early)
68 68
  )
......
73 73
  (and (= speed.__speed_2 (and speed.second (not speed.beacon)))
74 74
       (= speed.__speed_1 (and speed.beacon (not speed.second)))
75 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) 0 speed.diff speed.__COUNTER_1_c speed.__COUNTER_1_x)
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 77
       (= speed.__speed_7 speed.__speed_6_c)
78 78
       (= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0)
79 79
                             (<= speed.diff (- 10))))
......
95 95
(declare-var top.__top_1_c Bool)
96 96
(declare-var top.ni_1.speed.__speed_3_c Bool)
97 97
(declare-var top.ni_1.speed.__speed_6_c Bool)
98
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int)
98
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c Int)
99 99
(declare-var top.__top_1_x Bool)
100 100
(declare-var top.ni_1.speed.__speed_3_x Bool)
101 101
(declare-var top.ni_1.speed.__speed_6_x Bool)
102
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int)
102
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x Int)
103 103
(declare-var top.early Bool)
104 104
(declare-var top.late Bool)
105 105
(declare-rel top_init (Bool Bool Bool Bool Bool Bool Int))
106 106
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int))
107 107

  
108 108
(rule (=> 
109
  (and (speed_init top.beacon top.second top.late top.early top.__speed_3_x top.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
110
       (= top.OK 1)
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 111
       (= top.__top_1_x top.early)
112 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.ni_4.COUNTER.__COUNTER_1_x)
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 114
))
115 115

  
116 116
(rule (=> 
117
  (and (speed_step top.beacon top.second top.late top.early top.__speed_3_c top.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.__speed_3_x top.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
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 118
       (= top.OK (or (not top.__top_1_c) (not top.late)))
119 119
       (= top.__top_1_x top.early)
120 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.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.ni_4.COUNTER.__COUNTER_1_x)
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 122
))
123 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)

Also available in: Unified diff