# Quick Reference

> A FizzBee cheat sheet: common spec patterns such as mutexes and retries, plus debugging tips for failing or slow model checks.

Canonical: https://fizzbee.io/reference/language/quick-reference/
Source: https://github.com/fizzbee-io/fizzbee/blob/main/examples/references/LANGUAGE_REFERENCE.md#quick-reference


## Common Patterns

**Mutex**:
```python
action AcquireLock:
    require lock_holder == None
    lock_holder = "me"
```

**Producer-Consumer**:
```python
action Produce:
    if len(buffer) >= CAPACITY:
        return
    buffer.append(item)

action Consume:
    require len(buffer) > 0
    item = buffer.pop(0)
```

**Retry with Backoff**:
```python
action Retry:
    if retries >= MAX_RETRIES:
        return
    if attempt():
        success = True
    else:
        retries = retries + 1
```

**Action Coordination with Require and Yield** ([Example 0083](/reference/language/configuration/#action-coordination)):

Use `require` in the middle of an action to wait for conditions set by other actions:

```python
---
deadlock_detection: false
options:
    crash_on_yield: false
---

action Init:
    a = 0

action Step1:
    require a == 0     # Only start when a is 0
    a = 1              # Update a, then yield point
    require a == 2     # Wait here until a becomes 2
    a = 3              # Continue when condition met

action Step2:
    require a == 1     # Only enabled when a is 1
    a = 2              # Set a to 2, unblocking Step1
```

**How this works**:

1. Step1 starts (a == 0), sets a = 1
2. **Yield point** after `a = 1`
3. Step1 thread tries to continue, hits `require a == 2` which **fails**
4. Step1 continuation is **disabled** (not scheduled)
5. Model checker schedules another action
6. Step2 is now **enabled** (a == 1), runs and sets a = 2
7. Step1 can now be **rescheduled**, `require a == 2` passes
8. Step1 continues to set a = 3

**Effect**: Step1 effectively "waits" for Step2 to update the state before continuing

**Use cases**:
- Synchronization between actions
- Handshake protocols
- Multi-phase coordination
- Waiting for preconditions without busy-waiting

**Key insight**: `require` in the middle of an action + yield points = coordination mechanism

**Note**: This pattern explores interleavings where actions wait for each other, useful for modeling synchronization primitives

## Debugging Tips

1. **Start small**: Test with small bounds first
2. **Check state space**: Monitor node/state counts
3. **Use assertions**: Verify invariants as you go
4. **Disable crashes**: Test happy path first with `crash_on_yield: false`
5. **Add NoOp actions**: Prevent deadlocks at terminal states