Automated Verification of Asynchronous Communicating Systems
(with TLA+)
Model Checker
Help
Examples
Download
About
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)