products/sources/formale Sprachen/PVS/ACCoRD/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: dml002.mco   Sprache: PVS

Original von: PVS©
%------------------------------------------------------------------------------
%    Loss of Separation Criterion: Vertical
%    
%    This criterion allows for a backup system that performs
%    Collision Avoidance in the Event of A Near Collision (E.g. TCAS).
%    The collision avoidance system is assumed to activate when a cylinder
%    around the intruder of radius caD and height caH is expected to be 
%    entered by the ownship within time caTime.
%------------------------------------------------------------------------------
vertical_los_crit_CA[D,H,caD,caH,caTime: posreal,
         ( IMPORTING definitions_3D )
         break_vz_symm:[Vect3 ->  Sign] %% Break symmetry when v`z = 0
      ] : THEORY                        
BEGIN

  ASSUMING

    break_vz_symm_comm : ASSUMPTION
      FORALL (s:Vect3):
        s /= zero IMPLIES
        break_vz_symm(-s) = -break_vz_symm(s)

    break_vz_symm_sz : ASSUMPTION
      FORALL (s:Vect3):
        s`z /= 0 IMPLIES 
        break_vz_symm(s) = sign(s`z)

    % Future work: continuity of break symmetry

  ENDASSUMING

  IMPORTING vertical_los_criterion[D,H],
     cd3d[caD,caH,0,caTime],
     cd3d_ever[caD,caH]

  vo,vi,
  nvi,nvo,
  v,nv    : VAR Vect3
  s : VAR Vect3
  t,t1,t2,
  tm      : VAR real
  tr      : VAR posreal %% Parameter that specifies maximum time to recover
  eps   : VAR Sign
  tn   : VAR nnreal
  sz,vz,
  nvz,
  voz,viz,
  nvoz,
  nviz,
  soz,siz    : VAR real
  MinRelVertSpeed,
  MinRelVertSpeedo,
  MinRelVertSpeedi: VAR posreal

  %%% This file implements a specific element of the type EpsChooser,
  %%% which is defined in vertical_los_generic. It then constructs the
  %%% associated criterion with the function vertical_los_crit_epschooser?
  %%% that is defined in that file.

  %%% Recall from vertical_los_generic that EpsChooser picks an epsilon
  %%% (-1 or 1) (up or down). A decision vector is a function that takes
  %%% s, vo, and vi and returns another vector on which the decision
  %%% of epsilon will be made.

  Decision_Vector : TYPE+ = {f:[[Vect3,Vect3]->Vect3]| FORALL (s,v): 
    (s /= zero OR v/=zero) => (f(s,v)/=zero AND f(-s,-v)=-f(s,v))}

  dv: VAR Decision_Vector

  dv_to_ec(dv)(s,v): Sign =
    break_vz_symm(dv(s,v))

  dv_to_ec_antisymmetric: JUDGEMENT
    dv_to_ec(dv) HAS_TYPE Vertical_Strategy[D,H]

  %%% The interior cylinder where CA applies:

  CA_applies?(s,v): bool = cd3d?[caD,caH,0,caTime](s,v)

  CA_cyl_conflict_ever?(s,v): bool =
    cd3d_ever?[caD,caH](s,v)

  %%% A specific decision vector for the new criterion:

  vertical_decision_vect(s,v): {vq: Vect3 | (s /= zero OR v/=zero) IMPLIES vq/=zero} =
    IF (s/=zero AND CA_cyl_conflict_ever?(s,v)) OR (s/=zero AND v`z=0) THEN
       (IF s`z /= 0 OR sqv(v)=0 THEN s ELSE v ENDIF)
    ELSIF vect2(v) = zero OR s = zero THEN
       v
    ELSIF vect2(s)*vect2(v) <= 0 THEN
       s + horizontal_tca(s,v)*v
    ELSE
       s
    ENDIF

  vertical_decision_vect_antisymmetric: JUDGEMENT
    vertical_decision_vect HAS_TYPE Decision_Vector

  %%% The new criterion:

  vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv) : bool =
    vertical_los_criterion?(s,v,dv_to_ec(vertical_decision_vect)(s,v),MinRelVertSpeed)(nv)

  % It is coordinated:

  vertical_los_crit_CA_independent: LEMMA
    LET eps: Sign = dv_to_ec(vertical_decision_vect)(s, v)
    IN 
        s/=zero AND
 vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv) AND
 vect2(s)*vect2(v) < 0 AND vect2(s)*vect2(nv) < 0 AND
 norm(vect2(s+horizontal_tca(s,nv)*nv)) <= norm(vect2(s+horizontal_tca(s,v)*(v)))
 IMPLIES
 eps*(s+horizontal_tca((s),nv)*nv)`z >= eps*(s+horizontal_tca((s),v)*(v))`z

  vertical_los_crit_CA_independent_strong: LEMMA
     s/=zero AND
 vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv) AND
 vect2(s)*vect2(v) < 0 AND vect2(s)*vect2(nv) < 0 AND
 norm(vect2(s+horizontal_tca(s,nv)*nv)) <= norm(vect2(s+horizontal_tca(s,v)*(v)))
 IMPLIES
 ((v`z=0 OR CA_cyl_conflict_ever?(s,v)) AND 
   sign(s`z)/=sign(v`z) AND abs((s+horizontal_tca((s),nv)*nv)`z) >= abs(s`z))
 OR
 abs((s+horizontal_tca((s),nv)*nv)`z) >= abs((s+horizontal_tca((s),v)*(v))`z)

  vertical_los_crit_CA_independent_vspeed: LEMMA
    s/=zero AND
      vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv)
      IMPLIES
      break_vz_symm(vertical_decision_vect(s,v))*(nv`z)>=MinRelVertSpeed

  vertical_los_crit_CA_coordinated_vspeed: LEMMA
      s/=zero AND
      vertical_los_crit_CA?(s,vo-vi,MinRelVertSpeedo)(nvo-vi) AND
      vertical_los_crit_CA?(-s,vi-vo,MinRelVertSpeedi)(nvi-vo)
      IMPLIES
      break_vz_symm(vertical_decision_vect(s,vo-vi))*(nvo`z-nvi`z)>=max(MinRelVertSpeedo,MinRelVertSpeedi)

  vertical_los_crit_CA_coordinated: LEMMA
      s/=zero AND
      vertical_los_crit_CA?(s,vo-vi,MinRelVertSpeedo)(nvo-vi) AND
      vertical_los_crit_CA?(-s,vi-vo,MinRelVertSpeedi)(nvi-vo)
      IMPLIES
      vertical_los_crit_CA?(s,vo-vi,max(MinRelVertSpeedo,MinRelVertSpeedi))(nvo-nvi)

  vertical_los_crit_CA_coordinated_strong: LEMMA
      LET v = vo-vi, nv = nvo-nvi IN
      s/=zero AND
      vertical_los_crit_CA?(s,vo-vi,MinRelVertSpeedo)(nvo-vi) AND
      vertical_los_crit_CA?(-s,vi-vo,MinRelVertSpeedi)(nvi-vo) AND
      vect2(s)*vect2(v) < 0
      IMPLIES
      vect2(s)*vect2(nv) >= 0 OR
      norm(vect2(s+horizontal_tca(s,nv)*nv)) > norm(vect2(s+horizontal_tca(s,v)*(v))) OR
      ((v`z=0 OR CA_cyl_conflict_ever?(s,v)) AND 
         sign(s`z)/=sign(v`z) AND abs((s+horizontal_tca((s),nv)*nv)`z) >= abs(s`z)) OR
      abs((s+horizontal_tca((s),nv)*nv)`z) >= abs((s+horizontal_tca((s),v)*(v))`z)

END vertical_los_crit_CA

¤ Dauer der Verarbeitung: 0.40 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff