Automated Verification of Asynchronous Communicating Systems
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.
Add the analyzed_by_pf,,a,b,e communication model, then
attempt to infer the correct channel priorities.