Tlsd: Generate (message) sequence diagrams from TLA+ state traces | Hacker News Reader

Tlsd: Generate (message) sequence diagrams from TLA+ state traces

github.com

75 pointstodsacerdoti7 comments

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.

TLAplus: https://en.wikipedia.org/wiki/TLA%2B

https://github.com/tlaplus

A learnxinyminutes for TLA+ might be helpful: https://learnxinyminutes.com/

awesome-tlaplus > Books, (University) courses teaching (with) TLA+: https://github.com/tlaplus/awesome-tlaplus#books

Have you looked at using mermaidjs instead of SVG as an output? It might translate easier and plug into other solutions easier.

blockdiag > seqdiag is another syntax for Unicode sequence diagrams, optionally in ReST or MyST in Sphinx docs: http://blockdiag.com/en/seqdiag/examples.html#edge-types

blockdiag > nwdiag > rackdiag does server rack charts: http://blockdiag.com/en/nwdiag/

Otherwise mermaidjs probably has advantages including Jupyter Notebook support.

E.g. Gephi supports JSON of some sort. Supported graph formats: https://gephi.org/users/supported-graph-formats/

More graph and edge layout options might help with larger traces

yEd has many graph layout algorithms and parameters and supports GraphML XML; yEd: https://en.wikipedia.org/wiki/YEd

MermaidJS docs > Syntax > sequenceDiagram: https://mermaid.js.org/syntax/sequenceDiagram.html

It doesn't seem any of these would be naturally be able to express the example case https://raw.githubusercontent.com/eras/tlsd/master/doc/seque... . But maybe it's possible?

In addition there's also the case of messages that are never processed, but I suppose that could be its own "never handled" box.

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.

Reply on news.ycombinator.com