PVS dump file cruise.dmp
To extract the specifications and proofs, download this file to
cruise.dmp and from a running PVS type the command
M-x undump-pvs-files
You will be prompted for the dump file name (cruise.dmp) and the
directory in which to dump the extracted files.
%Patch files loaded: (patch2-test patch2) version 2.377
$$$cruise.pvs
cruise: THEORY
BEGIN
lever_pos: TYPE = {activate, deactivate, resume}
engine_state: TYPE = { off, ignition, running }
monitored_vars: TYPE = [#
engine: engine_state,
toofast: bool,
brake: bool,
lever: lever_pos
#]
modes: TYPE = {off,inactive,cruise,override}
null: TYPE
IMPORTING scr[monitored_vars,modes,null]
ignited: condition = LAMBDA (m:monitored_vars):
ignition?(engine(m)) OR running?(engine(m))
running: condition = LAMBDA (m:monitored_vars): running?(engine(m))
brake : condition = LAMBDA (m:monitored_vars): brake(m)
activate: condition = LAMBDA (m:monitored_vars): activate?(lever(m))
deactivate: condition = LAMBDA (m:monitored_vars): deactivate?(lever(m))
resume: condition = LAMBDA (m:monitored_vars): resume?(lever(m))
toofast: condition = LAMBDA (m:monitored_vars): toofast(m)
p: VAR monitored_vars
engine_prop: AXIOM toofast(p) => running(p)
end cruise
cruise_tab: THEORY
BEGIN
IMPORTING cruise
original(s:modes, (p, q:monitored_vars)): modes =
LET
x: conds7 =
(ignited, running, toofast, brake, activate, deactivate, resume),
X = (LAMBDA (a,b,c,d,e,f,g:EC): PC(a,b,c,d,e,f,g)(x)(p,q))
IN TABLE s
|off| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atT, dc, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |off ||
%----|----------------------------------------|------------||
ENDTABLE ||
|inactive| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( T , T , dc, F , atT, dc, dc )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |inactive||
%----|----------------------------------------|------------||
ENDTABLE ||
|cruise| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, atF, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, dc, atT, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, dc , dc , atT, dc, dc, dc )|override||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, dc , dc , dc , dc , atT, dc )|override||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |cruise ||
%----|----------------------------------------|------------||
ENDTABLE ||
|override| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc , atF, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( T, T , dc, F , atT, dc, dc )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( T, T , dc, F , dc, dc, atT )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |override||
% ---|----------------------------------------|------------||
ENDTABLE ||
ENDTABLE
deterministic(s: modes, (p, q: monitored_vars)): modes =
LET
x:conds7 =
(ignited, running, toofast, brake, activate, deactivate, resume),
X = (LAMBDA (a,b,c,d,e,f,g:EC): PC(a,b,c,d,e,f,g)(x)(p,q))
IN TABLE s
|off| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atT, dc, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |off ||
%----|----------------------------------------|------------||
ENDTABLE ||
|inactive| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , dc, F , atT, dc, dc )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |inactive||
%----|----------------------------------------|------------||
ENDTABLE ||
|cruise| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( T , atF, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, dc, atT, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , F , atT, dc, dc, dc )|override||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , F , dc, dc, atT, dc )|override||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |cruise ||
%----|----------------------------------------|------------||
ENDTABLE ||
|override| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( T , atF, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , dc, F , atT, dc, dc )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , dc, F , dc, dc, atT )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |override||
% ---|----------------------------------------|------------||
ENDTABLE ||
ENDTABLE
corrected(s: modes, (p, q: monitored_vars)): modes =
LET
x:conds7 =
(ignited, running, toofast, brake, activate, deactivate, resume),
X = (LAMBDA (a,b,c,d,e,f,g:EC): PC(a,b,c,d,e,f,g)(x)(p,q))
IN TABLE s
|off| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atT, dc, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |off ||
%----|----------------------------------------|------------||
ENDTABLE ||
|inactive| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , F, F , atT, dc, dc )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |inactive||
%----|----------------------------------------|------------||
ENDTABLE ||
|cruise| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( T , atF, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, dc, atT, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , F , atT, dc, dc, dc )|override||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , F , dc, dc, atT, dc )|override||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |cruise ||
%----|----------------------------------------|------------||
ENDTABLE ||
|override| TABLE
%----|----|----|----|----|----|----|----|-----|------------||
|X( atF, dc, dc, dc, dc, dc, dc )|off ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( T , atF, dc, dc, dc, dc, dc )|inactive||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , F, F , atT, dc, dc )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
|X( dc, T , F, F , dc, dc, atT )|cruise ||
%----|----|----|----|----|----|----|----|-----|------------||
| ELSE |override||
% ---|----------------------------------------|------------||
ENDTABLE ||
ENDTABLE
END cruise_tab
cruise_test:THEORY
BEGIN
IMPORTING MU@ctlops, cruise_tab
p,q,r: var state
init(p): bool = off?(p) and not ignited(p)
trans:transition_relation = trans(deterministic)
safe1: THEOREM init(p)
=> AG(trans, (LAMBDA q: off?(q) => NOT ignited(q)))(p)
safe2: THEOREM init(p)
=> AG(trans, (LAMBDA q: NOT off?(q) => ignited(q)))(p)
safe3: THEOREM init(p) % FALSE replace by 6
=> AG(trans, (LAMBDA q: inactive?(q) => ignited(q)
AND NOT (running(q) and activate(q))))(p)
safe4: THEOREM init(p) % FALSE
=> AG(trans, (LAMBDA q: cruise?(q) =>
ignited(q) & running(q) & NOT toofast(q) & NOT brake(q)
& NOT deactivate(q)))(p)
safe5: THEOREM init(p)
=> AG(trans, (LAMBDA q: override?(q) => ignited(q) AND running(q)))(p)
safe6: THEOREM init(p)
=> AG(trans, (LAMBDA q: inactive?(q) & ignited(q) & running(q)
& NOT toofast(q) & NOT brake(q) & NOT activate(q))
IMPLIES NOT EX(trans, (LAMBDA r: inactive?(r) & ignited(r) &
running(r) & NOT toofast(r) & NOT
brake(r) & activate(r))))(p)
END cruise_test
cruise_test2:THEORY
BEGIN
IMPORTING MU@ctlops, cruise_tab
p,q,r: var state
init(p): bool = off?(p) and not ignited(p)
trans:transition_relation = trans(corrected)
safe1: THEOREM init(p)
=> AG(trans, (LAMBDA q: off?(q) => NOT ignited(q)))(p)
safe2: THEOREM init(p)
=> AG(trans, (LAMBDA q: NOT off?(q) => ignited(q)))(p)
safe3: THEOREM init(p) % FALSE replace by 6
=> AG(trans, (LAMBDA q: inactive?(q) => ignited(q)
AND NOT (running(q) and activate(q))))(p)
safe4: THEOREM init(p)
=> AG(trans, (LAMBDA q: cruise?(q) =>
ignited(q) & running(q) & NOT toofast(q) & NOT brake(q)
& NOT deactivate(q)))(p)
safe5: THEOREM init(p)
=> AG(trans, (LAMBDA q: override?(q) => ignited(q) AND running(q)))(p)
safe6: THEOREM init(p)
=> AG(trans, (LAMBDA q: inactive?(q) & ignited(q) & running(q)
& NOT toofast(q) & NOT brake(q) & NOT activate(q))
IMPLIES NOT EX(trans, (LAMBDA r: inactive?(r) & ignited(r) &
running(r) & NOT toofast(r) & NOT
brake(r) & activate(r))))(p)
END cruise_test2
$$$cruise.prf
(|cruise|)(|cruise_tab| (|original_TCC1| "" (COND-DISJOINT-TCC) NIL)
(|original_TCC2| "" (COND-DISJOINT-TCC)
(("1" (POSTPONE) NIL) ("2" (POSTPONE) NIL) ("3" (POSTPONE) NIL)
("4" (POSTPONE) NIL) ("5" (POSTPONE) NIL) ("6" (POSTPONE) NIL)
("7" (POSTPONE) NIL) ("8" (POSTPONE) NIL)))
(|original_TCC3| "" (GRIND) (("" (POSTPONE) NIL)))
(|deterministic_TCC1| "" (GRIND)
(("" (LEMMA "engine_prop") (("" (GRIND :IF-MATCH ALL) NIL)))))
(|deterministic_TCC2| "" (GRIND)
(("1" (LEMMA "engine_prop") (("1" (GRIND :IF-MATCH ALL) NIL)))
("2" (LEMMA "engine_prop") (("2" (GRIND :IF-MATCH ALL) NIL)))
("3" (LEMMA "engine_prop") (("3" (GRIND :IF-MATCH ALL) NIL)))))
(|deterministic_TCC3| "" (GRIND)
(("1" (LEMMA "engine_prop") (("1" (GRIND :IF-MATCH ALL) NIL)))
("2" (LEMMA "engine_prop") (("2" (GRIND :IF-MATCH ALL) NIL)))
("3" (LEMMA "engine_prop") (("3" (GRIND :IF-MATCH ALL) NIL)))))
(|corrected_TCC1| "" (GRIND)
(("" (LEMMA "engine_prop") (("" (GRIND :IF-MATCH ALL) NIL)))))
(|corrected_TCC2| "" (GRIND)
(("1" (LEMMA "engine_prop") (("1" (GRIND :IF-MATCH ALL) NIL)))
("2" (LEMMA "engine_prop") (("2" (GRIND :IF-MATCH ALL) NIL)))
("3" (LEMMA "engine_prop") (("3" (GRIND :IF-MATCH ALL) NIL))))))(|cruise_test|
(|safe1|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test")
((""
(MODEL-CHECK)
NIL)))
(|safe2|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test")
((""
(MODEL-CHECK)
NIL)))
(|safe3|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test")
((""
(MODEL-CHECK)
((""
(POSTPONE)
NIL)))))
(|safe4|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test")
((""
(MODEL-CHECK)
NIL)))
(|safe5|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test")
((""
(MODEL-CHECK)
NIL)))
(|safe6|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test")
((""
(MODEL-CHECK)
NIL))))(|cruise_test2|
(|safe1|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test2")
((""
(MODEL-CHECK)
NIL)))
(|safe2|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test2")
((""
(MODEL-CHECK)
NIL)))
(|safe3|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test2")
((""
(MODEL-CHECK)
NIL)))
(|safe4|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test2")
((""
(MODEL-CHECK)
NIL)))
(|safe5|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test2")
((""
(MODEL-CHECK)
NIL)))
(|safe6|
""
(AUTO-REWRITE-THEORIES
("scr"
:DEFS
T)
"cruise_tab"
"cruise"
"cruise_test2")
((""
(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