Re: TLA+ Video Course

[Balaji Arun <ba2...@xxxxxx>]

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