Nuprl Definition : Paxos-spec5-body

Paxos-spec5-body{i:l}(Info;
                      es;
                      T;
                      f;
                      acceptors;
                      Reserve;
                      VoteState;
                      Proposal;
                      Accept;
                      leader;
                      Decide;
                      OK;
                      Input) ==
  ((||acceptors|| = ((2 * f) + 1))

no_repeats(Id;acceptors))

((

e:E(VoteState)

e':E(Reserve)
(e' c

e

(loc(e')

acceptors)

(Reserve(e') = Reservation(VoteState(e)))

(loc(e') = Name(VoteState(e)))

MaxVote(es;T;Accept;e';Info(VoteState(e)))))

(

e1,e2:E(VoteState).
((Name(VoteState(e1)) = Name(VoteState(e2)))

(Reservation(VoteState(e1)) = Reservation(VoteState(e2)))

(e1 = e2))))

(

e:E(Proposal)
       let i = leader (fst(Proposal(e))) in
           e is first@ i s.t.
            q.||filter(

e'.(Reservation(VoteState(e')) =

fst(Proposal(e)));

(VoteState)(q))||
= (f + 1)

let l = filter(...;

(VoteState)(e)) in
let b' = imax-list(map(

e'.Ballot(VoteState(e'));l)) in
((b' = (-1))

(

e':E(Input). (e'

loc e

((snd(Proposal(e))) = Input(e')))))

((0

b')

(b' < (fst(Proposal(e))))

(

e'

l. Info(VoteState(e')) = (inl <b', snd(Proposal(e))> ))))

(

e:E(Accept)
((loc(e)

acceptors)

(

e':E(Reserve). (e'

loc e

(Reserve(e')

(fst(Accept(e))))))

(

e':E(Proposal). (e' c

e

(Proposal(e') = Accept(e))))))

(

e:E(OK).

e':E(Accept). (e' c

e

(OK(e) = <loc(e'), fst(Accept(e'))>)))

(

e1,e2:E(OK). ((OK(e1) = OK(e2))

(loc(e1) = loc(e2))

(e1 = e2)))

(

d:E(Decide)

b:

(d is first@ leader b s.t.
q.||filter(

e'.(snd(OK(e')) =

b);

(OK)(q))|| = (f + 1)

(

e:E(Proposal). ((e <loc d)

(Proposal(e) = <b, Decide(d)>)))))

Definitions : multiply: n * m, no_repeats: no_repeats(T;l), 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), paxos-state-ballot: Ballot(s), or: P

Q, minus: -n, less_than: a < b, l_exists: (

x

L. P[x]), union: left + right, unit: Unit, paxos-state-info: Info(s), inl: inl x , l_member: (x

l), es-le: e

loc e' , le: A

B, es-causle: e c

e', pi1: fst(t), implies: P

Q, Id: Id, es-loc: loc(e), es-E: E, all:

x:A. B[x], es-first-at: e is first@ i s.t. e.P[e], apply: f a, int:

, length: ||as||, filter: filter(P;l), lambda:

x.A[x], eq_int: (i =

j), pi2: snd(t), es-interface-predecessors:

(X)(e), add: n + m, natural_number: $n, exists:

x:A. B[x], es-E-interface: E(X), and: P

Q, es-locl: (e <loc e'), equal: s = t, product: x:A

B[x], nat:

, pair: <a, b>, eclass-val: X(e)

Paxos-spec5-body\{i:l\}(Info; es; T; f; acceptors; Reserve; VoteState; Proposal; Accept; leader; Decide; OK; Input) == ((||acceptors|| = ((2 * f) + 1)) \mwedge{} no\_repeats(Id;acceptors)) \mwedge{} ((\mforall{}e:E(VoteState) \mexists{}e':E(Reserve) (e' c\mleq{} e \mwedge{} (loc(e') \mmember{} acceptors) \mwedge{} (Reserve(e') = Reservation(VoteState(e))) \mwedge{} (loc(e') = Name(VoteState(e))) \mwedge{} MaxVote(es;T;Accept;e';Info(VoteState(e))))) \mwedge{} (\mforall{}e1,e2:E(VoteState). ((Name(VoteState(e1)) = Name(VoteState(e2))) {}\mRightarrow{} (Reservation(VoteState(e1)) = Reservation(VoteState(e2))) {}\mRightarrow{} (e1 = e2)))) \mwedge{} (\mforall{}e:E(Proposal) let i = leader (fst(Proposal(e))) in e is first@ i s.t. q.||filter(\mlambda{}e'.(Reservation(VoteState(e')) =\msubz{} fst(Proposal(e))); \mleq{}(VoteState)(q))|| = (f + 1) \mwedge{} let l = filter(\mlambda{}e'.(Reservation(VoteState(e')) =\msubz{} fst(Proposal(e)));\mleq{}(VoteState)(e)) in let b' = imax-list(map(\mlambda{}e'.Ballot(VoteState(e'));l)) in ((b' = (-1)) \mwedge{} (\mexists{}e':E(Input). (e' \mleq{}loc e \mwedge{} ((snd(Proposal(e))) = Input(e'))))) \mvee{} ((0 \mleq{} b') \mwedge{} (b' < (fst(Proposal(e)))) \mwedge{} (\mexists{}e'\mmember{}l. Info(VoteState(e')) = (inl <b', snd(Proposal(e))> )))) \mwedge{} (\mforall{}e:E(Accept) ((loc(e) \mmember{} acceptors) \mwedge{} (\mforall{}e':E(Reserve). (e' \mleq{}loc e {}\mRightarrow{} (Reserve(e') \mleq{} (fst(Accept(e)))))) \mwedge{} (\mexists{}e':E(Proposal). (e' c\mleq{} e \mwedge{} (Proposal(e') = Accept(e)))))) \mwedge{} (\mforall{}e:E(OK). \mexists{}e':E(Accept). (e' c\mleq{} e \mwedge{} (OK(e) = <loc(e'), fst(Accept(e'))>))) \mwedge{} (\mforall{}e1,e2:E(OK). ((OK(e1) = OK(e2)) {}\mRightarrow{} (loc(e1) = loc(e2)) {}\mRightarrow{} (e1 = e2))) \mwedge{} (\mforall{}d:E(Decide) \mexists{}b:\mBbbN{} (d is first@ leader b s.t. q.||filter(\mlambda{}e'.(snd(OK(e')) =\msubz{} b);\mleq{}(OK)(q))|| = (f + 1) \mwedge{} (\mexists{}e:E(Proposal). ((e <loc d) \mwedge{} (Proposal(e) = <b, Decide(d)>))))) Date html generated: 2010_08_28-PM-12_47_57 Last ObjectModification: 2010_04_16-PM-01_17_36 Home Index