Hi everyone! I have completed writing TLA+ specification for ZooKeeper.(see ZOOKEEPER-3615, with links <https://issues.apache.org/jira/browse/ZOOKEEPER-3615> and https://github.com/apache/zookeeper/pull/1690).
I have discussed this issue with community members on github, and now it has been shelved. I hope anyone interested in it could give me some suggestions for improvement, and finally merge this issue. Please communicate with me anytime if you have suggestions. Best wishes, Huang
