Automated Verification of Asynchronous Communicating Systems (with TLA+)

A System to Illustrate "Good" and "Bad" Solutions

With any communication model, this system reaches a terminating state (with a message in transit).
Constraint ({a} BLOCKS b) also works, but cuts off valid executions. See it by replacing the async model with channel_priorities,[a blocks b],a,b. In the trace below, the number of distinct states is lower (the transition b? is never done and the second terminating state of peer 1 is never reached).

Communication Model(s):

Peer (LTS):

Peer (LTS):