% % % Purpose : properties of a check in the time domain. A check % in the time domain can be considered as answering the % question does an event fall within a timing window. % % %
timing_window[
rho : nonneg_real, % Bound on drift for a good oscillator
min_latency : nonneg_real, % minimum real time latency (in ticks % of real time) of the communication link % determined by things like length of wire, speed % of light, and clock rate.
var_latency: nonneg_real % Max variation (in ticks of real % time) caused by both wire length % differences and clock jitter.
]: THEORY
% The Timestamped event ev at the destination falls within the % reception window for time T of destination clock c.
timing_conforms?(c, T, skew)(ev): bool =
c(T - Delta_max(skew)) <= ev & ev <= c(T + Delta_max(skew))
% The timing check can also be expressed as a property on % Clocktimes. This is the basis for its implementation.
timing_conforms_def: LEMMA
timing_conforms?(c, T, skew)(c(Timestamp(c, ev))) IFF
abs(Timestamp(c, ev) - T) <= Delta_max(skew)
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.
