|
%------------------------------------------------------------------------------
% 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.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
