PVS dump file autopilot.dmp
To extract the specifications and proofs, download this file to
autopilot.dmp and from a running PVS type the command
M-x undump-pvs-files
You will be prompted for the dump file name (autopilot.dmp) and the
directory in which to dump the extracted files.
%Patch files loaded: (patch2-test patch2) version 2.377
$$$autopilot.pvs
linkedmodes: THEORY
BEGIN
modes: TYPE = {off, armed, on}
combined_modes: TYPE = [# climbmode, levelmode: modes #]
m, n: VAR combined_modes
Coff(m): bool = off?(climbmode(m))
Carm(m): bool = armed?(climbmode(m))
Con(m): bool = on?(climbmode(m))
Loff(m): bool = off?(levelmode(m))
Larm(m): bool = armed?(levelmode(m))
Lon(m): bool = on?(levelmode(m))
monitored_vars: TYPE = [# Cbutton, Lbutton: bool #]
p, q: VAR monitored_vars
null: TYPE
IMPORTING MU@ctlops, scr[monitored_vars, combined_modes, null]
r, s, t: VAR state
Cbutton: condition = LAMBDA p: Cbutton(p)
Lbutton: condition = LAMBDA p: Lbutton(p)
Ctransition(s,t): bool =
LET x: conds2 = (Cbutton, Lbutton),
X = (LAMBDA (a,b:EC): PC(a,b)(x)(vars(s),vars(t)))
IN TABLE climbmode(mode(s))
|off| TABLE
%---------------------------------%
|X( atT, dc) | Carm(t) OR Con(t) ||
%---------------------------------%
|ELSE | Coff(t) ||
%---------------------------------%
ENDTABLE ||
|armed| TABLE
%---------------------------------%
|X( atT, dc) | Coff(t) ||
%---------------------------------%
|ELSE | Carm(t) OR Con(t) ||
%---------------------------------%
ENDTABLE ||
|on| TABLE
%---------------------------------%
|X( atT, dc) | Coff(t) ||
%---------------------------------%
|ELSE | Carm(t) OR Con(t) ||
%---------------------------------%
ENDTABLE ||
ENDTABLE
Ltransition(s, t): bool =
LET x: conds2 = (Cbutton, Lbutton),
X = (LAMBDA (a,b:EC): PC(a,b)(x)(vars(s),vars(t)))
IN TABLE levelmode(mode(s))
|off| TABLE
%---------------------------------%
|X( dc, atT) | Larm(t) OR Lon(t) ||
%---------------------------------%
|ELSE | Loff(t) ||
%---------------------------------%
ENDTABLE ||
|ELSE| TABLE
%---------------------------------%
|X( dc, atT) | Loff(t) ||
%---------------------------------%
|ELSE | Larm(t) OR Lon(t) ||
%---------------------------------%
ENDTABLE ||
ENDTABLE
exclude(s): bool = (Con(s) IFF Lon(s)) AND NOT (Carm(s) AND Larm(s))
req(s,t): bool =
(Ctransition(s,t) OR Ltransition(s,t)) AND exclude(s) AND exclude(t)
init(s): bool = Coff(s) AND Loff(s)
safe1: THEOREM init(s) => AG(req, (LAMBDA t: Con(t) => Lon(t)))(s)
safe2: THEOREM init(s) => AG(req, (LAMBDA t: NOT (Carm(t) & Larm(t))))(s)
live1: THEOREM init(s) => EF(req, (LAMBDA t: Carm(t) & Loff(t)))(s)
live2: THEOREM init(s) => EF(req, (LAMBDA t: Con(t) & Lon(t)))(s)
P: VAR condition
Phase1(s, t): bool =
LET atT = (LAMBDA P: atT(P)(vars(s),vars(t))),
climbmode = (LAMBDA s: climbmode(mode(s))),
levelmode = (LAMBDA s: levelmode(mode(s)))
IN
IF atT(Cbutton) THEN
If Coff(s) THEN Carm(t) ELSE Coff(t) ENDIF
ELSE climbmode(s) = climbmode(t)
ENDIF
OR
IF atT(Lbutton) THEN
If Loff(s) THEN Larm(t) ELSE Loff(t) ENDIF
ELSE levelmode(t) = levelmode(s)
ENDIF
Phase2(s, t): bool =
LET climbmode = (LAMBDA s: climbmode(mode(s))),
levelmode = (LAMBDA s: levelmode(mode(s)))
IN
IF NOT (Coff(s) OR Loff(s)) THEN Con(t) AND Lon(t)
ELSIF Coff(s) AND Lon(s) THEN Coff(t) AND Larm(t)
ELSIF Loff(s) AND Con(s) THEN Loff(t) AND Carm(t)
ELSE climbmode(t) = climbmode(s)
AND levelmode(t) = levelmode(s)
ENDIF
AND Cbutton(t) = Cbutton(s)
AND Lbutton(s) = Lbutton(t)
impl(s, t): bool = (EXISTS r: Phase1(s, r) AND Phase2(r, t))
safe1_i: THEOREM init(s) => AG(impl, (LAMBDA r: Con(r) => Lon(r)))(s)
safe2_i: THEOREM init(s) => AG(impl, (LAMBDA r: NOT (Carm(r) & Larm(r))))(s)
live1_i: THEOREM init(s) => EF(impl, (LAMBDA r: Carm(r) & Loff(r)))(s)
live2_i: THEOREM init(s) => EF(impl, (LAMBDA r: Con(r) & Lon(r)))(s)
A, B: VAR transition_relation
super(A,B)(s:state):bool = AG(B, (LAMBDA t: AX(B, (LAMBDA r: A(t,r)))(t)))(s)
req_impl: LEMMA init(s) => super(req,impl)(s)
impl_req: LEMMA init(s) => super(impl,req)(s)
END linkedmodes
$$$autopilot.prf
(|linkedmodes|
(|safe1| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|safe2| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|live1| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|live2| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|safe1_i| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|safe2_i| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|live1_i| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|live2_i| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|req_impl| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL)))
(|impl_req| "" (AUTO-REWRITE-THEORY "scr" :DEFS T) (("" (MODEL-CHECK) NIL))))
$$$scr.pvs
scr[input,mode,output:type]:THEORY
BEGIN
condition: TYPE = pred[input]
event: TYPE = pred[[input, input]]
event_constructor: TYPE = [condition -> event]
EC: TYPE = event_constructor
p,q: VAR input
P: VAR condition
% define event constructors
atT(P)(p,q): bool = NOT P(p) & P(q) % @T(P)
atF(P)(p,q): bool = P(p) & NOT P(q) % @F(P)
T(P)(p,q): bool = P(p) & P(q)
F(P)(p,q): bool = NOT P(p) & NOT P(q)
dc(P)(p,q): bool = true % don't care
mode_table: TYPE = [mode, input, input -> mode]
state: TYPE = [# mode: mode, vars: input #]
transition_relation: TYPE = pred[[state, state]]
trans(mt: mode_table): transition_relation =
(LAMBDA (s,t:state): mode(t) = mt(mode(s), vars(s), vars(t)))
liftc(c:condition): pred[state] = LAMBDA (s:state): c(vars(s))
CONVERSION liftc
liftm(m: pred[mode]): pred[state] = LAMBDA (s:state): m(mode(s))
CONVERSION liftm
conds1:type = [condition]
conds2:type = [condition, condition]
conds3:type = [condition, condition, condition]
conds4:type = [condition, condition, condition, condition]
conds5:type = [condition, condition, condition, condition, condition]
conds6:type = [condition, condition, condition, condition,
condition, condition]
conds7:type = [condition, condition, condition, condition,
condition, condition, condition]
conds8:type = [condition, condition, condition, condition,
condition, condition, condition, condition]
conds9:type = [condition, condition, condition, condition,
condition, condition, condition, condition, condition]
conds10:type = [condition, condition, condition, condition, condition,
condition, condition, condition, condition, condition]
A,B,C,D,E,FF,G,H,I,J: VAR EC
a,b,c,d,e,f,g,h,i,j: VAR condition
PC(A)(a)(p,q):bool = A(a)(p,q)
PC(A,B)(a,b)(p,q):bool = A(a)(p,q) & B(b)(p,q)
PC(A,B,C)(a,b,c)(p,q):bool = A(a)(p,q) & B(b)(p,q) & C(c)(p,q)
PC(A,B,C,D)(a,b,c,d)(p,q):bool = A(a)(p,q) & B(b)(p,q) & C(c)(p,q) & D(d)(p,q)
PC(A,B,C,D,E)(a,b,c,d,e)(p,q):bool = A(a)(p,q) & B(b)(p,q) & C(c)(p,q) &
D(d)(p,q) & E(e)(p,q)
PC(A,B,C,D,E,FF)(a,b,c,d,e,f)(p,q):bool = A(a)(p,q) & B(b)(p,q) &
C(c)(p,q) & D(d)(p,q) & E(e)(p,q) & FF(f)(p,q)
PC(A,B,C,D,E,FF,G)(a,b,c,d,e,f,g)(p,q):bool = A(a)(p,q) & B(b)(p,q) &
C(c)(p,q) & D(d)(p,q) & E(e)(p,q) & FF(f)(p,q) & G(g)(p,q)
PC(A,B,C,D,E,FF,G,H)(a,b,c,d,e,f,g,h)(p,q):bool = A(a)(p,q) & B(b)(p,q) &
C(c)(p,q) & D(d)(p,q) & E(e)(p,q) & FF(f)(p,q) & G(g)(p,q) & H(h)(p,q)
PC(A,B,C,D,E,FF,G,H,I)(a,b,c,d,e,f,g,h,i)(p,q):bool = A(a)(p,q) & B(b)(p,q) &
C(c)(p,q) & D(d)(p,q) & E(e)(p,q) & FF(f)(p,q) & G(g)(p,q) & H(h)(p,q)
PC(A,B,C,D,E,FF,G,H,I,J)(a,b,c,d,e,f,g,h,i,j)(p,q):bool = A(a)(p,q) &
B(b)(p,q) & C(c)(p,q) & D(d)(p,q) & E(e)(p,q) & FF(f)(p,q) &
G(g)(p,q) & H(h)(p,q)
END scr