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...@xxxxxxxxxxxxxxxx
<mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
<mailto:tla...@xxxxxxxxxxxxxxxx>.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.