| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 874 B |
|
Quelle node_functions.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28