Difference between revisions of "Producer-Consumer System/Input"

From PKC
Jump to navigation Jump to search
(Created page with "<noinclude> The definition of the logic model is an input of the model. [to discuss] Below is the original code with definition <syntaxhighlight> EXTENDS Naturals, Sequence...")
 
Line 1: Line 1:
<noinclude>  
<noinclude>  
The definition of the logic model is an input of the model. [to discuss] Below is the original code with definition
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
<syntaxhighlight>  
<syntaxhighlight>  
EXTENDS Naturals, Sequences
EXTENDS Naturals, Sequences

Revision as of 07:53, 25 August 2021

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    *)