From 76a456d66b4202fad25235a581fc1287d68f1cfa Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Sun, 21 Aug 2022 21:51:16 -0700 Subject: [PATCH] fix an attribution --- README.md | 2 +- specifications/Termination/README.md | 11 ++++++----- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index e84a40dd..3ba3181c 100644 --- a/README.md +++ b/README.md @@ -65,7 +65,7 @@ Do you have your own case study that you like to share with the community? Send | 51 | Stones | The same problem as CarTalkPuzzle | | | ✔ | FinSet, Int, Seq | | | 52 | sums_even | Two proofs for showing that x+x is even, for any natural number x. | | ✔ | ✔ | Int | | | 53 | SyncConsensus | Synchronized round consensus algorithm (Demirbas) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | -| 54 | Termination | Channel counting algorithm (Mattern, 1987) | Giuliano Losa | | ✔ | FinSet, Bags, Nat | ✔ | +| 54 | Termination | Channel-counting algorithm (Kumar, 1985) | Giuliano Losa | | ✔ | FinSet, Bags, Nat | ✔ | | 55 | Tla-tortoise-hare | Robert Floyd's cycle detection algorithm | Lorin Hochstein | | ✔ | Nat | ✔ | | 56 | tower_of_hanoi | The well-known Towers of Hanoi puzzle. | Markus Kuppe, Alexander Niederbühl | | ✔ | Bit, FinSet, Int, Nat, Seq | | | 57 | transaction_commit | Consensus on transaction commit (Gray & Lamport, 2006) | Leslie Lamport | | ✔ | Int | | diff --git a/specifications/Termination/README.md b/specifications/Termination/README.md index 8087f21d..5870a9c3 100644 --- a/specifications/Termination/README.md +++ b/specifications/Termination/README.md @@ -1,9 +1,10 @@ #### Termination - Specification's authors: Giuliano Losa -- Original paper: Mattern, Friedemann. Algorithms for distributed termination detection. Distributed computing 2.3 (1987): 161-175. -- Extended modules: FinSet, Bags, Nat -- Computation models: no faults -- Some properties checked with TLC: termination -- TLA+ files +- Original paper: Kumar, Devendra. *A class of termination detection algorithms for distributed computations.* International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, Berlin, Heidelberg, 1985. +- Also appears in: Mattern, Friedemann. Algorithms for distributed termination detection. Distributed computing 2.3 (1987): 161-175. +- Extended modules: Integers, FiniteSets, Apalache, Sequences +- Computation models: asynchronous without faults +- Some properties checked with Apalache: an inductive invariant implying safety (checked inductive for 5 processes) +- TLA+ files and explanations