Automated Verification of Asynchronous Communicating Systems
(with TLA+)
Three Peers Interacting With Three Channels
Using a FIFO 1-1 communication model (or pure asynchronism) async,,a,b,c, the peer below
may end up in the forbidden state.
Here are some ways to fix this:
Replace async or fifo11 by the causal communication model: causal,,a,b,c.
Add the
channel_priorities,[a blocks c],a,c
communication model.
(alternative syntax: channel_priorities,"BLOCKS <- {<<{""a""},""c"">>}",a,c)
Add the analyzed_by_pf,,a,b,c communication model, then
attempt to infer the correct channel priorities.