TLA+ Video Course

[Leslie Lamport]

I am planning to create a series of video lectures that will
constitute a course on writing TLA+ specifications.  A pilot that
shows what the lectures might look like is at

  http://research.microsoft.com/en-us/um/people/lamport/mooc/prop-logic-c9.html

I would appreciate your feedback on how well it works and how I can
make it better.  Don't bother telling me about the terrible sound or
about little glitches--that will all be fixed in the actual lectures.

Thanks,

Leslie

[fl]

I would appreciate your feedback on how well it works and how I can

make it better.

Impressive. Hollywood is expecting your come. The way you speak is quite clear for a foreigner. If you want to help them

more, subheadings in English is a help for them. Since you seem to have access to a large choice of medias, 

I recall that the digital tablets used by Kahn are fit to the purpose of teaching. (Not for the whole lecture but for

some parts of it maybe.)

https://www.youtube.com/watch?v=kpCJyQ2usJ4

Otherwise I appreciate the video is divided into pieces with a heading. We can come back to any moment easily.

-- 

FL

[Leslie Lamport]

I forgot to add:  Please send your comments to me directly (address at http://lamport.org) rather than posting them to the group.

Thanks,

Leslie

[fl]

Kahn

Khan.

-- 

FL 

[Leslie Lamport]

I’m moving this from the “TLA+ community event 2016” topic to the “TLA+ Video Course” topic.

 

I gather that YouTube provides a nice method of adding subtitles.  Unfortunately, as far as I’ve been able to determine, hosting the video on YouTube doesn’t permit the features that I want and that were shown on the pilot that I produced.  (I’d be happy to be proved wrong by a Web programming wizard, but I’ve been unable to find one who can help me.)  I’ve thought of a way that I might be able to produce a single version of the videos in which the subtitles can be displayed or hidden, but I’m not sure if it will work. 

 

In any case, lacking the kind of feature that YouTube apparently provides, adding subtitles to my videos will be a time-consuming enterprise—even if I restrict it to portions of the video that show me rather than text.  So it makes most sense for me to release all the videos without subtitle and add them later.  So, I intend to forget about subtitling now. 

 

Leslie

 

 

From: 'fl' via tlaplus

Sent: Friday, November 18, 2016 3:45 AM
To: tlaplus

Subject: [tlaplus] Re: TLA+ community event 2016

 

 

 - While I would not be able to attend, I'd be interested in watching

   a live stream.

 

 

Regarding the live Stream, here is an interesting discussion on how to add subtitles to a video easily (it begins

4 messages before the end.)

 

https://groups.google.com/forum/?hl=fr#!topic/metamath/FGn-O0u7OjI

 

I think Stephan has a teaching activity and can certainly confirm that subtitles are of

use in the rest of the world. (And even for those who are older than his students.)

 

--

FL

[fl]

OK

Here is an interesting video on what learning a foreign language means from the neuronal point of view.

It is in French (with no subtitles) and I don't expect that anbybody can understand what is being told but there

is an interesting graph at 12 minutes 30 that shows the rapid decline of the ability to discriminate the

sounds pronounced by a foreigner past the earliest years of life. And since it is neuronal it is

without remedy obviously.

https://www.college-de-france.fr/site/colloque-2016/symposium-2016-10-13-12h15.htm

--

FL

[Leslie Lamport]

The first two videos of the TLA+ Video Course are now on the Web at

    http://lamport.azurewebsites.net/video/videos.html

They are far from perfect, but I think they're good enough and I don't intend to change them unless there are real errors that need to be corrected.  However, there are many more videos to come, and suggestions for improving them are welcome.

Leslie

[Leslie Lamport]

The third video of  the TLA+ Video Course is now available from

    http://lamport.azurewebsites.net/video/videos.html

[Leslie Lamport]

The fourth video in the TLA+ Video Course has been released.  It's titled "Die Hard".  The course is at:

   http://lamport.azurewebsites.net/video/videos.html

Leslie

[fl]

The fourth video in the TLA+ Video Course has been released.

These are not criticisms, these are remarks I had in mind while I was listening to the video.

"It's not mathematics" : well the experience shows that in any mathematical texts many things are

left implicit. Not to mention the "intuitive" definition of continuity or limits in the XIXth texts,

the modern texts are full of missing information: for example mathematical texts use the phrase 

"topological space" to mean either the structure

(so an ordered pair) or the base set (so the first element of the ordered pair). Likewise the

provisos are always missing. Likewise limit points in summations are often highly acrobatic. 

Etc.

2) The fact that TLC solves the problem is purely fortuitous. It might be endless.

3) I like the idea that TLAPLUS can represent any digital system. Its ability to represent protocols

or standards and not only algorithms is usually not enough emphasized.

-- 

FL

[Leslie Lamport]

It's not mathematics because what people want it to mean is that every variable other than small is unchanged, and there is no way to write a mathematical formula that asserts this.  (Since there are infinitely many possible variables, such a formula would have to be infinitely long.)  Of course you can design a language in which the statement has that meaning and give that language a precise mathematical semantics.  But if that makes it math, then a C program is also math.

Leslie

[fl]

  But if that makes it math, then a C program is also math.

It is the case I think. It's an imperative algorithm description language like CCAL. It might be translated into pure mathematical terms

using a "temporal logic of actions" symbolism. It is not expressive enough to be used comfortably to specify or to 

exchange ideas as you have shown it but it's all mathematics.

To put it into Pfenning's words every time you have a different kind of logic you have a class of program languages. There's an isomorphism.

-- 

FL

[Leslie Lamport]

The next three lectures in the video course have been released (lectures 5-7).  Go to https://lamport.azurewebsites.net/video/videos.html .

Leslie

[Leslie Lamport]

The scripts of all the lectures in the TLA+ Video Course are now available.  Each script contains everything shown and said on the video, except for shots of me.  It can be useful for the hearing impaired, viewers who want to review a lecture, and people who hate videos.  However, the html file that displays the video may be needed if the video requires the viewer to download material.

Leslie

[Balaji Arun]

Dr. Lamport

Thanks for the wonderful lectures. I was trying video4.html and saw that the definition for BigToSmall differs from mine:

video4.html

BigToSmall == IF big + small =< 3

               THEN /\ big'   = 0 

                    /\ small' = big + small

               ELSE /\ big'   = small - (3 - big)

                    /\ small' = 3

My Solution

BigToSmall == IF big + small =< 3

               THEN /\ big'   = 0 

                    /\ small' = big + small

               ELSE /\ big'   = big - (3 - small)

                    /\ small' = 3

Notice the ELSE statement. Wouldnt big' = small - (3 - big) lead to negative values (e.g. big = 5 and small = 2)? In that case, why does TLC model checker not catch this with the invariant TypeOK?

[Alexander Fasching]

The two definitions are equivalent:

big' = small - (3 - big) <==> big' = small - 3 + big <==> big' = big -
(3 - small)

On 09/06/2017 08:33 PM, Balaji Arun wrote:
> Dr. Lamport
>
> Thanks for the wonderful lectures. I was trying video4.html and saw that
> the definition for BigToSmall differs from mine:
>

> *video4.html*
> *
> *

>
> BigToSmall == IF big + small =< 3
>
> THEN /\ big' = 0
>
> /\ small' = big + small
>
> ELSE /\ big' = small - (3 - big)
>
> /\ small' = 3
>
>

> *My Solution*

>
>
> BigToSmall == IF big + small =< 3
>
> THEN /\ big' = 0
>
> /\ small' = big + small
>
> ELSE /\ big' = big - (3 - small)
>
> /\ small' = 3
>
>
> Notice the ELSE statement. Wouldnt big' = small - (3 - big) lead to
> negative values (e.g. big = 5 and small = 2)? In that case, why does TLC
> model checker not catch this with the invariant TypeOK?
>
>
>
>
> On Monday, August 14, 2017 at 10:06:16 PM UTC-4, Leslie Lamport wrote:
>
> The scripts of all the lectures in the TLA+ Video Course are now
> available.  Each script contains everything shown and said on the
> video, except for shots of me.  It can be useful for the hearing
> impaired, viewers who want to review a lecture, and people who hate
> videos.  However, the html file that displays the video may be
> needed if the video requires the viewer to download material.
>
> Leslie
>

> --
> You received this message because you are subscribed to a topic in the
> Google Groups "tlaplus" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/tlaplus/lAeWdCE9MLw/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
> tlaplus+u...@googlegroups.com
> <mailto:tlaplus+u...@googlegroups.com>.
> To post to this group, send email to tla...@googlegroups.com
> <mailto:tla...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Balaji Arun]

Oops. Missed the parenthesis!

[Leslie Lamport]

Lecture 8 of the TLA+ video course is now available.   It's in two parts, with two separate videos.  As always, it's at https://lamport.azurewebsites.net/video/videos.html .

Leslie

[Leslie Lamport]

Lecture 9 of the TLA+ Video Course, consisting of two videos, is now available on the course site: 

       https://lamport.azurewebsites.net/video/videos.html

 

[CRIMX]

Love the videos Dr. Lamport. Very inspiring and funny. Stay tuned. ;D

[Leslie Lamport]

Lecture 10, the final lecture of the TLA+ Video Course, consisting of two videos, has now been posted.  As always, the home page of the course is:

    https://lamport.azurewebsites.net/video/videos.html

Leslie

[Andrew Helwer]

Congrats on finishing the course!!!

[Morgan Weetman]

Hi,

This may not be the right thread to post in, please feel free to correct me.

I'm enjoying the video series, currently up to video 6 (two phase commit) and I had a question:

From memory the state machine only allowed progress to the "committed" state from "prepared", however the definition for RMRcvCommitMsg(r) does not enforce that rmState[r] is equal to "prepared". The model works none the less, is this simply an oversight or am I misunderstanding something?

RMRcvCommitMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the TM to commit. *)
(*************************************************************************)
/\ rmState[r] = "prepared" /* I added this to my definition */
/\ [type |-> "Commit"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>

Many thanks for creating this video series, I was finding it hard going just using the book,

regards

[Leslie Lamport]

This is as good a place as any for questions about the content of the video course.

The existence of the commit message implies that the RM is in either the "prepared" or "committed" state.  In either case, the action asserts that the new value of the RM's state is "committed".  If it was already in the "committed" state, this does nothing, so there is no need to disallow the step permitted by the action in that case.  A step that does nothing does no harm.

In a later lecture you will learn that a step which leaves the state unchanged,is always allowed.  Therefore the change that you made to the definition does not change the spec.  But you needn't worry about that now.

Leslie

[Morgan Weetman]

Ah...of course, TMCommit requires tmPrepared = RM...sorry for the noise

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.

[neil.o...@koodoo.io]

Hey Balaji,

I just finished watching the video, and had the same headscratcher as you for a few moments. As an engineer, my instinct was to think of the operation I would need to perform to change state, and I wrote it out that way accordingly.

But Alexander is right - mathematically they are the same! For me this is a great example of how it's important to shift into a mode of thinking mathematically, not programmatically. I'm sure this won't be the last time I get caught out this way on my TLA+ journey :)

Neil