diff --git a/README.md b/README.md index 3085635..ea403d8 100644 --- a/README.md +++ b/README.md @@ -11,9 +11,7 @@ e.g. understanding why a process "gives its turn away." For a pretty-printed PDF version, see [https://github.com/changlinli/peterson-tlaplus/releases/download/v1.1/Peterson.pdf](https://github.com/changlinli/peterson-tlaplus/releases/download/v1.1/Peterson.pdf). -This is meant as an intermediate introduction to TLA+ users. An example is -someone who has just finished Leslie Lamport's video course on TLA+. The -specification also has a lot of comments which I hope help even non-TLA+ users +This specification may seem long, but it is largely comments, which I hope help even non-TLA+ users understand the intuition behind Peterson's algorithm better. Note that I've chosen to take a loose translation of Peterson's algorithm as it