Automated Verification of Asynchronous Communicating Systems (with TLA+)

Comparison of the Optimistic/Pessimistic Approaches

This trivial system is immediately found valid by the optimistic approach, whereas the pessimistc one requires 5 runs of the framework to conclude.
This system may terminate with an non-empty network.
Here are some ways to fix it:

Communication Model(s):

Peer (LTS):

Peer (LTS):