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

[Martin <martin...@xxxxxxxxxxxxxx>]

Hi Leslia,

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

thanks, Martin

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
> <mailto: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.