Automated Verification of Asynchronous Communicating Systems (with TLA+)

Three Peers Interacting With Three Channels

Using a FIFO 1-1 communication model (or pure asynchronism) async,,a,b,c, the peer below may end up in the forbidden state.
Here are some ways to fix this:

Communication Model(s):

Peer (LTS):

Peer (LTS):

Peer (LTS):

Properties: