|
%
% Purpose : Definitions of various period related constants,
% based on paramters derived from the synchronization
% protocol.
%
% P - nominal duration (in ticks) between
% resynchronization events.
% rho - bound on drift for a good oscillator
% alpha_l - lower bound on loss of accuracy due to
% computing and applying adjustment (may be 0).
% alpha_u - upper bound on loss of accuracy due to
% computing and applying adjustment (may be 0).
% pi_0 - intantaneous precision bound immediately
% after applying computed adjustment (> 1)
%
synch_constant_definitions
[(IMPORTING synch_parameter_constraints)
P: posnat,
T0: int,
rho: nnreal,
alpha_l, alpha_u: nnreal,
pi_0: {pi : posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}
]: THEORY
BEGIN
IMPORTING
physical_clocks[rho] % for definition of rate, drift
j, k: VAR nat
P_bound: LEMMA
rate * (pi_0 + max(alpha_l, alpha_u) + drift * P) < P
rho_bound: LEMMA rho * (2 + rho) < 1 %%% NOT USED
ADJ: nat = floor(rate * (pi_0 + max(alpha_l, alpha_u) + drift * P))
ADJ_ineq: LEMMA
ADJ >= floor((drift * P + pi_0) * rate)
ADJ_ineq_l: LEMMA
ADJ >= floor((drift * P + alpha_l + pi_0) * rate)
ADJ_ineq_h: LEMMA
ADJ >= floor((drift * P + alpha_u + pi_0) * rate)
ADJ_bound: LEMMA ADJ < P
P_min: posnat = P - ADJ %%% NOT USED
P_max: posnat = P + ADJ
p_min_bound: LEMMA rate * (pi_0 + max(alpha_l, alpha_u)) < P
p_lower: posreal = P / rate - alpha_l
p_upper: posreal = P * rate + alpha_u
p_min: posreal = P / rate - alpha_l - pi_0
p_max: posreal = P * rate + alpha_u + pi_0
p_min_lower: LEMMA p_min = p_lower - pi_0
p_max_upper: LEMMA p_max = p_upper + pi_0
drift_P_bound: LEMMA drift * P < p_min
Pi: posnat = ceiling(rate * (max(alpha_l, alpha_u) + pi_0 + drift * (P_max + 1)))
END synch_constant_definitions
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
