Conflict

Two processes attempt to read the same message (as seen in red), depending on which one succeed, the system will be able to terminate or not.

• Add the analyzed_by_pf,,a,P1LocalLock,P1aLock,P2GoAhead,P4LocalLock communication model, then attempt to infer the correct channel priorities.

Communication Model(s):

async,,a,P1LocalLock,P1aLock,P2GoAhead,P4LocalLock

XPeer (LTS):

1,2,!,P1LocalLock 2,3,!,P1aLock 3,4,?,a 4,5,?,a 5,6,?,P1LocalLock 6,7,!,P1aLock 7,8,?,P1aLock init,1

XPeer (LTS):

1,2,?,a 2,3,!,a 3,4,!,a 4,5,!,P2GoAhead init,1

XPeer (LTS):

1,2,!,a init,1

XPeer (LTS):

1,2,!,P4LocalLock 2,3,?,P2GoAhead 3,4,?,P4LocalLock 4,5,?,P1aLock 2,1,?,P4LocalLock 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)