Producer-Consumer System/Input

• the (nonempty) set of producers
• the (nonempty) set of consumers
• the maximum number of messages in the bounded buffer
• the set of values that can be produced and/or consumed

The definition of the logic model could serve as an input of the model. If it is part of the process, then the goal could remain undefined. It also corresponds to the local variable of a program module. This issue is open to discussion.

Below is the corresponding code with the 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    *)