Nuprl Definition : pv8_p2_ReplicaState
pv8_p2_ReplicaState(Cid;Op;RepState;Result;apply_op;eq_Cid;init_rstate;ldrs) ==
SM2-class-du(
z.{<pv8_p2_init_replica(Cid;Op;RepState;init_rstate), {}>};
...;
<pv8_p2_out_tr(Cid;Op;RepState) pv8_p2_on_decision(Cid;Op;RepState;Result;apply_op;eq_Cid;ldrs)
, pv8_p2_decision'base(Cid;Op)
>)
Definitions occuring in Statement :
pv8_p2_on_decision: pv8_p2_on_decision(Cid;Op;RepState;Result;apply_op;eq_Cid;ldrs),
pv8_p2_propose: pv8_p2_propose(Cid;Op;RepState;eq_Cid;ldrs),
pv8_p2_init_replica: pv8_p2_init_replica(Cid;Op;RepState;init_rstate),
pv8_p2_decision'base: pv8_p2_decision'base(Cid;Op),
pv8_p2_request'base: pv8_p2_request'base(Cid;Op),
pv8_p2_out_tr: pv8_p2_out_tr(Cid;Op;RepState),
SM2-class-du: SM2-class-du,
apply: f a,
lambda: x.A[x],
pair: <a, b>,
single-bag: {x},
empty-bag: {}
FDL editor aliases :
pv8_p2_ReplicaState
pv8_p2_ReplicaState
pv8\_p2\_ReplicaState(Cid;Op;RepState;Result;apply$_{op}$;eq$_{Cid\mbackslash{}ff7\000Cd$;init$_{rstate}$;ldrs) ==
SM2-class-du(\mlambda{}z.\{<pv8\_p2\_init\_replica(Cid;Op;RepState;init$_{rstate}$), \{\}>\};
<pv8\_p2\_out\_tr(Cid;Op;RepState) pv8\_p2\_propose(Cid;Op;RepState;eq$_{Cid\mbackslash{}f\000Cf7d$;ldrs)
, pv8\_p2\_request'base(Cid;Op)
>
<pv8\_p2\_out\_tr(Cid;Op;RepState)
pv8\_p2\_on\_decision(Cid;Op;RepState;Result;apply$_{op}$;eq$\mbackslash{}f\000Cf5f{Cid}$;ldrs)
, pv8\_p2\_decision'base(Cid;Op)
>)
Date html generated:
2012_02_20-PM-07_41_00
Last ObjectModification:
2012_02_06-PM-03_07_53
Home
Index