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.