Merge branch 'master' of github.com:changlinli/peterson-tlaplus

README.md

@@ -4,12 +4,14 @@ This repository contains a TLA specification of [Peterson's
 algorithm](https://en.wikipedia.org/wiki/Peterson%27s_algorithm), an algorithm
 that allows multiple processes to share a single-use resource without conflict.
 
+Peterson's algorithm is one of the simplest mutual exclusion concurrency 
+algorithms out there, but already has some potentially non-intuitive components,
+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.0/Peterson.pdf](https://github.com/changlinli/peterson-tlaplus/releases/download/v1.0/Peterson.pdf).
+[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