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".