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

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.