|
%------------------------------------------------------------------------------
% circle_criterion.pvs
% ACCoRD v1.0
%
%------------------------------------------------------------------------------
circle_criterion[D,H: posreal]: THEORY
BEGIN
IMPORTING space_3D[D,H],
horizontal_criteria[D],
vz_criteria[H]
spz : VAR Spz_vect3 % Vertically separated
vzgs : VAR Zv2_vect3 % Ground speed is zero
s,v : VAR Vect3
eps,dir : VAR Sign
t : VAR real
%% Vertical separation
vertical_sep_independence : THEOREM
vertical_exit?(spz`z,v`z)
IMPLIES
NOT conflict?(spz,v)
%% Ground speed is 0
nogs_criterion?(s,vzgs): bool =
vertical_sep?(s`z) AND vertical_exit?(s`z,vzgs`z) OR
horizontal_sep?(s)
nogs_criterion_independence : THEOREM
nogs_criterion?(s,vzgs) IFF NOT conflict?(s,vzgs)
%% Aircarft are separated
circle_criterion?(s,v,dir): bool =
horizontal_sep?(s) AND
vertical_sep?(s`z) AND
horizontal_dir?(s,v,dir) AND
vertical_dir?(s`z,v`z,-dir)
circle_criterion_at?(s,v,t,dir): MACRO bool =
circle_criterion?(s+t*v,v,dir)
circle_criterion_independence : THEOREM
circle_criterion?(s,v,dir) IMPLIES
NOT conflict_ever?(s,v)
circle_criterion_at_independence: THEOREM
circle_criterion_at?(s,v,t,dir)
IMPLIES
NOT conflict_ever?(s,v)
END circle_criterion
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
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.
|
