It's a bit unfortunate that tlaplus.net is dead, because apparently at
some point it was the "official" homepage, and references to it have
made their way into books
People should know better. I've proposed a solution to this problem,
but it's too simple and low-tech for anyone to have paid attention.
You can find it here
http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#www9
and an example of its use is at the bottom of the TLA+ home page.
It might not be a popular sentiment with the inventor of LaTeX, but
things in PDFs seem "locked away" compared to being on the web.
A pdf may seem "locked away", but a pdf file on the web is more likely
to look the same to all readers than an html file. (Have you ever
come across a page with completely unreadable purple text on a black
background? It looks fine on the author's browser.) I have been
unable to do the simplest things in html and get them to look the same
on all browsers. I would appreciate help from an html expert that
would allow me to improve the TLA+ web pages. But I have seen no
evidence that there is any suitable way to put mathematical formulas
on the web other than with pdf files.
3. Port the documentation in Specifying Systems and its
errata to some man pages.
4. Add a summary in a --help flag.
(3) and (4) are awkward due to licensing issues of the book.
I don't know what "documentation", and "a summary" of what, you have in
mind. In any event, man pages are of no interest to me because they
don't exist on all systems, and --help flags are meaningful only when
running a tool from a command line. While there is some reason to use
TLC from a command line on very large specs, people should learn TLA+
and should do the initial debugging of even large specs with the
Toolbox. Any useful documentation or summary should therefore be
accessed with the Toolbox. I would be glad to discuss ways to make
the Toolbox more useful to beginners with anyone who volunteers to do
the work. Licensing issues of the book should not be a problem.
Leslie