Re: [tlaplus] Re: Analysis: Runway, a new formal specification system

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 18.10.2017 02:45, William Schultz wrote:
> Similar to what Ron Pressler noted, I found the visualization tool
> provided by Runway to be very compelling, and I wonder if something
> similar could be integrated into the TLA+ tools. As I see it, there
> are two main approaches to visualization of specifications like those
> written in Runway/TLA+ (there may be others). The first, which the
> TLA+ toolbox seems to have added recently, is the "state diagram"
> visualization. That is, some kind of graph that represents states as
> nodes (usually boxes or circles), and actions/transitions as edges
> between them. This is useful for examining the large scale structure
> of an algorithm/specification, but in my opinion, it is less
> practical. For one, it becomes unwieldy when the state space is
> extremely large, and it is harder to understand small scale behaviors.
> The second mode of visualization, the approach taken by Runway, is
> more interactive in nature. It provides a way to interactively explore
> a single trace of the algorithm, by providing a way to "execute" the
> transitions that are enabled given a current state. I know that TLC
> provides a depth-first mode, but it could be interesting if it also
> provided some kind of "interactive" mode, that allowed a client to
> send commands to TLC to, for example, list the enabled actions given
> the current state, or perform a specific action to advance the current
> state. I could imagine an "interactive server" mode of TLC, which
> would allow external applications, like a web browser, to communicate
> with it in order to provide a visualization tool that users could
> interact with.

Hi William,

I have no idea how the Runway visualization works, but I believe that
what you need on the TLC end for what you call "interactive mode" is to
some extent available already. The tlc2.util.IStateWriter [1] is a hook
into the next-state generation. It is synchronously invoked during BFS
and DFS state graph exploration. Alternatively, you should look at the
JMX API provided by TLC [2].

I suggest to explore both approaches and if feasible, we eventually
extend either one to control the next-state generation. We might want to
migrate the technical discussion into a new Github issue [3] though.

Cheers
Markus

[1]
https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/util/IStateWriter.java

[2]
https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/tool/management/ModelCheckerMXWrapper.java

[3] https://github.com/tlaplus/tlaplus/issues