Skip to content

Commit 9a38c9b

Browse files
committed
Update copyright notice for the TLA model.
1 parent 2a7cdc6 commit 9a38c9b

1 file changed

Lines changed: 10 additions & 2 deletions

File tree

test/tla/README.md

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
# TLA+ Model for Syn Registry
22

3-
The TLA+ specification in this directory is based on [Graham Hay's syn_tla](https://github.com/grahamrhay/syn_tla),
4-
a formal model of Syn's distributed registry conflict resolution protocol.
3+
The TLA+ specifications in this directory were authored by [Graham Hay](https://github.com/grahamrhay/syn_tla)
4+
as a formal model of Syn's distributed registry conflict resolution protocol.
55

66
## The Bug
77

@@ -90,3 +90,11 @@ The model checks three properties:
9090
```
9191
java -cp tla2tools.jar tlc2.TLC -config syn_tests.cfg syn_tests.tla
9292
```
93+
94+
## Copyright
95+
96+
The TLA+ specifications in this directory were authored by
97+
[Graham Hay](https://github.com/grahamrhay) and are included here with minor modifications
98+
(the bug fix described above). The original model is available at
99+
https://github.com/grahamrhay/syn_tla. All rights to the original work remain with
100+
the author.

0 commit comments

Comments
 (0)