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

From PKC
Jump to navigation Jump to search
Line 6: Line 6:


<noinclude>  
<noinclude>  
Original code for success criteria
<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 *)

Revision as of 12:44, 25 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


Original code for success criteria 

 
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=10211"