This is an automated email from the ASF dual-hosted git repository.
tison pushed a commit to branch master
in repository https://gitbox.apache.org/repos/asf/zookeeper.git
The following commit(s) were added to refs/heads/master by this push:
new de6762c1f ZOOKEEPER-3615: [ADDENDUM] fix rat error (#2013)
de6762c1f is described below
commit de6762c1f0e1a0d7b0dec0c79b67378df44f738d
Author: Kezhu Wang <[email protected]>
AuthorDate: Sat Jun 17 13:31:45 2023 +0800
ZOOKEEPER-3615: [ADDENDUM] fix rat error (#2013)
---
zookeeper-specifications/protocol-spec/Zab.tla | 20 +++++++++++++++++++-
zookeeper-specifications/protocol-spec/doc.md | 18 ++++++++++++++++++
zookeeper-specifications/protocol-spec/issues.md | 18 ++++++++++++++++++
.../protocol-spec/verification-statistics.md | 18 ++++++++++++++++++
zookeeper-specifications/system-spec/doc.md | 18 ++++++++++++++++++
.../system-spec/zk-3.7/FastLeaderElection.tla | 18 ++++++++++++++++++
.../system-spec/zk-3.7/ZkV3_7_0.tla | 18 ++++++++++++++++++
7 files changed, 127 insertions(+), 1 deletion(-)
diff --git a/zookeeper-specifications/protocol-spec/Zab.tla
b/zookeeper-specifications/protocol-spec/Zab.tla
index 4016f08e1..25379f550 100644
--- a/zookeeper-specifications/protocol-spec/Zab.tla
+++ b/zookeeper-specifications/protocol-spec/Zab.tla
@@ -1,3 +1,21 @@
+(*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *)
+
-------------------------------- MODULE Zab ---------------------------------
(* This is the formal specification for the Zab consensus algorithm,
in DSN'2011, which represents protocol specification in our work.*)
@@ -1230,4 +1248,4 @@ PrimaryIntegrity == \A i, j \in Server: /\ IsLeader(i)
/\ IsMyLearner(i, j)
\* Modification History
\* Last modified Tue Jan 31 20:40:11 CST 2023 by huangbinyu
\* Last modified Sat Dec 11 22:31:08 CST 2021 by Dell
-\* Created Thu Dec 02 20:49:23 CST 2021 by Dell
\ No newline at end of file
+\* Created Thu Dec 02 20:49:23 CST 2021 by Dell
diff --git a/zookeeper-specifications/protocol-spec/doc.md
b/zookeeper-specifications/protocol-spec/doc.md
index 1c351de1d..f4bb09b34 100644
--- a/zookeeper-specifications/protocol-spec/doc.md
+++ b/zookeeper-specifications/protocol-spec/doc.md
@@ -1,3 +1,21 @@
+<!--
+Licensed to the Apache Software Foundation (ASF) under one
+or more contributor license agreements. See the NOTICE file
+distributed with this work for additional information
+regarding copyright ownership. The ASF licenses this file
+to you under the Apache License, Version 2.0 (the
+"License"); you may not use this file except in compliance
+with the License. You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+//-->
+
# ZooKeeper's Protocol Specification of TLA+
## Overview
diff --git a/zookeeper-specifications/protocol-spec/issues.md
b/zookeeper-specifications/protocol-spec/issues.md
index 6d7b41c93..559434dd9 100644
--- a/zookeeper-specifications/protocol-spec/issues.md
+++ b/zookeeper-specifications/protocol-spec/issues.md
@@ -1,3 +1,21 @@
+<!--
+Licensed to the Apache Software Foundation (ASF) under one
+or more contributor license agreements. See the NOTICE file
+distributed with this work for additional information
+regarding copyright ownership. The ASF licenses this file
+to you under the Apache License, Version 2.0 (the
+"License"); you may not use this file except in compliance
+with the License. You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+//-->
+
# Issues
>This document describes issues related to the ambiguous description of the
>Zab protocol.
diff --git a/zookeeper-specifications/protocol-spec/verification-statistics.md
b/zookeeper-specifications/protocol-spec/verification-statistics.md
index b7cc02746..df7d0f1b9 100644
--- a/zookeeper-specifications/protocol-spec/verification-statistics.md
+++ b/zookeeper-specifications/protocol-spec/verification-statistics.md
@@ -1,3 +1,21 @@
+<!--
+Licensed to the Apache Software Foundation (ASF) under one
+or more contributor license agreements. See the NOTICE file
+distributed with this work for additional information
+regarding copyright ownership. The ASF licenses this file
+to you under the Apache License, Version 2.0 (the
+"License"); you may not use this file except in compliance
+with the License. You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+//-->
+
# Verification Statistics
##### Experiment configuration
diff --git a/zookeeper-specifications/system-spec/doc.md
b/zookeeper-specifications/system-spec/doc.md
index c30ec1d54..1a7d33b72 100644
--- a/zookeeper-specifications/system-spec/doc.md
+++ b/zookeeper-specifications/system-spec/doc.md
@@ -1,3 +1,21 @@
+<!--
+Licensed to the Apache Software Foundation (ASF) under one
+or more contributor license agreements. See the NOTICE file
+distributed with this work for additional information
+regarding copyright ownership. The ASF licenses this file
+to you under the Apache License, Version 2.0 (the
+"License"); you may not use this file except in compliance
+with the License. You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+//-->
+
# ZooKeeper's System Specification of TLA+
## Overview
diff --git a/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla
b/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla
index 753ba96ef..a5a44ba2c 100644
--- a/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla
+++ b/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla
@@ -1,3 +1,21 @@
+(*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *)
+
------------------------- MODULE FastLeaderElection -------------------------
\* This is the formal specification for Fast Leader Election in Zab protocol.
(* Reference:
diff --git a/zookeeper-specifications/system-spec/zk-3.7/ZkV3_7_0.tla
b/zookeeper-specifications/system-spec/zk-3.7/ZkV3_7_0.tla
index 060ed3d0a..cf8ca8fa1 100644
--- a/zookeeper-specifications/system-spec/zk-3.7/ZkV3_7_0.tla
+++ b/zookeeper-specifications/system-spec/zk-3.7/ZkV3_7_0.tla
@@ -1,3 +1,21 @@
+(*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *)
+
------------------------------ MODULE ZkV3_7_0 ------------------------------
(* This is the system specification for Zab in apache/zookeeper with version
3.7.0 *)
