% The following type is a flight plan. It consists of pairs (t (time),p (position)), where t is a time and % p is a vector. At the corresponding segement of the flight plan, the aircraft will have % position p at time t. % Times are strictly increasing, but may be negative.
FlightPlan: TYPE+ = {fp: [below[N] -> [# time: real,position: Vect3 #]] | FORALL (i: below[N]): i-1 >= 0 IMPLIES fp(i)`time > fp(i-1)`time}
flp: VAR FlightPlan
start_time(flp): real = flp(0)`time
end_time(flp): real = flp(N-1)`time
%%%%%%%%% < over flightplan times is transitive
flight_plan_ascending_time: LEMMA
k < i IMPLIES flp(k)`time < flp(i)`time
% the times that the flightplan covers (range)
FlightTimes(flp): TYPE+ ={a: real | start_time(flp) <= a AND a <= end_time(flp)}
% the velocity after leaving the k-th waypoint and on the way to the k+1-st waypoint
velocity(flp: FlightPlan)(j: below[N-1]): Vect3 =
(1/(flp(j+1)`time-flp(j)`time))*(flp(j+1)`position - flp(j)`position)
% Lookup of the flightplan segment index, given a time
segment(flp: FlightPlan)(tt: FlightTimes(flp)): below[N] = segment_max({j: below[N] | tt >= flp(j)`time})
% time tt is either between two indices or after the last one
segment_def: LEMMA FORALL (tt: FlightTimes(flp)):
flp(segment(flp)(tt))`time <= tt AND
(segment(flp)(tt) < N-1 IMPLIES tt < flp(segment(flp)(tt) + 1)`time)
% if we have index bounds on the time, we have the segment
segment_index: LEMMA FORALL (tt:FlightTimes(flp)):
flp(j)`time <= tt AND tt < flp(j+1)`time IFF segment(flp)(tt) = j
% the position at a given time tt in the flightplan
location_at(flp)(tt: FlightTimes(flp)): Vect3 = Let seg = segment(flp)(tt) IN IF seg = N-1 THEN flp(N-1)`position ELSE
flp(seg)`position + (tt - flp(seg)`time)*velocity(flp)(seg) ENDIF
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.
