paxos-decide-def(es;f;leader;T;Decide;Proposal;Vote) ==
b,d such that d is first@ leader b s.t.
q.||filter(
e'.((snd(fst(Vote(e'))) =
b)
snd(Vote(e')) =b tt);
(Vote)(q))||
= (f + 1)
((
d 
(Proposal)') ((fst((Proposal)'(d))) = b))
e'<d.(e' Vote)
(((snd(fst(Vote(e')))) b)
(((snd(fst(Vote(e')))) = b) ((snd(Vote(e'))) = tt)))
dDecide with value snd((Proposal)'(d))
Definitions :
es-class-def: es-class-def,
nat: 
,
es-first-at: e is first@ i s.t. e.P[e],
apply: f a,
length: ||as||,
filter: filter(P;l),
lambda: x.A[x],
band: p q,
eq_int: (i = j),
eq_bool: p =b q,
es-interface-predecessors: (X)(e),
add: n + m,
natural_number: $n,
alle-lt: e<e'.P[e],
assert: b,
in-eclass: e X,
and: P Q,
le: A B,
implies: P Q,
int: 
,
pi1: fst(t),
equal: s = t,
bool: 
,
btrue: tt,
pi2: snd(t),
eclass-val: X(e),
es-prior-val: (X)'
FDL editor aliases :
paxos-decide-def
paxos-decide-def(es;f;leader;T;Decide;Proposal;Vote) ==
\mforall{}b,d such that d is first@ leader b s.t. q.||filter(\mlambda{}e'.((snd(fst(Vote(e'))) =\msubz{} b)
\mwedge{}\msubb{} snd(Vote(e')) =b tt);\mleq{}(Vote)(q))||
= (f + 1)
\mwedge{} ((\muparrow{}d \mmember{}\msubb{} (Proposal)') \mwedge{} ((fst((Proposal)'(d))) = b))
\mwedge{} \mforall{}e'<d.(\muparrow{}e' \mmember{}\msubb{} Vote)
{}\mRightarrow{} (((snd(fst(Vote(e')))) \mleq{} b) \mwedge{} (((snd(fst(Vote(e')))) = b) {}\mRightarrow{} ((snd(Vote(e'))) = tt)))
d\mmember{}Decide with value snd((Proposal)'(d))
Date html generated:
2010_08_28-PM-12_48_53
Last ObjectModification:
2010_04_16-PM-02_04_49
Home
Index