Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: line_solutions.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% line_solutions.pvs
% ACCoRD v1.0
%
% Line solutions are a special case of horizontal solutions. They are
% are tangent to the protected zone. In this case, eps determines the
% side of the protected zone that the is touched.
% It is proven that line solutions satisfy independence and (implicit)
% coordination.
%------------------------------------------------------------------------------

line_solutions[D: posreal]: THEORY
BEGIN

  IMPORTING horizontal_criteria[D],
           vectors@linear_transformations_2D

  sp,s2         : VAR Sp_vect2
  s,v,v1,v2,v3,
  vo,vi,nvo,nvi : VAR Vect2
  eps,eps1,eps2 : VAR Sign
  t,t2,t3    : VAR real
  nzv,nzv1,nzv2 : VAR Nz_vect2
  k             : VAR real
  pk            : VAR posreal
  tt  : VAR nnreal

  line_solution?(sp,v,eps):bool =
      R(sp)*eps*det(sp,v) = sp*v AND eps*det(sp,v) <= 0

  line_solution_dot_neg : LEMMA
    line_solution?(sp,v,eps) IMPLIES
    sp*v <= 0

  line_solution_sep_dot_negative: LEMMA
    sqv(sp) > sq(D) AND v /= zero AND
    line_solution?(sp,v,eps) IMPLIES
    sp*v < 0

  line_solution?(sp,v) : MACRO bool =
     EXISTS (eps: Sign): line_solution?(sp,v,eps)

  line_solution_on_D: LEMMA
    on_D?(s) IMPLIES
    line_solution?(s,eps*perpR(s),eps)

  on_D_line : LEMMA
    on_D?(s) AND s*v = 0 IMPLIES line_solution?(s,v)

  line_solution_scal : LEMMA
    line_solution?(sp,v,eps) IFF line_solution?(sp,pk*v,eps)

  line_solution_zero_eps : LEMMA
    line_solution?(sp,zero,eps)

  line_solution_zero : LEMMA
    line_solution?(sp,zero)

  line_solution_Delta: LEMMA
    line_solution?(sp,v) IFF Delta(sp,v) = 0 AND horizontal_entry?(sp,v)

  det_neq_0 : LEMMA
    line_solution?(sp,nzv) IMPLIES
    det(sp,nzv) /= 0

  eps_line(s,v): Sign = -sign(det(s,v))

  line_solution_eps : LEMMA
    line_solution?(sp,nzv,eps) IMPLIES
    eps = eps_line(sp,nzv)

  line_solution_eps_line : LEMMA
    line_solution?(sp,v) IMPLIES
    line_solution?(sp,v,eps_line(sp,v))

  line_solution_meets_horizontal_criterion: LEMMA
    line_solution?(sp,v,eps) IMPLIES
    horizontal_criterion?(sp,eps)(v)

  line_solution_independence : THEOREM
    line_solution?(sp,v) IMPLIES
    NOT horizontal_conflict_ever?(sp,v)

  line_solution_invariant: LEMMA
    sign(-(sp*v)) = sign(-((sp+t*v)*v)) IMPLIES
   (line_solution?(sp,v) IMPLIES line_solution?(sp+t*v,v))

  line_solution_rewrite: LEMMA line_solution?(sp,nzv) IFF
    EXISTS (tt): on_D?(sp+tt*nzv) AND (sp+tt*nzv)*nzv = 0

  line_solution_det: LEMMA line_solution?(sp,v,eps)
    IFF (-eps*det(sp,v) = D*norm(v) AND horizontal_entry?(sp,v))

  line_solution_scal_unique: LEMMA
    line_solution?(sp,nzv1,eps) AND line_solution?(sp,nzv2,eps)
    AND
    sqv(sp) > sq(D)
    IMPLIES
    EXISTS (pk:posreal): nzv1 = pk*nzv2

  line_solution_coordination : THEOREM
     horizontal_conflict?(sp,vo-vi) AND
     line_solution?(sp,nvo-vi,eps) AND
     line_solution?(-sp,nvi-vo,eps)
     IMPLIES
     NOT horizontal_conflict?(sp,nvo-nvi)

  line_solution_along_line: LEMMA
    det(v1,v2) /= 0 IMPLIES
    LET t1 = ((-eps)*D*norm(v2) - det(sp,v2))/det(v1,v2) IN
    (sp + t1*v1)*v2 <= 0 IMPLIES line_solution?(sp + t1*v1,v2,eps)

END line_solutions

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