SSL protocol_integration.pvs   Sprache: PVS

%
%
% 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