This is a trivial example from the document "Teaching Conccurrency" that appeared in
ACM SIGACT News Volume 40, Issue 1 (March 2009), 58-62
A copy of that article is at
http://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf
It is also the example in Section 7.2 of "Proving Safety Properties", which is at
http://lamport.azurewebsites.net/tla/proving-safety.pdf