| 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 984 B |
|
Quelle k_ordered.pvs Sprache: PVS |
|||||||||
|
%
% % Purpose : choice functions with ordered values (exact or % inexact); definition of a middle value voter; definition % of min and max (as compute functions). % % k_ordered [ N : [nat -> posnat], % Number of source nodes at each stage T : TYPE+, <= : (total_order?[T]), error: [nat -> T] ]: THEORY BEGIN IMPORTING reduce_choice, node_functions[N, T], select_minmax j: VAR nat node_set: VAR [j : nat -> non_empty_finite_set[below(N(j))]] sent: VAR sent_vec local: VAR sent_vec v_min(sent, node_set)(j) : T = v_min[N(j), T, <=](sent(j), node_set(j)) v_max(sent, node_set)(j) : T = v_max[N(j), T, <=](sent(j), node_set(j)) k_consensus_function: TYPE = [j:nat -> consensus_function[T,<=]] cf: VAR k_consensus_function tau: VAR [j:nat -> tau_type] reduce_choice(tau, cf): choice_function = LAMBDA j: reduce_choice[N(j), N(j+1), T, <=, error(j)](tau(j), cf(j)) END k_ordered ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28