---

Paxos-spec7{i:l}(Info; es; T; leader; failset; Reserve; Decide; Input) ==
  f:
   acceptors:Id List
    VoteState:EClass(AcceptorState)
     Proposal:EClass(  T)
      AcceptOrReject:EClass(  T  )
       Vote:EClass(Id    )
        Collect:EClass(    T)
         NoProposal,NewBallot:EClass()
          Paxos-spec7-body{i:l}(Info;
                                es;
                                T;
                                f;
                                acceptors;
                                Reserve;
                                VoteState;
                                Proposal;
                                AcceptOrReject;
                                leader;
                                Decide;
                                Vote;
                                Input;
                                Collect;
                                NoProposal;
                                NewBallot;
                                failset)

---

Definitions :  nat_plus: ,  list: type List,  paxos-acceptor-state: AcceptorState,  Id: Id,  bool: ,  product: x:A  B[x],  int: ,  exists: x:A. B[x],  eclass: EClass(A[eo; e]),  nat: ,  Paxos-spec7-body: Paxos-spec7-body

---

Paxos-spec7\{i:l\}(Info;  es;  T;  leader;  failset;  Reserve;  Decide;  Input)  ==
    \mexists{}f:\mBbbN{}\msupplus{}
      \mexists{}acceptors:Id  List
        \mexists{}VoteState:EClass(AcceptorState)
          \mexists{}Proposal:EClass(\mBbbN{}  \mtimes{}  T)
            \mexists{}AcceptOrReject:EClass(\mBbbN{}  \mtimes{}  T  \mtimes{}  \mBbbB{})
              \mexists{}Vote:EClass(Id  \mtimes{}  \mBbbN{}  \mtimes{}  \mBbbB{})
                \mexists{}Collect:EClass(\mBbbN{}  \mtimes{}  \mBbbZ{}  \mtimes{}  T)
                  \mexists{}NoProposal,NewBallot:EClass(\mBbbN{})
                    Paxos-spec7-body\{i:l\}(Info;
                                                                es;
                                                                T;
                                                                f;
                                                                acceptors;
                                                                Reserve;
                                                                VoteState;
                                                                Proposal;
                                                                AcceptOrReject;
                                                                leader;
                                                                Decide;
                                                                Vote;
                                                                Input;
                                                                Collect;
                                                                NoProposal;
                                                                NewBallot;
                                                                failset)


Date html generated: 2010_08_28-PM-01_02_29
Last ObjectModification: 2010_04_17-PM-08_35_46

Home Index