Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vernacstate.mli Sprache: PVS

Original von: PVS^©

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

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.