|
%------------------------------------------------------------------------------
% horizontal_criterion_line.pvs
% ACCoRD v1.0
%
% This theory simplifies the predicate horizontal_criterion and proves
% a stronger coordination theorem.
%------------------------------------------------------------------------------
horizontal_criterion_line[D: posreal]: THEORY
BEGIN
IMPORTING horizontal_criteria[D],
tangent_line[D],
vectors@linear_transformations_2D
v,nv,nv1,nv2 : VAR Vect2
sp : VAR Sp_vect2
vo,vi,
nvo,nvi : VAR Vect2
eps : VAR Sign
horizontal_criterion_rewrite: THEOREM
horizontal_criterion?(sp,eps)(v) IFF
(eps*det(v,tangent_line(sp,eps)) <= 0 AND
eps*det(sp,v)<=0)
% horizontal_criterion_rewrite2: THEOREM
% norm(sp)>D IMPLIES
% (horizontal_criterion?(sp,eps)(v) IFF
% eps*det(sp,v) >= norm(v)*D)
horizontal_criterion_special_coordination: LEMMA
horizontal_criterion?(-sp,eps)(nvi-vo) AND
horizontal_criterion?(sp,eps)(nvo-vo)
IMPLIES
NOT horizontal_conflict?(sp,nvo-nvi)
horizontal_criterion_dot_equality: LEMMA
line_solution?(sp,nvo-vi,eps) AND
line_solution?(sp,v,eps) IMPLIES
det(vi-nvi,v) = det(nvo-nvi,v)
horizontal_criterion_line_invariance: LEMMA
line_solution?(sp,nvo-vi,eps) IMPLIES
(horizontal_criterion?(sp,eps)(vi-nvi) IMPLIES
horizontal_criterion?(sp,eps)(nvo-nvi))
horizontal_criterion_line_coordination: LEMMA
line_solution?(-sp,nvi-vo,eps) AND
horizontal_criterion?(sp,eps)(nvo-vo)
IMPLIES
NOT horizontal_conflict?(sp,nvo-nvi)
% The horizontal criterion is maximal!
SCRIT: VAR SignedCrit2D
% horizontal_criterion_maximal: LEMMA
% LET
% conflictpred = (LAMBDA (ss,v:Vect2): (LAMBDA (nv:Vect2): horizontal_conflict?(ss,nv)))
% IN
% (FORALL (sp:Sp_vect2,v:Vect2,eps:Sign):
% subset?(horizontal_criterion?(sp,eps),SCRIT(eps)(sp,v)) AND
% crit_symmetric_2D?(SCRIT(eps)) AND
% crit_independent_of_length_2D?(SCRIT(eps)) AND
% coordinated_2D?(SCRIT(eps),SCRIT(eps),conflictpred))
% IMPLIES
% (FORALL (sp:Sp_vect2,v:Vect2,eps:Sign):
% horizontal_conflict?(sp,v) IMPLIES horizontal_criterion?(sp,eps)=SCRIT(eps)(sp,v))
% The horizontal criterion is not coordinated if the
% aircraft are not orginally in conflict. The following criteria,
% which depends on s (original relative position),
% v (original relative velocity), nv (new relative velocity), and eps (+-1),
% is coordinated even if the aircraft are not originally in conflict.
% In fact, if the original aircraft are in conflict, then this criteria is
% equal to the horizontal_criterion. An even stronger result is true which
% states that as long as the original trajectory does not
% satisfy horizontal_criterion, this new criterion is equal to
% the horizontal criterion.
horizontal_criterion_ext?(sp,v,eps)(nv): bool =
IF horizontal_criterion?(sp,eps)(v)
THEN horizontal_criterion?(sp,eps)(nv-(1/2)*v)
ELSIF
horizontal_criterion?(sp,eps)(-v) OR
(NOT horizontal_criterion?(sp,-eps)(v))
THEN horizontal_criterion?(sp,eps)(nv)
ELSE
horizontal_criterion?(sp,eps)(nv) AND
horizontal_criterion?(sp,eps)(nv-(1/2)*v)
ENDIF
horizontal_criterion_ext_subset: LEMMA
horizontal_criterion_ext?(sp,v,eps)(nv) IMPLIES
horizontal_criterion?(sp,eps)(nv)
horizontal_criterion_ext_restrict: LEMMA
horizontal_conflict?(sp,v) IMPLIES
(horizontal_criterion_ext?(sp,v,eps)(nv) IFF
horizontal_criterion?(sp,eps)(nv))
horizontal_criterion_ext_restrict_conflict: LEMMA
horizontal_conflict?(sp,v) IMPLIES
(horizontal_criterion_ext?(sp,v,eps)(nv) IFF
horizontal_criterion?(sp,eps)(nv))
horizontal_criterion_ext_independence: LEMMA
horizontal_criterion_ext?(sp,v,eps)(nv) IMPLIES
NOT horizontal_conflict?(sp,nv)
% horizontal_criterion_ext_coordinated_criterion: LEMMA
% horizontal_criterion_ext?(sp,vo-vi,eps)(nvo-vi) AND
% horizontal_criterion_ext?(-sp,vi-vo,eps)(nvi-vo)
% IMPLIES
% horizontal_criterion?(sp,eps)(nvo-nvi)
horizontal_criterion_ext_coordinated: LEMMA
horizontal_criterion_ext?(sp,vo-vi,eps)(nvo-vi) AND
horizontal_criterion_ext?(-sp,vi-vo,eps)(nvi-vo)
IMPLIES
NOT horizontal_conflict?(sp,nvo-nvi)
%%%%%%%%%%%%%%%%%%%%%%%%%%%
horizontal_criterion_ext_sum_closed: LEMMA
horizontal_criterion_ext?(sp,v,eps)(nv1) AND
horizontal_criterion_ext?(sp,v,eps)(nv2)
IMPLIES
horizontal_criterion_ext?(sp,v,eps)(nv1+nv2)
horizontal_criterion_ext_scal: LEMMA
FORALL (c:real): c>=1 AND
horizontal_criterion_ext?(sp,v,eps)(nv)
IMPLIES
horizontal_criterion_ext?(sp,v,eps)(c*nv)
horizontal_criterion_ext_seg_convex: LEMMA
FORALL (eps: Sign, sp: Sp_vect2[D], v, nv1, nv2: Vect2):
horizontal_criterion_ext?(sp, v, eps)(nv1) AND
horizontal_criterion_ext?(sp, v, eps)(nv2)
IMPLIES
(FORALL (t: real):
0 <= t AND t <= 1 IMPLIES
horizontal_criterion_ext?(sp,v,eps)((1-t)*nv1 + t *nv2))
% In next lemma, sp1 = rel position at time t1,
% sp2 = rel position at time t2
horizontal_criterion_ext_seg_independence: LEMMA
FORALL (sp1,sp2:Vect2,t1,t2:real): t1<t2 AND
horizontal_criterion_ext?(sp,v,eps)(sp1-sp) AND
horizontal_criterion_ext?(sp,v,eps)(sp2-sp) IMPLIES
FORALL (t:real): t1 <= t AND t <= t2
IMPLIES NOT horizontal_los?(sp1 + ((t-t1)/(t2-t1))*(sp2-sp1))
% IMPORANT NOTE: nso - so = (nso-si) - (so-si)
% nsi - si = (nsi-so) - (si-so)
horizontal_criterion_ext_seg_coordination: LEMMA
FORALL (so,si,vo,vi,nso1,nso2,nsi1,nsi2:Vect2,t1,t2:real):
t1<t2 AND sqv(so-si) >= sq(D) AND
horizontal_criterion_ext?(so-si,vo-vi,eps)(nso1-so) AND
horizontal_criterion_ext?(so-si,vo-vi,eps)(nso2-so) AND
horizontal_criterion_ext?(si-so,vi-vo,eps)(nsi1-si) AND
horizontal_criterion_ext?(si-so,vi-vo,eps)(nsi2-si) IMPLIES
FORALL (t:real):
LET time01 = (t-t1)/(t2-t1),
ownshippos = nso1 + time01*(nso2-nso1),
intruderpos = nsi1 + time01*(nsi2-nsi1)
IN
t1 <= t AND t <= t2 IMPLIES NOT horizontal_los?(ownshippos-intruderpos)
END horizontal_criterion_line
¤ Dauer der Verarbeitung: 0.16 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.
|
