%------------------------------------------------------------------------------ % vz_criteria.pvs % ACCoRD v1.0 % % This theory proposes a criterion for vertical separation for non-negative % times. %------------------------------------------------------------------------------
vz_criteria[H: posreal]: THEORY BEGIN
IMPORTING vertical[H]
spz : VAR Spz
sz,vz,nvz,
voiz,vioz,
t : VAR real
nnt : VAR nnreal
dir : VAR Sign
vertical_exit_coordination: THEOREM
vertical_conflict?(spz,vz) AND
vertical_exit_criterion?(spz,voiz) AND
vertical_exit_criterion?(-spz,vioz) IMPLIES
vertical_exit_criterion?(spz,voiz-vioz-vz)
%% The following lemma assumes vertical separation at a given time in the %% future and gives sufficient conditions over a new vertical velocity %% that also yields vertical separation at that time.
vertical_sep_dir_at : LEMMA LET signsz = sign(sz+nnt*vz) IN
vertical_sep?(sz+nnt*vz) AND
vertical_dir?(sz+nnt*vz,vz,dir) AND
(dir = Entry IMPLIES signsz*nvz <= 0) AND
signsz*nvz >= signsz*vz IMPLIES
vertical_sep?(sz+nnt*nvz) AND
vertical_dir?(sz+nnt*nvz,nvz,dir)
END vz_criteria
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
