Index of /users/moore/acl2/v3-0/distrib/acl2-sources/books/workshops/1999/mu-calculus/solutions
Name Last modified Size Description
![[DIR]](/icons/back.gif)
Parent Directory -
![[ ]](/icons/unknown.gif)
Makefile 20-Sep-2004 20:27 1.0K
![[TXT]](/icons/text.gif)
build.lisp 04-Jun-2000 23:24 2.5K
ctl.acl2 04-Jun-2000 23:29 2.1K
ctl.lisp 17-Jan-2000 02:33 3.2K
defung-intro.txt 15-Jan-2000 17:16 1.9K
defung.lisp 06-Mar-2000 10:22 1.8K
fast-sets.acl2 04-Jun-2000 23:28 1.4K
fast-sets.lisp 07-Apr-2000 18:02 3.6K
fixpoints.acl2 04-Jun-2000 23:28 1.2K
fixpoints.lisp 19-Jan-2004 16:37 5.4K
meta.lisp 10-Apr-2001 22:54 74
models.acl2 04-Jun-2000 23:28 2.1K
models.lisp 07-Apr-2000 18:02 2.8K
perm.lisp 16-Jan-2000 22:19 2.0K
relations.acl2 04-Jun-2000 23:28 1.6K
relations.lisp 07-Apr-2000 18:22 3.9K
semantics.acl2 04-Jun-2000 23:27 2.1K
semantics.lisp 19-Jan-2004 16:38 9.9K
sets.acl2 04-Jun-2000 23:28 1.2K
sets.lisp 07-Apr-2000 18:03 15K
solutions.txt 17-Jan-2000 02:16 823
syntax.acl2 04-Jun-2000 23:28 2.1K
syntax.lisp 07-Apr-2000 18:24 2.9K
The files in this directory contain the solutions to the exercises.
Because adding and proving guards is an implicit exercise, all of the
functions (except for functions used only for proofs) have guards
(which are verified). If you want to see the functions as they are
defined in the chapter, look at the files in the directory "../book".
Before you look at the files in this directory, note the following.
1. We make heavy use of the "defung" macro. Briefly, the defung
macro is used to define a function and to describe the output type
of a function. There was no room in the article to describe the
macro, so read "defung-intro.txt" before looking at the solutions.
2. If this directory resides under an ACL2 distribution in
books/case-studies/mu-calculus/solutions/ (the default), then to
certify the books in this directory:
If you want to do it within acl2, start acl2 and type:
(ld "build.lisp")
You can also type:
make
3. If this directory is not in the default place, then
certification requires:
a. Edit "meta.lisp" so that the argument to include-book is the
"top-with-meta" book which comes with the ACL2 distribution.
b. If you want to do it within acl2, start acl2 and type:
(ld "build.lisp")
You can also type:
make
You will have to set the value of ACL2 in "makefile".
4. Typing "make clean" will remove files added by the certification
process.
The books in this directory are:
Filename - Description
-------------------------------------------
README - This file
meta.lisp - Top-with-meta book
makefile - Makefile to build and clean
build.lisp - Used to certify all the ACL2 books
defung-intro.txt - Description of defung macro and exercises
defung.lisp - Defung macro
perm.lisp - Function/theorems regarding perm.
sets.lisp - Functions/exercises in Section Sets
fast-sets.lisp - Functions/exercises in Section Fast-sets
fixpoints.lisp - Functions/exercises in Section Fixpoint Theory
relations.lisp - Functions/exercises in Section Relation Theory
models.lisp - Functions/exercises in Section Models
syntax.lisp - Functions/exercises in Section Mu-calculus Syntax
semantics.lisp - Functions/exercises in Section Mu-calculus Semantics
ctl.lisp - CTL to Mu-calculus translator
solutions.txt - Solutions to exercises 20 and 24
The solutions to exercises are spread over all the files in this
directory. The following table will allow you to find solutions
quickly. Suppose that you are looking for the solution to Exercise 3,
part 5. Start by finding the file which contains the solution, using
the table below. Then, search for "; Exercise 3, part 5" in the file.
Exercise File with solution
-------------------------------------------
1 sets.lisp
2, parts 1-4 sets.lisp
3, parts 1-6 sets.lisp
4, parts 1-4 sets.lisp
5, parts 1-2 sets.lisp
6, part 1 perm.lisp
6, part 2 sets.lisp
7 sets.lisp
8 fast-sets.lisp
9 fast-sets.lisp
10, parts 1-2 fast-sets.lisp
11 fast-sets.lisp
12, parts 1-2 fixpoints.lisp
13, parts 1-2 fixpoints.lisp
14 relations.lisp
15 relations.lisp
16, parts 1-2 relations.lisp
17, parts 1-8 models.lisp
18 syntax.lisp
19 syntax.lisp
20, parts 1-3 solutions.txt
21 semantics.lisp
22, parts 1-4 semantics.lisp
23 semantics.lisp
24, parts 1-6 solutions.txt
25 ctl.lisp