Automated Verification of Asynchronous Communicating Systems (with TLA+)

Three Peers Interacting With Three Channels

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

Comparison of the Optimistic/Pessimistic Approaches

Additional Constraints

Incomparable Solutions and Unexpected Cuts

A Client-Server System

Alphabet

Alphabet (simplified)

Conflict

The Elevator

disabled blocker

University (CCS)