Finite State Machine Visualization

[Mike O'Shea]

As I have gone through the video lectures, the TLA+ book, and the additional papers that Lamport has written on TLA, it really clicked with me that the what is being described mathematically is a state machine SM (or rather a nested set of SMs for non-trivial specs). It should be possible to produce a visualization of the FSM(s) directly from the TLC+ spec.

This idea seemed so obvious to me that I Googled and also searched the tlaplus group here to find who had already done this. So far I've found you can get a visualization of the state search space, which is cool, but it's pretty useless for anything non-trivial. No, what I'm thinking is more useful is being able to see the spec itself as a graph. Then, of course, you can go the other way: build a spec by drawing the SM and filling in the state and action descriptions using TLA+ expressions. 

So, just wanted to check with the group - has this been done already?

One advantage I got to visualizing the SM based on a specification (I did this by hand): I found some enabling conditions missing from two action definitions in the example model given in the video lectures for the TwoPhase spec which did not technically affect the correctness, but after filling them in reduced by 25% the number of states searched. Fairly significant reduction - but depends - since the BFS can generate potentially exponentially many state paths. That said, the additional conditions added made the model easier to understand - which is a positive.

It makes me thing there is some potential for a "linter" that could catch such things in a TLA spec, and being able to build a specification graphically might help make it more accessible for other team members when creating a new protocol/algorithm.

Just a thought. Would appreciate any pointers to WIP on this kind of thing. Thanks!

* edit: State Machine

 

[Markus Kuppe]

On 28.06.19 22:07, Mike O'Shea wrote:
> One advantage I got to visualizing the FSM based on a specification (I

> did this by hand): I found some enabling conditions missing from two
> action definitions in the example model given in the video lectures for
> the TwoPhase spec which did not technically affect the correctness, but
> after filling them in reduced by 25% the number of states searched.
> Fairly significant reduction - but depends - since the BFS can generate
> potentially exponentially many state paths. That said, the additional
> conditions added made the model easier to understand - which is a positive.

Hi Mike,

not exactly a drawing of the FSM, but the upcoming TLC/Toolbox profiler
shows statistics for states found and distinct states at the action
level (see attached screenshot). The profiler should be useful in
scenarios as described above. It is part of all recent nightly toolbox
builds [1].

Markus

[1] https://nightly.tlapl.us/