Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: horizontal_criteria.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% horizontal_criteria.pvs
% ACCoRD v1.0
%
% This theory proposes criteria for horizontal separation for non-negative
% times. These criteria guarantee independence and (implicit) coordination.
%------------------------------------------------------------------------------

horizontal_criteria[D: posreal]: THEORY
BEGIN

  IMPORTING predicate_coordination_2D,horizontal[D]

  v,w       : VAR Vect2
  nzv       : VAR Nz_vect2
  sp        : VAR Sp_vect2
  ss        : VAR Ss_vect2
  vo,vi,
  nvo,nvi   : VAR Vect2
  eps,
  eps1,eps2 : VAR Sign

  R(sp):nnreal = sqrt(sqv(sp)-sq(D))/D

  R_eq_0 : LEMMA
    on_D?(sp) IFF
    R(sp) = 0

  R_gt_0 : JUDGEMENT
    R(ss) HAS_TYPE posreal

  R_symm : LEMMA
    R(-sp) = R(sp)

  sq_R_det : LEMMA
    sp*v <= 0 IMPLIES
      (sq(sp*v) > sq(R(sp))*sq(det(sp, v)) IFF
       sp*v < R(sp)*det(sp,v) AND R(sp)*det(sp,v) < -(sp*v))

  Delta_sq_det: LEMMA
    Delta(sp,nzv) > 0 IFF sq(R(sp))*sq(det(sp,nzv)) < sq(sp*nzv)

  Delta_sq_det_equality: LEMMA
    Delta(sp,nzv) = 0 IFF sq(R(sp))*sq(det(sp,nzv)) = sq(sp*nzv)

  Delta_zero_eps_line_equality: LEMMA
    Delta(sp,nzv) = 0 AND sp*nzv <= 0
    IMPLIES
    EXISTS (eps: Sign):
      eps*R(sp)*det(sp,nzv) = sp*nzv
      AND
      eps*det(sp,nzv) <= 0

  horizontal_solution: LEMMA
    horizontal_conflict?(sp,v)
    IFF
      (sp*v) < R(sp)*det(sp,v) AND R(sp)*det(sp,v) < -(sp*v)

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

  % horizontal_criterion_neg: LEMMA
  %   NOT horizontal_criterion?(sp,eps)(v) IMPLIES horizontal_criterion?(sp,eps)(-v)

  horizontal_criterion_scal: LEMMA
    FORALL (cc:nnreal): horizontal_criterion?(sp,eps)(v)
           IMPLIES
    horizontal_criterion?(sp,eps)(cc*v)

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

  horizontal_criterion_eps : LEMMA
    horizontal_criterion?(sp,v) IMPLIES
    horizontal_criterion?(sp,sign(-det(sp,v)))(v)

  horizontal_criterion_symmetric: LEMMA
   horizontal_criterion?(sp,eps)(v) IFF
   horizontal_criterion?(-sp,eps)(-v)

  horizontal_criterion_eps_unique : LEMMA
    horizontal_criterion?(sp,eps1)(v) AND
    horizontal_criterion?(sp,eps2)(v) AND
    NOT (det(sp,v) = 0 AND sp*v >= 0)
    IMPLIES
    eps1=eps2

  horizontal_criterion_independence : THEOREM
    horizontal_criterion?(sp,v) IFF
    NOT horizontal_conflict?(sp,v)

  horizontal_criterion_sum_closed: LEMMA
    horizontal_criterion?(sp,eps)(v) AND
    horizontal_criterion?(sp,eps)(w)
    IMPLIES
    horizontal_criterion?(sp,eps)(v+w)

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

  horizontal_sep_dir: LEMMA
    horizontal_dir?(sp,v,eps)
    IMPLIES
      horizontal_sep_dir_at?(sp,v,0,eps)

  horizontal_exit_independence: THEOREM
    horizontal_exit?(sp,v) OR Delta(sp,v) <= 0
    IFF
      NOT horizontal_conflict?(sp,v)

  horizontal_exit_coordination: THEOREM
    horizontal_conflict?(sp,vo-vi) AND
    horizontal_exit?(sp,nvo-vi) AND
    horizontal_exit?(-sp,nvi-vo)
    IMPLIES
      NOT horizontal_conflict?(sp,nvo-nvi)

END horizontal_criteria

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