---

Paxos-spec3-body{i:l}(Info;
                      es;
                      T;
                      f;
                      acceptors;
                      Reserve;
                      VoteState;
                      Proposal;
                      Accept;
                      leader;
                      Decide) ==
  ((||acceptors|| = ((2 * f) + 1))  no_repeats(Id;acceptors))
   ((e:E(VoteState)
        e':E(Reserve)
         ((loc(e')  acceptors)
          (Reserve(e') = Reservation(VoteState(e)))
          (loc(e') = Name(VoteState(e)))
          MaxVote(es;T;Accept;e';Info(VoteState(e)))))
     (e1,e2:E(VoteState).
         ((Name(VoteState(e1)) = Name(VoteState(e2)))
          (Reservation(VoteState(e1)) = Reservation(VoteState(e2)))
          (e1 = e2))))
   (e:E(Proposal)
       let i = leader (fst(Proposal(e))) in
           e is first@ i s.t. 
            q.||filter(e'.(Reservation(VoteState(e')) = fst(Proposal(e)));
                       (VoteState)(q))||
           = (f + 1)
            let l = filter(...;(VoteState)(e)) in
              let b' = imax-list(map(e'.Ballot(VoteState(e'));l)) in
              (b' = (-1))
               ((0  b')
                 (b' < (fst(Proposal(e))))
                 (e'l. Info(VoteState(e')) = (inl <b', snd(Proposal(e))> ))))
   (e:E(Accept)
       ((loc(e)  acceptors)
        (e':E(Reserve). (e' loc e   (Reserve(e')  (fst(Accept(e))))))
        (e':E(Proposal). (Proposal(e') = Accept(e)))))
   (d:E(Decide)
       Q:Id List
        (((||Q|| = (f + 1))  no_repeats(Id;Q))
         (b:
            (aQ.e:E(Accept)
                   ((loc(e) = a)  (Accept(e) = <b, Decide(d)>))))))

---

Definitions :  multiply: n * m,  MaxVote: MaxVote(es;T;Vote;e;s),  paxos-state-name: Name(s),  es-E: E,  apply: f a,  es-first-at: e is first@ i s.t.  e.P[e],  filter: filter(P;l),  eq_int: (i = j),  paxos-state-reservation: Reservation(s),  es-interface-predecessors: (X)(e),  let: let,  imax-list: imax-list(L),  map: map(f;as),  lambda: x.A[x],  paxos-state-ballot: Ballot(s),  or: P  Q,  minus: -n,  less_than: a < b,  l_exists: (xL. P[x]),  union: left + right,  unit: Unit,  paxos-state-info: Info(s),  inl: inl x ,  pi2: snd(t),  l_member: (x  l),  implies: P  Q,  es-le: e loc e' ,  le: A  B,  pi1: fst(t),  all: x:A. B[x],  list: type List,  int: ,  length: ||as||,  add: n + m,  natural_number: $n,  no_repeats: no_repeats(T;l),  l_all: (xL.P[x]),  exists: x:A. B[x],  es-E-interface: E(X),  and: P  Q,  Id: Id,  es-loc: loc(e),  equal: s = t,  product: x:A  B[x],  nat: ,  pair: <a, b>,  eclass-val: X(e)

---

Paxos-spec3-body\{i:l\}(Info;
                                            es;
                                            T;
                                            f;
                                            acceptors;
                                            Reserve;
                                            VoteState;
                                            Proposal;
                                            Accept;
                                            leader;
                                            Decide)  ==
    ((||acceptors||  =  ((2  *  f)  +  1))  \mwedge{}  no\_repeats(Id;acceptors))
    \mwedge{}  ((\mforall{}e:E(VoteState)
                \mexists{}e':E(Reserve)
                  ((loc(e')  \mmember{}  acceptors)
                  \mwedge{}  (Reserve(e')  =  Reservation(VoteState(e)))
                  \mwedge{}  (loc(e')  =  Name(VoteState(e)))
                  \mwedge{}  MaxVote(es;T;Accept;e';Info(VoteState(e)))))
        \mwedge{}  (\mforall{}e1,e2:E(VoteState).
                  ((Name(VoteState(e1))  =  Name(VoteState(e2)))
                  {}\mRightarrow{}  (Reservation(VoteState(e1))  =  Reservation(VoteState(e2)))
                  {}\mRightarrow{}  (e1  =  e2))))
    \mwedge{}  (\mforall{}e:E(Proposal)
              let  i  =  leader  (fst(Proposal(e)))  in
                      e  is  first@  i  s.t.    q.||filter(\mlambda{}e'.(Reservation(VoteState(e'))  =\msubz{}  fst(Proposal(e)));
                                                                                    \mleq{}(VoteState)(q))||
                      =  (f  +  1)
                      \mwedge{}  let  l  =  filter(\mlambda{}e'.(Reservation(VoteState(e'))  =\msubz{}  fst(Proposal(e)));\mleq{}(VoteState)(e))  in
                            let  b'  =  imax-list(map(\mlambda{}e'.Ballot(VoteState(e'));l))  in
                            (b'  =  (-1))
                            \mvee{}  ((0  \mleq{}  b')
                                \mwedge{}  (b'  <  (fst(Proposal(e))))
                                \mwedge{}  (\mexists{}e'\mmember{}l.  Info(VoteState(e'))  =  (inl  <b',  snd(Proposal(e))>  ))))
    \mwedge{}  (\mforall{}e:E(Accept)
              ((loc(e)  \mmember{}  acceptors)
              \mwedge{}  (\mforall{}e':E(Reserve).  (e'  \mleq{}loc  e    {}\mRightarrow{}  (Reserve(e')  \mleq{}  (fst(Accept(e))))))
              \mwedge{}  (\mexists{}e':E(Proposal).  (Proposal(e')  =  Accept(e)))))
    \mwedge{}  (\mforall{}d:E(Decide)
              \mexists{}Q:Id  List
                (((||Q||  =  (f  +  1))  \mwedge{}  no\_repeats(Id;Q))
                \mwedge{}  (\mexists{}b:\mBbbN{}.  (\mforall{}a\mmember{}Q.\mexists{}e:E(Accept).  ((loc(e)  =  a)  \mwedge{}  (Accept(e)  =  <b,  Decide(d)>))))))


Date html generated: 2010_08_28-PM-12_47_02
Last ObjectModification: 2010_04_16-AM-11_44_49

Home Index