|
%
%
% Purpose : validity and agreement properties for a multi-stage inexact
% exchange with the results-based fault model.
%
%
inexact_reduce
[
N : [nat -> posnat],
error: [nat -> real]
] : THEORY
BEGIN
IMPORTING
inexact_comm[N],
protocol[N, real],
k_ordered[N, real, <=, error],
inexact_reduce_stage,
reals@sigma_nat
i, j, k: VAR nat
v: VAR real
sent: VAR sent_vec
rcvd: VAR rcvd_matrix
check: VAR check_function
epsilon, eps_u, eps_l, eps: VAR [nat -> nonneg_real]
delta : VAR nonneg_real
node_set: VAR [i: nat -> non_empty_finite_set[below(N(i))]]
tau: VAR [j: nat -> tau_type]
idx: VAR [nat -> nat]
cf: VAR k_consensus_function
% Main results
lower_validity: THEOREM
protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
quorum_lower?(sent, rcvd, check, tau, eps_l, j, j + k) AND
enabled_within?(rcvd, check, j, j + k)(node_set)
IMPLIES
v_min(sent, node_set)(j) - sigma(j, j + k - 1, eps_l) <= v_min(sent, node_set)(j + k)
upper_validity: THEOREM
protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
quorum_upper?(sent, rcvd, check, tau, eps_u, j, j + k) AND
enabled_within?(rcvd, check, j, j + k)(node_set)
IMPLIES
v_max(sent, node_set)(j + k) <= v_max(sent, node_set)(j) + sigma(j, j + k - 1, eps_u)
agreement_propagation: THEOREM
protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
quorum_imprecision?(sent, rcvd, check, tau, epsilon, j, j + k) AND
enabled_within?(rcvd, check, j, j + k)(node_set) AND
v_max(sent, node_set)(j) - v_min(sent, node_set)(j) <= delta
IMPLIES
v_max(sent, node_set)(j + k) - v_min(sent, node_set)(j + k)
<= delta + sigma(j, j + k - 1, epsilon)
X: VAR posnat
convergent_stage?(rcvd, check, tau, epsilon, cf, X, j, k): bool =
EXISTS i: j <= i AND i < k AND
overlap_imprecision?[N(i), N(i + 1), error(i)](rcvd(i), check(i), tau(i), epsilon(i)) AND
convergent?(cf(i), max_length[N(i), N(i + 1), real, <=, error(i)](rcvd(i), check(i), tau(i)), X)
convergence: THEOREM
protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
quorum_imprecision?(sent, rcvd, check, tau, epsilon, j, j + k) AND
enabled_within?(rcvd, check, j, j + k)(node_set) AND
convergent_stage?(rcvd, check, tau, epsilon, cf, X, j, j + k) AND
v_max(sent, node_set)(j) - v_min(sent, node_set)(j) <= delta
IMPLIES
v_max(sent, node_set)(j + k) - v_min(sent, node_set)(j + k)
<= delta * ((X - 1) / X) + sigma(j, j + k - 1, epsilon)
agreement_generation: THEOREM
protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
exists_all_symmetric?(sent, rcvd, check, tau, epsilon, cf, j, j + k) AND
enabled_within?(rcvd, check, j, j + k)(node_set)
IMPLIES
v_max(sent, node_set)(j + k) - v_min(sent, node_set)(j + k) <= sigma(j, j + k - 1, epsilon)
END inexact_reduce
¤ Dauer der Verarbeitung: 0.17 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.
|
