All,
As part of teaching myself TLA+, I built up a set of TLA+ modules to model message passing between processes, with various guarantees (e.g. perfectly reliable vs duplicates vs out-of-order). I also put together a python script which, on a failed run, parses the TLA+ output and generates an SVG representation of the timeline, showing when each message was sent and received.
I wrote up a full README on the GitHub project, along with example images, would welcome feedback:
https://github.com/dmilstein/channelsThanks,
-Dan Milstein