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

[Isaac DeFrain <isaacdefrain@xxxxxxxxx>]

Pablo,

To specify a successor state, we must say how the values of all variables change from the current state (they can also be UNCHANGED). All actions must specify the values of all variables in a successor state.

Since we represent the value of the variable i in the successor state as i’, the Add action is simply incrementing the value of i from the current state to the successor state regardless of the current value of i.

Additionally, we may add enabling conditions to actions which will make it so that the action can only take place if those conditions are met. Thus, adding i \in 0..1000, which is a condition on the value of i in the current state, only affects when this action can be applied; i.e. with this condition, Add will only be enabled when 0 <= i <= 1000. This may or may not be what you want, I’m not sure.

The point is that we don’t need to specify anything about the values of our variables in the current state unless we want the action to only be enabled under those conditions. However, we must always specify how the variables change from the current state to a successor state.

I hope this helps.

Best,

Isaac

On Thu, Mar 18, 2021 at 7:54 AM pablo fernandez <fernandezpablo85@xxxxxxxxx> wrote:

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:

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.

--

Isaac DeFrain

-- 
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/CAM3xQxHqQBU9xVY%3Dpw4%2B0t8pNV2q5G8tfePffweNUu%3DtNpfL0w%40mail.gmail.com.