Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: kb.pvs Sprache: PVS

Original von: PVS^©

%
% Karl Bilimoria's Geometric Optimization Algorithm
%

kb[D:posreal] : THEORY
BEGIN

  IMPORTING repulsive,
            track,
     trig_fnd@trig_values,
     trig_fnd@atan_values,
     horizontal[D],
     tangent_line[D]

  s       : VAR Ss_vect2
  vo,vi,v : VAR Nz_vect2
  nvo,nvi : VAR Vect2
  f,fo,fi : VAR nnreal
  eps,irt : VAR Sign
  p   : VAR posreal
  x,y,r,
  phi   : VAR real

  angle_from_to(x,y): {aa:real|aa>=-pi AND aa<pi} =
    to2pi((y-x) + pi)-pi

  % The next lemma proves with grind
  angle_from_to_id: LEMMA
    to2pi(x + angle_from_to(x,y)) = to2pi(y)

  angle_from_to_lt_pi: LEMMA abs(x-y)<pi IMPLIES
    angle_from_to(x,y) = y-x

  % The next lemma proves with (grind :exclude "pi")
  angle_from_to_test: LEMMA
    angle_from_to(2*pi,pi) = -pi AND
    angle_from_to(pi,2*pi) = -pi AND
    angle_from_to(pi/6,11*pi/6) = -pi/3 AND
    angle_from_to(pi/2,5*pi/3) = -5*pi/6 AND
    angle_from_to(pi/4,7*pi/6) = 11*pi/12 AND
    angle_from_to(7*pi/6,pi/4) = -11*pi/12 AND
    angle_from_to(0,2*pi) = 0 AND
    angle_from_to(2*pi,0) = 0 AND
    angle_from_to(3*pi/4,23*pi/12) = -5*pi/6 AND
    angle_from_to(23*pi/12,3*pi/4) = 5*pi/6 AND
    angle_from_to(17*pi/12,pi/6) = 3*pi/4 AND
    angle_from_to(pi/6,17*pi/12) = -3*pi/4 AND
    angle_from_to(34*pi + pi/4,-24*pi+7*pi/6) = 11*pi/12 AND
    angle_from_to(34*pi+17*pi/12,-18*pi+pi/6) = 3*pi/4

  chirel_star(s,v,f,eps) : nnreal_lt_2pi =
    to2pi(track(v) + f*angle_from_to(track(v),track(-s) - eps*asin(D/norm(s))))

  chirel_star_equiv: LEMMA
    abs(track(v) - (track(-s) - eps*asin(D/norm(s)))) < pi AND
    f >= 0 AND
    f<=1
    IMPLIES
    chirel_star(s,v,f,eps) = to2pi(track(v)+f*(track(-s) - eps*asin(D/norm(s)) - track(v)))

  chirel_star_test: LEMMA
     D = 5 AND s = (-10/sqrt(3),0) AND
     vo = (2,0) AND
     vi = (1,0) IMPLIES
     track(vo) = pi/2 AND track(vi) = pi/2
     AND horizontal_conflict?(s,vo-vi) AND
     track(vo-vi) = pi/2 AND
     track(-s) = pi/2 AND
     norm(s) = 10/sqrt(3) AND
     chirel_star(s,vo-vi,1/2,-1) = 2*pi/3 AND
     chirel_star(s,vo-vi,1,-1) = 5*pi/6 AND
     chirel_star(s,vo-vi,0,-1) = pi/2

  chirel_star_0_id: LEMMA chirel_star(s,v,0,eps) = track(v)

  chirel_star_1_id: LEMMA chirel_star(s,v,1,eps) = to2pi(track(-s) - eps*asin(D/norm(s)))

  chirel_star_f_entry_scaf: LEMMA abs(phi)<=pi AND cos(r)<0 AND cos(r-phi)<0 AND f>=0 AND f<=1
    IMPLIES cos(r-f*phi)<0

  chirel_star_tangent: LEMMA line_solution?(s,trkgs2vect(chirel_star(s,v,1,eps),p),eps)

  chirel_star_f_entry: LEMMA f<1 AND s*v < 0 IMPLIES s*trkgs2vect(chirel_star(s,v,f,eps),p) < 0

  chi_hc(f,eps,irt)(s,vo,vi) : [nnreal_lt_2pi,bool] =
    LET v = vo - vi IN
      IF zero_vect2?(v) THEN (0,false)
      ELSE
        LET chirelstar = chirel_star(s,v,f,eps),
            expr       = (norm(vi)/norm(vo))*sin(chirelstar-track(vi)),
     asinex     = IF abs(expr) > 1 THEN FALSE ELSE asin(expr) ENDIF,
     exsign     = sign(asinex),
     expidiff   = exsign*(pi/2)-asinex,
     arcsindir  = exsign*(pi/2)+irt*expidiff,
     theta      = to2pi(chirelstar - arcsindir),
     nvovect    = trkgs2vect(theta,norm(vo))
IN
          IF (abs(expr) > 1 OR s*(nvovect-vi)>=0) THEN (0,false)
          ELSE (theta,true)
          ENDIF
      ENDIF

  sin_track_minus: LEMMA
    vo-vi /= zero IMPLIES
    norm(vo)*sin(track(vo-vi)-track(vo)) = norm(vi)*sin(track(vo-vi)-track(vi))

  chi_hc_sin_equivalence_2: LEMMA
    LET ch = chi_hc(f,eps,irt)(s,vo,vi),
        nvo = trkgs2vect(ch`1,norm(vo))
    IN
    ch`2 IMPLIES
    norm(vi)*sin(chirel_star(s,vo-vi,f,eps) - track(vi)) = norm(vo)*sin(chirel_star(s,vo-vi,f,eps) - track(nvo))

  chi_hc_track_eq: LEMMA
    FORALL (v,w:Nz_vect2): v`y/=0 AND w`y/=0 AND v`x/v`y = w`x/w`y AND s*v<0 AND s*w<0 IMPLIES track(v) = track(w)

  chi_hc_1_chirel: LEMMA
    chi_hc(1,eps,irt)(s,vo,vi)`2 IMPLIES
    track(trkgs2vect(chi_hc(1,eps,irt)(s,vo,vi)`1,norm(vo)) - vi) = chirel_star(s,vo-vi,1,eps)

  chi_hc_f_chirel: LEMMA
    s*(vo-vi)<0 AND
    chi_hc(f,eps,irt)(s,vo,vi)`2 AND f < 1 IMPLIES
    track(trkgs2vect(chi_hc(f,eps,irt)(s,vo,vi)`1,norm(vo)) - vi) = chirel_star(s,vo-vi,f,eps)

  chi_hc_0_id: LEMMA
      chi_hc(0,eps,-1)(s,vo,vi)`2 AND
      -pi/2 < track(vo-vi)-track(vo) AND
      track(vo-vi)-track(vo) < pi/2
    IMPLIES
      chi_hc(0,eps,-1)(s,vo,vi)`1 = track(vo)

  chi_hc_0_id_rel: LEMMA
      chi_hc(0,eps,irt)(s,vo,vi)`2 AND
      -pi/2 < track(vo-vi)-track(vo) AND
      track(vo-vi)-track(vo) < pi/2 AND
      s*(vo-vi) < 0
    IMPLIES
    LET
      nvo = trkgs2vect(chi_hc(0,eps,irt)(s,vo,vi)`1,norm(vo))
    IN
      track(nvo-vi) = track(vo-vi)

  kb(eps,irt,f)(s,vo,vi) : Vect2 =
    LET (trk,b) = chi_hc(f,eps,irt)(s,vo,vi) IN
      IF b THEN trkgs2vect(trk,norm(vo))
      ELSE zero
      ENDIF

  kb_0_id : LEMMA
      chi_hc(0,eps,-1)(s,vo,vi)`2 AND
      -pi/2 < track(vo-vi)-track(vo) AND
      track(vo-vi)-track(vo) < pi/2
    IMPLIES
      kb(eps,-1,0)(s,vo,vi) = vo

  kb_tangent_line : LEMMA
        chi_hc(1,eps,irt)(s,vo,vi)`2 AND
        -pi/2 < track(vo-vi)-track(vo) AND
        track(vo-vi)-track(vo) < pi/2
    IMPLIES
        line_solution?(s,kb(eps,irt,1)(s,vo,vi)-vi,eps)

  kb_is_independent : THEOREM
    horizontal_conflict?(s,vo-vi) AND
    abs(track(vo-vi)-track(vo)) < 0 AND
    abs(track(vi-vo)-track(vi)) < 0 AND
    nvo = kb(eps,irt,1)(s,vo,vi) AND
    nvo /= zero AND
    nvi = kb(eps,0,irt)(-s,vi,vo) AND
    nvi /= zero
    IMPLIES
      NOT horizontal_conflict?(s,nvo-vi)

  %% 3 Counterexamples to the claim that kb is coordinated with respect
  %% to the conflict-free safety property.

  kb_is_not_coordinated_1 : THEOREM
     D = 5 AND s = (-10/sqrt(3),0) AND
     vo = (2,0) AND
     vi = (1,0) AND
      nvo = kb(-1,-1,1/2)(s,vo,vi) AND
      nvi = kb(-1,-1,1/2)(-s,vi,vo)
      IMPLIES
      nvo /= zero AND
      nvi /= zero AND
      horizontal_conflict?(s,vo-vi) AND
      horizontal_conflict?(s,nvo-nvi)

  kb_is_not_coordinated_2 : THEOREM
     D = 5 AND s = (-10/sqrt(3),0) AND
     vo = (500,0) AND
     vi = (250,0) AND
      nvo = kb(-1,-1,1/2)(s,vo,vi) AND
      nvi = kb(-1,-1,1/2)(-s,vi,vo)
      IMPLIES
      nvo /= zero AND
      nvi /= zero AND
      horizontal_conflict?(s,vo-vi) AND
      horizontal_conflict?(s,nvo-nvi)

  % A different proof of the above result, this time showing
  % that minimum separation is less than 4.1
  kb_is_not_coordinated_3 : THEOREM
     D = 5 AND s = (-10/sqrt(3),0) AND
     vo = (500,0) AND
     vi = (250,0) AND
      nvo = kb(-1,-1,1/2)(s,vo,vi) AND
      nvi = kb(-1,-1,1/2)(-s,vi,vo)
      IMPLIES
      nvo /= zero AND
      nvi /= zero AND
      horizontal_conflict?(s,vo-vi) AND
      horizontal_conflict?(s,nvo-nvi)

END kb

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