Generate (message) sequence diagrams from TLA+ state traces
This is a tool for generating sequence diagrams from
TLC state traces. It produces
SVGs that look like:
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