Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 6 kB

Quelle horizontal_criterion_line.pvs Sprache: PVS

%------------------------------------------------------------------------------
% 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

quality97%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.