TLA+ modules to model message-passing with different guarantees (reliable, duplicating, out-of-order, at-least-once), and create visualizations of the results