BinyuHuang-nju commented on a change in pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#discussion_r634132822
##########
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:
Hi there! I have modified the project according to your requirements.
Due to the insertion of Apache License in spec, I forgot to modify the line
number in README (offset 17 lines backward). I will modify this minor issue in
future commits. If you have any questions, please let me know.
Next, I will take time to learn about ZAB 1.0. And if necessary, I will
optimize spec from the perspective of explosive state space of model checking,
and this may be a relatively long work.
By the way, since zookeeper-specifications is a new folder, Travis CI
rejects this commit at the beginning of building. Could you please tell me how
to pass it?(Actually I haven't touched Travis CI before) Thank you!
--
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]
