%------------------------------------------------------------------------------ % 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_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
[ Verzeichnis aufwärts0.6unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
