Thank you all for the responses, all very helpful! Finally found some time to try all of them out. Currently, the TLA+ Debugger with a Spec breakpoint seems the most immediately applicable solution for me right now. ProB chokes with an exception on translating my spec (happy to share the spec if it helps), and tla-web doesn't seem to support my models as they use multiple modules and instantiations.
I wasn't aware that ProB could ingest TLA+, nor of tla-web, both are very cool!
Best,
Ognjen--On Thursday, September 7, 2023 at 9:07:50 AM UTC+2 Gareth Smith wrote:I sent you an email from my gmail accountOn Tue, Sep 5, 2023 at 8:40 PM Ognjen Maric <ognjen...@xxxxxxxxx> wrote: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--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ae6a0196-8cf3-427b-b1dc-0265af635689n%40googlegroups.com.
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/df32449a-97a4-4e27-9788-ab2a7447f2c9n%40googlegroups.com.