|
%
% Purpose : This theory provides the basic definitions and
% properties concerning the relative drift of good
% oscillators. The drift bounds for a good oscillator
% are captured in the declared type `good_clock'.
% A good_clock is a function from Clocktime (integer) to
% realtime (real) with a bounded rate of drift.
%
% Assumptions : Oscillators have a bounded rate of drift with respect
% to (Newtonian) real time. This bound is captured by
% formal parameter rho.
%
physical_clocks
[
rho : nonneg_real
] : THEORY
BEGIN
IMPORTING
abs_props, floor_ceiling_ineq
% First define drift in terms of rho so that that we can use simpler
% terms for bounding relative drift.
rate: posreal = 1 + rho
drift: nonneg_real = rate - 1 / rate
drift_def: LEMMA drift = (rate * rate - 1) / rate
drift_bound: LEMMA drift <= 2 * rho
% Various variable declarations
X: VAR nat
T, T1, T2: VAR int
t: VAR real
clock: VAR [int -> real]
skew : VAR nnreal
adj: VAR real
% TYPE good_clock formalizes the notion of oscillator drift within
% some bound, rho. In essence, a good oscillator is characterized by
% the behavior of an (imaginary) unbounded counter.
good_clock: NONEMPTY_TYPE =
{ clock |
FORALL T:
1 / rate <= clock(T + 1) - clock(T) AND
clock(T + 1) - clock(T) <= rate
} CONTAINING LAMBDA T: T
c, c1, c2: VAR good_clock
clock_edge?(c, t): bool = EXISTS T: t = c(T)
drift_left_nat: LEMMA
X / rate <= c(T + X) - c(T)
drift_right_nat: LEMMA
c(T + X) - c(T) <= X * rate
drift_left: LEMMA
T1 <= T2 IMPLIES
(T2 - T1) / rate <= c(T2) - c(T1)
drift_right: LEMMA
T1 <= T2 IMPLIES
c(T2) - c(T1) <= (T2 - T1) * rate
abs_drift_lb: LEMMA
abs(T1 - T2) / rate <= abs(c(T1) - c(T2))
clock_nondecreasing: LEMMA
T1 <= T2 IMPLIES c(T1) <= c(T2)
clock_increasing: LEMMA
T1 < T2 IMPLIES c(T1) < c(T2)
clock_nondecreasing_alt: LEMMA
c(T1) <= c(T2) IMPLIES T1 <= T2
clock_eq_arg: LEMMA
c(T1) = c(T2) IMPLIES T1 = T2
offset_clocks?(c1, c2): bool =
EXISTS T2: FORALL T1: c1(T1) = c2(T1 + T2)
relative_drift: LEMMA
c1(T1 + X) - c2(T2 + X) <= c1(T1) - c2(T2) + drift * X
nonoverlap_basis: LEMMA
c1(T) - c2(T) <= adj AND
T2 - T1 > rate * adj AND
T1 <= T AND
T <= T2
IMPLIES
c1(T1) < c2(T2)
skew_basis_0: LEMMA
c1(T) - c2(T) <= adj AND
c2(T2) < c1(T1) AND
T1 <= T AND
T <= T2
IMPLIES
T2 - T1 < rate * adj
skew_bound_1: LEMMA
c1(T) - c2(T) <= skew AND
c2(T2) <= c1(T1) AND
T1 <= T + X AND
T - X <= T2
IMPLIES
T2 - T1 <= rate * (skew + drift * X)
skew_bound_2: LEMMA
c1(T) - c2(T) <= skew AND
c2(T2) < c1(T1) AND
T1 <= T + X AND
T - X <= T2
IMPLIES
T2 - T1 < rate * (skew + drift * X)
% basis of skew_conversion_sym in inverse_clocks:
skew_bound: LEMMA
abs(c1(T) - c2(T)) <= skew AND
abs(T2 - T) <= X AND
c1(T1) <= c2(T2) AND
c2(T2) < c1(T1 + 1)
IMPLIES
abs(T1 - T2) <= ceiling(rate * (skew + drift * X))
% offset properties for accuracy
lower_offset: LEMMA
T1 - X <= T2
IMPLIES
T2 - T1 <= rate * (c(T2) - c(T1) + drift * X)
upper_offset: LEMMA
T1 - X <= T2
IMPLIES
(c(T2) - c(T1) - drift * X) / rate <= T2 - T1
END physical_clocks
¤ Dauer der Verarbeitung: 0.32 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.
|
