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.

Communication Model(s):

analyzed_by_pf,,a,b,c

XPeer (LTS):

1,2,?,a 2,3,?,c init,1

XPeer (LTS):

1,2,?,b 2,3,!,c init,1

XPeer (LTS):

1,2,!,a 2,3,!,b init,1

Add CCS peerAdd LTS peer

Properties:

• All peers terminate.
• The network ends up empty.
• No peer goes into a forbidden state.
• No (global) deadlocks

Test properties Infer all constraint sets (pessimistic) Infer one constraint set (pessimistic) Infer some constraint sets (optimistic) Infer one constraint set (optimistic) Infer all constraint sets (pessimistic, listened) Infer one constraint set (pessimistic, listened) Infer some constraint sets (optimistic, listened) Infer one constraint set (optimistic, listened)