|
%------------------------------------------------------------------------------
% cd2d_inf.pvs
% ACCoRD v1.0
%
% Correctness and completeness of 2-D conflict detection algorithm for infinite
% lookahead time
% D : Horizontal separation
%------------------------------------------------------------------------------
cd2d_inf[D:posreal] : THEORY
BEGIN
IMPORTING horizontal[D],
vect_analysis@vect_cont_2D,
vect_analysis@vect2_cont_dot[real],
vectors@det_2D,
tangent_line[D]
s,v : VAR Vect2
sp : VAR Sp_vect2
ss : VAR Ss_vect2
nzv : VAR Nz_vect2
t : VAR nnreal
detection_2D_inf(s,nzv) : [nnreal,nnreal] =
IF Delta(s,nzv) > 0 THEN
LET tin = Theta_D(s,nzv,Entry),
tout = Theta_D(s,nzv,Exit) IN
(max(tin,0),max(tout,0))
ELSE
(0,0)
ENDIF
detection_2D_inf_correct : THEOREM
LET (tin,tout) = detection_2D_inf(s,nzv) IN
tin < t AND t < tout IMPLIES horizontal_los?(s+t*nzv)
detection_2D_inf_complete : THEOREM
LET (tin,tout) = detection_2D_inf(s,nzv) IN
horizontal_los?(s+t*nzv) IMPLIES tin <= t AND t <= tout AND tin < tout
conflict_detection_2D_inf : THEOREM
LET (tin,tout) = detection_2D_inf(s,nzv) IN
horizontal_conflict?(s,nzv) IFF tin < tout
%-----------------------------------------------%
% 2-D Conflict Detection (cd2d_inf) %
%-----------------------------------------------%
cd2d_inf?(s,v) : bool =
horizontal_los?(s) OR
(Delta(s,v) > 0 AND s*v < 0)
%-----------------------------------------------%
% THEOREM: cd2d_inf is correct and complete %
%-----------------------------------------------%
cd2d_inf : THEOREM
horizontal_conflict?(s,v)
IFF
cd2d_inf?(s,v)
END cd2d_inf
¤ Dauer der Verarbeitung: 0.14 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.
|
