This folder shows Pluscal/TLA+ modeling of Voldemort distributed key value store.
VoldemortSimple modeling post http://muratbuffalo.blogspot.com/2016/11/modeling-replicated-storage-system-in.html
VoldChain modeling post (chain-replicated distributed k-v) http://muratbuffalo.blogspot.com/2016/12/tla-project2-solution-2016.html
To run these Pluscal/TLA+ models, you need the TLA+ toolkit, available at http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html
@muratdem
MIT license.