blob: 07180cf4fb43334992104d952cf18ffe3782a8c0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
|
; COMMAND-LINE: --finite-model-find --lang=smt2.5
; EXPECT: unsat
; Preamble --------------
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
(declare-datatypes () ((UNIT (Unit))))
(declare-datatypes () ((BOOL (Truth) (Falsity))))
; Decls --------------
(declare-sort node$type 0)
(declare-sort value$type 0)
(define-sort Nodes$elem$type () node$type)
(declare-sort Nodes$t$type 0)
(declare-fun Nodes$empty () Nodes$t$type)
(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL)
(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type)
(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type)
(declare-fun Nodes$cardinality (Nodes$t$type) Int)
(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type)
(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL)
;Nodes$disjoint_empty :
(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth)))
;Nodes$disjoint_comm :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b)
(Nodes$disjoint b a))))
;Nodes$mem_empty :
(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty)
Truth))))
;Nodes$mem_add :
(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type))
(= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s)
Truth)) Truth
Falsity))))
;Nodes$mem_remove :
(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type))
(= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (=
(Nodes$mem
x s)
Truth))
Truth Falsity))))
;Nodes$mem_union1 :
(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a)
Truth) (forall
((b Nodes$t$type))
(=
(Nodes$mem
x (Nodes$union
a b))
Truth)))))
;Nodes$mem_union2 :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b)
(Nodes$union b a))))
;Nodes$mem_union3 :
(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type))
(=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a)
Truth) (= (Nodes$mem
x b)
Truth)))))
;Nodes$mem_union4 :
(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a)))
;Nodes$mem_union5 :
(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a)))
;Nodes$empty_union :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b)
Nodes$empty)
(= a Nodes$empty))))
;Nodes$card_empty :
(assert (= (Nodes$cardinality Nodes$empty) 0))
;Nodes$card_zero :
(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (=
s
Nodes$empty))))
;Nodes$card_non_negative :
(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0)))
;Nodes$card_add :
(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality
(Nodes$add x s))
(ite (= (Nodes$mem
x s) Truth)
(Nodes$cardinality
s) (+ (Nodes$cardinality
s) 1)))))
;Nodes$card_remove :
(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality
(Nodes$remove x s))
(ite (= (Nodes$mem
x s) Truth) (-
(Nodes$cardinality
s) 1) (Nodes$cardinality
s)))))
;Nodes$card_union :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint
a b) Truth)
(= (Nodes$cardinality
(Nodes$union a b)) (+
(Nodes$cardinality
a) (Nodes$cardinality b))))))
(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL)
;Nodes$eq_is_equality :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b)
(ite (= a b) Truth
Falsity))))
;Nodes$equal1 :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type))
(= (Nodes$mem x a)
(Nodes$mem x b)))
(= (Nodes$eq a b)
Truth))))
(define-sort Values$elem$type () value$type)
(declare-sort Values$t$type 0)
(declare-fun Values$empty () Values$t$type)
(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL)
(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type)
(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type)
(declare-fun Values$cardinality (Values$t$type) Int)
(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type)
(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL)
;Values$disjoint_empty :
(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty)
Truth)))
;Values$disjoint_comm :
(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint
a b) (Values$disjoint
b a))))
;Values$mem_empty :
(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty)
Truth))))
;Values$mem_add :
(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type))
(= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem
x s) Truth))
Truth Falsity))))
;Values$mem_remove :
(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type))
(= (Values$mem x (Values$remove y s)) (ite (and (not (= x y))
(= (Values$mem x s)
Truth)) Truth Falsity))))
;Values$mem_union1 :
(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem
x a)
Truth) (forall
(
(b Values$t$type))
(=
(Values$mem
x
(Values$union
a b))
Truth)))))
;Values$mem_union2 :
(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b)
(Values$union b a))))
;Values$mem_union3 :
(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type))
(=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem
x a) Truth)
(= (Values$mem x b)
Truth)))))
;Values$mem_union4 :
(assert (forall ((a Values$t$type)) (= (Values$union a a) a)))
;Values$mem_union5 :
(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a)))
;Values$empty_union :
(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union
a b) Values$empty)
(= a Values$empty))))
;Values$card_empty :
(assert (= (Values$cardinality Values$empty) 0))
;Values$card_zero :
(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0)
(= s Values$empty))))
;Values$card_non_negative :
(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0)))
;Values$card_add :
(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality
(Values$add x s))
(ite (= (Values$mem
x s)
Truth)
(Values$cardinality
s) (+ (Values$cardinality
s) 1)))))
;Values$card_remove :
(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality
(Values$remove
x s)) (ite
(=
(Values$mem
x s)
Truth) (-
(Values$cardinality
s)
1)
(Values$cardinality
s)))))
;Values$card_union :
(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint
a b) Truth)
(= (Values$cardinality
(Values$union a b)) (+
(Values$cardinality
a) (Values$cardinality
b))))))
(declare-fun Values$eq (Values$t$type Values$t$type) BOOL)
;Values$eq_is_equality :
(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b)
(ite (= a b) Truth
Falsity))))
;Values$equal1 :
(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type))
(= (Values$mem x a)
(Values$mem
x b))) (= (Values$eq
a b)
Truth))))
(define-sort node_set$type () (Array node$type BOOL))
(declare-fun mk_array_1 () (Array node$type BOOL))
;mk_array_1_def :
(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1
mk_array_1_index) Falsity)))
(define-fun empty_node_set () node_set$type mk_array_1)
(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL)))
(declare-fun mk_array_2 () (Array node$type BOOL))
;mk_array_2_def :
(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2
mk_array_2_index) Falsity)))
(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL)))
;mk_array_3_def :
(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3
mk_array_3_index) mk_array_2)))
(define-fun empty_node_pair_set () node_pair_set$type mk_array_3)
(declare-fun mk_array_4 () (Array node$type BOOL))
;mk_array_4_def :
(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4
mk_array_4_index) Truth)))
(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL)))
;mk_array_5_def :
(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5
mk_array_5_index) mk_array_4)))
(define-fun full_node_pair_set () node_pair_set$type mk_array_5)
(declare-fun input () (Array node$type value$type))
(declare-fun t () Int)
;positive_bound :
(assert (> t 0))
(define-sort message$type () Values$t$type)
(define-sort message_set$type () (Array node$type message$type))
(define-sort state$type () Values$t$type)
(define-sort state_set$type () (Array node$type state$type))
(define-fun null_message () message$type Values$empty)
(declare-fun mk_array_6 () (Array node$type message$type))
;mk_array_6_def :
(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6
mk_array_6_index) null_message)))
(define-fun null_message_set () message_set$type mk_array_6)
(define-fun null_state () state$type Values$empty)
(declare-fun mk_array_7 () (Array node$type state$type))
;mk_array_7_def :
(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7
mk_array_7_index) null_state)))
(define-fun null_state_set () state_set$type mk_array_7)
(declare-fun choose (Values$t$type) value$type)
;choosen_value :
(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem
(choose
vals)
vals)
Truth))))
(define-sort failure_pattern$type () node_pair_set$type)
(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL
(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth)))
Truth Falsity))
(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL
(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth)))
Truth Falsity))
(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase))))
(declare-datatypes () ((clean_state$type (before) (active) (after))))
; Var Decls --------------
(declare-fun init_done () node_set$type)
(declare-fun crashed () Nodes$t$type)
(declare-fun comp_done () node_set$type)
(declare-fun chosen () (Array node$type BOOL))
(declare-fun recv_done () node_pair_set$type)
(declare-fun phase () phase_state$type)
(declare-fun clean () clean_state$type)
(declare-fun global_state () state_set$type)
(declare-fun messages () (Array node$type message_set$type))
(declare-fun deliver_message () failure_pattern$type)
(declare-fun crashing () Nodes$t$type)
(declare-fun round () Int)
(declare-fun send_done () node_pair_set$type)
; Asserts --------------
(declare-fun mk_array_8 () (Array node$type BOOL))
;mk_array_8_def :
(assert (forall ((mk_array_8_index node$type)) (= (select mk_array_8
mk_array_8_index) Falsity)))
(declare-fun mk_array_9 () (Array node$type message_set$type))
;mk_array_9_def :
(assert (forall ((mk_array_9_index node$type)) (= (select mk_array_9
mk_array_9_index) null_message_set)))
(assert (not (=> (and (and (and (and (and (and (and (and (and (and (and
(and
(=
clean
before)
(=
global_state
null_state_set))
(=
messages
mk_array_9))
(= deliver_message
full_node_pair_set))
(= comp_done
empty_node_set))
(= recv_done empty_node_pair_set))
(= send_done empty_node_pair_set))
(= init_done empty_node_set))
(= phase init_phase)) (= crashing
Nodes$empty))
(= crashed Nodes$empty)) (= round 0)) (= chosen
mk_array_8))
(forall ((n node$type)) (=> (and (= (select chosen n) Truth)
(= round (+ t 1))) (and (forall
((n node$type) (m node$type))
(= (select
(select
send_done
n)
m)
Truth))
(forall (
(n node$type) (m node$type))
(= (select
(select
recv_done
n) m)
Truth))))))))
(check-sat)
|
