Skip to content

Instantly share code, notes, and snippets.

@grogers0

grogers0/GryadkaCasRegister_next_state_relation.tla

Last active May 31, 2017 22:44
Show Gist options
  • Save grogers0/44b9ca7c1a38f38f992925800c79472e to your computer and use it in GitHub Desktop.
Save grogers0/44b9ca7c1a38f38f992925800c79472e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
GryadkaCasRegister_next_state_relation.tla
Next == \/ \E ts \in Timestamps : \/ Prepare(ts)
\/ Accept(ts)
\/ Accepted(ts)
\/ \E m \in msgs : \/ m.type = "prepare" /\ RecvPrepare(m.acceptor, m.ts)
\/ m.type = "accept" /\ RecvAccept(m.acceptor, m.ts, m.val)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment