← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2003/ray-matthews-tuttle/support/certify.lsp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2003/ray-matthews-tuttle/support/certify.lsp
 
1
#|
 
2
 
 
3
  certify.lisp
 
4
  ~~~~~~~~~~~~
 
5
 
 
6
The collection of events below provides a proof of our compositional reduction
 
7
algorithm in ACL2. The script works in v2-7, but takes an inordinate amount of
 
8
time (about 24 hours on a 1.8GHz P3 machine running GCL on top of
 
9
linux). Admittedly, the proof is not optimized and the rewrite rules are not
 
10
that great, but I am too tired to look at that at this moment.
 
11
 
 
12
To see the proof silently go thru, just type (ld "certify.lisp") and that will
 
13
work. To see ACL2 work thru the proof, simply comment out the first line of
 
14
this file and do the ld.
 
15
 
 
16
|#
 
17
 
 
18
(set-inhibit-output-lst '(proof-tree prove))
 
19
 
 
20
(ubt! 1)
 
21
 
 
22
;; This is simply Pete's total order book. I have it in the directory so that I
 
23
;; dont have to change the path-names in the different books that call it.
 
24
 
 
25
(certify-book "total-order")
 
26
(u)
 
27
 
 
28
;; We add some other functionality to total-order, including keys etc. to
 
29
;; support reasoning about vectors. We use this book here since it has
 
30
;; definitions of memberp.
 
31
 
 
32
(certify-book "apply-total-order")
 
33
(u)
 
34
 
 
35
;; This is the records book provide with the distribution of ACL2. This book is
 
36
;; terribly important for us, since everything we do is with respect to this book.
 
37
 
 
38
(certify-book "records")
 
39
(u)
 
40
 
 
41
;; We just define a collection of functions for flat sets in ACL2. This book is
 
42
;; used in the context of our proof. This is not intended to be a general-purpose
 
43
;; book on (even flat) sets.
 
44
 
 
45
(certify-book "sets")
 
46
(u)
 
47
 
 
48
;; This book models the syntax and semantics of LTL. We have managed to define
 
49
;; the semantics with respect to eventually periodic paths. Of course, we moved
 
50
;; the actual function in concrete-ltl.lisp. Please see the accompanying note
 
51
;; for concrete-ltl, and the actual file ltl.lisp, for explanation as to what we
 
52
;; did and why.
 
53
 
 
54
(certify-book "ltl")
 
55
(u)
 
56
 
 
57
;; Just a trivial book justifying that conjunctive reduction is sound.
 
58
 
 
59
(certify-book "conjunction") 
 
60
(u) 
 
61
 
 
62
;; This is one hell of a book. It should be cleaned up when I have time, but I
 
63
;; have not done that yet. This book proves that bisimilar Kripke Structures
 
64
;; have the same ltl-semantics. Notice we needed to define bisimilarity with
 
65
;; respect to vars. For explanation, please refer to our paper.
 
66
 
 
67
(certify-book "bisimilarity") 
 
68
(u) 
 
69
 
 
70
;; We define the bisimulation relation for circuit models, which are special
 
71
;; types of Kripke Structures built out of our finite state machine
 
72
;; representations defined below.
 
73
 
 
74
(certify-book "circuit-bisim") 
 
75
(u) 
 
76
 
 
77
;; In this book, we model circuits or finite state machines. These are
 
78
;; efficient representations of Kripke Structures.
 
79
 
 
80
(certify-book "circuits") 
 
81
(u) 
 
82
 
 
83
;; This book verifies the cone of influence reduction implementation in ACL2.
 
84
 
 
85
(certify-book "cone-of-influence") 
 
86
(u) 
 
87
 
 
88
;; This book proves the final theorem about compositional reductions.
 
89
 
 
90
(certify-book "reductions") 
 
91
(u) 
 
92
 
 
93
;; This does not have any technical material at all. But the book allows us to
 
94
;; rewrite the ltl-semantics function into a function that we can efficiently
 
95
;; execute. In the underlying lisp, we replace calls to this efficient function
 
96
;; ltl-semantics-hack by a sys-call calling the external model checker (SMV).
 
97
 
 
98
(certify-book "impl-hack" 0 t :defaxioms-okp t) 
 
99
(u) 
 
100
 
 
101
;; Note: The book concrete-ltl is not used in the rest of the materials any
 
102
;; more. The book is present simply as a demonstration that we could actually
 
103
;; define the semantics of LTL. The proof of the theorem
 
104
;; ltl-ppath-semantics-cannot-distinguish-between-equal-labels used to take a
 
105
;; lot of time with v2-6, and considering the relative slowdown between v2-6
 
106
;; and v2-7, I did not experiment with that proof on v2-7 using
 
107
;; concrete-ltl. The proof has therefore been removed from this book. I do wish
 
108
;; to leave the comment here that the proof is not very trivial (actually I
 
109
;; also simplified the theorem a lot when I changed from concrete-ltl-semantics
 
110
;; to ltl-ppath-semantics which has the property encapsulated.) although very
 
111
;; simple at the high level. The proof simply inducts using the induction
 
112
;; suggested by concrete-ltl-semantics. However, I still find reasoning about
 
113
;; mutually recursive functions difficult in ACL2, and I did not want to
 
114
;; clutter the scripts with those theorems. (After all, if an implementation of
 
115
;; ltl-ppath-semantics does not satisfy that theorem, then we need to change
 
116
;; the definition rather than the theorem...:->)
 
117
 
 
118
 
 
119
(certify-book "concrete-ltl")
 
120
(u)
 
121
 
 
122
(set-inhibit-output-lst '(proof-tree))
 
123