Difference between revisions of "Producer-Consumer System/Criteria"
Jump to navigation
Jump to search
| (One intermediate revision by the same user not shown) | |||
| Line 6: | Line 6: | ||
<noinclude> | <noinclude> | ||
Turning into TLA+ code | |||
<syntaxhighlight> | <syntaxhighlight> | ||
ASSUME /\ Producers # {} (* at least one producer *) | ASSUME /\ Producers # {} (* at least one producer *) | ||
| Line 13: | Line 13: | ||
/\ BufCapacity > 0 (* buffer capacity is at least 1 *) | /\ BufCapacity > 0 (* buffer capacity is at least 1 *) | ||
/\ Data # {} (* the type of data is nonenpty *) | /\ Data # {} (* the type of data is nonenpty *) | ||
</syntaxhighlight> | </syntaxhighlight> | ||
</noinclude> | </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 *)