Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: vs_only.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.