# Producer-Consumer Pattern

> The producer-consumer problem with a bounded buffer: a runnable model checked so the buffer never overflows and consumers only take items that were produced.

Canonical: https://fizzbee.io/design/patterns/producer-consumer/
Source: https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-04-01-producer-consumer


Classic bounded buffer problem

**Demonstrates:** queue operations, capacity limits, coordination

```fizz
# Example 0060: Producer-Consumer Pattern
# Classic bounded buffer problem
# Demonstrates: queue operations, capacity limits, coordination

BUFFER_SIZE = 3
MAX_ITEMS = 5

action Init:
    buffer = []
    produced = 0
    consumed = 0

atomic action Produce:
    require produced < MAX_ITEMS
    # Check buffer capacity
    require len(buffer) < BUFFER_SIZE

    item = produced
    buffer.append(item)
    produced = produced + 1

atomic action Consume:
    # Check buffer has items
    require len(buffer) > 0

    item = buffer[0]
    buffer.remove(item)
    consumed = consumed + 1

# Safety: buffer never exceeds capacity
always assertion BufferBounded:
    return len(buffer) <= BUFFER_SIZE

# Safety: consumed items were produced
always assertion ValidConsumption:
    return consumed <= produced

atomic action NoOp:
    if produced >= MAX_ITEMS and len(buffer) == 0:
        pass
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 18, queued: 0
Valid Nodes: 18 Unique states: 18
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-04-01-producer-consumer)

## Language features used

[Assertions](/reference/language/assertions/), [Flow Modifiers](/reference/language/flow-modifiers/)