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