------------------------- MODULE MCProducerConsumer -------------------------
EXTENDS ProducerConsumer, Naturals
MCRtnVal(v) == v^2
=============================================================================