It's also easier to state sweep if you write the spec in pluscal,
which will handle the UNCHANGED for you automatically.
--I've done this with a shell script before. I used a prototype CLI for parameterizing TLC but you can probably do it with templated CFG files too.
H
On 10/3/2024 10:17 PM, 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--
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/071596e8-0a49-489d-b06e-c850e7c1a5e0n%40googlegroups.com.