Skip to content

Instantly share code, notes, and snippets.

@grogers0

grogers0/GryadkaCasRegister_recv_accept.tla

Created May 31, 2017 23:19
Show Gist options
  • Save grogers0/451c2a328a30094a25fff08c954aaf14 to your computer and use it in GitHub Desktop.
Save grogers0/451c2a328a30094a25fff08c954aaf14 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
GryadkaCasRegister_recv_accept.tla
RecvAccept(a, ts, v) == /\ acceptorTS[a] = ts
/\ acceptorValTS' = [acceptorValTS EXCEPT ![a] = ts]
/\ acceptorValue' = [acceptorValue EXCEPT ![a] = v]
/\ msgs' = msgs \union [type: {"accepted"}, acceptor: {a}, ts: {ts}, val: {v}]
/\ UNCHANGED <<ops, acceptorTS, history>>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment