You can verify that it is, indeed, state explosion by examining the TLC page in the Toolbox. If you see a very small radius (say, 3) but a very large number of unique explored states (say, a billion), then it's state explosion. However, the problem may not be too many variables but rather limiting constants (the finite constraints on the specification when model checking, e.g. the number of nodes in the distributed system etc.) that are too large. I recommend watching this great talk about how to use TLC in practice, by Markus Kuppe, who maintains it, with plenty of helpful advice: https://youtu.be/zGIK2p6csAo
Ron
On Monday, October 15, 2018 at 2:15:07 AM UTC+1, Matt Jennings wrote:
My spec is composed of many variables and I'm not able to check it due to due to what I assume is state space explosion. I'm wondering if for certain kinds of specs, it would be better for the model checker to start by assuming a particular invariant is violated, and work backwards looking for a path that leads back to the initial state.