hanm commented on a change in pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#discussion_r631473566
##########
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:
Yeah, please don't feel any pressures and take your time. I'll also take
some time to comment on details of the spec this week, I think even it's not
ZAB 1.0 the relevant experience are valuable when we make the 1.0 spec.
--
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]
