Automated Verification of Asynchronous Communicating Systems
(with TLA+)
Comparison of the Optimistic/Pessimistic Approaches
This trivial system is immediately found valid by the optimistic approach,
whereas the pessimistc one requires 5 runs of the framework to conclude.
This system may terminate with an non-empty network.
Here are some ways to fix it:
Replace async by fifo11.
Add the fifo11,,a,b communication model.
Add the
channel_priorities,"BLOCKS <- {<<{""a""},""b"">>}",a,b
communication model.
Add the analyzed_by_pf,,a,b communication model, then
attempt to infer the correct channel priorities.