blob: e8d163c2ae12abdbb579d7f3b39ff14364413f37 (
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
|
; EXPECT: unsat
;; minimized from UFLIA/tokeneer/enclave/progressadminactivity-3.smt2
(set-info :smt-lib-version 2.6)
(set-logic UFLIA)
(set-info :source |
Tokeneer case study <http://www.adacore.com/home/products/gnatpro/tokeneer/>
|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun field.statetype.status () Int)
(declare-fun admin__archivelog () Int)
(declare-fun admin__nullop () Int)
(declare-fun admin__opandnullt__base__first () Int)
(declare-fun admin__opandnullt__base__last () Int)
(declare-fun admin__opandnullt__first () Int)
(declare-fun admin__opandnullt__last () Int)
(declare-fun admin__opandnullt__size () Int)
(declare-fun admin__overridelock () Int)
(declare-fun admin__shutdownop () Int)
(declare-fun admin__updateconfigdata () Int)
(declare-fun alarmtypes__alarming () Int)
(declare-fun alarmtypes__silent () Int)
(declare-fun alarmtypes__statust__base__first () Int)
(declare-fun alarmtypes__statust__base__last () Int)
(declare-fun alarmtypes__statust__first () Int)
(declare-fun alarmtypes__statust__last () Int)
(declare-fun alarmtypes__statust__size () Int)
(declare-fun door__closed () Int)
(declare-fun door__open () Int)
(declare-fun door__t__base__first () Int)
(declare-fun door__t__base__last () Int)
(declare-fun door__t__first () Int)
(declare-fun door__t__last () Int)
(declare-fun door__t__size () Int)
(declare-fun enclavequiescent () Int)
(declare-fun gotadmintoken () Int)
(declare-fun nonquiescentstates__base__first () Int)
(declare-fun nonquiescentstates__base__last () Int)
(declare-fun nonquiescentstates__first () Int)
(declare-fun nonquiescentstates__last () Int)
(declare-fun nonquiescentstates__size () Int)
(declare-fun notenrolled () Int)
(declare-fun privtypes__auditmanager () Int)
(declare-fun privtypes__guard () Int)
(declare-fun privtypes__privileget__base__first () Int)
(declare-fun privtypes__privileget__base__last () Int)
(declare-fun privtypes__privileget__first () Int)
(declare-fun privtypes__privileget__last () Int)
(declare-fun privtypes__privileget__size () Int)
(declare-fun privtypes__securityofficer () Int)
(declare-fun privtypes__useronly () Int)
(declare-fun shutdown () Int)
(declare-fun statust__base__first () Int)
(declare-fun statust__base__last () Int)
(declare-fun statust__first () Int)
(declare-fun statust__last () Int)
(declare-fun statust__size () Int)
(declare-fun waitingendenrol () Int)
(declare-fun waitingenrol () Int)
(declare-fun waitingfinishadminop () Int)
(declare-fun waitingremoveadmintokenfail () Int)
(declare-fun waitingstartadminop () Int)
(declare-fun admintoken__state () Int)
(declare-fun admintoken__state__1 () Int)
(declare-fun init.admintoken__state__1 () Int)
(declare-fun admintoken__state__2 () Int)
(declare-fun init.admintoken__state__2 () Int)
(declare-fun admintoken__state__3 () Int)
(declare-fun init.admintoken__state__3 () Int)
(declare-fun init.admintoken__state () Int)
(declare-fun clock__currenttime () Int)
(declare-fun init.clock__currenttime () Int)
(declare-fun door__state () Int)
(declare-fun door__state__3 () Int)
(declare-fun init.door__state__3 () Int)
(declare-fun init.door__state () Int)
(declare-fun latch__state () Int)
(declare-fun latch__state__3 () Int)
(declare-fun init.latch__state__3 () Int)
(declare-fun init.latch__state () Int)
(declare-fun state () Int)
(declare-fun init.state () Int)
(declare-fun |status'| () Int)
(declare-fun status__1 () Int)
(declare-fun init.status__1 () Int)
(declare-fun status__2 () Int)
(declare-fun init.status__2 () Int)
(declare-fun status__3 () Int)
(declare-fun init.status__3 () Int)
(declare-fun init.status () Int)
(declare-fun theadmin () Int)
(declare-fun theadmin__1 () Int)
(declare-fun init.theadmin__1 () Int)
(declare-fun theadmin__3 () Int)
(declare-fun init.theadmin__3 () Int)
(declare-fun init.theadmin () Int)
(declare-fun admin__opandnullt__pos (Int) Int)
(declare-fun admin__opandnullt__pred (Int) Int)
(declare-fun admin__opandnullt__succ (Int) Int)
(declare-fun admin__opandnullt__val (Int) Int)
(declare-fun admin__prf_rolepresent (Int) Int)
(declare-fun admin__thecurrentop (Int) Int)
(declare-fun admintoken__theauthcertrole (Int) Int)
(declare-fun alarmtypes__statust__pos (Int) Int)
(declare-fun alarmtypes__statust__pred (Int) Int)
(declare-fun alarmtypes__statust__succ (Int) Int)
(declare-fun alarmtypes__statust__val (Int) Int)
(declare-fun bit__and (Int Int) Int)
(declare-fun bit__not (Int Int) Int)
(declare-fun bit__or (Int Int) Int)
(declare-fun bit__xor (Int Int) Int)
(declare-fun character__pos (Int) Int)
(declare-fun character__val (Int) Int)
(declare-fun clock__thecurrenttime (Int) Int)
(declare-fun door__prf_alarmtimeout (Int) Int)
(declare-fun door__t__pos (Int) Int)
(declare-fun door__t__pred (Int) Int)
(declare-fun door__t__succ (Int) Int)
(declare-fun door__t__val (Int) Int)
(declare-fun door__thecurrentdoor (Int) Int)
(declare-fun door__thedooralarm (Int) Int)
(declare-fun integer__pred (Int) Int)
(declare-fun integer__succ (Int) Int)
(declare-fun privtypes__privileget__pos (Int) Int)
(declare-fun privtypes__privileget__pred (Int) Int)
(declare-fun privtypes__privileget__succ (Int) Int)
(declare-fun privtypes__privileget__val (Int) Int)
(declare-fun round__ (Int) Int)
(declare-fun statust__pos (Int) Int)
(declare-fun statust__pred (Int) Int)
(declare-fun statust__succ (Int) Int)
(declare-fun statust__val (Int) Int)
(declare-fun i.div (Int Int) Int)
(declare-fun i.mod (Int Int) Int)
(declare-fun i.mult (Int Int) Int)
(declare-fun i.exp (Int Int) Int)
(declare-fun tm.true () Int)
(declare-fun tm.false () Int)
(declare-fun tm.not (Int) Int)
(declare-fun tm.and (Int Int) Int)
(declare-fun tm.or (Int Int) Int)
(declare-fun tm.iff (Int Int) Int)
(declare-fun tm.eq (Int Int) Int)
(declare-fun tm.ne (Int Int) Int)
(declare-fun tm.lt (Int Int) Int)
(declare-fun tm.le (Int Int) Int)
(declare-fun tuple.2 (Int Int) Int)
(declare-fun a.store (Int Int Int) Int)
(declare-fun a.select (Int Int) Int)
(declare-fun a.mk_const_array (Int) Int)
(declare-fun a.default_array () Int)
(declare-fun r.default_record () Int)
(declare-fun admin__isdoingop (Int) Bool)
(declare-fun admin__ispresent (Int) Bool)
(declare-fun admin__opandnullt__LE (Int Int) Bool)
(declare-fun admin__opandnullt__LT (Int Int) Bool)
(declare-fun admintoken__prf_authcertvalid (Int) Bool)
(declare-fun admintoken__prf_isgood (Int) Bool)
(declare-fun alarmtypes__statust__LE (Int Int) Bool)
(declare-fun alarmtypes__statust__LT (Int Int) Bool)
(declare-fun clock__greaterthanorequal (Int Int) Bool)
(declare-fun currentadminactivitypossible (Int Int) Bool)
(declare-fun door__t__LE (Int Int) Bool)
(declare-fun door__t__LT (Int Int) Bool)
(declare-fun enclave__currentadminactivitypossible (Int Int) Bool)
(declare-fun enclave__enrolmentisinprogress (Int) Bool)
(declare-fun enrolmentisinprogress (Int) Bool)
(declare-fun latch__islocked (Int) Bool)
(declare-fun prf_statusisenclavequiescent (Int) Bool)
(declare-fun prf_statusisgotadmintoken (Int) Bool)
(declare-fun prf_statusisshutdown (Int) Bool)
(declare-fun prf_statusiswaitingfinishadminop (Int) Bool)
(declare-fun prf_statusiswaitingremoveadmintokenfail (Int) Bool)
(declare-fun prf_statusiswaitingstartadminop (Int) Bool)
(declare-fun privtypes__privileget__LE (Int Int) Bool)
(declare-fun privtypes__privileget__LT (Int Int) Bool)
(declare-fun statust__LE (Int Int) Bool)
(declare-fun statust__LT (Int Int) Bool)
(assert (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming)))
(assert (=> (not (admin__ispresent theadmin)) (not (admin__isdoingop theadmin))))
(assert (=> (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop)) (and (admin__ispresent theadmin) (admin__isdoingop theadmin))))
(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__shutdownop)) (= |status'| waitingstartadminop)))
(assert (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard)))))
(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__overridelock)) (= (admin__prf_rolepresent theadmin) privtypes__guard)))
(assert (let ((?v_0 (admin__isdoingop theadmin))) (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (or (and ?v_0 (= (admin__thecurrentop theadmin) admin__overridelock)) (not ?v_0)))))
(assert (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop)))
(assert (let ((?v_1 (admin__isdoingop theadmin)) (?v_0 (= |status'| waitingstartadminop)) (?v_2 (admin__thecurrentop theadmin)) (?v_3 (= (admin__prf_rolepresent theadmin) privtypes__guard))) (let ((?v_4 (and ?v_1 (= ?v_2 admin__overridelock)))) (not (and (or ?v_0 (= |status'| waitingfinishadminop)) (=> (and ?v_1 (= ?v_2 admin__shutdownop)) ?v_0) (admin__ispresent theadmin) ?v_1 (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming)) (=> ?v_3 (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard)))) (=> ?v_4 ?v_3) (=> ?v_3 (or ?v_4 (not ?v_1))))))))
(check-sat)
(exit)
|
