Quelle synch_constant_definitions.pvs
Sprache: PVS
% % 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
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.
