Re: TLA+ Video Course

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

On Wednesday, 6 September 2017 19:33:35 UTC+1, 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