Paxos-spec5{i:l}(Info; es; T; Decide; Input) ==
f:
acceptors:Id List
Reserve:EClass()
VoteState:EClass(AcceptorState)
Proposal,Accept:EClass( 
T)
leader: 
Id
OK:EClass(Id )
Paxos-spec5-body{i:l}(Info;
es;
T;
f;
acceptors;
Reserve;
VoteState;
Proposal;
Accept;
leader;
Decide;
OK;
Input)
Definitions :
list: type List,
paxos-acceptor-state: AcceptorState,
function: x:A B[x],
exists: x:A. B[x],
eclass: EClass(A[eo; e]),
product: x:A B[x],
Id: Id,
nat: ,
Paxos-spec5-body: Paxos-spec5-body
Paxos-spec5\{i:l\}(Info; es; T; Decide; Input) ==
\mexists{}f:\mBbbN{}
\mexists{}acceptors:Id List
\mexists{}Reserve:EClass(\mBbbN{})
\mexists{}VoteState:EClass(AcceptorState)
\mexists{}Proposal,Accept:EClass(\mBbbN{} \mtimes{} T)
\mexists{}leader:\mBbbN{} {}\mrightarrow{} Id
\mexists{}OK:EClass(Id \mtimes{} \mBbbN{})
Paxos-spec5-body\{i:l\}(Info;
es;
T;
f;
acceptors;
Reserve;
VoteState;
Proposal;
Accept;
leader;
Decide;
OK;
Input)
Date html generated:
2010_08_28-PM-12_48_04
Last ObjectModification:
2010_04_16-PM-01_21_58
Home
Index