hanm commented on a change in pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#discussion_r634909509
##########
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:
New folder structure looks awesome.
Travis CI failed because some newly introduced files missing Apache license
(same reason Travis failed the first time for this pull request):
`[WARNING] Files with unapproved licenses:
zookeeper-specifications/zab/Zab.toolbox/Model_1/MC.cfg
zookeeper-specifications/zab/Zab.toolbox/Zab.aux
zookeeper-specifications/zab/Zab.toolbox/Zab.tex
zookeeper-specifications/zab/experiment/ZabWithQTest2.toolbox/ZabWithQTest2.tex
zookeeper-specifications/zab/experiment/ZabWithQTest2.toolbox/ZabWithQTest2.aux
zookeeper-specifications/zab/experiment/ZabWithQTest2.toolbox/Model_1/MC.cfg
zookeeper-specifications/zab/experiment/ZabWithQTest.toolbox/ZabWithQTest.tex
zookeeper-specifications/zab/experiment/ZabWithQTest.toolbox/ZabWithQTest.aux
zookeeper-specifications/zab/experiment/ZabWithQTest.toolbox/Model_1/MC.cfg
[ERROR] Failed to execute goal org.apache.rat:apache-rat-plugin:0.13:check
(default-cli) on project parent: Too many files with unapproved license: 9 See
RAT report in: /home/travis/build/apache/zookeeper/target/rat.txt -> [Help 1]
`
Add license header to these files should make the build pass.
To debug Travis issue - simply click the "Details" link and then go to the
job page (in this case it's
https://travis-ci.com/github/apache/zookeeper/jobs/506036712), and check the
log for specific errors.
--
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]
