[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: marc magrans de abril <marcmagra...@xxxxxxxxx>*Date*: Sun, 18 Oct 2015 23:30:44 -0700 (PDT)*References*: <a475916a-37de-4c9c-8421-e17d35692019@googlegroups.com>

Hi Leslie,

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

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

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?

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

**References**:**What should I do next in the Hyperbook?***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] TLAPS-proved invariant violated in TLC?** - Next by Date:
**Re: [tlaplus] TLAPS-proved invariant violated in TLC?** - Previous by thread:
**Re: What should I do next in the Hyperbook?** - Next by thread:
**Re: What should I do next in the Hyperbook?** - Index(es):