Yeah, i think this situation has been discussed elsewhere on the forum. The only workaround I know is, as you noted, to turn constants into variables. It guess it would be nice to just instruct TCL to do different runs for a set of different values for the constant, but I don't know if the added complexity on the tools worth it.
JS
On Friday, October 4, 2024 at 12:17:34 AM UTC-3 Andrew Helwer wrote:
Often I will have specs that take a constant representing input to the system. It is good to write specs this way because then you can write proofs over the unfixed value of that input constant. However, it is usually nice to model-check theorems before trying to prove them. It is also nice to model-check a set of possible values, rather than a single value chosen as input in the model. To this end I usually end up turning the input constant into a variable that is nondeterministically assigned some value from a set in the initial state and then never subsequently modified. However, this interferes with statement and proof of theorems. This must be a common issue, so does anybody have a good way around this? It seems like I would want to iteratively execute TLC across a range of values for a given constant.
Andrew Helwer