I have been thinking about what to do next on the Hyperbook. Below
are some possibilities I'm considering. None of them preclude any of
the others, so I'm interested in what you consider to be their
relative importance. Of course, I'm also interested in things you'd
like to see that aren't mentioned.
Please send your replies directly to me rather than posting them to
the group. I will eventually report on what you've said and what I've
decided to do.
A. The following two options require rewriting the existing parts of
of the Hyperbook.
1. Partition the text into units, each of which would approximately
correspond to a single classroom lecture. A few people have told me
that this would make it easier to read.
2. Instructions for using the Toolbox and TLC now appear in the text,
combined with the development of the specs. I am thinking of moving
all these instructions into a single tools manual, and replacing the
material now in the text with links to the appropriate parts of that
manual. This manual might be the Toolbox help pages, expanded to make
it easier to use.
B. While the following possibilities are independent of those in part
A, either (or both) of the part A options should be done before any of
them.
3. More "raw" examples. This means that the emphasis is on how TLA+
or PlusCal is used, with little motivation behind why the specs have
been written. I am open to suggestions for what kind of
specifications: the domain (e.g., distributed algorithms) and the
length/difficulty (short toy examples vs. more realistic complicated
ones). And do you prefer TLA+ or PlusCal examples?
4. Examples of how to go from an often ill-formed idea to a formal
spec. I will probably need help finding such examples.
5. More about principles of concurrent algorithms rather than about
PlusCal/TLA+.
6. More about writing proofs.
5a. Finding invariants.
5b. Detailed practical advice on how to use the TLAPS prover.
7. More advanced topics. These include:
6a. Auxiliary variables (history, stuttering, and prophecy variables.)
6b. Composing specifications.
6c. Real-time and hybrid specs.
8. Something about writing informal specs.
Thanks,
Leslie