Specifying all states on SimpleProgram from the TLA Course

[Pablo Fernandez]

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

[Imran Meah]

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.

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

[pablo fernandez]

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.

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CADaysi%2B_zsOrWKjizeb2V3Gv5Tp236LbC7JeTFAvWh3p2zRn2g%40mail.gmail.com.

[Stephan Merz]

If you omit "big' = big" in the definition of the action FillSmall, the value of the variable big is completely unconstrained in the successor state (it could be unchanged but also equal 42, {}, "foo" or whatever value). It is almost impossible to reason about a specification that includes such an action, and TLC will produce an error. Leslie's point is to emphasize the fact that a TLA action

  x' = some_expression

is different from the assignment

  x = some_expression

in an imperative programming language such as C.

Looking at the "first_number" example, it is easy to see (or check with TLC) that the invariant

  pc = "middle" => i \in 0 .. 1000

holds of that specification, so adding "i \in 0 .. 1000" as a pre-condition to action Add is redundant. And in fact, the specification also verifies the invariant

  pc = "start" => i = 0

so the conjunct "i=0" in the Pick action is redundant as well. Of course, there is nothing logically wrong with adding redundant constraints.

Stephan

On 18 Mar 2021, at 14:53, pablo fernandez <fernande...@gmail.com> 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 <imran...@gmail.com> 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 <fernande...@gmail.com> 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+u...@googlegroups.com.
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+u...@googlegroups.com.
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+u...@googlegroups.com.

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]

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

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