|
%------------------------------------------------------------------------------
% cd_vertical.pvs
% ACCoRD v1.0
%
% Correctness and completeness of vertical conflict detection algorithm.
% H : Vertical separation
% B : Lookahead time
% T : Lookahead time
%------------------------------------------------------------------------------
cd_vertical[H:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY
BEGIN
IMPORTING vertical[H],
util,
Lookahead[B,T],
reals@min_max
sz,vz,t : VAR real
nzvz : VAR nzreal
eps,dir : VAR Sign
nzt : VAR nzreal
pt : VAR posreal
% Conflict during interval [0,T]
conflict_vertical?(sz,vz) : bool =
EXISTS (t: Lookahead): vertical_los_at?(sz,vz,t)
cd_vertical?(sz,vz) : bool =
(vz = 0 AND abs(sz)<H) OR
(vz /= 0 AND min(max(-H-sign(vz)*sz,B*abs(vz)),T*abs(vz)) < max(min(H-sign(vz)*sz,T*abs(vz)),B*abs(vz)))
cd_vertical_rewrite: LEMMA cd_vertical?(sz,vz) IFF
(vz = 0 AND abs(sz)<H) OR
(vz /= 0 AND min(max(Theta_H(sz,vz,Entry),B),T) < max(min(Theta_H(sz,vz,Exit),T),B))
cd_vertical_correct : THEOREM
cd_vertical?(sz,vz) IMPLIES
conflict_vertical?(sz,vz)
cd_vertical_complete : THEOREM
conflict_vertical?(sz,vz)
IMPLIES
cd_vertical?(sz,vz)
%-----------------------------------------------%
% THEOREM: cd_vertical is correct and complete %
%-----------------------------------------------%
cd_vertical : THEOREM
conflict_vertical?(sz,vz) IFF
cd_vertical?(sz,vz)
conflict_vertical_on_open_interval: LEMMA conflict_vertical?(sz,vz) IFF
EXISTS (topen: Lookahead): B<topen AND topen <T AND vertical_los_at?(sz,vz,topen)
END cd_vertical
¤ Dauer der Verarbeitung: 0.1 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.
|
