This is a tool for generating sequence diagrams from TLC state traces. It produces SVGs that look like:
or like this PDF.
Link to the tool here.