Automated Verification of Asynchronous Communicating Systems (with TLA+)

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):

Peer (LTS):

Peer (LTS):