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

From PKC
Jump to navigation Jump to search
 
(2 intermediate revisions by the same user not shown)
Line 6: Line 6:


<noinclude>  
<noinclude>  
Turning into TLA+ code
<syntaxhighlight>  
<syntaxhighlight>  
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    *)
ASSUME /\ Producers # {}                      (* at least one producer *)
ASSUME /\ Producers # {}                      (* at least one producer *)
       /\ Consumers # {}                      (* at least one consumer *)
       /\ Consumers # {}                      (* at least one consumer *)
Line 19: 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 *)
Retrieved from "https://pkc.pub/index.php?title=Producer-Consumer_System/Criteria&oldid=10848"