I'm the author of this tool (and mentioned it a short while back in a comment here..), so I can answer questions about it. Or TLA+. Or life.
I wrote it to make it more easy to understand why and how some message exchange scenarios failed (in a model) and the charts turned out to be quite helpful for that.
Wish it was easier to express directly in the models, though, or perhaps use this tool without any particular ALIASing, just with better analysis of the trace dumps tlc produces, but parsing TLA+ in general is not that easy. It should be easier to interactively study the state diagrams as well, because non-trivial scenarios can get a lot of states.
this looks pretty sweet. tla+ looks scary and mathy at first, but it's really a pretty simple concept: define some state machines, explore the state space, see if you run into trouble. with this you get a nice classic sequence diagram to show how things went down.
I haven't, but I'm under the impression some scenarios might be impossible to express in Mermaid. For example, how would you render the example svg from the page? It is essential to describe that while the ping was sent in state 3, some actions are taken first and then client 2 handles the ping in state 6.
I wrote it to make it more easy to understand why and how some message exchange scenarios failed (in a model) and the charts turned out to be quite helpful for that.
Wish it was easier to express directly in the models, though, or perhaps use this tool without any particular ALIASing, just with better analysis of the trace dumps tlc produces, but parsing TLA+ in general is not that easy. It should be easier to interactively study the state diagrams as well, because non-trivial scenarios can get a lot of states.