Automated Verification of Asynchronous Communicating Systems (with TLA+)

Conflict

Two processes attempt to read the same message (as seen in red), depending on which one succeed, the system will be able to terminate or not.

Communication Model(s):

Peer (LTS):

Peer (LTS):

Peer (LTS):

Peer (LTS):

Properties: