Develop a TLA specification of a software system, which has several producers and consumers, communicating via a shared buffer. The buffer holds data, created by producing processes until the data are retrieved by consuming processes. The buffer acts as a synchronizer, blocking and suspending processes when there is nothing for processes to do. When the buffer is empty, any consuming process needs to wait until there are data in the buffer. The buffer has finite capacity; therefore, producing processes must be suspended when the buffer is full.

Define structure of specification (declaration of constants and variables; initial and next state predicates; a type invariant and a theorem).

Define Put data and Get data actions.

Formulate the following safety properties, in which:
at least one producer is in the system;

at least one consumer is in the system;

a process cannot be both consumer and producer;

a buffer contains a sequence of the data elements sent; and

the length of the data in the buffer are inside of the buffer boundaries.

Define liveness property, that eventually often buffer is either empty or full.

Give definition of no deadlock property, when producers and consumers wait on the same object.