This is example 2.26 from "MPI: The Complete Reference, vol 1," 2nd
edition.  It is the third version of the multiple-producer
single-consumer example to be considered in this section of the book.
It replaces the busy-wait test loop in example 2.19 with a single call
to MPI_Waitany.  As pointed out in the book, this has the disadvantage
that it allows "starvation"---the consumer can repeatedly consume
messages from one process while ignoring messages sent by all other
procesess.  This is reflected in our analysis:

Property 0 (Freedom From Deadlock + Assertions):  still holds.

Property 1 (Every message produced is consumed): fails.  You end up in
an infinite loop in which producer 1 has sent a message and the
request has completed, but the consumer repeatedly chooses the message
from process 0 in the Waitany.

Property 2 (No Producer can become permanently blocked): also fails,
even with progress assumptions and weak fairness.  As you can see by
running ./pan -n -r on one of the counterexamples produced by Spin,
producer 1 can send a message, this is matched by the recv posted by
the consumer, completes, producer 1 posts the second send, this one
isn't matched (because the Waitany in the consumer repeatedly returns
the producer 0 match), and it doesn't complete (the MPI infrastructure
has decided to block this completion until a matching recv is posted),
so the producer blocks at the wait.  Meanwhile the consumer repeatedly
selects the match for producer 0.

Property 3 (For fixed producer, messages are consumed in order
produced): still holds.

