#|
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.

Event: Start with the initial nqthm theory.

;; SOME SUBSIDIARY LEMMAS

Theorem: not-lessp-sub1 (x ≮ y) → ((x < (y − 1)) = f)

Theorem: plus-add1 ((x + (1 + y)) = (1 + (x + y))) ∧ (((1 + x) + y) = (1 + (x + y)))

Theorem: difference-add1-sub1 (x ≄ 0) → ((x − (1 + y)) = ((x − y) − 1))

;; 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.

Conservative Axiom: choose-time-intro (min ≤ max) → ((choose-time (min, max, oracle) ∈ N)

∧ (choose-time (min, max, oracle) ≮ min) ∧ (max ≮ choose-time (min, max, oracle)))

Simultaneously, we introduce the new function symbol choose-time.

Theorem: lessp-sub1-choose-sub1-max (((max − 1) < x) ∧ (min ≤ max)) → (((choose-time (min, max, oracle) − 1) < x) = t)

;; The gate can be in 4 states: open, closed, going-up, going-down.

Conservative Axiom: gate-parameters-intro (gate-closing-min-time ∈ N) ∧ (gate-closing-max-time ∈ N) ∧ (0 < gate-closing-max-time) ∧ (gate-closing-max-time ≮ gate-closing-min-time) ∧ (gate-opening-min-time ∈ N) ∧ (0 < gate-opening-max-time) ∧ (gate-opening-max-time ∈ N) ∧ (gate-opening-max-time ≮ gate-opening-min-time)

Simultaneously, we introduce the new function symbols gate-closing-min-time, gate-closing-max-time, gate-opening-min-time, and gate-opening-max-time.

;; 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.

Definition:

gate-positionp (x) = (x ∈ '(open closed going-up going-down))

Definition: gate-current-state (state) = car (state)

Definition: gate-state-duration (state) = cdr (state)

Definition: open (state) = (gate-current-state (state) = 'open)

Definition: closed (state) = (gate-current-state (state) = 'closed)

Definition: going-up (state) = (gate-current-state (state) = 'going-up)

Definition: going-down (state) = (gate-current-state (state) = 'going-down)

Theorem: gate-state-accessors (gate-current-state (cons (x, y)) = x) ∧ (gate-state-duration (cons (x, y)) = y)

Definition: legal-gate-statep (x) = (gate-positionp (gate-current-state (x))

∧ ((going-up (x) ∨ going-down (x)) → (gate-state-duration (x) ∈ N)))

Event: Disable gate-current-state.

Event: Disable gate-state-duration.

Definition: compute-going-down-state (state) = let n be gate-state-duration (state)

in

if n ≃ 0 then cons ('closed, 0)

else cons ('going-down, n − 1) endif endlet Definition: compute-going-up-state (state) = let n be gate-state-duration (state)

in if n ≃ 0 then cons ('open, 0) else cons ('going-up, n − 1) endif endlet

Definition: gate-next-state (cmd, state, oracle) = case on cmd:

case = close then case on gate-current-state (state):

case = open

then cons ('going-down,

choose-time (gate-closing-min-time, gate-closing-max-time, oracle) − 1)

case = closed then state case = going-up

then cons ('going-down,

choose-time (gate-closing-min-time, gate-closing-max-time, oracle) − 1)

case = going-down then compute-going-down-state (state) otherwise f endcase

case = open then case on gate-current-state (state):

case = open then state case = closed then cons ('going-up,

choose-time (gate-opening-min-time, gate-opening-max-time, oracle) − 1)

case = going-up then compute-going-up-state (state) case = going-down then cons ('going-up,

choose-time (gate-opening-min-time, gate-opening-max-time, oracle) − 1)

otherwise f endcase

otherwise f endcase

;; 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.

Definition:

train-positionp (x) = (x ∈ '(approaching in-gate elsewhere))

Definition: approaching (x) = (x = 'approaching)

Definition: in-gate (x) = (x = 'in-gate)

Definition: elsewhere (x) = (x = 'elsewhere)

Definition: legal-next-positions (x) = case on x:

case = elsewhere

    then '(elsewhere approaching)

case = approaching

     then '(approaching in-gate)

case = in-gate

     then '(in-gate elsewhere)

otherwise nil endcase

Definition: legal-transitionp (x, y) = (y ∈ legal-next-positions (x))

Definition: legal-train-trace1 (trace) = if trace ≃ nil then trace = nil

else train-positionp (car (trace)) ∧ if listp (cdr (trace))

then legal-transitionp (car (trace), cadr (trace)) else t endif

∧ legal-train-trace1 (cdr (trace)) endif Conservative Axiom: train-constraints (approaching-min-time ∈ N) ∧ (approaching-min-time ≮ (1 + gate-closing-max-time))

Simultaneously, we introduce the new function symbol approaching-min-time.

Definition: seq-long-enough (x, trace, seen-so-far, min) = if seen-so-far ≃ 0

then if trace ≃ nil then t elseif car (trace) = x then seq-long-enough (x, cdr (trace), 1, min) else seq-long-enough (x, cdr (trace), 0, min) endif

elseif trace ≃ nil then min ≤ seen-so-far

elseif car (trace) = x

then seq-long-enough (x, cdr (trace), 1 + seen-so-far, min)

else (min ≤ seen-so-far)

∧ seq-long-enough (x, cdr (trace), 0, min) endif

Definition: approaches-long-enough (trace, seen-so-far) = seq-long-enough ('approaching,

trace,

seen-so-far,

approaching-min-time)

Definition: distance-to-gate (trace) = if trace ≃ nil then 1 + (1 + approaching-min-time)

elseif in-gate (car (trace)) then 0

else 1 + distance-to-gate (cdr (trace)) endif

Event: Disable approaches-long-enough.

Definition: legal-train-trace (trace, n) = (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.

Definition: control-output (input)

= if input = 'elsewhere then 'open

else 'close endif

;; THE SYSTEM

Definition: gate-behavior (train-trace, gate-state) = let next-state be gate-next-state (control-output (car (train-trace)),

gate-state, train-trace)

in

if train-trace ≃ nil then nil

else cons (next-state, gate-behavior (cdr (train-trace), next-state)) endif endlet

Theorem: approaches-stay-long-enough (approaches-long-enough (train-trace, approaching-time) ∧ (car (train-trace) = 'approaching)) → approaches-long-enough (cdr (train-trace), 1 + approaching-time)

;; 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.

Theorem: approaches-long-enough-zero listp (train-trace) → (approaches-long-enough (train-trace, approaching-time)

= if approaching-time ≃ 0

then if car (train-trace) = 'approaching then approaches-long-enough (cdr (train-trace), 1) else approaches-long-enough (cdr (train-trace), 0) endif

elseif car (train-trace) = 'approaching

then approaches-long-enough (cdr (train-trace),

1 + approaching-time)

else approaches-long-enough (cdr (train-trace), 0) ∧ (approaching-time ≮ approaching-min-time) endif)

Definition: distance-to-gate-induction (train-trace, n) = if train-trace ≃ nil then t

elseif cdr (train-trace) ≃ nil then t elseif car (train-trace) = 'approaching then distance-to-gate-induction (cdr (train-trace), 1 + n) else distance-to-gate-induction (cdr (train-trace), 0) endif

Theorem: distance-to-gate-first-approaching (listp (train-trace) ∧ (car (train-trace) = 'approaching) ∧ approaches-long-enough (train-trace, n)) → (approaching-min-time < (n + (1 + distance-to-gate (train-trace))))

Theorem: distance-to-gate-first-approaching2 (listp (train-trace) ∧ (car (train-trace) = 'approaching) ∧ approaches-long-enough (train-trace, 0)) → ((approaching-min-time − 1) < distance-to-gate (train-trace))

Definition: good-statep (train-state, gate-state, distance-to-gate, time-elsewhere) = ((going-down (gate-state)

→ (gate-state-duration (gate-state) < gate-closing-max-time)) ∧ (going-up (gate-state)

→ (gate-state-duration (gate-state)

< gate-opening-max-time))

∧ case on train-state: case = in-gate then closed (gate-state) case = approaching then closed (gate-state)

∨ (going-down (gate-state)

∧ (gate-state-duration (gate-state) < distance-to-gate))

∨ (gate-closing-max-time < distance-to-gate) case = elsewhere then ((gate-opening-max-time < time-elsewhere)

→ open (gate-state))

∧ ((closed (gate-state) ∧ (time-elsewhere ≃ 0)) ∨ open (gate-state) ∨ (going-up (gate-state)

∧ (gate-state-duration (gate-state)

≤ (gate-opening-max-time − time-elsewhere))))

otherwise f endcase)

Definition: su-invariant (train-trace, gate-trace, time-elsewhere)

= if train-trace ≃ nil then t elseif gate-trace ≃ nil then f else 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)) then 1 + time-elsewhere else 0 endif) endif

Definition: controller-induction (train-trace, gate-state, time-approaching, time-elsewhere) = if train-trace ≃ nil then t

elseif cdr (train-trace) ≃ nil then t else controller-induction (cdr (train-trace),

gate-next-state (control-output (car (train-trace)), gate-state, train-trace),

if car (train-trace)

                           = 'approaching

then 1 + time-approaching

else 0 endif, if car (train-trace)

                           = 'elsewhere

then 1 + time-elsewhere else 0 endif) endif

Theorem: controller-su-invariant (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)

;; Now we define the desired safety and utility properties and prove that
;; they follow from the su-invariant property.

Definition: safety (train-trace, gate-trace) = if train-trace ≃ nil then t

elseif in-gate (car (train-trace)) then closed (car (gate-trace))

∧ safety (cdr (train-trace), cdr (gate-trace)) else safety (cdr (train-trace), cdr (gate-trace)) endif

Theorem: su-invariant-implies-safety su-invariant (train-trace, gate-trace, time-elsewhere) → safety (train-trace, gate-trace)

Definition: utility (train-trace, gate-trace, time-elsewhere) = if train-trace ≃ nil then t

elseif elsewhere (car (train-trace))

then if gate-opening-max-time < time-elsewhere then open (car (gate-trace)) else t endif ∧ utility (cdr (train-trace),

cdr (gate-trace), 1 + time-elsewhere) else utility (cdr (train-trace), cdr (gate-trace), 0) endif

Theorem: su-invariant-implies-utility su-invariant (train-trace, gate-trace, time-elsewhere) → utility (train-trace, gate-trace, time-elsewhere)

Theorem: controller-maintains-safety-and-utility (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))

→ (safety (train-trace, gate-behavior (train-trace, gate-state))

∧ utility (train-trace, gate-behavior (train-trace, gate-state), time-elsewhere))

;; We now characterize an initial state and show that our invariant
;; is true in that initial state.

Definition: initial-statep (train-state, gate-state) = ((train-state = 'elsewhere)

∧ (gate-current-state (gate-state) = 'open))

Theorem: controller-safety (initial-statep (car (train-trace), gate-state) ∧ legal-train-trace (train-trace, time-approaching)) → safety (train-trace, gate-behavior (train-trace, gate-state))

Theorem: controller-utility (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)

;; 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.

Definition: length (x) = if listp (x) then 1 + x

else 0 endif

Definition: get (n, lst) = if n ≃ 0 then car (lst)

else get (n − 1, cdr (lst)) endif

Definition: safety2 (train-trace, gate-trace) ↔ ∀ i (in-gate (get (i, train-trace)) → closed (get (i, gate-trace)))

Theorem: safety2-suff (in-gate (get (i (gate-trace, train-trace), train-trace)) → closed (get (i (gate-trace, train-trace), gate-trace))) → safety2 (train-trace, gate-trace)

Theorem: safety2-necc (¬ (in-gate (get (i, train-trace)) → closed (get (i, gate-trace)))) → (¬ safety2 (train-trace, gate-trace))

Definition: get-induct (i, x, y) = if i ≃ 0 then t

else get-induct (i − 1, cdr (x), cdr (y)) endif Theorem: safety-implies-safety2-get (safety (train-trace, gate-trace) ∧ in-gate (get (i, train-trace))) → closed (get (i, gate-trace))

Theorem: safety-implies-safety2 safety (train-trace, gate-trace) → safety2 (train-trace, gate-trace)

Theorem: controller-safety2 (initial-statep (car (train-trace), gate-state) ∧ legal-train-trace (train-trace, time-approaching)) → safety2 (train-trace, gate-behavior (train-trace, gate-state))

Definition: time-elsewhere (i, found-so-far, train-trace) = if i ≃ 0 then found-so-far

elseif elsewhere (car (train-trace))

then time-elsewhere (i − 1, 1 + found-so-far, cdr (train-trace))

else time-elsewhere (i − 1, 0, cdr (train-trace)) endif

Definition: utility2 (train-trace, gate-trace, n) ↔ ∀ i ((elsewhere (get (i, train-trace))

∧ (gate-opening-max-time

< time-elsewhere (i, n, train-trace))) → open (get (i, gate-trace)))

Theorem: utility2-suff ((elsewhere (get (i-1 (gate-trace, n, train-trace), train-trace)) ∧ (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)

Theorem: utility2-necc (¬ ((elsewhere (get (i, train-trace))

∧ (gate-opening-max-time < time-elsewhere (i, n, train-trace))) → open (get (i, gate-trace))))

→ (¬ utility2 (train-trace, gate-trace, n))

Definition: get-induct2 (i, x, y, n) = if i ≃ 0 then t

else get-induct2 (i − 1, cdr (x), cdr (y), if elsewhere (car (x)) then 1 + n else 0 endif) endif Theorem: utility-implies-utility2-get (utility (train-trace, gate-trace, n) ∧ elsewhere (get (i, train-trace)) ∧ (gate-opening-max-time < time-elsewhere (i, n, train-trace))) → open (get (i, gate-trace))

Theorem: utility-implies-utility2 utility (train-trace, gate-trace, time-elsewhere) → utility2 (train-trace, gate-trace, time-elsewhere)

Theorem: controller-utility2 (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)

Index

approaches-long-enough, 6–8 approaches-long-enough-zero, 7 approaches-stay-long-enough, 7 approaching, 5 approaching-min-time, 6–8

choose-time, 2, 4 choose-time-intro, 2 closed, 3, 8, 10–12 compute-going-down-state, 3, 4 compute-going-up-state, 4 control-output, 7, 9 controller-induction, 9 controller-maintains-safety-and

-utility, 10 controller-safety, 11 controller-safety2, 12 controller-su-invariant, 9 controller-utility, 11 controller-utility2, 13

difference-add1-sub1, 1 distance-to-gate, 6, 8–10 distance-to-gate-first-approachi

ng, 8 ng2, 8

distance-to-gate-induction, 7, 8

elsewhere, 5, 9, 10, 12, 13

forall, 11, 12

gate-behavior, 7, 9–13 gate-closing-max-time, 2, 4, 6, 8 gate-closing-min-time, 2, 4 gate-current-state, 3, 4, 10 gate-next-state, 4, 7, 9 gate-opening-max-time, 2, 4, 8, 10,

12, 13 gate-opening-min-time, 2, 4 gate-parameters-intro, 2 gate-positionp, 3 gate-state-accessors, 3 gate-state-duration, 3, 4, 8 get, 11–13 get-induct, 11 get-induct2, 12 going-down, 3, 8 going-up, 3, 8 good-statep, 8–10

i, 11 i-1, 12 in-gate, 5, 6, 10–12 initial-statep, 10–13

legal-gate-statep, 3, 9, 10 legal-next-positions, 5 legal-train-trace, 6, 9–13 legal-train-trace1, 5, 6 legal-transitionp, 5 length, 11 lessp-sub1-choose-sub1-max, 2

not-lessp-sub1, 1

open, 3, 8, 10, 12, 13

plus-add1, 1

safety, 9–12 safety-implies-safety2, 12 safety-implies-safety2-get, 12 safety2, 11, 12 safety2-necc, 11 safety2-suff, 11 seq-long-enough, 6 su-invariant, 8–10 su-invariant-implies-safety, 10 su-invariant-implies-utility, 10

time-elsewhere, 12, 13 train-constraints, 6 train-positionp, 5 utility, 10, 11, 13 utility-implies-utility2, 13 utility-implies-utility2-get, 13 utility2, 12, 13 utility2-necc, 12 utility2-suff, 12