Difference between revisions of "Producer-Consumer System/Input"
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...") |
|||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
* 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 | |||
<noinclude> | <noinclude> | ||
The definition of the logic model | 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 | ||
Latest revision as of 07:54, 25 August 2021
- 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 *)