Producer-Consumer System/Criteria

• 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 *) 
...