It is disheartening that the error was not discovered until now.
Personnaly I learned TLA+ by reading "Specifying Systems". But I suppose that if people knows how to use TLA+ they have read something:
either the "HyperBook" or "Specifying Systems". Simply examples or exercices are rarely worked out thoroughly.
--
FL