Incomparable Solutions and Unexpected Cuts

If the first received message is from a or b, no order is imposed on the next receptions; if the first received message is from c, then the system expects to consecutively receive either the two messages from a or the two messages from b.
Note that since there are no accepting states, the "All peers terminate" property cannot be verified.
The recommended target properties are: "The network ends up empty", and "No peer goes into a forbidden state".

Communication Model(s):

async,,a,b,c analyzed_by_pf,,a,b,c

XPeer (LTS):

1,2,!,a 2,3,!,a 3,4,!,b 4,5,!,b 5,6,!,c init,1

XPeer (LTS):

1,2,?,a 1,3,?,b 1,4,?,c 2,2,?,a 2,2,?,b 2,2,?,c 3,3,?,a 3,3,?,b 3,3,?,c 4,5,?,a 4,7,?,b 5,6,?,a 5,-1,?,b 6,6,?,b 7,8,?,b 7,-1,?,a 8,8,?,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)