Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: cd3d.pvs   Sprache: PVS

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

¤ 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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik