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

*From*: TLA Plus <tlapl...@xxxxxxxxx>*Date*: Wed, 16 Sep 2015 05:41:50 -0700*References*: <a475916a-37de-4c9c-8421-e17d35692019@googlegroups.com> <55F961DB.8090008@gmail.com>

Hi Martin,

I'm sorry, but because of the mistake I made in the email, it's not clear if you meant the subparts of 6 (writing proofs) labeled in my email as 5a and 5b, or the first two off the three subparts of 7 (more advanced topics).

Leslie

On Wed, Sep 16, 2015 at 5:34 AM, 'Martin' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

Hi Leslia,

I'd be interested in chapters 6a and 6b.

thanks, Martin

> <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>.

On 09/04/2015 01:01 PM, 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

>

> --

> You received this message because you are subscribed to the Google

> Groups "tlaplus" group.

> To unsubscribe from this group and stop receiving emails from it, send

> an email to tlaplus+u...@xxxxxxxxxxxxxxxx

> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx

> <mailto:tla...@xxxxxxxxxxxxxxxx>.

> Visit this group at http://groups.google.com/group/tlaplus.

> For more options, visit https://groups.google.com/d/optout.

--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.

To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

Visit this group at http://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

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

**Re: [tlaplus] What should I do next in the Hyperbook?***From:*Martin

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