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
|
(in-package "ACL2")
#|
concrete-ltl.lisp
~~~~~~~~~~~~~~~~~
In this book, we define functions to reason about concrete semantics of
LTL. This book is shipped with the certification of our compositional reduction
paper for the purpose of demonstration. We first define a mutually recusrive
clique that defines the semantics of LTL and then we define a single recursive
function to justify that definition. We then go ahead and prove some properties
about the functions. Our goal is to prove the properties that are necessary
about the mutually recursive4 clique as the properties we wish to export about
semantics of LTL. For conjunctive and cone of influence reductions, we need
basically two properties.
(1) That the ltl semantics can be decomposed over conjunction. (Obvious from
definition)
(2) That it is oblivious to paths that are bisimilar.
We have removed the second part of the theorems from this book, primarily
because it was taking a humongous amount of time in v2-6, and I did not have
the guts to see how much time it takes to prove in v2-7. And further, we
contend that if we have defined the semantics of ltl such that the theorem
cannot be proved, then we need to consider redefining the semantics of
LTL. (This book, I hope will provide enough evidence that the semantics can be
defined.) Hence we reasoned completely using a function that is encapsulated
and known to satisfy this property. If the reader feels unsatisfied with this,
we can provide the actual theorems about ltl-periodic-path-emantics, (which are
actually slightly more general than those I exported from the constrained
functions).
|#
(include-book "ltl")
;; Added for compatibility with previous versions of ACL2.
(include-book "../../../../ordinals/e0-ordinal")
(set-well-founded-relation e0-ord-<)
(mutual-recursion
(defun ltl-periodic-path-semantics (f init prefix cycle label)
(declare (xargs :measure (cons (1+ (acl2-count f)) 0)))
(cond ((atom f)
(if (ltl-constantp f)
(equal f 'true)
(memberp f (<- label init))))
((equal (len f) 3)
(case (second f)
(& (and (ltl-periodic-path-semantics (first f) init prefix cycle
label)
(ltl-periodic-path-semantics (third f) init prefix cycle
label)))
(+ (or (ltl-periodic-path-semantics (first f) init prefix cycle
label)
(ltl-periodic-path-semantics (third f) init prefix cycle
label)))
(U (let* ((found-and-index
(find-state-satisfying-formula
(third f) init prefix cycle label
(+ 1 (len prefix) (len cycle))))
(found (first found-and-index))
(index (second found-and-index)))
(if (not found)
nil
(ltl-periodic-path-semantics* (first f) init prefix
cycle label index))))
(W (let* ((found-and-index
(find-state-satisfying-formula
(third f) init prefix cycle label
(+ 1 (len prefix) (len cycle))))
(found (first found-and-index))
(index (second found-and-index)))
(if (not found)
(ltl-periodic-path-semantics* (first f) init prefix
cycle label
(+ 1 (len prefix) (len cycle)))
(ltl-periodic-path-semantics* (first f) init prefix
cycle label index))))
(t nil)))
((equal (len f) 2)
(case (first f)
(~ (not (ltl-periodic-path-semantics (second f) init prefix cycle
label)))
(G (ltl-periodic-path-semantics* (second f) init prefix
cycle label
(+ 1 (len prefix) (len cycle))))
(F (let* ((found-and-index
(find-state-satisfying-formula
(second f) init prefix cycle label
(+ 1 (len prefix) (len cycle))))
(found (first found-and-index)))
(if found t nil)))
(X (ltl-periodic-path-semantics (second f) (first prefix)
(if (endp (rest prefix))
cycle
(rest prefix))
cycle
label))
(t nil)))
(t nil)))
(defun ltl-periodic-path-semantics* (f init prefix cycle label dist)
(declare (xargs :measure (cons (1+ (acl2-count f)) (nfix dist))))
(if (zp dist) t
(and (ltl-periodic-path-semantics f init prefix cycle label)
(ltl-periodic-path-semantics* f (first prefix)
(if (endp (rest prefix))
cycle
(rest prefix))
cycle label (1- dist)))))
(defun find-state-satisfying-formula (f init prefix cycle label dist)
(declare (xargs :measure (cons (1+ (acl2-count f)) (nfix dist))))
(cond ((zp dist) (list nil 0))
((ltl-periodic-path-semantics f init prefix cycle label)
(list t 0))
(t (let* ((found-and-index
(find-state-satisfying-formula
f (first prefix)
(if (endp (rest prefix)) cycle (rest prefix))
cycle label (1- dist)))
(found (first found-and-index))
(ndx (second found-and-index)))
(list found (1+ ndx))))))
)
;; Now we have ther semantics of LTL that we will call the spec. We now proceed
;; to define a singly recursive version that is equivalent to the spec. Our
;; proofs will be using the singly recursive definition critically in order to
;; get us to what we want.
(defun ltl-semantics-single-recursion (f init prefix cycle label dist index)
(declare (xargs :measure (cons (1+ (acl2-count f)) (if (equal index 0) 0 (nfix dist)))
:otf-flg nil))
(if (equal index 0)
(cond ((atom f)
(if (ltl-constantp f)
(equal f 'true)
(memberp f (<- label init))))
((equal (len f) 3)
(case (second f)
(& (and (ltl-semantics-single-recursion (first f) init prefix cycle
label dist 0)
(ltl-semantics-single-recursion (third f) init prefix cycle
label dist 0)))
(+ (or (ltl-semantics-single-recursion (first f) init prefix cycle
label dist 0)
(ltl-semantics-single-recursion (third f) init prefix cycle
label dist 0)))
(U (let* ((found-and-index
(ltl-semantics-single-recursion
(third f) init prefix cycle label
(+ 1 (len prefix) (len cycle))
2))
(found (first found-and-index))
(ndx (second found-and-index)))
(if (not found)
nil
(ltl-semantics-single-recursion (first f) init prefix
cycle label ndx 1))))
(W (let* ((found-and-index
(ltl-semantics-single-recursion
(third f) init prefix cycle label
(+ 1 (len prefix) (len cycle))
2))
(found (first found-and-index))
(ndx (second found-and-index)))
(if (not found)
(ltl-semantics-single-recursion (first f) init prefix
cycle label
(+ 1 (len prefix) (len
cycle))
1)
(ltl-semantics-single-recursion (first f) init prefix
cycle label ndx 1))))
(t nil)))
((equal (len f) 2)
(case (first f)
(~ (not (ltl-semantics-single-recursion (second f) init prefix cycle
label dist 0)))
(G (ltl-semantics-single-recursion (second f) init prefix
cycle label
(+ 1 (len prefix) (len cycle)) 1))
(F (let* ((found-and-index
(ltl-semantics-single-recursion
(second f) init prefix cycle label
(+ 1 (len prefix) (len cycle))
2))
(found (first found-and-index)))
(if found T nil)))
(X (ltl-semantics-single-recursion (second f) (first prefix)
(if (endp (rest prefix))
cycle
(rest prefix))
cycle
label dist 0))
(t nil)))
(t nil))
(if (equal index 1)
(if (zp dist) t
(and (ltl-semantics-single-recursion f init prefix cycle label dist 0)
(ltl-semantics-single-recursion f (first prefix)
(if (endp (rest prefix))
cycle
(rest prefix))
cycle label (1- dist)
1)))
(if (equal index 2)
(cond ((zp dist) (list nil 0))
((ltl-semantics-single-recursion f init prefix cycle label dist 0)
(list t 0))
(t (let* ((found-and-index
(ltl-semantics-single-recursion
f (first prefix)
(if (endp (rest prefix)) cycle (rest prefix))
cycle label (1- dist) 2))
(found (first found-and-index))
(ndx (second found-and-index)))
(list found (1+ ndx)))))
nil))))
;; So do we believe that this big hodge-podge is same as the mutually recursive
;; code? Well, let us prove it.
(local
;; [Jared] added this because the following proof broke when I built it into ACL2.
(in-theory (disable FOLD-CONSTS-IN-+)))
(defthm single-and-mutually-recursive-code-same
(equal (ltl-semantics-single-recursion f init prefix cycle label dist index)
(if (equal index 0)
(ltl-periodic-path-semantics f init prefix cycle label)
(if (equal index 1)
(ltl-periodic-path-semantics* f init prefix cycle label dist)
(if (equal index 2)
(find-state-satisfying-formula f init prefix cycle
label dist)
nil))))
:rule-classes nil)
(defthm ltl-semantics-is-boolean
(if (not (equal i 2))
(booleanp (ltl-semantics-single-recursion f init prefix cycle label
dist i))
(and (booleanp (first (ltl-semantics-single-recursion f init prefix
cycle label dist
i)))
(integerp (second (ltl-semantics-single-recursion f init prefix
cycle label dist
i)))))
:rule-classes nil)
(defthm ltl-semantics-0-is-boolean
(booleanp (ltl-semantics-single-recursion f init prefix cycle label dist 0))
:hints (("Goal"
:use ((:instance single-and-mutually-recursive-code-same
(index 0)))))
:rule-classes :type-prescription)
(defthm ltl-semantics-1-boolean
(booleanp (ltl-semantics-single-recursion f init prefix cycle label dist 1))
:hints (("Goal"
:use ((:instance single-and-mutually-recursive-code-same
(index 1)))))
:rule-classes :type-prescription)
(defthm ltl-semantics->2-boolean
(implies (and (not (equal i 0))
(not (equal i 1))
(not (equal i 2)))
(not (ltl-semantics-single-recursion f init prefix cycle label
dist i)))
:rule-classes :type-prescription)
(defthm ltl-semantics-2-boolean
(booleanp (first (ltl-semantics-single-recursion f init prefix cycle label
dist 2)))
:hints (("Goal"
:use ((:instance ltl-semantics-is-boolean
(i 2)))))
:rule-classes :type-prescription)
(defthm ltl-semantics-2-integer
(integerp (second (ltl-semantics-single-recursion f init prefix cycle label
dist 2)))
:hints (("Goal"
:use ((:instance ltl-semantics-is-boolean
(i 2)))))
:rule-classes :type-prescription)
(defthm ltl-periodic-path-semantics-decomposed-for-conjunction
(implies (and ;; (ltl-formulap f)
(equal (len f) 3)
(equal (second f) '&))
(equal (ltl-periodic-path-semantics f init prefix cycle label)
(and (ltl-periodic-path-semantics (first f) init prefix cycle
label)
(ltl-periodic-path-semantics (third f) init prefix cycle
label))))
:rule-classes nil)
|
