Add TLAPS check mark to Termination entry and fix unrelated comment (#…

…111) * Add TLAPS checkmark to Termination entry Signed-off-by: Giuliano Losa <[email protected]> * fix comment in Paxos Signed-off-by: Giuliano Losa <[email protected]> --------- Signed-off-by: Giuliano Losa <[email protected]>
tlaplus · Jan 20, 2024 · adccef9 · adccef9
1 parent a46ca79
commit adccef9
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -117,7 +117,7 @@ Ideally these will be moved into this repo over time.
 | [raft](specifications/raft)                                                                                                       | Raft consensus algorithm (Ongaro, 2014)                                                                                                   | Diego Ongaro                                                                   |              |     ✔      |          |           |
 | [SnapshotIsolation](specifications/SnapshotIsolation)                                                                             | Serializable snapshot isolation (Cahill et al., 2010)                                                                                     | Michael J. Cahill, Uwe Röhm, Alan D. Fekete                                    |              |     ✔      |          |           |
 | [SyncConsensus](specifications/SyncConsensus)                                                                                     | Synchronized round consensus algorithm (Demirbas)                                                                                         | Murat Demirbas                                                                 |              |     ✔      |    ✔     |           |
-| [Termination](specifications/Termination)                                                                                         | Channel-counting algorithm (Kumar, 1985)                                                                                                  | Giuliano Losa                                                                  |              |     ✔      |    ✔     |     ✔     |
+| [Termination](specifications/Termination)                                                                                         | Channel-counting algorithm (Kumar, 1985)                                                                                                  | Giuliano Losa                                                                  |      ✔       |     ✔      |    ✔     |     ✔     |
 | [Tla-tortoise-hare](specifications/Tla-tortoise-hare)                                                                             | Robert Floyd's cycle detection algorithm                                                                                                  | Lorin Hochstein                                                                |              |     ✔      |    ✔     |           |
 | [VoldemortKV](specifications/VoldemortKV)                                                                                         | Voldemort distributed key value store                                                                                                     | Murat Demirbas                                                                 |              |     ✔      |    ✔     |           |
 | [Tencent-Paxos](specifications/TencentPaxos)                                                                                      | PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017)                     | Xingchen Yi, Hengfeng Wei                                                      |      ✔       |     ✔      |          |           |

diff --git a/specifications/Paxos/Paxos.tla b/specifications/Paxos/Paxos.tla
@@ -17,7 +17,7 @@ Ballot ==  Nat
 
 None == CHOOSE v : v \notin Value
   (*************************************************************************)
-  (* An unspecified value that is not a ballot number.                     *)
+  (* An unspecified value that is not a choosable value.                   *)
   (*************************************************************************)
 
 (***************************************************************************)