blob: 3558715a8a14267c854cb4450c8b1d580ae5fd95 (
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
|
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(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 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 auxnode () node$type)
(declare-fun curcmd () msg_cmd$type)
; Asserts --------------
(assert (not (=> (and (and (forall ((n node$type))
(=> (= (m_cmd (select
chan2
n))
gnte) (= exgntd
Truth)))
(forall ((n node$type))
(=> (= exgntd Truth)
(= (select shrset n)
(ite (= n auxnode) Truth
Falsity))))) (forall
((n node$type))
(=> (=
(m_cmd
(select
chan3
n))
invack)
(= (m_cmd
(select
chan2
n))
empty))))
(=> (= (m_cmd (select chan3 recv_invack$i))
invack) (=> (not (= curcmd empty))
(=> (= chan3$1 (store
chan3
recv_invack$i
(let (
(vup_228
(select
chan3
recv_invack$i)))
(c_msg$type
empty
(m_data
vup_228)))))
(=> (= 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))
(=> (= (m_cmd
(select
chan2
n))
gnte)
(= exgntd$1
Truth)))))
Truth Falsity)
(ite (forall (
(n node$type))
(=> (= (m_cmd
(select
chan2
n))
gnte)
(= exgntd
Truth)))
Truth Falsity))
Truth))))))))
(check-sat)
(exit)
|