BinyuHuang-nju commented on a change in pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#discussion_r630750303
##########
File path: zookeeper-contrib/zookeeper-contrib-zabtla/README.md
##########
@@ -0,0 +1,71 @@
+# Zab-tla
+
+## Overview
+This project is devoted to providing formal specification and verification
using TLA+ for the Zookeeper Atomic Broadcast(Zab) consensus protocol proposed
in *Junqueira F P, Reed B C, Serafini M. Zab: High-performance broadcast for
primary-backup systems[C]//2011 IEEE/IFIP 41st International Conference on
Dependable Systems & Networks (DSN). IEEE, 2011: 245-256*.
+
+We have made a formal [specification](Zab.tla) for Zab using TLA+ toolbox, and
we have done a certain scale of model checking to verify the correctness of Zab.
+
+Due to the simplification of Zab algorithm description in the paper, some
details in specification were modified and added. If you have any question,
please let us know.
+
+You can find this document in chinese in
[doc-in-chinsese](doc-in-chinese/README.md).
+
+## Requirements
+TLA+ toolbox version 1.7.0
+
+## Run
+Create specification and run models in the usual way.
Review comment:
Thank you! I can write a more detailed manual in README about how to
configure TLC parameters. Since the .toolbox space is too large, I can upload
some more important files in .toolbox folder(such as .settings, .projejct,
Model/MC.tla, Model/MC.cfg).
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
[email protected]
