---

Paxos-spec2-body{i:l}(Info;es;T;Reserve;VoteState;Proposal;Vote;W;Decide) ==
  (e:E(VoteState)
     e':E(Reserve)
      ((Reserve(e') = Reservation(VoteState(e)))
       (loc(e') = Name(VoteState(e)))
       MaxVote(es;T;Vote;e';Info(VoteState(e)))))
   (ws1W.(ws2W.a:Id. ((a  ws1)  (a  ws2))))
   (e:E(Proposal)
       Q:Id List
        ((Q  W)
         (l:E(VoteState) List
            ((aQ.(e'l. (Name(VoteState(e')) = a)
                 (Reservation(VoteState(e')) = (fst(Proposal(e))))))
             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))> )))))))
   (e1,e2:E(Proposal).
       (((fst(Proposal(e1))) = (fst(Proposal(e2))))
        (Proposal(e1) = Proposal(e2))))
   (e:E(Vote)
       ((e':E(Reserve). (e' loc e   (Reserve(e')  (fst(Vote(e))))))
        (e':E(Proposal). (Proposal(e') = Vote(e)))))
   (d:E(Decide)
       Q:Id List
        ((Q  W)
         (b:
            (aQ.e:E(Vote). ((loc(e) = a)  (Vote(e) = <b, Decide(d)>))))))

---

Definitions :  MaxVote: MaxVote(es;T;Vote;e;s),  paxos-state-name: Name(s),  paxos-state-reservation: Reservation(s),  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,  natural_number: $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),  int: ,  implies: P  Q,  es-le: e loc e' ,  le: A  B,  pi1: fst(t),  all: x:A. B[x],  l_member: (x  l),  list: type List,  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)
FDL editor aliases :  Paxos-spec2-body

---

Paxos-spec2-body\{i:l\}(Info;es;T;Reserve;VoteState;Proposal;Vote;W;Decide)  ==
    (\mforall{}e:E(VoteState)
          \mexists{}e':E(Reserve)
            ((Reserve(e')  =  Reservation(VoteState(e)))
            \mwedge{}  (loc(e')  =  Name(VoteState(e)))
            \mwedge{}  MaxVote(es;T;Vote;e';Info(VoteState(e)))))
    \mwedge{}  (\mforall{}ws1\mmember{}W.(\mforall{}ws2\mmember{}W.\mexists{}a:Id.  ((a  \mmember{}  ws1)  \mwedge{}  (a  \mmember{}  ws2))))
    \mwedge{}  (\mforall{}e:E(Proposal)
              \mexists{}Q:Id  List
                ((Q  \mmember{}  W)
                \mwedge{}  (\mexists{}l:E(VoteState)  List
                        ((\mforall{}a\mmember{}Q.(\mexists{}e'\mmember{}l.  (Name(VoteState(e'))  =  a)
                                \mwedge{}  (Reservation(VoteState(e'))  =  (fst(Proposal(e))))))
                        \mwedge{}  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{}e1,e2:E(Proposal).
              (((fst(Proposal(e1)))  =  (fst(Proposal(e2))))  {}\mRightarrow{}  (Proposal(e1)  =  Proposal(e2))))
    \mwedge{}  (\mforall{}e:E(Vote)
              ((\mforall{}e':E(Reserve).  (e'  \mleq{}loc  e    {}\mRightarrow{}  (Reserve(e')  \mleq{}  (fst(Vote(e))))))
              \mwedge{}  (\mexists{}e':E(Proposal).  (Proposal(e')  =  Vote(e)))))
    \mwedge{}  (\mforall{}d:E(Decide)
              \mexists{}Q:Id  List
                ((Q  \mmember{}  W)  \mwedge{}  (\mexists{}b:\mBbbN{}.  (\mforall{}a\mmember{}Q.\mexists{}e:E(Vote).  ((loc(e)  =  a)  \mwedge{}  (Vote(e)  =  <b,  Decide(d)>))))))


Date html generated: 2010_08_28-PM-12_46_41
Last ObjectModification: 2010_04_16-AM-10_49_45

Home Index