| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle cd_vertical.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% cd_vertical.pvs % ACCoRD v1.0 % % Correctness and completeness of vertical conflict detection algorithm. % H : Vertical separation % B : Lookahead time % T : Lookahead time %------------------------------------------------------------------------------ cd_vertical[H:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY BEGIN IMPORTING vertical[H], util, Lookahead[B,T], reals@min_max sz,vz,t : VAR real nzvz : VAR nzreal eps,dir : VAR Sign nzt : VAR nzreal pt : VAR posreal % Conflict during interval [0,T] conflict_vertical?(sz,vz) : bool = EXISTS (t: Lookahead): vertical_los_at?(sz,vz,t) cd_vertical?(sz,vz) : bool = (vz = 0 AND abs(sz)<H) OR (vz /= 0 AND min(max(-H-sign(vz)*sz,B*abs(vz)),T*abs(vz)) < max(min(H-sign(vz)*sz,T*abs cd_vertical_rewrite: LEMMA cd_vertical?(sz,vz) IFF (vz = 0 AND abs(sz)<H) OR (vz /= 0 AND min(max(Theta_H(sz,vz,Entry),B),T) < max(min(Theta_H(sz,vz,Exit),T),B)) cd_vertical_correct : THEOREM cd_vertical?(sz,vz) IMPLIES conflict_vertical?(sz,vz) cd_vertical_complete : THEOREM conflict_vertical?(sz,vz) IMPLIES cd_vertical?(sz,vz) %-----------------------------------------------% % THEOREM: cd_vertical is correct and complete % %-----------------------------------------------% cd_vertical : THEOREM conflict_vertical?(sz,vz) IFF cd_vertical?(sz,vz) conflict_vertical_on_open_interval: LEMMA conflict_vertical?(sz,vz) IFF EXISTS (topen: Lookahead): B<topen AND topen <T AND vertical_los_at?(sz,vz,topen) END cd_vertical ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28