Quellcode-Bibliothek 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

  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

quality100%

¤ 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.0.3Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.