Quelle cd3d.pvs Sprache: PVS

%------------------------------------------------------------------------------
% cd3d.pvs
% ACCoRD v1.0
%
% Correctness and completeness of 3-D conflict detection algorithm.
%   D : Horizontal separation
%   H : Vertical separation
%   T : Lookahead time
%------------------------------------------------------------------------------

cd3d[D,H:posreal,B:nnreal,T: {AB: posreal|AB>B}]  : THEORY
BEGIN

  IMPORTING circle_criterion[D,H],
       cd_vertical,
            omega_2D,
     util

  s,v : VAR Vect3
  t   : VAR Lookahead[B,T]

  % Conflict during interval [0,T]
  conflict_3D?(s,v) : bool =
    EXISTS (t: Lookahead[B,T]): conflict_at?(s,v,t)

  conflict_3D_2D_stable: LEMMA v`z/=0 AND max(-H-sign(v`z)*s`z,B*abs(v`z)) < min(H-sign(v`z)*s`z,T*abs(v`z))
    IMPLIES
    (conflict_3D?(s,v) IFF
    conflict_2D?[D*abs(v`z),max(-H-sign(v`z)*s`z,B*abs(v`z)),min(H-sign(v`z)*s`z,T*abs(v`z))](abs(v`z)*s,v))

  conflict_3D_vz_swap: LEMMA conflict_3D?(s,v) IFF conflict_3D?(s WITH [z:=-(s`z)],v WITH [z:=-(v`z)])

  conflict_3D_on_open_interval: LEMMA conflict_3D?(s,v) IFF
    EXISTS (topen: Lookahead[B,T]): B<topen AND topen <T AND sqv(vect2(s)+topen*vect2(v))<sq(D) AND abs(s`z + topen*v`z) < H

  conflict_3D_vertical: LEMMA vect2(v) /= zero AND Delta(s,v) >= 0 AND max(Theta_D(s,v,Entry),B) < min(Theta_D(s,v,Exit),T)
    IMPLIES
    (conflict_3D?(s,v) IFF
    conflict_vertical?[H,max(Theta_D(s,v,Entry),B),min(Theta_D(s,v,Exit),T)](s`z,v`z))

  %-----------------------------------------------%
  % 3-D Conflict interval detection [tin,tout]    %
  %     (tin,tout) is the conflict interval       %
  %-----------------------------------------------%

  detection(s,v) : [Lookahead[B,T],Lookahead[B,T]] =
    IF zero_vect2?(v) AND horizontal_los?(s) THEN
      IF v`z /= 0 THEN
        (min(max(Theta_H(s`z,v`z,Entry),B),T),max(min(Theta_H(s`z,v`z,Exit),T),B))
      ELSIF vertical_los?(s`z) THEN
        (B,T)
      ELSE
        (B,B)
      ENDIF
    ELSIF Delta(s,v) > 0 THEN
      LET td1 = Theta_D(s,v,Entry),
          td2 = Theta_D(s,v,Exit) IN
      IF v`z /= 0 THEN
        LET tin  = max(td1,Theta_H(s`z,v`z,Entry)),
            tout = min(td2,Theta_H(s`z,v`z,Exit)) IN
        (min(max(tin,B),T),max(min(tout,T),B))
      ELSIF vertical_los?(s`z) THEN
        (min(max(td1,B),T),max(min(td2,T),B))
      ELSE
        (B,B)
      ENDIF
    ELSE
      (B,B)
    ENDIF

  detection_correct : THEOREM
    LET (tin,tout) = detection(s,v) IN
     tin < t AND t < tout IMPLIES conflict_at?(s,v,t)

  detection_complete : THEOREM
    LET (tin,tout) = detection(s,v) IN
      conflict_at?(s,v,t) IMPLIES tin <= t AND t <= tout AND tin < tout

  conflict_detection : THEOREM
    LET (tin,tout) = detection(s,v) IN
    conflict_3D?(s,v) IFF tin < tout

  %-----------------------------------------------%
  % 3-D Conflict Detection (cd3d)                 %
  %-----------------------------------------------%

  cd3d?(s,v) : bool =
    IF v`z = 0 AND abs(s`z)<H
       THEN cd2d?[D,B,T](s,v)
    ELSIF v`z /= 0 AND max(-H-sign(v`z)*s`z,B*abs(v`z)) < min(H-sign(v`z)*s`z,T*abs(v`z))
       THEN cd2d?[D*abs(v`z),max(-H-sign(v`z)*s`z,B*abs(v`z)),min(H-sign(v`z)*s`z,T*abs(v`z))](abs(v`z)*s,v)
    ELSE
       FALSE
    ENDIF

  cd3d_rewrite: LEMMA cd3d?(s,v) IFF
    IF v`z = 0 AND abs(s`z)<H
       THEN cd2d?[D,B,T](s,v)
    ELSIF v`z /= 0 AND max(Theta_H(s`z,v`z,Entry),B) < min(Theta_H(s`z,v`z,Exit),T)
       THEN cd2d?[D,max(Theta_H(s`z,v`z,Entry),B),min(Theta_H(s`z,v`z,Exit),T)](s,v)
    ELSE
       FALSE
    ENDIF

  cd3d_test: LEMMA
        FORALL (nvo,vi:Vect3):
        D = 10000.8 AND
      H = 283.464 AND
      B = 0 AND
      T = 300 AND
      s = (0,110733.65,0) AND
      nvo = (0,-236.48,0) AND
      vi = (0,236.48,0)
      IMPLIES cd3d?(s,nvo-vi)

  cd3d_correct : THEOREM
    cd3d?(s,v) IMPLIES
    conflict_3D?(s,v)

  cd3d_complete : THEOREM
    conflict_3D?(s,v)
    IMPLIES
    cd3d?(s,v)

  %-----------------------------------------------%
  % THEOREM: cd3d is correct and complete         %
  %-----------------------------------------------%

  cd3d : THEOREM
    conflict_3D?(s,v) IFF
    cd3d?(s,v)

  %-----------------------------------------------%
  % Additional Lemmas on conflict_3D              %
  %-----------------------------------------------%

  % Rewriting cd3d in terms of cd_vertical - the vertical conflict probe

  cd3d_rewrite_vertical: LEMMA cd3d?(s,v) IFF
    (vect2(v) = zero AND sqv(vect2(s)) < sq(D) AND cd_vertical?[H,B,T](s`z,v`z))
    OR
    (Delta(s,v)>0 AND max(Theta_D(s,v,Entry),B) < min(Theta_D(s,v,Exit),T) AND
    cd_vertical?[H,max(Theta_D(s,v,Entry),B),min(Theta_D(s,v,Exit),T)](s`z,v`z))

  % ----------------------------------------------%

  vertical_solution_not_conflict_3D : LEMMA
    vertical_solution?(s`z,v`z,T,Entry) IMPLIES
    NOT conflict_3D?(s,v)

  conflict_3D_horizontal_conflict : LEMMA
    conflict_3D?(s,v) IMPLIES
      horizontal_conflict?(s,v)

  conflict_3D_vertical_conflict : LEMMA
    conflict_3D?(s,v) IMPLIES
      vertical_conflict?(s`z,v`z)

  circle_solution_2D_not_conflict_3D: LEMMA
    circle_solution_2D?(s,v,T,Entry) IMPLIES
    NOT conflict_3D?(s,v)

END cd3d

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.