Quelle  vs_only.pvs

%------------------------------------------------------------------------------
% vs_only.pvs
% ACCoRD v1.0
%
% This theory proposes criteria for vertical only resolutions. Circle solutions 
% solve the following equation on vz:
%
%   sz+t*vz = eps*H,
%   
% where t = Theta_D(s,v,epsp), and eps determines the bottom
%   eps =  1: top circle
%   eps = -1: bottom circle
%------------------------------------------------------------------------------

vs_only[D,H: posreal] : THEORY
BEGIN

  IMPORTING circle_criterion[D,H]

  ss         : VAR Ss2_vect3    % Horizontally separated
  vgs        : VAR Nzv2_vect3   % Ground speed is non-zero 
  s,v        : VAR Vect3
  eps        : VAR Sign
  nnt        : VAR nnreal
  t,vz       : VAR real
  v2         : VAR Vect2

  %------------%
  % ALGORITHMS %
  %------------%

  % If first projection is true, the second projection is a relative vertical 
  % only resolution maneuver.

  vs_only(s,v2,t,eps) : [bool,real] =
    IF eps*s`z < H AND strict_horizontal_sep?(s) AND Delta(s,v2) > 0 THEN  
      (true,vs_at(s`z,Theta_D(s,v2,Entry),eps))
    ELSIF eps*s`z >= H AND t > 0 THEN
      (true,vs_at(s`z,t,eps))
    ELSE
      (false,0)
    ENDIF

  %------------%
  % LEMMAS     %
  %------------%

  circle_vs_only_ge : LEMMA
    LET signsz = sign(s`z+nnt*vz) IN
    circle_criterion_at?(s,v WITH [z := vz],nnt,eps) AND
    (eps = Exit IMPLIES signsz*v`z <= 0) AND
    signsz*v`z >= signsz*vz
    IMPLIES
      circle_criterion_at?(s,v,nnt,eps)

  vs_entry_meets_circle_criterion : LEMMA
     horizontal_conflict?(ss,vgs) AND
     eps*ss`z < H AND
     eps*vgs`z >= eps*vs_at(ss`z,Theta_D(ss,vgs,Entry),eps)
     IMPLIES
       circle_criterion_at?(ss,vgs,Theta_D(ss,vgs,Entry),Entry)

  vs_exit_meets_circle_criterion : LEMMA
    eps*s`z >= H AND
    horizontal_conflict?(s,vgs) AND
    vgs`z = vs_at(s`z,Theta_D(s,vgs,Exit),eps)
    IMPLIES
      circle_criterion_at?(s,vgs,Theta_D(s,vgs,Exit),Exit)

END vs_only