|
%------------------------------------------------------------------------------
% 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
%%
%% Assumption: abs(sz) >= H
vertical_exit_criterion?(spz,vz) : bool =
vertical_exit?(spz,vz)
vertical_exit_independence: THEOREM
vertical_exit_criterion?(spz,vz) IFF NOT vertical_conflict?(spz,vz)
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.16 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
