%
%
% Purpose : a reduce-select choice multiple-stage exchange
% under an integration fault model and exact communication.
%
%
exact_reduce_integration
[
N: [nat -> posnat],
T: TYPE+,
<= : (total_order?[T]),
(IMPORTING ordered_message[T,<=])
source_error: [nat -> message]
] : THEORY
BEGIN
i, j, k: VAR nat
IMPORTING
ordered_message[T,<=],
protocol_integration[N, T],
exact_reduce[N, message, ordered_message.<=, source_error]
status: VAR [i : nat -> node_status[N(i)]]
sent: VAR [i : nat -> [below(N(i)) -> message]]
local: VAR [i : nat -> [below(N(i)) -> T]]
common_check: VAR [i: nat -> non_empty_finite_set[below(N(i))]]
msg_check: VAR valid_check_function
check: VAR valid_check_function
tau: VAR [j: nat -> tau_type]
cf: VAR k_consensus_function
lower_validity: THEOREM
check = conforms(msg_check, common_check) AND
protocol(sent, check, reduce_choice(tau, cf), status, j, j + k) AND
quorum_correct?(sent, check, status, tau, j, j + k)
IMPLIES
v_min(sent, common_check)(j) <= v_min(sent, common_check)(j + k)
upper_validity: THEOREM
check = conforms(msg_check, common_check) AND
protocol(sent, check, reduce_choice(tau, cf), status, j, j + k) AND
quorum_correct?(sent, check, status, tau, j, j + k)
IMPLIES
v_max(sent, common_check)(j + k) <= v_max(sent, common_check)(j)
agreement_generation: THEOREM
check = conforms(msg_check, common_check) AND
protocol(sent, check, reduce_choice(tau, cf), status, j, j + k) AND
exists_all_symmetric?(sent, check, status, tau, j, j + k)
IMPLIES
v_max(sent, common_check)(j + k) = v_min(sent, common_check)(j + k)
END exact_reduce_integration
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
|
|
