Missionaries and Cannibals
   This is a very simple TLA+ spec that can be read by someone knowing
   nothing about TLA+.  The spec, including all the TLA+ constructs it
   uses, are explained in comments.  The pdf file contains a
   pretty-printed version of the actual spec.