← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/projects/hybrid-systems/example.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/projects/hybrid-systems/example.lisp
 
1
; Copyright (C) 2007 by Shant Harutunian
 
2
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
3
 
 
4
(in-package "ACL2")
 
5
 
 
6
(include-book "arith-nsa4")
 
7
(include-book "abs")
 
8
(include-book "computed-hints")
 
9
(include-book "o-real-p")
 
10
(include-book "nsa")
 
11
 
 
12
;; Enable abs, <-cancel-divisors and divisor cancellation as needed.
 
13
 
 
14
(in-theory (disable equal-cancel-divisors <-cancel-divisors))
 
15
 
 
16
(set-default-hints '((staged-hints stable-under-simplificationp
 
17
                                   nil ;;restart on new id
 
18
                                   '((:in-theory (enable abs
 
19
                                                         equal-cancel-divisors <-cancel-divisors)))
 
20
                                   nil nil 0)))
 
21
 
 
22
;; Macro defining non-negative real
 
23
 
 
24
(defmacro nneg-realp (r)
 
25
  `(and (realp ,r)
 
26
        (<= 0 ,r)))
 
27
 
 
28
;; Macro defining the constraint on the variable eps.
 
29
;; In this case, we require that 0 < eps <= 1/100.
 
30
 
 
31
(defmacro small-realp (eps)
 
32
  `(and (realp ,eps)
 
33
        (<= ,eps 1/100)
 
34
        (< 0 ,eps)))
 
35
 
 
36
;; Define accessor function for accessing particular variables
 
37
;; from the state X
 
38
 
 
39
(defun getPosReq (X)
 
40
  (nth 0 X))
 
41
 
 
42
(defun getPreset (X)
 
43
  (nth 1 X))
 
44
 
 
45
(defun getPos (X)
 
46
  (nth 2 X))
 
47
 
 
48
(defun getPosAo (X)
 
49
  (nth 3 X))
 
50
 
 
51
(defun getTmr (X)
 
52
  (nth 4 X))
 
53
 
 
54
;; Define a function which creates a system state, consisting
 
55
;; of the variables of the system.
 
56
 
 
57
(defun make-state (posReq preset pos posAo tmr)
 
58
  (list posReq preset pos posAo tmr))
 
59
 
 
60
;; Define theorems relating the accessor function and the make
 
61
;; state functions.
 
62
 
 
63
(defthm state-thm
 
64
  (and
 
65
   (equal (getPosReq (make-state posReq preset pos posAo tmr)) posReq)
 
66
   (equal (getPreset (make-state posReq preset pos posAo tmr)) preset)
 
67
   (equal (getPos (make-state posReq preset pos posAo tmr)) pos)
 
68
   (equal (getPosAo (make-state posReq preset pos posAo tmr)) posAo)
 
69
   (equal (getTmr (make-state posReq preset pos posAo tmr)) tmr)))
 
70
 
 
71
;; Disable the accessor functions and make-state function and rely upon the
 
72
;; rewrite rules associated with above theorem.
 
73
 
 
74
(in-theory (disable getPosReq getPreset getPos getPosAo getTmr
 
75
                    make-state))
 
76
 
 
77
;; StateP is a predicate which recognizes whether some variable is a
 
78
;; state variable.
 
79
 
 
80
(defun statep (x)
 
81
  (equal x
 
82
         (make-state (getPosReq x)
 
83
                     (getPreset x)
 
84
                     (getPos x)
 
85
                     (getPosAo x)
 
86
                     (getTmr x))))
 
87
 
 
88
;; The system assignment function, Y, includes the definition of the
 
89
;; computer program,
 
90
;; the floor function representing the analog to digital conversion,
 
91
;; and the reset of the timer variable.
 
92
 
 
93
(defun Y (X)
 
94
  (make-state
 
95
   (getPosReq x)
 
96
   (getPreset x)
 
97
   (getPos x)
 
98
   ;;posAo
 
99
   (cond
 
100
    ((> (- (floor1 (getPos X)) (getposReq X)) 2)
 
101
     (- (getposAo X) 5))
 
102
    ((< (- (floor1 (getPos X)) (getposReq X)) -3)
 
103
     (+ (getposAo X) 5))
 
104
    (t (getposAo X)))
 
105
   ;;tmr
 
106
   0))
 
107
 
 
108
;; The step definition of the physical system, including timer
 
109
 
 
110
(defun sigma (X eps)
 
111
  (make-state
 
112
   (getPosReq x)
 
113
   (getPreset x)
 
114
   ;;pos
 
115
   (cond
 
116
    ((> (getPos X) (getPosAo X))
 
117
     (- (getpos X) eps))
 
118
    ((< (getPos X) (getPosAo X))
 
119
     (+ (getpos X) eps))
 
120
    (t (getPos X)))
 
121
   (getposAo X)
 
122
   ;;tmr
 
123
   (+ (getTmr X) eps)))
 
124
 
 
125
(defun B-Y (X)
 
126
  (>= (getTmr X) (getPreset X)))
 
127
 
 
128
;; The system step function, as define by the single step function
 
129
;; sigma, the assignment function Y, and assignment predicate B-Y.
 
130
 
 
131
(defun sys-step (X eps)
 
132
  (cond
 
133
   ((B-Y X) (Y X))
 
134
   (t       (sigma X eps))))
 
135
 
 
136
;; The positive clamp function "clamps" the given r to a non-negative value.
 
137
;; If the value is negative, it returns zero. Otherwise, it returns
 
138
;; the given value.
 
139
;; It should be noted that the function is continuous in r.
 
140
 
 
141
(defun pos-clamp (r)
 
142
  (if (<= 0 r)
 
143
      r 0))
 
144
 
 
145
;; A component function of the overall measure m.
 
146
;; Intuitively, this measure function measures that the difference
 
147
;; between pos and posAo decreases over time.
 
148
;; This measure is 'active' when the difference between pos and
 
149
;; posAo is large.
 
150
 
 
151
(defun m1 (X eps)
 
152
  (cond
 
153
   ((<= (abs (- (getPosAo X) (getPos X)))
 
154
        (+ eps (pos-clamp (- (getPreset X) (getTmr X))))) 0)
 
155
   (t (+ 1 (/ (- (abs (- (getPosAo X) (getPos X)))
 
156
                 (+ (- (getPreset X) (getTmr X)) eps))
 
157
              eps)))))
 
158
 
 
159
;; A component function of the overall measure m.
 
160
;; Intuitively, this measure function measures that the difference
 
161
;; between posReq and posAo decreases over time.
 
162
 
 
163
(defun m2 (X eps)
 
164
  (declare (ignore eps))
 
165
  (if (and
 
166
       (<= (- (getPosAo X) (getPosReq X)) 3)
 
167
       (>= (- (getPosAo X) (getPosReq X)) -3))
 
168
      0
 
169
    (abs (- (getPosAo X) (getPosReq X)))))
 
170
 
 
171
;; A component function of the overall measure m.
 
172
;; Intuitively, this measure function measures that the difference
 
173
;; between pos and posAo decreases over time.
 
174
;; This measure is 'active' when the difference between pos and
 
175
;; posAo is small.
 
176
 
 
177
(defun m3 (X eps)
 
178
  (if (<= (abs (- (getPos X) (getPosAo X))) eps)
 
179
      0
 
180
    (/ (abs (- (getPos X) (getPosAo X))) eps)))
 
181
 
 
182
;; A component function of the overall measure m.
 
183
;; Intuitively, this measure function measures that the
 
184
;; timer changes in each step. This is useful for showing a
 
185
;; decreasing measure while the other system variables are unchanging.
 
186
 
 
187
(defun m4 (X eps)
 
188
  (cond
 
189
   ((< (getPreset X) (getTmr X)) 0)
 
190
   (t (+ 1 (/ (- (getPreset X) (getTmr X)) eps)))))
 
191
 
 
192
;; The overall measure function
 
193
 
 
194
(defun m (X eps)
 
195
  (cond ((and
 
196
          (< (m1 x eps) 1)
 
197
          (< (m2 x eps) 1))
 
198
         (make-ord 1 (+ 1 (m3 x eps))
 
199
                   (m4 x eps)))
 
200
        ((< (m1 x eps) 1)
 
201
         (make-ord 2 (+ 1 (m2 x eps))
 
202
                   (make-ord 1 (+ 1 (m3 x eps))
 
203
                             (m4 x eps))))
 
204
        (t (make-ord 3 (+ 1 (m1 x eps)) (m4 x eps)))))
 
205
 
 
206
;; Definition of the domain of the system variables and constants.
 
207
 
 
208
(defun valid-state (X eps)
 
209
  (and (realp (getPos X))
 
210
       (realp (getPreset X))
 
211
       (realp (getTmr X))
 
212
       (integerp (getPosAo X))
 
213
       (integerp (getPosReq X))
 
214
       (<= 51/10 (getPreset X))
 
215
       (<= 0 (getTmr x))
 
216
       (<= (getTmr x) (+ (getpreset x) eps))))
 
217
 
 
218
;; Cuong Chau: Disable the following control output setting.
 
219
;; (set-inhibit-output-lst '(proof-tree prove))
 
220
 
 
221
;; By requirement A1, we must show that if the assignment
 
222
;; predicate is satisfied in the current step, it is
 
223
;; not satisfied in the next step.
 
224
 
 
225
(defthm step-A1-thm
 
226
  (implies
 
227
   (and
 
228
    (valid-state x eps)
 
229
    (B-Y x))
 
230
   (not (B-Y (Y X))))
 
231
  :rule-classes nil)
 
232
 
 
233
;; Since the computer executes every delta time
 
234
;; period which is greater than preset, and since this
 
235
;; preset is a positive, standard number, then
 
236
;; to satisfy requirement A2, we must show that
 
237
;; the assignment function is limited if the
 
238
;; state variables are limited and satisfy B-Y.
 
239
 
 
240
(defthm step-A2-thm
 
241
  (implies
 
242
   (and
 
243
    (valid-state x eps)
 
244
    (B-Y x)
 
245
    (i-limited (getPosAo x))
 
246
    (i-limited (getTmr x))
 
247
    (i-limited (getPos x))
 
248
    (i-limited (getPreset x))
 
249
    (i-limited (getPosReq x)))
 
250
   (and
 
251
    (i-limited (getPosAo (Y x)))
 
252
    (i-limited (getTmr (Y x)))
 
253
    (i-limited (getPos (Y x)))
 
254
    (i-limited (getPreset (Y x)))
 
255
    (i-limited (getPosReq (Y x)))))
 
256
  :rule-classes nil
 
257
  :hints (("Goal" :in-theory (disable i-large))))
 
258
 
 
259
; Added by Matt K.: Avoids rewriter loop in m1-lt-1.
 
260
(local (in-theory (disable commutativity-2-of-+)))
 
261
 
 
262
;; A theorem that states the formula (< (m1 x eps) 1) is equal
 
263
;; to the corresponding safety predicate
 
264
;; Hence, we will use the shorter formula
 
265
;; (< (m1 x eps) 1) in the remainder of this session.
 
266
 
 
267
(defthm m1-lt-1
 
268
  (implies
 
269
   (and
 
270
    (valid-state x eps)
 
271
    (small-realp eps))
 
272
   (iff (< (m1 x eps) 1)
 
273
        (<= (abs (- (getPosAo X) (getPos X)))
 
274
            (+ eps (pos-clamp (- (getPreset X) (getTmr X)))))))
 
275
  :rule-classes nil)
 
276
 
 
277
;; A theorem that states the formula (< (m2 x eps) 1) is equal
 
278
;; to the corresponding safety predicate
 
279
;; Hence, we will use the shorter formula (< (m2 x eps) 1)
 
280
;; in the remainder of this session.
 
281
 
 
282
(defthm m2-lt-1
 
283
  (implies
 
284
   (and
 
285
    (valid-state x eps)
 
286
    (small-realp eps))
 
287
   (iff (< (m2 x eps) 1)
 
288
        (and
 
289
         (<= (- (getPosAo X) (getPosReq X)) 3)
 
290
         (>= (- (getPosAo X) (getPosReq X)) -3))))
 
291
  :rule-classes nil)
 
292
 
 
293
;; Check that a valid state is an ordinal real
 
294
 
 
295
(defthm ordinal-real-thm
 
296
  (implies
 
297
   (and (valid-state x eps)
 
298
        (small-realp eps)
 
299
        (not (and
 
300
              (< (m1 x eps) 1)
 
301
              (< (m2 x eps) 1)
 
302
              (<= (abs (- (getpos x) (getPosReq x))) (+ 3 (* 2 eps))))))
 
303
   (o-real-p (m x eps))))
 
304
 
 
305
;; If we start in valid state, then next state also satisfies valid state
 
306
 
 
307
(defthm valid-state-preserve
 
308
  (implies
 
309
   (and (valid-state x eps)
 
310
        (small-realp eps))
 
311
   (valid-state (sys-step x eps) eps)))
 
312
 
 
313
;; The following theorem shows that once m1 < 1, then it remains so
 
314
;; similarly, once m2 < 1, it remains so. These results
 
315
;; are used to show that if m1 < 1 and m2 < 1, then
 
316
;; -3-eps <= (abs (- pos PosReq)) <= 3+eps is true
 
317
;; for all ensuing states.
 
318
 
 
319
(defthm m-1-preserve
 
320
  (implies
 
321
   (and (valid-state x eps)
 
322
        (small-realp eps)
 
323
        (< (m1 x eps) 1))
 
324
   (< (m1 (sys-step x eps) eps) 1))
 
325
  :rule-classes :linear)
 
326
 
 
327
(defthm m-2-preserve
 
328
  (implies
 
329
   (and (valid-state x eps)
 
330
        (small-realp eps)
 
331
        (< (m1 x eps) 1)
 
332
        (< (m2 x eps) 1))
 
333
   (< (m2 (sys-step x eps) eps) 1))
 
334
  :rule-classes :linear)
 
335
 
 
336
(defthm pos-posReq-preserve
 
337
  (implies
 
338
   (and (valid-state x eps)
 
339
        (small-realp eps)
 
340
        (< (m1 x eps) 1)
 
341
        (< (m2 x eps) 1)
 
342
        (<= (abs (- (getpos x) (getPosReq x))) (+ 3 (* 2 eps))))
 
343
   (<= (abs (- (getpos (sys-step x eps))
 
344
               (getposReq (sys-step x eps)))) (+ 3 (* 2 eps))))
 
345
  :rule-classes :linear)
 
346
 
 
347
(defthm safety-property-preserve
 
348
  (implies
 
349
   (and (valid-state x eps)
 
350
        (small-realp eps)
 
351
        (< (m1 x eps) 1)
 
352
        (< (m2 x eps) 1)
 
353
        (<= (abs (- (getpos x) (getPosReq x))) (+ 3 (* 2 eps))))
 
354
   (and
 
355
    (valid-state (sys-step x eps) eps) ;; Cuong Chau: I changed "(valid-state x
 
356
    ;; eps)" to "(valid-state (sys-step x eps) eps)" 
 
357
    (< (m1 (sys-step x eps) eps) 1)
 
358
    (< (m2 (sys-step x eps) eps) 1)
 
359
    (<= (abs (- (getpos (sys-step x eps))
 
360
                (getposReq (sys-step x eps)))) (+ 3 (* 2 eps)))))
 
361
  :rule-classes nil
 
362
  :hints (("Goal" :in-theory (disable sys-step valid-state m1 m2))
 
363
          ("Subgoal 2" :use ((:instance pos-posReq-preserve)))))
 
364
 
 
365
;; The measure is decreasing on the real ordinals, with
 
366
;; comparison o<-1
 
367
 
 
368
(defthm m-1-decreases
 
369
  (implies
 
370
   (and (valid-state x eps)
 
371
        (small-realp eps)
 
372
        (not (< (m1 x eps) 1)))
 
373
   (o<-1 (m (sys-step x eps) eps) (m x eps))))
 
374
 
 
375
(defthm m-2-decreases
 
376
  (implies
 
377
   (and (valid-state x eps)
 
378
        (small-realp eps)
 
379
        (< (m1 x eps) 1)
 
380
        (not (< (m2 x eps) 1)))
 
381
   (o<-1 (m (sys-step x eps) eps) (m x eps))))
 
382
 
 
383
(defthm m-decreases
 
384
  (implies
 
385
   (and (valid-state x eps)
 
386
        (small-realp eps)
 
387
        (not (and
 
388
              (< (m1 x eps) 1)
 
389
              (< (m2 x eps) 1)
 
390
              (<= (abs (- (getpos x) (getPosReq x))) (+ 3 (* 2 eps))))))
 
391
   (o<-1 (m (sys-step x eps) eps) (m x eps))))
 
392
 
 
393
;; Cuong Chau: Disable the following control output setting.
 
394
;; (set-inhibit-output-lst '(proof-tree))
 
395
 
 
396
(in-theory (disable o<-1 o-floor1 o-real-p sys-step valid-state m m1 m2 m3))
 
397
 
 
398
;; Fix m so that it always returns an ordinal
 
399
 
 
400
(defun m-fix (x eps)
 
401
  (cond
 
402
   ((not (and (valid-state x eps)
 
403
              (small-realp eps)
 
404
              (not (and
 
405
                    (< (m1 x eps) 1)
 
406
                    (< (m2 x eps) 1)
 
407
                    (<= (abs (- (getpos x) (getPosReq x)))
 
408
                        (+ 3 (* 2 eps)))))))
 
409
    0)
 
410
   (t (o-floor1 (m x eps)))))
 
411
 
 
412
;; m-fix is an ordinal
 
413
 
 
414
(defthm m-fix-o-p
 
415
  (o-p (m-fix x eps)))
 
416
 
 
417
;; sys-step decreases, using measure m-fix
 
418
 
 
419
(defthm m-fix-decreases
 
420
  (implies
 
421
   (and (valid-state x eps)
 
422
        (small-realp eps)
 
423
        (not (and
 
424
              (< (m1 x eps) 1)
 
425
              (< (m2 x eps) 1)
 
426
              (<= (abs (- (getpos x) (getPosReq x)))
 
427
                  (+ 3 (* 2 eps))))))
 
428
   (o< (m-fix (sys-step x eps) eps) (m-fix x eps))))