meaning of CONSTANT

[ns]

Hello, I was unable to find an explanation for the meaning of CONSTANT anywhere in the "Specifying Systems" book. Is it true that while a VARIABLE can change its value over a behavior, a CONSTANT must keep the same value over a given behavior but can have a different value across behaviors? And that if instead of CONSTANT k and giving it the value 42 in TLC, if I write k==42 that would fix k even across all behaviors.  If that's the case, then defining constants in TLC seems to be over constrained in that it requires you to assign one fixed value across all behaviors. 

thanks

[Apostolis Xekoukoulotakis]

Constant means that it is constant. For example , If we want to describe the behavior of N agents, then N is a constant, because the number of agents does not change.

On Wed, Mar 11, 2020 at 10:53 PM ns <nedsr...@gmail.com> wrote:

Hello, I was unable to find an explanation for the meaning of CONSTANT anywhere in the "Specifying Systems" book. Is it true that while a VARIABLE can change its value over a behavior, a CONSTANT must keep the same value over a given behavior but can have a different value across behaviors? And that if instead of CONSTANT k and giving it the value 42 in TLC, if I write k==42 that would fix k even across all behaviors.  If that's the case, then defining constants in TLC seems to be over constrained in that it requires you to assign one fixed value across all behaviors. 

thanks

--
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/a0c81c85-cf49-424d-9e7a-0c8876db6cec%40googlegroups.com.

[loki der quaeler]

If that's the case, then defining constants in TLC seems to be over constrained in that it requires you to assign one fixed value across all behaviors. 

I think this is perhaps part of the problem with writing specifications that is somewhat lost when people new to TLA+ (and for which the Toolbox is beneficial.)

Ideally, you write a specification in which there is a CONSTANT definition which abstractly is bounding something; then, at a later point, you define that constant value for a specific model checking definition (perhaps 42 in one model checking case, perhaps 13 in another.)  In the continued-ideal-world (and what is done for you behind the scenes by the Toolbox) is that you make another specification with its own configuration that EXTENDS your actual specification and the model checking is done on this extended specification. In this manner, you concern yourself with writing a case generalized specification, and only constraining it via extension for model checking.

[ns]

This article https://www.reddit.com/r/tlaplus/comments/aj018f/constant_antipatterns/ seems to imply that its not a symbolic constant but rather a free variable (that doesn't change during a behavior), and therefore any theorem involving your spec must hold for all values of that constant. 

On Wednesday, March 11, 2020 at 1:58:39 PM UTC-7, Apostolis Xekoukoulotakis wrote:

Constant means that it is constant. For example , If we want to describe the behavior of N agents, then N is a constant, because the number of agents does not change.

On Wed, Mar 11, 2020 at 10:53 PM ns <nedsr...@gmail.com> wrote:

Hello, I was unable to find an explanation for the meaning of CONSTANT anywhere in the "Specifying Systems" book. Is it true that while a VARIABLE can change its value over a behavior, a CONSTANT must keep the same value over a given behavior but can have a different value across behaviors? And that if instead of CONSTANT k and giving it the value 42 in TLC, if I write k==42 that would fix k even across all behaviors.  If that's the case, then defining constants in TLC seems to be over constrained in that it requires you to assign one fixed value across all behaviors. 

thanks

--
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 tla...@googlegroups.com.

[Apostolis Xekoukoulotakis]

https://lamport.azurewebsites.net/tla/book.html

You can look at page 25 for the definition of CONSTANT. Maybe others can help more.

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/156ed98e-9c77-4dbf-911e-7ddedb2b3b7c%40googlegroups.com.

[Stephan Merz]

In this discussion, it is important to make a distinction between a specification and an instance of a specification. A CONSTANT parameter in a specification represents an arbitrary value (possibly constrained by an assumption that delimits values for which the module is intended to be meaningful). By assigning different values to the constant parameters, we obtain different instances of the specification. The value is fixed for every instance, in particular it never changes during or across behaviors considered for that particular instance of the specification.

TLC checks the correctness of instances of TLA+ specifications, and that's why you fix the values of constants when you launch TLC.

A TLA+ specification is correct (cf. section 17.6 of Specifying Systems) if the assumptions imply the theorems, and this means that any instance has to be correct (observe that the non-meaningful instances are trivially correct). Because there are infinitely many values, you cannot use TLC to check the correctness of a specification, but you can reason symbolically about TLA+ specifications, as with TLAPS.

Hope this helps,

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFEV_-geq22WxpXF49yRZ7UQys9KDU68RFhCsOeR8HCXAm%2BiMw%40mail.gmail.com.

[ss.ne...@gmail.com]

Thanks Stephan, that does help. I have a clarification question: In the second case, where we are trying to prove a theorem about (all instances of) the spec, is it still (intuitively) the case that a CONSTANT is only required to remain constant over a behavior? And in that case the difference between declaring CONSTANT K and K == <some value> is that in the latter case, any behavior that satisfies the assumptions must also satisfy all instances of the spec for all behaviors in which K has <some value>?

thank

On Thursday, March 12, 2020 at 12:55:55 AM UTC-7, Stephan Merz wrote:

In this discussion, it is important to make a distinction between a specification and an instance of a specification. A CONSTANT parameter in a specification represents an arbitrary value (possibly constrained by an assumption that delimits values for which the module is intended to be meaningful). By assigning different values to the constant parameters, we obtain different instances of the specification. The value is fixed for every instance, in particular it never changes during or across behaviors considered for that particular instance of the specification.

TLC checks the correctness of instances of TLA+ specifications, and that's why you fix the values of constants when you launch TLC.

A TLA+ specification is correct (cf. section 17.6 of Specifying Systems) if the assumptions imply the theorems, and this means that any instance has to be correct (observe that the non-meaningful instances are trivially correct). Because there are infinitely many values, you cannot use TLC to check the correctness of a specification, but you can reason symbolically about TLA+ specifications, as with TLAPS.

Hope this helps,

Stephan

On 11 Mar 2020, at 23:12, Apostolis Xekoukoulotakis <apostolis.xe...@gmail.com> wrote:

https://lamport.azurewebsites.net/tla/book.html

You can look at page 25 for the definition of CONSTANT. Maybe others can help more.

On Thu, Mar 12, 2020 at 12:02 AM ns <nedsr...@gmail.com> wrote:

This article https://www.reddit.com/r/tlaplus/comments/aj018f/constant_antipatterns/ seems to imply that its not a symbolic constant but rather a free variable (that doesn't change during a behavior), and therefore any theorem involving your spec must hold for all values of that constant. 

On Wednesday, March 11, 2020 at 1:58:39 PM UTC-7, Apostolis Xekoukoulotakis wrote:

Constant means that it is constant. For example , If we want to describe the behavior of N agents, then N is a constant, because the number of agents does not change.

On Wed, Mar 11, 2020 at 10:53 PM ns <nedsr...@gmail.com> wrote:

Hello, I was unable to find an explanation for the meaning of CONSTANT anywhere in the "Specifying Systems" book. Is it true that while a VARIABLE can change its value over a behavior, a CONSTANT must keep the same value over a given behavior but can have a different value across behaviors? And that if instead of CONSTANT k and giving it the value 42 in TLC, if I write k==42 that would fix k even across all behaviors.  If that's the case, then defining constants in TLC seems to be over constrained in that it requires you to assign one fixed value across all behaviors. 

thanks

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a0c81c85-cf49-424d-9e7a-0c8876db6cec%40googlegroups.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 tla...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/156ed98e-9c77-4dbf-911e-7ddedb2b3b7c%40googlegroups.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 tla...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFEV_-geq22WxpXF49yRZ7UQys9KDU68RFhCsOeR8HCXAm%2BiMw%40mail.gmail.com.

[Stephan Merz]

Hello,

On 12 Mar 2020, at 23:15, ss.ne...@gmail.com wrote:

Thanks Stephan, that does help. I have a clarification question: In the second case, where we are trying to prove a theorem about (all instances of) the spec, is it still (intuitively) the case that a CONSTANT is only required to remain constant over a behavior?

I am not sure I understand the question very well, or why it matters. A CONSTANT parameter certainly has a fixed value over a behavior, as well as across all possible behaviors for the instance of the specification that corresponds to that value. But being true for an instance is relevant only for model checking, not for theorem proving. For a given CONSTANT parameter K, you could state a theorem 

THEOREM

  ASSUME K = ...

  PROVE  Spec => <some formula>

but it is not clear to me why you would do that.

And in that case the difference between declaring CONSTANT K and K == <some value> is that in the latter case, any behavior that satisfies the assumptions must also satisfy all instances of the spec for all behaviors in which K has <some value>?

You can compare a definition K == ... to writing

CONSTANT K

ASSUME K = ...

and then there is only one meaningful instance of the module. (That instance may still admit infinitely many behaviors, in particular due to non-determinism.)

Stephan

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/70315c1c-e81e-4953-a777-d1aba13c1e86%40googlegroups.com.