Oops. Missed the parenthesis!
On Wednesday, September 6, 2017 at 3:02:24 PM UTC-4, Alexander Fasching wrote:
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...@xxxxxxxxxxxxxxxx
> <mailto:tla...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.