Hi James,
Thanks for taking the time to write up your feedback. And thanks also
for your offer to try to help solve some of the problems you found. I
hope we'll be able to take you up on your offer.
Before getting to specifics, I want to say that I believe your desire
for the command-line interface to come first represents a small
minority view in the general programming community. Gerard Holzmann,
the inventor of the Spin model checker, told me a while ago that when
he put a very simple GUI on Spin, the number of users increased by an
order of magnitude. I have had a number of comments that the Toolbox
does not provide the power they have come to expect from the IDEs they
use to write programs. Although others have complained about the
absence of good documentation for the command line interfaces, no one
else has ever said that the Toolbox should not be the principle method
of using the tools.
However, I have not based my career on copying what other people do.
I have always tried to find what works best, regardless of what others
think should work best. I'm not a fan of screen flash. I started
programming before there were even command-line interfaces. I use
whatever I find most convenient. For example, for manipulating files
I will use either the Windows File Explorer GUI or a Cygwin
command-line shell depending on what I'm doing.
If you think running the TLC model checker from a command line could
be better than running it from the Toolbox, then you do not appreciate
all that you can do from the Toolbox--perhaps because you have just
been writing simple specs and have not yet had serious debugging of
specs to do, and perhaps because of poor documentation. And only a
blind person could prefer running the prover from a command line
rather than from the Toolbox. (We don't have the resources to try to
provide interfaces for disabled people.)
So, we are not going to spend resources trying to improve command-line
interfaces. However, they should be documented better than they are.
That's one of the many things I haven't had time to do and am not
likely to find time in the near future. But the information is easily
accessible, so it's not rocket science.
I'm willing to devote some energy to helping someone produce better
documentation for the Toolbox. I would appreciate any help you can
provide. I suggest that you start by reading the Toolbox's help pages
and tell me what can be done to improve them. What I would like is to
have the Toolbox read the user's mind and, when she doesn't know what
to do next, present her with the appropriate help page. I don't know
how to implement that. Simply presenting the information in a single,
logically structured document doesn't seem to work very well. 25
years ago I found that LaTeX users weren't very good at reading the
manual, and people have gotten a lot less willing to read than they
were then.
You wanted HTML documentation. There are two things that need to be
documented: TLA+ and the tools. I considered alternatives to
LaTeX-produced pdf when I started writing the Hyperbook. HTML would
have been ten times harder to use to produce something that was a
tenth as good. As for the "pretty-printed" version versus the ASCII,
a TLA+ user at Intel wrote that one of the good things about TLA+ is
that if he doesn't understand what a TLA+ construct means, he can
look it up in a math book. Math books don't write math in ASCII, they
use standard mathematical symbols. I want TLA+ users to think in
terms of math, which means thinking in terms of its symbols. You will
soon get to be bilingual, reading math and its TLA+ ASCII versions
equally well. And if you learn TLA+ by reading the Hyperbook, you
will find that the ASCII versions are all sitting there for you to
just copy into the Toolbox.
By the way, I believe the Hyperbook has a page with a table of ASCII
<-> Math translations. It's part of the few-page summary of TLA+ in
Specifying Systems, which is also available as a separate pdf file.
As to the zip file, the only way to write hypertext in pdf is with
hundreds of separate files. You want those files on your own machine;
you don't want to have to be going out over the web for every pop-up.
I don't know any alternative to a zip file.
As to documenting the tools, there seem to be two issues: the
mechanics of the various bells and whistles that the Toolbox provides,
and the more subtle issues that involve understanding TLA+. For the
latter, the Hyperbook seems to be the best medium. The former is what
the help pages try to document, but don't seem to be doing a good job.
Leslie