---

Paxos-spec6{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-spec6-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-spec6-body: Paxos-spec6-body

---

Paxos-spec6\{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-spec6-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-12_49_27
Last ObjectModification: 2010_04_16-PM-02_47_18

Home Index