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