Interactive exploration of the TLC state graph?

[Ognjen Maric]

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

[Markus Kuppe]

Hi Ognjen,

the TLA+ debugger [1] could potentially address some of the features you're interested in. For 2. you will have to run the TLA+ debugger in simulation mode.

M.

[1] https://youtu.be/DsfbdsE4hJ0?t=250

[Michael Leuschel]

Hi Ognjen,

the ProB tool provides exactly the “clickety-click” interface you wish for:
https://prob.hhu.de/w/index.php?title=TLA
However, it works by translating TLA+ to B and uses a somewhat older version of SANY.
It also requires typed TLA+ specifications.

Both the Tcl/Tk UI or the new JavaFX-based UI (https://prob.hhu.de/w/index.php?title=Download#ProB2-UI) support TLA+ out of the box.

Greetings,
Michael

[Willy Schultz]

Though it is still somewhat in prototype stage, tla-web aims to provide most of the functionality you are describing. The interface isn't exactly the same as TLC (e.g. no use of config files), but the core idea was to have a quick way to explore specs interactively, share counterexample traces, etc.

[Gareth Smith]

I sent you an email from my gmail account

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ae6a0196-8cf3-427b-b1dc-0265af635689n%40googlegroups.com.

[Ognjen Maric]

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

[A. Jesse Jiryu Davis]

Two years ago Samy Lanka and I proposed an interactive debugger exactly like that, and soon after Markus demonstrated how it can be done, I don't know if there's been additional development to make it more convenient since then.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/df32449a-97a4-4e27-9788-ab2a7447f2c9n%40googlegroups.com.