---

Paxos-properties(es;T;Decide;Input;Reserve;leader;failset) ==
  Decide values come from Input values
   Consistent(Decide)
   (Finitely many leaders
     (ldr:Id
         (((ldr  failset))
          eventually ldr is the only leader
          (n:E(Input). (loc(n) = ldr))))
     (d:E. (d  Decide)))

---

Definitions :  in-eclass: e  X,  assert: b,  es-E: E,  exists: x:A. B[x],  es-loc: loc(e),  Id: Id,  equal: s = t,  es-E-interface: E(X),  eventually-one-leader: eventually ldr is the only leader,  and: P  Q,  l_member: (x  l),  not: A,  implies: P  Q,  leaders-finite: Finitely many leaders,  consensus-spec1: Consistent(Decide),  consensus-spec2: Decide values come from Input values
FDL editor aliases :  Paxos-properties

---

Paxos-properties(es;T;Decide;Input;Reserve;leader;failset)  ==
    Decide  values  come  from  Input  values
    \mwedge{}  Consistent(Decide)
    \mwedge{}  (Finitely  many  leaders
        {}\mRightarrow{}  (\mexists{}ldr:Id
                  ((\mneg{}(ldr  \mmember{}  failset))  \mwedge{}  eventually  ldr  is  the  only  leader  \mwedge{}  (\mexists{}n:E(Input).  (loc(n)  =  ldr))))
        {}\mRightarrow{}  (\mexists{}d:E.  (\muparrow{}d  \mmember{}\msubb{}  Decide)))


Date html generated: 2010_08_30-AM-12_59_45
Last ObjectModification: 2010_08_24-PM-05_14_00

Home Index