#|
Copyright (C) 1995 by William D. Young.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
William D. Young PROVIDES ABSOLUTELY NO WARRANTY. THE EVENT SCRIPT IS
PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU. SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL William D. Young BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
;; >> Might try to relax the assumption that there is only
;; one train and it always is going in the same direction.
(boot-strap nqthm)
;; SOME SUBSIDIARY LEMMAS
(prove-lemma not-lessp-sub1 (rewrite)
(implies (not (lessp x y))
(equal (lessp x (sub1 y)) f)))
(prove-lemma plus-add1 (rewrite)
(and (equal (plus x (add1 y)) (add1 (plus x y)))
(equal (plus (add1 x) y) (add1 (plus x y)))))
(prove-lemma difference-add1-sub1 (rewrite)
(implies (not (zerop x))
(equal (difference x (add1 y))
(sub1 (difference x y)))))
;; THE SYSTEM
;; Our simple control system consists of three distinct components.
;; The train is an part of the environment; it produces in a way that
;; we cannot control but subject to certain constraints that we specify.
;; The gate is our controlled system and responds to a series of commands
;; generated by the controller. The controller is a device that inputs
;; a series of sensor readings from the environment, giving the position of
;; the train. It generates a series of actuator commands for the gate.
;;
;; Our task is to model the system comprised of these three components.
;; GATE SIMULATION
;; The gate is the controlled system, so we consider that it responds
;; reliably to a series of commands that are generated by the control
;; algorithm. These commands come in the form of a sequence of atoms
;; 'open and 'close. The simulation of the gate tells us its state
;; at each moment of time.
(constrain choose-time-intro (rewrite)
;; This defines a function that arbitrarily but consistently
;; chooses a member of the interval [min..max] if there is one.
;; The additional parameter is added to make it more random.
(implies (leq min max)
(and (numberp (choose-time min max oracle))
(not (lessp (choose-time min max oracle) min))
(not (lessp max (choose-time min max oracle)))))
((choose-time (lambda (x y z) (fix x)))))
(prove-lemma lessp-sub1-choose-sub1-max (rewrite)
(implies (and (lessp (sub1 max) x)
(leq min max))
(equal (lessp (sub1 (choose-time min max oracle))
x)
t)))
;; The gate can be in 4 states: open, closed, going-up, going-down.
(constrain gate-parameters-intro (rewrite)
(and (numberp (gate-closing-min-time))
(numberp (gate-closing-max-time))
(lessp 0 (gate-closing-max-time))
(not (lessp (gate-closing-max-time)
(gate-closing-min-time)))
(numberp (gate-opening-min-time))
(lessp 0 (gate-opening-max-time))
(numberp (gate-opening-max-time))
(not (lessp (gate-opening-max-time)
(gate-opening-min-time))))
((gate-closing-min-time (lambda nil 0))
(gate-closing-max-time (lambda nil 1))
(gate-opening-min-time (lambda nil 0))
(gate-opening-max-time (lambda nil 1))))
;; The gate state is a pair (current-state . n) where n is the time that
;; the gate will remain in that state. This is only required for going
;; up and going down and tells us how long they can expect to be in that
;; condition unless they are given a countervening order. This doesn't
;; take into account some anomolous situations as , for example, when we
;; may have just told the gate to close and immediately tell it to open,
;; so that it has only a short distance to move.
(defn gate-positionp (x)
(member x '(open closed going-up going-down)))
(defn gate-current-state (state)
(car state))
(defn gate-state-duration (state)
(cdr state))
(defn open (state)
(equal (gate-current-state state) 'open))
(defn closed (state)
(equal (gate-current-state state) 'closed))
(defn going-up (state)
(equal (gate-current-state state) 'going-up))
(defn going-down (state)
(equal (gate-current-state state) 'going-down))
(prove-lemma gate-state-accessors (rewrite)
(and (equal (gate-current-state (cons x y)) x)
(equal (gate-state-duration (cons x y)) y)))
(defn legal-gate-statep (x)
(and (gate-positionp (gate-current-state x))
(implies (or (going-up x)
(going-down x))
(numberp (gate-state-duration x)))))
(disable gate-current-state)
(disable gate-state-duration)
(defn compute-going-down-state (state)
(let ((n (gate-state-duration state)))
(if (zerop n)
(cons 'closed 0)
(cons 'going-down (sub1 n)))))
(defn compute-going-up-state (state)
(let ((n (gate-state-duration state)))
(if (zerop n)
(cons 'open 0)
(cons 'going-up (sub1 n)))))
(defn gate-next-state (cmd state oracle)
;; Assuming the input command is either 'open or 'close,
;; this gives the next state for any potential current state
;; of the gate. This needs the sub1's because otherwise, if
;; the gate-closing-max-time is 4 and that is chosen, then
;; the gate will actually take 5 cycles to close. Notice
;; that if the max time is 0, it still takes one tick for the
;; gate to close.
(case cmd
(close
(case (gate-current-state state)
(open (cons 'going-down
(sub1 (choose-time (gate-closing-min-time)
(gate-closing-max-time)
oracle))))
(closed state)
(going-up (cons 'going-down
(sub1 (choose-time (gate-closing-min-time)
(gate-closing-max-time)
oracle))))
(going-down (compute-going-down-state state))
(otherwise f)))
(open
(case (gate-current-state state)
(open state)
(closed (cons 'going-up
(sub1 (choose-time (gate-opening-min-time)
(gate-opening-max-time)
oracle))))
(going-up (compute-going-up-state state))
(going-down (cons 'going-up
(sub1 (choose-time (gate-opening-min-time)
(gate-opening-max-time)
oracle))))
(otherwise f)))
(otherwise f)))
;; TRAIN BEHAVIOR
;; The train provides our input to the system. The gate must act in
;; response to the train. It can do so only if the behavior of the
;; train meets certain reasonable criteria. Therefore, the specification
;; of the train consists of a set of constraints on the possible traces of
;; the train behavior as sensed by input sensors along the track. The
;; train can be in one of 4 states: approaching the crossing,
;; in the crossing, past the crossing (or outside of our field of view).
;; We assume that the sensors are accurate (debounced) and that trains are
;; sufficiently widely separated.
(defn train-positionp (x)
(member x '(approaching in-gate elsewhere)))
(defn approaching (x)
(equal x 'approaching))
(defn in-gate (x)
(equal x 'in-gate))
(defn elsewhere (x)
(equal x 'elsewhere))
(defn legal-next-positions (x)
;; This defines the legal transitions in the
;; trace of the train's behavior. It says, for
;; example, that a trace can't have the train jump
;; from elsewhere to in-gate.
(case x
(elsewhere '(elsewhere approaching))
(approaching '(approaching in-gate))
(in-gate '(in-gate elsewhere))
(otherwise nil)))
(defn legal-transitionp (x y)
(member y (legal-next-positions x)))
(defn legal-train-trace1 (trace)
;; Defines part of what it means for a trace to be legal.
;; Notice that the constraint on legal transitions ensures
;; that every transition be at least 1 in length. That is,
;; the sequence of 'approaching between 'elsewhere and
;; 'in-gate couldn't be empty because that would not be a
;; legal-transitionp.
(if (nlistp trace)
(equal trace nil)
(and (train-positionp (car trace))
(if (listp (cdr trace))
(legal-transitionp (car trace) (cadr trace))
t)
(legal-train-trace1 (cdr trace)))))
(constrain train-constraints (rewrite)
;; This characterizes the amount of time the train
;; must spend in approaching, before it can actually
;; enter the gate. This must be at least long enough
;; for the gate to come down.
(and (numberp (approaching-min-time))
(not (lessp (approaching-min-time)
(add1 (gate-closing-max-time)))))
((approaching-min-time
(lambda nil (plus 1 (gate-closing-max-time))))))
(defn seq-long-enough (x trace seen-so-far min)
(if (zerop seen-so-far)
(if (nlistp trace)
t
(if (equal (car trace) x)
(seq-long-enough x (cdr trace) 1 min)
(seq-long-enough x (cdr trace) 0 min)))
(if (nlistp trace)
(leq min seen-so-far)
(if (equal (car trace) x)
(seq-long-enough x (cdr trace) (add1 seen-so-far) min)
(and (leq min seen-so-far)
(seq-long-enough x (cdr trace) 0 min))))))
(defn approaches-long-enough (trace seen-so-far)
(seq-long-enough 'approaching trace seen-so-far (approaching-min-time)))
(defn distance-to-gate (trace)
;; This guarantees that if the trace runs out
;; that the computed distance is larger than it would
;; need to be guarantee safety.
(if (nlistp trace)
(add1 (add1 (approaching-min-time)))
(if (in-gate (car trace))
0
(add1 (distance-to-gate (cdr trace))))))
(disable approaches-long-enough)
(defn legal-train-trace (trace n)
;; Here n records the number of 'approaching's we have
;; already seen.
(and (legal-train-trace1 trace)
(approaches-long-enough trace n)))
;; CONTROLLER
;; The controller takes as input a sequence of readings from the track
;; sensors telling where the train is. It's output is a sequence of
;; actuator commands of the form 'open or 'close. The gate responds to
;; these.
(defn control-output (input)
;; This controller is too simple for the two train situation
;; where a train may be approaching while another is in the
;; gate.
(if (equal input 'elsewhere)
'open
'close))
;; THE SYSTEM
(defn gate-behavior (train-trace gate-state)
;; Takes in a sequence of readings of the train position
;; and outputs a sequence of states of the gate behavior.
(let ((next-state (gate-next-state (control-output (car train-trace))
gate-state
train-trace)))
(if (nlistp train-trace)
nil
(cons next-state
(gate-behavior (cdr train-trace) next-state)))))
(prove-lemma approaches-stay-long-enough (rewrite)
(implies (and (approaches-long-enough train-trace approaching-time)
(equal (car train-trace)
'approaching))
(approaches-long-enough (cdr train-trace)
(add1 approaching-time)))
((enable approaches-long-enough)))
;; Now we state safety properties of this system. In particular,
;; we devise constraints that assure that the gate will always be
;; closed when the train is in the gate.
(prove-lemma approaches-long-enough-zero (rewrite)
(implies (listp train-trace)
(equal (approaches-long-enough train-trace approaching-time)
(if (zerop approaching-time)
(if (equal (car train-trace) 'approaching)
(approaches-long-enough (cdr train-trace) 1)
(approaches-long-enough (cdr train-trace) 0))
(if (equal (car train-trace) 'approaching)
(approaches-long-enough (cdr train-trace)
(add1 approaching-time))
(and (approaches-long-enough (cdr train-trace) 0)
(not (lessp approaching-time
(approaching-min-time))))))))
((enable approaches-long-enough)
(do-not-induct t)))
(defn distance-to-gate-induction (train-trace n)
(if (nlistp train-trace)
t
(if (nlistp (cdr train-trace))
t
(if (equal (car train-trace) 'approaching)
(distance-to-gate-induction (cdr train-trace)
(add1 n))
(distance-to-gate-induction (cdr train-trace) 0)))))
(prove-lemma distance-to-gate-first-approaching (rewrite)
(implies (and (listp train-trace)
(equal (car train-trace) 'approaching)
(approaches-long-enough train-trace n))
(lessp (approaching-min-time)
(plus n (add1 (distance-to-gate train-trace)))))
((induct (distance-to-gate-induction train-trace n))))
(prove-lemma distance-to-gate-first-approaching2 (rewrite)
(implies (and (listp train-trace)
(equal (car train-trace) 'approaching)
(approaches-long-enough train-trace 0))
(lessp (sub1 (approaching-min-time))
(distance-to-gate train-trace)))
((use (distance-to-gate-first-approaching (n 0)))))
(defn good-statep (train-state gate-state distance-to-gate time-elsewhere)
;; This defines a relation between the train current position and
;; the state of the gate at that step that assures that the gate
;; can close before the train reaches the gate and that the gate is
;; going up as soon as possible after leaving the gate.
(and (implies (going-down gate-state)
(lessp (gate-state-duration gate-state)
(gate-closing-max-time)))
(implies (going-up gate-state)
(lessp (gate-state-duration gate-state)
(gate-opening-max-time)))
(case train-state
(in-gate (closed gate-state))
(approaching (or (closed gate-state)
(and (going-down gate-state)
(lessp (gate-state-duration gate-state)
distance-to-gate))
(lessp (gate-closing-max-time)
distance-to-gate)))
(elsewhere (and (implies (lessp (gate-opening-max-time)
time-elsewhere)
(open gate-state))
(or (and (closed gate-state)
(zerop time-elsewhere))
(open gate-state)
(and (going-up gate-state)
(leq (gate-state-duration gate-state)
(difference (gate-opening-max-time)
time-elsewhere))))))
(otherwise f))))
(defn su-invariant (train-trace gate-trace time-elsewhere)
(if (nlistp train-trace)
t
(if (nlistp gate-trace)
f
(and (good-statep (car train-trace)
(car gate-trace)
(distance-to-gate train-trace)
time-elsewhere)
(su-invariant (cdr train-trace)
(cdr gate-trace)
(if (elsewhere (car train-trace))
(add1 time-elsewhere)
0))))))
(defn controller-induction (train-trace gate-state
time-approaching time-elsewhere)
(if (nlistp train-trace)
t
(if (nlistp (cdr train-trace))
t
(controller-induction (cdr train-trace)
(gate-next-state (control-output
(car train-trace))
gate-state
train-trace)
(if (equal (car train-trace) 'approaching)
(add1 time-approaching)
0)
(if (equal (car train-trace) 'elsewhere)
(add1 time-elsewhere)
0)))))
(prove-lemma controller-su-invariant (rewrite)
;; This is the key inductive lemma.
(implies (and (legal-train-trace train-trace time-approaching)
(legal-gate-statep gate-state)
(good-statep (car train-trace)
gate-state
(distance-to-gate train-trace)
time-elsewhere))
(su-invariant train-trace
(gate-behavior train-trace gate-state)
time-elsewhere))
((induct (controller-induction train-trace gate-state
time-approaching time-elsewhere))))
;; Now we define the desired safety and utility properties and prove that
;; they follow from the su-invariant property.
(defn safety (train-trace gate-trace)
;; This property establishes the desired relation
;; between the train-trace and the gate-trace that
;; assures that whenever the train is in the
;; crossing, the gate is closed.
(if (nlistp train-trace)
t
(if (in-gate (car train-trace))
(and (closed (car gate-trace))
(safety (cdr train-trace)
(cdr gate-trace)))
(safety (cdr train-trace)
(cdr gate-trace)))))
(prove-lemma su-invariant-implies-safety (rewrite)
(implies (su-invariant train-trace
gate-trace
time-elsewhere)
(safety train-trace gate-trace)))
(defn utility (train-trace gate-trace time-elsewhere)
(if (nlistp train-trace)
t
(if (elsewhere (car train-trace))
(and (if (lessp (gate-opening-max-time)
time-elsewhere)
(open (car gate-trace))
t)
(utility (cdr train-trace)
(cdr gate-trace)
(add1 time-elsewhere)))
(utility (cdr train-trace)
(cdr gate-trace)
0))))
(prove-lemma su-invariant-implies-utility (rewrite)
(implies (su-invariant train-trace
gate-trace
time-elsewhere)
(utility train-trace gate-trace time-elsewhere)))
(prove-lemma controller-maintains-safety-and-utility (rewrite)
(implies (and (legal-train-trace train-trace time-approaching)
(legal-gate-statep gate-state)
(good-statep (car train-trace)
gate-state
(distance-to-gate train-trace)
time-elsewhere))
(and (safety train-trace
(gate-behavior train-trace gate-state))
(utility train-trace
(gate-behavior train-trace gate-state)
time-elsewhere)))
((use (controller-su-invariant))))
;; We now characterize an initial state and show that our invariant
;; is true in that initial state.
(defn initial-statep (train-state gate-state)
(and (equal train-state 'elsewhere)
(equal (gate-current-state gate-state) 'open)))
(prove-lemma controller-safety ()
;; This is the final safety version of the theorem.
(implies (and (initial-statep (car train-trace) gate-state)
(legal-train-trace train-trace time-approaching))
(safety train-trace
(gate-behavior train-trace gate-state)))
((use (controller-maintains-safety-and-utility))
(disable utility)))
(prove-lemma controller-utility ()
;; This is the final utility version of the theorem,
(implies (and (initial-statep (car train-trace) gate-state)
(legal-train-trace train-trace time-approaching))
(utility train-trace
(gate-behavior train-trace gate-state)
time-elsewhere))
((use (controller-maintains-safety-and-utility))))
;; AN ALTERNATIVE SPECIFICATION
;; The criticism may be raised that our specification functions
;; SAFETY and UTILITY are harder to understand than the alternatives
;; available in some other specification languages, using quantifiers
;; for example. We offer alternative versions SAFETY2 and UTILITY2
;; that are in a quantified style and prove that they are
;; consequences of our versions.
(defn length (x)
(if (listp x)
(add1 x)
0))
(defn get (n lst)
;; This is a list indexing function. "(Get n lst)"
;; is conceptually identical to "lst[n]" with 0-based
;; indexing.
(if (zerop n)
(car lst)
(get (sub1 n) (cdr lst))))
(defn-sk safety2 (train-trace gate-trace)
;; This version shows directly the component-wise
;; relation between train states and gate states.
(forall i
(implies (in-gate (get i train-trace))
(closed (get i gate-trace)))))
(prove-lemma safety2-suff (rewrite)
;; This lemma provides one of the two required proof rules
;; for safety2
(implies (implies (in-gate (get (i gate-trace train-trace)
train-trace))
(closed (get (i gate-trace train-trace)
gate-trace)))
(safety2 train-trace gate-trace)))
(prove-lemma safety2-necc (rewrite)
(implies (not (implies (in-gate (get i train-trace))
(closed (get i gate-trace))))
(not (safety2 train-trace gate-trace)))
((use (safety2))
(disable in-gate closed in-gate safety2)))
(defn get-induct (i x y)
(if (zerop i)
t
(get-induct (sub1 i) (cdr x) (cdr y))))
(prove-lemma safety-implies-safety2-get (rewrite)
(implies (and (safety train-trace gate-trace)
(in-gate (get i train-trace)))
(closed (get i gate-trace)))
((induct (get-induct i train-trace gate-trace))))
(prove-lemma safety-implies-safety2 (rewrite)
(implies (safety train-trace gate-trace)
(safety2 train-trace gate-trace))
((use (safety2-suff))
(disable closed)))
(prove-lemma controller-safety2 ()
(implies (and (initial-statep (car train-trace) gate-state)
(legal-train-trace train-trace time-approaching))
(safety2 train-trace
(gate-behavior train-trace gate-state)))
((use (controller-safety))))
(defn time-elsewhere (i found-so-far train-trace)
;; This defines how many 'elsewhere's have been
;; encountered immediately before position i in
;; the trace, assuming we have found found-so-far
;; up to now.
(if (zerop i)
found-so-far
(if (elsewhere (car train-trace))
(time-elsewhere (sub1 i)
(add1 found-so-far)
(cdr train-trace))
(time-elsewhere (sub1 i)
0
(cdr train-trace)))))
(defn-sk utility2 (train-trace gate-trace n)
(forall i
(implies (and (elsewhere (get i train-trace))
(lessp (gate-opening-max-time)
(time-elsewhere i n train-trace)))
(open (get i gate-trace)))))
(prove-lemma utility2-suff (rewrite)
(implies
(implies (and (elsewhere (get (i-1 gate-trace n train-trace)
train-trace))
(lessp (gate-opening-max-time)
(time-elsewhere (i-1 gate-trace n train-trace)
n train-trace)))
(open (get (i-1 gate-trace n train-trace)
gate-trace)))
(utility2 train-trace gate-trace n)))
(prove-lemma utility2-necc (rewrite)
(implies (not (implies (and (elsewhere (get i train-trace))
(lessp (gate-opening-max-time)
(time-elsewhere i n train-trace)))
(open (get i gate-trace))))
(not (utility2 train-trace gate-trace n)))
((use (utility2))))
(defn get-induct2 (i x y n)
(if (zerop i)
t
(get-induct2 (sub1 i)
(cdr x)
(cdr y)
(if (elsewhere (car x))
(add1 n)
0))))
(prove-lemma utility-implies-utility2-get (rewrite)
(implies (and (utility train-trace gate-trace n)
(elsewhere (get i train-trace))
(lessp (gate-opening-max-time)
(time-elsewhere i n train-trace)))
(open (get i gate-trace)))
((induct (get-induct2 i train-trace gate-trace n))))
(prove-lemma utility-implies-utility2 (rewrite)
(implies (utility train-trace gate-trace time-elsewhere)
(utility2 train-trace gate-trace time-elsewhere))
((use (utility2-suff (n time-elsewhere)))
(disable open)))
(prove-lemma controller-utility2 ()
(implies (and (initial-statep (car train-trace) gate-state)
(legal-train-trace train-trace time-approaching))
(utility2 train-trace
(gate-behavior train-trace gate-state)
time-elsewhere))
((use (controller-utility))))