Re: What should I do next in the Hyperbook?

Hi Leslie,

I would really love to see more documentation on "6c. Real-time and hybrid specs".

I have read the excellent TLA+ papers on the issue [1-2]. However,I have the impression that the focus is more on theorem proving. Is it? As far as I understand this is related to the fact that both topics require real numbers, and these can not be model-checked.

Still I would like to know how an engineer without the knowledge or time to do formal proofs could use TLA+ for this kind of problems. What are the limits? or do you think that an engineer facing this kind of problems should learn formal proofs?

In my case, when I face this kind of issues I use prototyping, C code with mockups of the real-time part of the system, and/or Matlab. What is the TLA+ approach for this kind of problems?

I'm also pretty curious about what can you write about "8. Something about writing informal specs." :)

Thanks,

Marc

[1] http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-hybrid

[2] http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#charme2005

On Friday, September 4, 2015 at 1:01:34 PM UTC+2, Leslie Lamport wrote:

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