[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Specifying all states on SimpleProgram from the TLA Course



Oh, my bad, I assumed (incorrectly) that everyone was familiar with the course and it's exercises. Here's the full example:

https://gist.github.com/fernandezpablo85/b927f342e6b93b94f8491df6be1d6f12

The commented line is not part of the proposed solution. I was wondering why is that, since Lamport emphasises on declaring all variables explicitly even those that don't change.

On Thu, Mar 18, 2021 at 12:21 AM Imran Meah <imranmeah91@xxxxxxxxx> wrote:
I will attempt to answer this one but welcome more knowledgeable folks to chime in.

It looks like you are asking why the range of i is not defined. 

Was the range of i defined before this statement? If yes then, the range definition will cary over when you invoke i.
On Wed, Mar 17, 2021 at 10:13 PM Pablo Fernandez <fernandezpablo85@xxxxxxxxx> wrote:
I've been watching the videos on Lamport's TLA Course. 

On the DieHard problem he makes a statement on why is it important to specify a state completely:
Screen Shot 2021-03-18 at 00.08.37.png

Here, he insists on adding /\ big' = big.

Now, on the SimpleProgram exercise (the first one), Add is defined like this:

Add == /\ pc = "middle"

              /\ pc' = "done"

              /\ i' = i + 1


My question is, if we need to specify the whole state space, shouldn't Add need to be defined this way instead?

Add == /\ pc = "middle"

              /\ pc' = "done"

              /\ i' = i + 1

              /\ i \in 0..1000

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8fa93e13-20e7-48fa-8225-75bb5744e93an%40googlegroups.com.

--
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/hmDZVDCSe84/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CADaysi%2B_zsOrWKjizeb2V3Gv5Tp236LbC7JeTFAvWh3p2zRn2g%40mail.gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAN3aEu5vuv%3DVLFOWwq%2BFfxj2_d0Mb5tDQXRhuLRb_-_mJbe2Dw%40mail.gmail.com.