|
%------------------------------------------------------------------------------
% opt_vertical.pvs
% ACCoRD v.1.0
%------------------------------------------------------------------------------
opt_vertical[D,H:posreal] : THEORY
BEGIN
IMPORTING opt_trk_gs[D],
vertical_criterion[D,H]
s,nvo : VAR Vect3
sp : VAR Sp2_vect3
vo,vi : VAR Nzv2_vect3
epsh,epsv : VAR Sign
opt_vertical(s,vo,vi,epsh,epsv): {nvo | nz_vect2?(nvo) =>
horizontal_only?(vo)(nvo)} =
IF vo`z = vi`z THEN zero
ELSE
LET v = vo-vi,
dir:Sign = IF abs(s`z) >= H THEN epsv*sign(s`z) ELSE Entry ENDIF,
t = Theta_H(s`z,v`z,-dir) IN
IF t > 0 AND epsv = sign(s`z + t*v`z) THEN
LET nvo2 = opt_trk_gs_vertical(s,vo,vi,t,dir) IN
IF horizontal_los?(s) OR horizontal_criterion?(s,epsh)(nvo2-vo) THEN
nvo2 WITH [z |-> vo`z]
ELSE
zero
ENDIF
ELSE
zero
ENDIF
ENDIF
opt_vertical?(s,vo,vi,epsh,epsv)(nvo) : bool =
nz_vect2?(nvo) AND
nvo = opt_vertical(s,vo,vi,epsh,epsv)
%------------%
% LEMMAS %
%------------%
opt_vertical_meets_horizontal_criterion : THEOREM
opt_vertical?(sp,vo,vi,epsh,epsv)(nvo) IMPLIES
horizontal_criterion?(sp,epsh)(nvo-vo)
opt_vertical_meets_vertical_criterion : THEOREM
opt_vertical?(s,vo,vi,epsh,epsv)(nvo) IMPLIES
vertical_criterion?(epsv)(s,vo-vi)(nvo-vi)
END opt_vertical
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
