|
%
% Purpose : instantiation of multiple-stage majority exchange with
% the integration fault model.
%
%
majority_integration
[
N: [nat -> posnat],
T: TYPE+
] : THEORY
BEGIN
i, j, k: VAR nat
IMPORTING
protocol_integration[N, T],
majority[N, message[T]]
v: VAR message[T]
status: VAR [i : nat -> node_status[N(i)]]
sent: VAR [i : nat -> [below(N(i)) -> message[T]]]
common_check: VAR [i: nat -> non_empty_finite_set[below(N(i))]]
msg_check: VAR valid_check_function
check: VAR valid_check_function
mf: VAR [nat -> majority_function[message[T]]]
consensus_validity: THEOREM
check = conforms(msg_check, common_check) AND
protocol(sent, check, majority_vote(mf), status, j, j + k) AND
majority_correct?(sent, check, status, j, j + k) AND
uniform?(sent(j), v)(common_check(j))
IMPLIES
uniform?(sent(j + k), v)(common_check(j + k))
agreement_generation: THEOREM
check = conforms(msg_check, common_check) AND
protocol(sent, check, majority_vote(mf), status, j, j + k) AND
exists_all_symmetric?(sent, check, status, j, j + k)
IMPLIES
EXISTS v:
uniform?(sent(j + k), v)(common_check(j + k))
END majority_integration
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
