|
%
%
% Purpose: The protocol (relationship between what is received and
% what is sent) when the message datatype is used with
% the integration fault model.
%
%
protocol_integration
[
N: [nat -> posnat],
T: TYPE+
] : THEORY
BEGIN
i, j, k: VAR nat
element: T % to eliminate TCC's
IMPORTING
comm_integration[N, T],
protocol[N, 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 check_function
vf: VAR choice_function
% cf: VAR compute_function
protocol(sent, check, vf, status, j, k): bool =
protocol(vf, sent, rcvd(sent, status), check, j, k)
% protocol(sent, check, vf, cf, status, j, k): bool =
% protocol(cf, vf, sent, rcvd(sent, status), check, j, k)
END protocol_integration
¤ Dauer der Verarbeitung: 0.18 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.
|
