← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/1999/mu-calculus/solutions/syntax.lisp

  • 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/1999/mu-calculus/solutions/syntax.lisp
 
1
(in-package "MODEL-CHECK")
 
2
 
 
3
(include-book "models")
 
4
 
 
5
(defun mu-symbolp (s)
 
6
  (declare (xargs :guard t))
 
7
  (and (symbolp s)
 
8
       (not (in s '(+ & MU NU true false)))))
 
9
; there can be unexpected behaviour if I don't do this, e.g., what
 
10
; is the semantics of (mu & f)? is it a mu or an &?
 
11
 
 
12
(defun basic-m-calc-formulap (f ap v) 
 
13
"True iff f is a mu-calculus formula given that ap is the list of
 
14
atomic proposition constants and v is the set of atomic proposition
 
15
variables. This checks that f is a basic mu-calc formula.  We allow
 
16
for abbreviations (e.g. =>) with translate. Formats of formulas are: p
 
17
-propositional variable or constant (EX f), (f1 & f2), (f1 + f2), 
 
18
 (~ f), (MU y f(y)), (NU y f(y))"
 
19
  (declare (xargs :guard (and (true-listp ap) (true-listp v))))
 
20
  (cond ((symbolp f)
 
21
         (or (in f '(true false))
 
22
             (and (mu-symbolp f)
 
23
                  (or (in f ap) (in f v)))))
 
24
        ((equal (len f) 2)
 
25
         (and (in (first f) '(~ EX))
 
26
              (basic-m-calc-formulap (second f) ap v)))
 
27
        ((equal (len f) 3)
 
28
         (let ((first (first f))
 
29
               (second (second f))
 
30
               (third (third f)))
 
31
           (or (and (in second '(& +))
 
32
                    (basic-m-calc-formulap first ap v)
 
33
                    (basic-m-calc-formulap third ap v))
 
34
               (and (or (in first '(MU NU)))
 
35
                    (mu-symbolp second)
 
36
                    (not (in second ap))
 
37
                    (basic-m-calc-formulap third ap (cons second v))))))))
 
38
 
 
39
 
 
40
(defthm truelistp-listlen0
 
41
  (implies (and (equal (len x) 0)
 
42
                (true-listp x))
 
43
           (equal x nil))
 
44
  :rule-classes :forward-chaining)
 
45
 
 
46
; Exercise 18
 
47
(defun translate-f (f)
 
48
"This is how I chose to extend the syntax of the Mu-calculus so one
 
49
now has AX, \| (same as +), => and -> (both are implies), and =, <->,
 
50
<=> (all are for boolean equality).  This function just rewrites these
 
51
in terms of the basic boolean operators."
 
52
  (declare (xargs :guard t))
 
53
  (cond ((symbolp f) f)
 
54
        ((equal (len f) 2) 
 
55
         (let ((first (first f))
 
56
               (second (second f)))
 
57
           (cond ((equal first 'AX)
 
58
                  `(~ (EX (~ ,(translate-f second)))))
 
59
                 (t `(,first ,(translate-f second))))))
 
60
        ((equal (len f) 3) 
 
61
         (let ((first (first f))
 
62
               (second (second f))
 
63
               (third (third f)))
 
64
           (cond ((equal second '\|)
 
65
                  `(,(translate-f first) + ,(translate-f third)))
 
66
                 ((in second '(=> ->))
 
67
                  `((~ ,(translate-f first)) + ,(translate-f third)))
 
68
                 ((in second '(= <=> <->))
 
69
                  `(((~ ,(translate-f first)) + ,(translate-f third)) &
 
70
                    ((~ ,(translate-f third)) + ,(translate-f first))))
 
71
                 ((in first '(MU NU))
 
72
                  `(,first ,second ,(translate-f third)))
 
73
                 (t `(,(translate-f first) ,second ,(translate-f third))))))
 
74
        (t f)))
 
75
 
 
76
(defun m-calc-formulap (f ap v)
 
77
  (declare (xargs :guard (and (true-listp ap) (true-listp v))))
 
78
  (basic-m-calc-formulap (translate-f f) ap v))
 
79
 
 
80
; Exercise 19
 
81
(defun m-calc-sentencep (f ap)
 
82
"Top level function.  True if f is a mu-calculus formula.  We require
 
83
that variable names and constant names do not overlap.  Also, we do
 
84
not allow free variables."
 
85
  (declare (xargs :guard (true-listp ap)))
 
86
  (m-calc-formulap f ap nil))
 
87