Automated Verification of Asynchronous Communicating Systems (with TLA+)

disabled blocker

There is no way to make this system work.
This example explores the effects of using other communication models in tandem with channel priorities.
As the communication models's are independantly evaluated, the BLOCKS constraints are applied even when the channel "enforcing" them is disabled in another communication model.

Communication Model(s):

Peer (LTS):