blob: e1d49997230f9a1982730c900211d2e8206dfd66 (
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
|
; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
(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 data$type 0)
(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive))))
(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type)))))
(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte))))
(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))))
(declare-fun dummy () data$type)
; Var Decls --------------
(declare-fun memdata$1 () data$type)
(declare-fun shrset$1 () (Array node$type BOOL))
(declare-fun recv_invack$i () node$type)
(declare-fun exgntd () BOOL)
(declare-fun invset () (Array node$type BOOL))
(declare-fun chan3$1 () (Array node$type msg$type))
(declare-fun shrset () (Array node$type BOOL))
(declare-fun exgntd$1 () BOOL)
(declare-fun chan2 () (Array node$type msg$type))
(declare-fun chan3 () (Array node$type msg$type))
(declare-fun curcmd () msg_cmd$type)
; Asserts --------------
(assert (not (=> (and (forall ((n node$type))
(=> (= (select invset n)
Truth) (= (select
shrset
n) Truth)))
(forall ((n node$type)) (=>
(or
(=
(m_cmd
(select
chan2
n))
inv)
(=
(m_cmd
(select
chan3
n))
invack))
(not
(=
(select
invset
n)
Truth)))))
(=> (= (m_cmd (select chan3 recv_invack$i))
invack) (=> (not (= curcmd empty))
(=> (= chan3$1 (store
chan3
recv_invack$i
(let (
(vup_101
(select
chan3
recv_invack$i)))
(c_msg$type
empty
(m_data
vup_101)))))
(=> (= shrset$1 (store
shrset
recv_invack$i
Falsity))
(= (ite (= exgntd Truth)
(ite (=> (= exgntd$1
Falsity)
(=> (= memdata$1
(m_data
(select
chan3$1
recv_invack$i)))
(forall (
(n node$type))
(=> (= (select
invset
n)
Truth)
(= (select
shrset$1
n) Truth)))))
Truth Falsity)
(ite (forall (
(n node$type))
(=> (= (select
invset
n)
Truth)
(= (select
shrset$1
n) Truth)))
Truth Falsity))
Truth))))))))
(check-sat)
(exit)
|