Skip to content

Latest commit

 

History

History
89 lines (68 loc) · 3.68 KB

README.md

File metadata and controls

89 lines (68 loc) · 3.68 KB
Raw

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 Seppälä [email protected] 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.