[HN Gopher] Tlsd: Generate (message) sequence diagrams from TLA+...
       ___________________________________________________________________
        
       Tlsd: Generate (message) sequence diagrams from TLA+ state traces
        
       Author : todsacerdoti
       Score  : 71 points
       Date   : 2024-07-15 16:33 UTC (1 days ago)
        
 (HTM) web link (github.com)
 (TXT) w3m dump (github.com)
        
       | sterlind wrote:
       | 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.
        
         | westurner wrote:
         | 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
        
       | _flux wrote:
       | 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.
        
       | mycall wrote:
       | Have you looked at using mermaidjs instead of SVG as an output?
       | It might translate easier and plug into other solutions easier.
        
         | westurner wrote:
         | 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
        
       ___________________________________________________________________
       (page generated 2024-07-16 23:01 UTC)