Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: graph_from_edges.prf Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% circle_criterion.pvs
% ACCoRD v1.0
%
%------------------------------------------------------------------------------

circle_criterion[D,H: posreal]: THEORY
BEGIN

  IMPORTING space_3D[D,H],
            horizontal_criteria[D],
            vz_criteria[H]

  spz     : VAR Spz_vect3   % Vertically separated
  vzgs    : VAR Zv2_vect3   % Ground speed is zero
  s,v     : VAR Vect3
  eps,dir : VAR Sign
  t       : VAR real

  %% Vertical separation
  vertical_sep_independence : THEOREM
    vertical_exit?(spz`z,v`z)
    IMPLIES
      NOT conflict?(spz,v)

  %% Ground speed is 0

  nogs_criterion?(s,vzgs): bool =
    vertical_sep?(s`z) AND vertical_exit?(s`z,vzgs`z) OR
    horizontal_sep?(s)

  nogs_criterion_independence : THEOREM
    nogs_criterion?(s,vzgs) IFF NOT conflict?(s,vzgs)

  %% Aircarft are separated
  circle_criterion?(s,v,dir): bool =
    horizontal_sep?(s) AND
    vertical_sep?(s`z) AND
    horizontal_dir?(s,v,dir) AND
    vertical_dir?(s`z,v`z,-dir)

  circle_criterion_at?(s,v,t,dir): MACRO bool =
    circle_criterion?(s+t*v,v,dir)

  circle_criterion_independence : THEOREM
    circle_criterion?(s,v,dir) IMPLIES
      NOT conflict_ever?(s,v)

  circle_criterion_at_independence: THEOREM
    circle_criterion_at?(s,v,t,dir)
    IMPLIES
      NOT conflict_ever?(s,v)

END circle_criterion

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.