Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% horizontal_los_criterion.pvs
%
% Criterion for horizontal recovery of Loss of Separation.
% The criterion is based on the fact that s*v > 0 implies that v diverges
% from the origin of the coordinate system.
%
% This criteria is no longer used in Chorus. This criteria ensures divergence.
% In the code, we are now using repulsive criteria instead. See repulsive.pvs.
%------------------------------------------------------------------------------

old_horiz_los_criterion : THEORY
BEGIN

  IMPORTING definitions,
       predicate_coordination_2D

  s,
  v,vo,vi,
  nvo,nvi,
  w,nv,nw    : VAR Vect2
  T,T1,T2,
  Tmax,Tmin  : VAR posreal
  MinRelSpeed,
  MinRelSpeedo,
  MinRelSpeedi: VAR nnreal
  eps : VAR Sign

  horizontal_los_crit?(s,MinRelSpeed,eps)(v): bool =
      s*v>=0 AND
      eps*det(s,v)<=0 AND
      norm(v)>=MinRelSpeed

  horizontal_los_crit_symm: LEMMA
      horizontal_los_crit?(s,MinRelSpeed,eps)(v) IFF
      horizontal_los_crit?(-s,MinRelSpeed,eps)(-v)

  horizontal_los_crit_independent: LEMMA
      nvo-vi /= zero AND
      horizontal_los_crit?(s,MinRelSpeed,eps)(nvo-vi) IMPLIES
      divergent?(s,nvo-vi) AND
      eps*det(s,nvo-vi)<=0 AND
      norm(nvo-vi)>=MinRelSpeed

  horizontal_los_crit_coordinated: LEMMA
      horizontal_los_crit?(s,MinRelSpeedo,eps)(nvo-vi) AND
      horizontal_los_crit?(-s,MinRelSpeedi,eps)(nvi-vo) AND
      s*(vo-vi)<0 IMPLIES
      divergent?(s,nvo-nvi)

END old_horiz_los_criterion

¤ Dauer der Verarbeitung: 0.18 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.