Skip to content

Commit

Permalink
fix an attribution
Browse files Browse the repository at this point in the history
  • Loading branch information
@nano-o
nano-o committed Aug 22, 2022
1 parent 075ae44 commit 76a456d
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 6 deletions.
2 changes: 1 addition & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ Do you have your own case study that you like to share with the community? Send
| 51 | Stones | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/Stones">The same problem as CarTalkPuzzle</a> | | | &#10004; | FinSet, Int, Seq | |
| 52 | sums_even | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/sums_even">Two proofs for showing that x+x is even, for any natural number x.</a> | | &#10004; | &#10004; | Int | |
| 53 | SyncConsensus | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/SyncConsensus">Synchronized round consensus algorithm (Demirbas)</a> | Murat Demirbas | | &#10004; | FinSet, Int, Seq | &#10004; |
| 54 | Termination | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/Termination">Channel counting algorithm (Mattern, 1987)</a> | Giuliano Losa | | &#10004; | FinSet, Bags, Nat | &#10004; |
| 54 | Termination | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/Termination">Channel-counting algorithm (Kumar, 1985)</a> | Giuliano Losa | | &#10004; | FinSet, Bags, Nat | &#10004; |
| 55 | Tla-tortoise-hare | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/Tla-tortoise-hare">Robert Floyd's cycle detection algorithm</a> | Lorin Hochstein | | &#10004; | Nat | &#10004; |
| 56 | tower_of_hanoi | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/tower_of_hanoi">The well-known Towers of Hanoi puzzle.</a> | Markus Kuppe, Alexander Niederbühl | | &#10004; | Bit, FinSet, Int, Nat, Seq | |
| 57 | transaction_commit | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/transaction_commit">Consensus on transaction commit (Gray & Lamport, 2006)</a> | Leslie Lamport | | &#10004; | Int | |
Expand Down
11 changes: 6 additions & 5 deletions specifications/Termination/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
#### <a href="https://github.com/nano-o/Distributed-termination-detection">Termination</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://link.springer.com/article/10.1007/BF01782776">Mattern, Friedemann. Algorithms for distributed termination detection. Distributed computing 2.3 (1987): 161-175.</a>
- Extended modules: FinSet, Bags, Nat
- Computation models: no faults
- Some properties checked with TLC: termination
- <a href="https://github.com/nano-o/Distributed-termination-detection">TLA<sup>+</sup> files</a>
- Original paper: <a href="https://link.springer.com/chapter/10.1007/3-540-16042-6_4">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.</a>
- Also appears in: <a href="https://link.springer.com/article/10.1007/BF01782776">Mattern, Friedemann. Algorithms for distributed termination detection. Distributed computing 2.3 (1987): 161-175.</a>
- 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)
- <a href="https://github.com/nano-o/Distributed-termination-detection">TLA<sup>+</sup> files and explanations</a>


0 comments on commit 76a456d

Please sign in to comment.