|
%------------------------------------------------------------------------------
% line_solutions.pvs
% ACCoRD v1.0
%
% Circle solutions are vectors v such that at time t the ownship is on the
% circle of radius D and altitude H. If dir=-1, v points into the circle and
% outside the rectangle; if dir=1, v points outside the circle and inside the
% rectangle.
%------------------------------------------------------------------------------
circle_solutions[D,H:posreal] : THEORY
BEGIN
IMPORTING circle_criterion[D,H]
s,v : VAR Vect3
t : VAR real
dir,eps : VAR Sign
pt : VAR posreal
circle_solution?(s,v,t,dir): bool =
t > 0 AND
circle_solution_2D?(s,v,t,dir) AND
vertical_solution?(s`z,v`z,t,-dir)
circle_solution_horizontal: LEMMA
vertical_conflict?(s`z,v`z) AND
circle_solution?(s,v,t,dir)
IMPLIES
v`z /= 0 AND circle_solution?(s,v,Theta_H(s`z,v`z,-dir),dir)
circle_solution_vertical: LEMMA
horizontal_conflict?(s,v) AND
circle_solution?(s,v,t,dir)
IMPLIES
NOT zero_vect2?(v) AND circle_solution?(s,v,Theta_D(s,v,dir),dir)
circle_solution_meets_criterion : LEMMA
circle_solution?(s,v,t,dir) IMPLIES
circle_criterion_at?(s,v,t,dir)
circle_solution_independence : THEOREM
circle_solution?(s,v,t,dir) IMPLIES
NOT conflict_ever?(s,v)
circle_solution?(s,v): MACRO bool =
EXISTS (dir,t): circle_solution?(s,v,t,dir)
END circle_solutions
¤ Dauer der Verarbeitung: 0.18 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.
|
