← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2000/lusk-mccune/lusk-mccune-final/mstate.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/2000/lusk-mccune/lusk-mccune-final/mstate.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "cstate")
 
4
(include-book "pstate")
 
5
(include-book "lstate")
 
6
 
 
7
;; At this point we start associating cstates with pstates (because
 
8
;; processes alter connections).
 
9
 
 
10
(defun something-to-receive (hpid fd css)
 
11
  (declare (xargs :guard (and (hpidp hpid)
 
12
                              (fdp fd)
 
13
                              (cstate-listp css))))
 
14
  (cond ((atom css) nil)
 
15
        ((and (equal hpid (third (first (car css))))
 
16
              (equal fd (fourth (first (car css))))
 
17
              (consp (inboxq (car css)))) t)
 
18
        (t (something-to-receive hpid fd (cdr css)))))
 
19
 
 
20
(defun message-to-select (hpid css)
 
21
  (declare (xargs :guard (and (hpidp hpid)
 
22
                              (cstate-listp css))))
 
23
  (cond ((atom css) nil)
 
24
        ((and (equal hpid (third (first (car css))))
 
25
              (consp (inboxq (car css)))) t)
 
26
        (t (message-to-select hpid (cdr css)))))
 
27
 
 
28
(in-theory (enable hpid-fdp))
 
29
 
 
30
(defun request-to-select (hpid lss)
 
31
  (declare (xargs :guard (and (hpidp hpid)
 
32
                              (lstate-listp lss))))
 
33
  (cond ((atom lss) nil)
 
34
        ((and (equal hpid (first (first (car lss))))
 
35
              (consp (requestq (car lss)))) t)
 
36
        (t (request-to-select hpid (cdr lss)))))
 
37
 
 
38
(in-theory (disable hpid-fdp))
 
39
 
 
40
(in-theory (enable statementp))
 
41
 
 
42
(defun pstate-status (ps css lss)
 
43
  (declare (xargs :guard (and (pstatep ps)
 
44
                              (cstate-listp css)
 
45
                              (lstate-listp lss))))
 
46
  (let ((stmt (if (zp (cc ps)) nil (ith (cc ps) (code ps)))))
 
47
    (cond ((atom stmt) 'idle)  ;; cc 0 or out of range
 
48
          ((equal (car stmt) 'receive)
 
49
           (let ((fd (evl2 (second stmt) (memory ps))))
 
50
             (cond ((not (fdp fd)) 'active)  ;; handle error elsewhere
 
51
                   (t (if (something-to-receive (car ps) fd css)
 
52
                          'active 'waiting)))))
 
53
          ((equal (car stmt) 'select)
 
54
           (if (or (message-to-select (car ps) css)
 
55
                   (request-to-select (car ps) lss))
 
56
               'active 'waiting))
 
57
          ;; We should also check here if the process is waiting for
 
58
          ;; a connect or waiting for an accept.  As it is, the
 
59
          ;; simulator will attempt these, so it might spin.
 
60
          (t 'active))))
 
61
     
 
62
(in-theory (disable statementp))
 
63
 
 
64
(defun waiting-pstates (pss css lss)
 
65
  ;; Return the number of processes hanging in receive or select.
 
66
  (declare (xargs :guard (and (pstate-listp pss)
 
67
                              (cstate-listp css)
 
68
                              (lstate-listp lss))))
 
69
  (cond ((atom pss) 0)
 
70
        (t (+ (if (equal (pstate-status (car pss) css lss)
 
71
                         'waiting) 1 0)
 
72
              (waiting-pstates (cdr pss) css lss)))))
 
73
 
 
74
(defun active-pstates (pss css lss)
 
75
  ;; Return the number of processes with something to do.
 
76
  (declare (xargs :guard (and (pstate-listp pss)
 
77
                              (cstate-listp css)
 
78
                              (lstate-listp lss))))
 
79
  (cond ((atom pss) 0)
 
80
        (t (+ (if (equal (pstate-status (car pss) css lss)
 
81
                         'active) 1 0)
 
82
              (active-pstates (cdr pss) css lss)))))
 
83
 
 
84
(defun ith-active-pstate (n pss css lss)  ;; This counts from 1.
 
85
  (declare (xargs :guard (and (pos-integerp n)
 
86
                              (pstate-listp pss)
 
87
                              (cstate-listp css)
 
88
                              (lstate-listp lss))))
 
89
  (cond ((atom pss) nil)
 
90
        ((equal (pstate-status (car pss) css lss) 'active)
 
91
         (if (equal n 1)
 
92
             (car pss)
 
93
           (ith-active-pstate (- n 1) (cdr pss) css lss)))
 
94
        (t (ith-active-pstate n (cdr pss) css lss))))
 
95
 
 
96
(defthm ith-active-pstate-properties
 
97
  (implies (and (pstate-listp pss)
 
98
                (cstate-listp css)
 
99
                (lstate-listp lss)
 
100
                (integerp n)
 
101
                (> n 0)
 
102
                (<= n (active-pstates pss css lss)))
 
103
           (and (pstatep (ith-active-pstate n pss css lss))
 
104
                (member-equal (ith-active-pstate n pss css lss) pss)))
 
105
  :hints (("Goal"
 
106
           :in-theory (disable pstatep))))
 
107
 
 
108
;;----------------------------------------
 
109
;; prog: (program-name program-code)
 
110
 
 
111
(defun progp (x)
 
112
  (declare (xargs :guard t))
 
113
  (and (true-listp x)
 
114
       (equal (len x) 2)
 
115
       (symbolp (first x))
 
116
       (codep (second x))))
 
117
 
 
118
(defun program-listp (x)
 
119
  (declare (xargs :guard t))
 
120
  (cond ((atom x) (null x))
 
121
        (t (and (progp (car x))
 
122
                (program-listp (cdr x))))))
 
123
 
 
124
(defthm program-listp-is-alistp
 
125
  (implies (program-listp pgms)
 
126
           (alistp pgms))
 
127
  :rule-classes :forward-chaining)
 
128
 
 
129
;;----------------------------------------
 
130
;; mstate -- multiprocess state
 
131
 
 
132
(defun mstatep (x)
 
133
  (declare (xargs :guard t))
 
134
  (and (equal (len x) 4)
 
135
       (pstate-listp (first x))
 
136
       (cstate-listp (second x))
 
137
       (lstate-listp (third x))
 
138
       (program-listp (fourth x))))
 
139
 
 
140
(defun pstates (ms)  ;; get the list of pstates from an mstate
 
141
  (declare (xargs :guard (mstatep ms)))
 
142
  (first ms))
 
143
 
 
144
(defun cstates (ms)  ;; get the list of cstates from an mstate
 
145
  (declare (xargs :guard (mstatep ms)))
 
146
  (second ms))
 
147
 
 
148
(defun lstates (ms)  ;; get the list of lstates from an mstate
 
149
  (declare (xargs :guard (mstatep ms)))
 
150
  (third ms))
 
151
 
 
152
(defun programs (ms)  ;; get the list of programs from an mstate
 
153
  (declare (xargs :guard (mstatep ms)))
 
154
  (fourth ms))
 
155
 
 
156
(defun update-pstates (ms pss)
 
157
  (declare (xargs :guard (and (mstatep ms)
 
158
                              (pstate-listp pss))))
 
159
  (update-first ms pss))
 
160
 
 
161
(defun update-cstates (ms css)
 
162
  (declare (xargs :guard (and (mstatep ms)
 
163
                              (cstate-listp css))))
 
164
  (update-second ms css))
 
165
 
 
166
(defun update-lstates (ms lss)
 
167
  (declare (xargs :guard (and (mstatep ms)
 
168
                              (lstate-listp lss))))
 
169
  (update-third ms lss))
 
170
 
 
171
 
 
172
#|
 
173
(mstatep '(
 
174
           (  ;; pstates:
 
175
            ((lutra 320) ((asgn z 6)) 13 nil ((x . 4) (y . 6)))
 
176
            ((gyro  440) ((procedure handle)) 14 nil nil)
 
177
            )
 
178
 
 
179
           (  ;; cstates:
 
180
            (((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2))
 
181
            )
 
182
           (  ;; lstates:
 
183
            (((gyro   440) 15) 8585 nil)
 
184
            (((lutra  320) 14) 7483 (((cosmo 354) 16)))
 
185
            (((donner 320) 17) 3535 (((fire  444) 18)))
 
186
            )
 
187
           nil ;; programs
 
188
           ))
 
189
|#
 
190
 
 
191
(defthm true-listp-append-list
 
192
  (true-listp (append a (list x))))
 
193
 
 
194
(defthm evaluated-expression-append
 
195
  (implies (and (evaluated-expression-listp a)
 
196
                (evaluated-expressionp x))
 
197
           (evaluated-expression-listp (append a (list x)))))
 
198
 
 
199
(defun deliver-message (ms cs)
 
200
  (declare (xargs :guard (and (mstatep ms)
 
201
                              (cstatep cs)
 
202
                              (member-equal cs (cstates ms))
 
203
                              (message-to-transfer cs))))
 
204
  (update-cstates
 
205
   ms
 
206
   (update-alist-member
 
207
    (car cs)
 
208
    (transfer-message cs)
 
209
    (cstates ms))))
 
210
 
 
211
;; For example,
 
212
 
 
213
#|
 
214
(deliver-message '((
 
215
                    ((lutra 320) ((asgn z 6)) 13 nil ((x . 4) (y . 6)))
 
216
                    ((gyro  440) ((procedure handle)) 14 nil nil)
 
217
                    )
 
218
                   (
 
219
                    (((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2))
 
220
                    )
 
221
                   nil
 
222
                   )
 
223
                 
 
224
                 '(((lutra 320) 5 (gyro 440) 6) ('m3 'm4) ('m1 'm2)))
 
225
|#
 
226
 
 
227
(defthm mstatep-deliver-message
 
228
  (implies (and (mstatep ms)
 
229
                (cstatep cs))
 
230
           (mstatep (deliver-message ms cs))))
 
231
 
 
232
;;---------------
 
233
 
 
234
(defun make-mstate (pstates cstates lstates programs)
 
235
  (declare (xargs :guard (and (pstate-listp pstates)
 
236
                              (cstate-listp cstates)
 
237
                              (lstate-listp lstates)
 
238
                              (program-listp programs)
 
239
                              )))
 
240
  (list pstates cstates lstates programs))