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.