[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Interactive exploration of the TLC state graph?

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.

On Tuesday, September 5, 2023 at 6:34:25 PM UTC+1 Michael Leuschel wrote:
Hi Ognjen,

the ProB tool provides exactly the “clickety-click” interface you wish for:
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.


>> On Sep 5, 2023, at 5:40 AM, Ognjen Maric <ognjen...@xxxxxxxxx> wrote:
>> 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?

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/192cd825-2655-48d9-9a9b-82cf501d3280n%40googlegroups.com.