[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: meaning of CONSTANT

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.

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/66f4f10a-6fae-4516-a3c2-8f6301d90e77%40googlegroups.com.