onethird-consensus(es;t;Input;Vote;Output;voters;clients) ==
  no_repeats(Id;voters)
   (||voters|| = ((3 * t) + 1))
   left(inning_val()[es-threshold(es;
                                   simple_consensus_init();
                                   inning_step();
                                   inning_test(1);
                                   nxt_inning();
                                   Input+Vote)])   Vote@voters
   right(inning_val()[es-threshold(es;
                                    simple_consensus_init();
                                    inning_step();
                                    inning_test(1);
                                    nxt_inning();
                                    Input+Vote)])   Output@clients



Definitions :  no_repeats: no_repeats(T;l) Id: Id equal: s = t length: ||as|| add: n + m multiply: n * m and: P  Q product: x:A  B[x] nat: es-interface-left: Error :es-interface-left,  es-weak-broadcast: Error :es-weak-broadcast,  int: es-interface-right: Error :es-interface-right,  es-filter-image: Error :es-filter-image,  es-threshold: Error :es-threshold,  natural_number: $n es-interface-union: Error :es-interface-union
FDL editor aliases :  onethird-consensus

onethird-consensus(es;t;Input;Vote;Output;voters;clients)  ==
    no\_repeats(Id;voters)
    \mwedge{}  (||voters||  =  ((3  *  t)  +  1))
    \mwedge{}  left(inning\_val()[es-threshold(es;
                                                                      simple\_consensus\_init();
                                                                      inning\_step();
                                                                      inning\_test(1);
                                                                      nxt\_inning();
                                                                      Input+Vote)])  \mLeftarrow{}{}\mRightarrow{}    Vote@voters
    \mwedge{}  right(inning\_val()[es-threshold(es;
                                                                        simple\_consensus\_init();
                                                                        inning\_step();
                                                                        inning\_test(1);
                                                                        nxt\_inning();
                                                                        Input+Vote)])  \mLeftarrow{}{}\mRightarrow{}    Output@clients


Date html generated: 2010_08_27-AM-09_40_57
Last ObjectModification: 2009_12_16-AM-09_59_31

Home Index