Hi,
one thing I'd find very useful in understanding (or debugging) the behaviors of TLA+ specs would be a mode that would support interactive exploration of the state space. At a high level I'm imagining something like (given a TLC config file and all that):
1. In the beginning, I get the list of valid initial states, I click on one and pick it as my "current state"
2. Given the current state, I'm presented with the list of enabled actions from this state. I can then clickety-click on an action, and then I get the list of possible successor states resulting from that action. I clickety-click again on a state from that list again, extending the current trace with that state and making it my new current state. Ideally, I also have a "back" button that takes me one state back in the trace.
Does anything like this exist, or is someone working on something similar? I'm aware that one can export the state graph to GraphViz, but TBH I haven't found this super useful, as my state graphs tend to have hundreds or thousands of states even for small choices of constants. But maybe there are some existing tools for GraphViz that would allow such an interactive exploration? If not, what would be a reasonable way to build this on top of TLC?
Cheers,
Ognjen