Quelle  cd2d_inf.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% 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