Producer-Consumer System/Input

The definition of the logic model is an input of the model. [to discuss] Below is the original code with definition

 
EXTENDS Naturals, Sequences
CONSTANTS Producers,   (* the (nonempty) set of producers                           *)
          Consumers,   (* the (nonempty) set of consumers                           *)
          BufCapacity, (* the maximum number of messages in the bounded buffer      *)
          Data         (* the set of values that can be produced and/or consumed    *)