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