Quelle  node_functions.pvs

%
%
% Purpose : types for the functions that operate in a node
%
%

node_functions
[
    N   : [nat -> posnat],  % Number of source nodes at each stage
    T   : TYPE+
]: THEORY

BEGIN

  i: VAR nat

  IMPORTING node_functions_stage

  choice_function:  TYPE = [i:nat -> choice_stage[N(i), N(i+1), T]]
  choice_system:    TYPE = [i:nat -> choice_stage_alt[N(i), N(i+1), T]]
  check_function:   TYPE = [i:nat -> check_stage[N(i), N(i+1), T]]
  check_system:     TYPE = [i:nat -> check_stage_alt[N(i), N(i+1), T]]
  compute_function: TYPE = [i:nat -> compute_stage[N(i), T]]

  sent_vec: TYPE = [i:nat -> sent_vec_stage[N(i), N(i+1), T]]
  rcvd_matrix: TYPE = [i:nat -> rcvd_matrix_stage[N(i), N(i+1), T]]


  filter_system: TYPE = [i:nat -> filter_stage[N(i),N(i+1),T]]

  nominal_filter(i): filter_stage[N(i), N(i+1), T] = nominal_filter[N(i),N(i+1),T]


END node_functions