Difference between revisions of "Producer-Consumer System/Criteria"
Jump to navigation
Jump to search
(Created page with "* At least one producer * At least one consumer * No thread is both consumer and producer * Buffer capacity is at least 1 * The type of data is nonempty") |
|||
| (3 intermediate revisions by the same user not shown) | |||
| Line 4: | Line 4: | ||
* Buffer capacity is at least 1 | * Buffer capacity is at least 1 | ||
* The type of data is nonempty | * The type of data is nonempty | ||
<noinclude> | |||
Turning into TLA+ code | |||
<syntaxhighlight> | |||
ASSUME /\ Producers # {} (* at least one producer *) | |||
/\ Consumers # {} (* at least one consumer *) | |||
/\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *) | |||
/\ BufCapacity > 0 (* buffer capacity is at least 1 *) | |||
/\ Data # {} (* the type of data is nonenpty *) | |||
</syntaxhighlight> | |||
</noinclude> | |||
Latest revision as of 03:42, 30 August 2021
- At least one producer
- At least one consumer
- No thread is both consumer and producer
- Buffer capacity is at least 1
- The type of data is nonempty
Turning into TLA+ code
ASSUME /\ Producers # {} (* at least one producer *)
/\ Consumers # {} (* at least one consumer *)
/\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *)
/\ BufCapacity > 0 (* buffer capacity is at least 1 *)
/\ Data # {} (* the type of data is nonenpty *)