Skip to content

Instantly share code, notes, and snippets.

@grogers0

grogers0/GryadkaCasRegister_accept.tla

Created May 31, 2017 23:05
Show Gist options
  • Save grogers0/76fd651d2927b77a23079fe2170dc5bf to your computer and use it in GitHub Desktop.
Save grogers0/76fd651d2927b77a23079fe2170dc5bf to your computer and use it in GitHub Desktop.
Download ZIP
Raw
GryadkaCasRegister_accept.tla
PromisedValue(ts) == LET promiseMsgs == SelectMessages("promise", ts)
IN (CHOOSE m \in promiseMsgs : \A m2 \in promiseMsgs : m.prevTS >= m2.prevTS).prevVal
Accept(ts) == /\ {m.acceptor : m \in SelectMessages("promise", ts)} \in Quorums
/\ ops[ts].oldVal = PromisedValue(ts)
/\ msgs' = msgs \union [type: {"accept"}, acceptor: Acceptors, ts: {ts}, val: {ops[ts].newVal}]
/\ UNCHANGED <<ops, acceptorTS, acceptorValTS, acceptorValue, history>>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment