https://github.com/eras/tlsd Skip to content Navigation Menu Toggle navigation Sign in * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + GitHub Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions By size + Enterprise + Teams + Startups By industry + Healthcare + Financial services + Manufacturing By use case + CI/CD & Automation + DevOps + DevSecOps * Resources Topics + AI + DevOps + Innersource + Open Source + Security + Software Development Explore + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Enterprise + Enterprise platform AI-powered developer platform Available add-ons + Advanced Security Enterprise-grade security features + GitHub Copilot Enterprise-grade AI features + Premium Support Enterprise-grade 24/7 support * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} eras / tlsd Public * Notifications You must be signed in to change notification settings * Fork 0 * Star 18 Generate (message) sequence diagrams from TLA+ state traces License MIT license 18 stars 0 forks Branches Tags Activity Star Notifications You must be signed in to change notification settings * Code * Issues 1 * Pull requests 0 * Actions * Projects 0 * Security * Insights Additional navigation options * Code * Issues * Pull requests * Actions * Projects * Security * Insights eras/tlsd This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master BranchesTags Go to file Code Folders and files Name Name Last commit message Last commit date Latest commit History 103 Commits doc doc examples examples tlsd tlsd .dir-locals.el .dir-locals.el .gitignore .gitignore .mypy.ini .mypy.ini LICENSE.MIT LICENSE.MIT README.md README.md setup.py setup.py View all files Repository files navigation * README * MIT license tla-sequence-diagram This is a tool for generating sequence diagrams from TLC state traces. It produces SVGs that look like: Sequence diagram or like this PDF. This tool is licensed under the MIT license. Copyright: Erkki Seppala erkki.seppala@vincit.fi 2022 You can contact me also via Matrix. What is TLA+? TLA+ (Temporal Logic of Actions+) is a way to describe the behavior of an algorithm or a system at a high, yet in a very mathematically precise manner. This allows one to reason about the system behavior in a more accurate way than with a textual description of system behavior. Combined with the tool TLC (Temporal Logic Checker) to do checks with those models it increases the confidence of getting the design right from the beginning--or later on finding corner cases in the design that had not been detected by rigorous testing or code reviews. You can learn more about TLA+ at the TLA+ home page. There's even a book! So what is this tool then? When using TLC and an invariant you have set up for it fails, you end up with a state dump. Sometimes this state dump can become unwieldy or at least very slow to to analyze. This tool aims to help analyzing certain kind of systems: the ones that are composed of individual nodes exchanging messages with each other. It achieves this by converting translated state traces into something that's very close to standard sequence diagrams. The only difference I see compared to standard sequence diagrams is that the message sending and reception are decoupled in the diagram: messages will be received later--sometimes much later--compared to when they've been sent, and other behavior can be interleaved during that time. I'm not sure if the standard diagrams would also be able to express this, though, but if this is the case then perhaps a lot of this SVG rendering code would be needles :). Any node can exchange messages with any other node, though the example doesn't yet demonstrate this. The tool doesn't try to avoid overlapping labels or lines with other objects yet, but this is also something I'm planning to implement at some point. Trying out the example 1. clone the repository, cd to it 2. pip install . You may wish to sudo apt install python3-pillow first in Debian-based systems. A good alternative to plain pip is to use pipx: pipx install .. 3. cd examples 4. run tlc pingpong | tlsd to get sequence.svg pingpong.cfg refers to ALIAS AliasMessages where the ALIAS is defined in pingpong.tla to produce output in the form the tool currently expects it at. To produce decent pdfs out of the svg files you can use Inkscape: inkscape --export-pdf=sequence.pdf sequence.svg Theory of operation At each state (in the dump) there is JSON value with the key messages_json, which contains all the pending messages between server and the clients. Currently the tool assumes there is a central server all want to exchange messages with, as there is no way to indicate which server a client is interacting with. There are two kinds of channels in the example: ones from the server to the clients and ones from the clients to the server. Once a message appears in a channel (e.g. the channel is busy), it is considered to be sent by the tool. Once a message disappears (no longer busy) from the channel, it is considered to have been received by the peer. About Generate (message) sequence diagrams from TLA+ state traces Topics model-checking sequence-diagram tlaplus Resources Readme License MIT license Activity Stars 18 stars Watchers 2 watching Forks 0 forks Report repository Releases No releases published Packages 0 Languages * Python 99.5% * Emacs Lisp 0.5% Footer (c) 2024 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.