[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Modules for Messages / Rendering Timelines


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:


-Dan Milstein

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHq0T5o0oHo%3DJFo8aSMRxnBBB54yMq6ZoT2EtUS%2BdjNFK3fR7A%40mail.gmail.com.