PVS dump file decision_tables.dmp
To extract the specifications and proofs, download this file to
decision_tables.dmp and from a running PVS type the command
M-x undump-pvs-files
You will be prompted for the dump file name (decision_tables.dmp) and the
directory in which to dump the extracted files.
%Patch files loaded: (patch2-test patch2) version 2.377
$$$tablewise.pvs
tablewise: THEORY
BEGIN
operational_procedures: TYPE = {Takeoff, Climb, Climb_Int_Level, Cruise}
flight_phases: TYPE = {climb, cruise}
Flightphase: VAR flight_phases
AC_Alt, Acc_Alt, Alt_Target, prev_Alt_Target,Cruise_Level: VAR nat
Alt_Capt_Hold: VAR bool
x,y:var nat
GT(x,y):bool = x>y
LT(x,y):bool = x=y
LE(x,y):bool = x<=y
;*(x,y):bool = true
b:var bool
true(b):bool = b
false(b):bool = not b
;*(b):bool = true
decision_table(Flightphase,
AC_Alt,
Acc_Alt,
Alt_Target,
prev_Alt_Target,
Alt_Capt_Hold): operational_procedures =
LET X = (LAMBDA (a: pred[flight_phases]),
(b: pred[bool]),
(c: pred[[nat,nat]]),
(d: pred[bool]),
(e: pred[[nat,nat]]):
a(Flightphase) &
b(AC_Alt > 400) &
c(AC_Alt,Acc_Alt) &
d(Alt_Capt_Hold) &
e(Alt_Target,prev_Alt_Target))
IN TABLE
% Flightphase
% | AC_Alt > 400
% | | cmp(AC_Alt,Acc_Alt)
% | | | Alt_Capt_Hold
% | | | | cmp(Alt_Target,prev_Alt_Target)
% | | | | |
% | | | | | Operational Procedure
%----------|-------|------|-------|-------|------------- ----%
| X(climb? , true , LT , false , * ) | Takeoff ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , true , LT , true , GT) | Takeoff ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , * , GE , false , * ) | Climb ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , * , GE , true , GT) | Climb ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , * , * , true , * ) | Climb_Int_Level ||
%----------|-------|------|-------|-------|------------------%
| X(cruise?, * , GT , true , EQ) | Cruise ||
%----------|-------|------|-------|-------|------------------%
ENDTABLE
decision_table2(Flightphase,
AC_Alt,
Acc_Alt,
Alt_Target,
prev_Alt_Target,
Alt_Capt_Hold): operational_procedures =
LET X = (LAMBDA (a: pred[flight_phases]),
(b: pred[bool]),
(c: pred[[nat,nat]]),
(d: pred[bool]),
(e: pred[[nat,nat]]):
a(Flightphase) &
b(AC_Alt > 400) &
c(AC_Alt,Acc_Alt) &
d(Alt_Capt_Hold) &
e(Alt_Target,prev_Alt_Target))
IN TABLE
% Flightphase
% | AC_Alt > 400
% | | cmp(AC_Alt,Acc_Alt)
% | | | Alt_Capt_Hold
% | | | | cmp(Alt_Target,prev_Alt_Target)
% | | | | |
% | | | | | Operational Procedure
%----------|-------|------|-------|-------|------------- ----%
| X(climb? , true , LT , false , * ) | Takeoff ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , true , LT , true , GT) | Takeoff ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , * , GE , false , * ) | Climb ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , * , GE , true , GT) | Climb ||
%----------|-------|------|-------|-------|------------------%
| X(climb? , false , LT , true , * ) | Climb_Int_Level ||
%----------|-------|------|-------|-------|------------------%
| X(cruise?, * , GT , true , EQ) | Cruise ||
%----------|-------|------|-------|-------|------------------%
| ELSE | Cruise ||
%----------|-------|------|-------|-------|------------------%
ENDTABLE
test: THEOREM AC_Alt=Acc_Alt =>
decision_table2(cruise, AC_Alt, Acc_Alt,
Alt_Target, prev_Alt_Target, Alt_Capt_Hold)
= Cruise
test2: THEOREM AC_Alt=Acc_Alt =>
decision_table2(climb, AC_Alt, Acc_Alt,
Alt_Target, prev_Alt_Target, Alt_Capt_Hold)
= Climb
END tablewise
$$$tablewise.prf
(|tablewise|
(|decision_table_TCC1| "" (GRIND :EXCLUDE ("<" ">" "<=" ">="))
(("1" (HIDE -1 -2 -3 -4 -5) (("1" (POSTPONE) NIL)))
("2" (HIDE -1 -2 -3 -4 -5) (("2" (POSTPONE) NIL)))))
(|decision_table_TCC2| "" (GRIND :EXCLUDE ("<" ">" "<=" ">="))
(("1" (HIDE -1 -2 -3 -4 -5) (("1" (POSTPONE) NIL)))
("2" (HIDE -1 -2 -3 -4 -5) (("2" (POSTPONE) NIL)))
("3" (HIDE -1 -2 -3 -4 -5) (("3" (POSTPONE) NIL)))
("4" (HIDE -1 -2 -3 -4 -5) (("4" (POSTPONE) NIL)))))
(|decision_table2_TCC1| "" (GRIND) NIL) (|test| "" (GRIND) NIL)
(|test2| "" (GRIND) (("" (POSTPONE) NIL))))(|tablewise2|
(|decision_table2_TCC1|
""
(COND-DISJOINT-TCC))
(|decision_table2_TCC2|
""
(COND-COVERAGE-TCC)))