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.

Communication Model(s):

analyzed_by_pf,,a,b

XPeer (LTS):

1,2,?,a 2,3,?,b 1,4,?,b 4,5,?,a init,1

XPeer (LTS):

1,2,!,a 2,3,!,b 1,4,!,b 4,5,!,a 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)