# Best Practices

> Writing FizzBee specs that check fast and mean what you think: bounding state, guard clauses, atomic vs serial, role design, assertions and fairness.

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


## State Space Management

**Always bound your state**:
```python
# ❌ BAD: Unbounded
action Increment:
    counter = counter + 1  # Grows forever!

# ✅ GOOD: Bounded
action Increment:
    if counter >= MAX_VALUE:
        return
    counter = counter + 1
```

**Use modulo for cyclic behavior**:
```python
counter = (counter + 1) % MAX_VALUE
```

## Guard Clauses

Use early returns for enabling conditions:

```python
action Process:
    if not ready:
        return
    if items_empty:
        return
    # Main logic here
```

## Multiple Assignment for Atomicity

Use tuple assignment to update multiple variables atomically:

```python
# ❌ Creates 3 yield points in serial context
action Update:
    a = 1  # Yield point
    b = 2  # Yield point
    c = 3  # Yield point
    # Other actions can run between these

# ✅ Single statement = atomic in serial context
action Update:
    a, b, c = 1, 2, 3  # Single yield point after
    # All three updated together
```

**Use cases**:
- Swapping values: `x, y = y, x`
- Coordinated updates: `min_val, max_val = 0, 100`
- Avoiding intermediate states visible to other actions

**Note**: This applies to serial contexts. In atomic blocks, all statements are atomic anyway.

## Variable Extraction Changes Behavior

Extracting local variables can alter execution order and atomicity:

```python
# Original: Function called every iteration
action Process:
    for i in range(get_count()):  # get_count() called each iteration
        process(i)

# Extracted: Function called once
action Process:
    count = get_count()  # Called once, creates yield point
    for i in range(count):
        process(i)
```

**Impact**:
- Changes when function is evaluated
- Creates additional yield points
- May change behavior if state changes between calls

**Best practice**: Be deliberate about extraction for clarity, but understand the semantic difference.

## Atomic vs Serial

**Prefer atomic when**:
- Operations must complete together
- Modeling transactions
- Reducing state space

**Use serial when**:
- Modeling real sequencing
- Testing crash scenarios
- Exploring interleavings

## Function Calls

**Remember restrictions**:
```python
# Functions must be called from:
# 1. Atomic context
atomic action CallFunc:
    result = my_function()  # OK

# 2. Roles
role MyRole:
    action DoWork:
        result = my_function()  # OK

# NOT from serial actions
action BadExample:
    result = my_function()  # ERROR!
```

## Role Design

**Encapsulate related state**:
```python
# ✅ GOOD: Cohesive role
role Account:
    action Init:
        self.balance = 0
        self.transactions = []

    func deposit(amount):
        self.balance += amount
```

**Mark ephemeral state explicitly**:
```python
@state(ephemeral=['cache', 'temp_results'])
role Worker:
    # Durable state persists across crashes
    # Ephemeral state is lost
```

## Assertions

**Write clear invariants**:
```python
# ✅ GOOD: Clear condition
always assertion BalanceNonNegative:
    return account.balance >= 0

# ❌ BAD: Complex, unclear
always assertion ComplexCheck:
    return (a > 0 and b < 10) or (c == d and e != f)
```

**Use appropriate assertion types**:
- `always`: Safety (invariants)
- `eventually always`: Liveness (termination)
- `exists`: Reachability
- `transition`: State transition properties

## Fairness

**Add fairness for liveness**:
```python
# Without fairness - may starve
action Progress:
    counter = counter + 1

# With fairness - will execute
fair action Progress:
    counter = counter + 1

eventually always assertion EventuallyDone:
    return counter >= 10  # Requires fairness
```

## Crash Injection

**Use selectively**:
```python
# Enable for fault-sensitive paths
options:
  crash_on_yield: true

# Disable for performance modeling
action_options:
  ComputeMetrics:
    crash_on_yield: false
```

## Examples

### State Space Best Practices {#state-space-best-practices}

Always bound your state variables to prevent explosion

**Demonstrates:** modulo arithmetic, guard clauses, bounded ranges

```fizz
# Example 0056: State Space Best Practices
# Always bound your state variables to prevent explosion
# Demonstrates: modulo arithmetic, guard clauses, bounded ranges

MAX_VALUE = 10

action Init:
    counter = 0
    cyclic_counter = 0
    items = []

# ✅ GOOD: Guard clause bounds the state
atomic action IncrementWithGuard:
    require counter < MAX_VALUE

    counter = counter + 1

# ✅ GOOD: Modulo arithmetic for cyclic behavior
atomic action IncrementCyclic:
    cyclic_counter = (cyclic_counter + 1) % MAX_VALUE

# ✅ GOOD: Bounded collection growth
atomic action AddItem:
    require len(items) < 5

    items.append(len(items))

# ❌ BAD: Would be unbounded without guard
# atomic action UnboundedIncrement:
#     counter = counter + 1  # Grows forever!

# Always use assertions to verify bounds
always assertion CounterInBounds:
    return counter <= MAX_VALUE and cyclic_counter < MAX_VALUE

atomic action NoOp:
    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: 660, queued: 0
Skipping dotfile generation. Too many Nodes: 660
Valid Nodes: 660 Unique states: 660
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/12-04-state-space-best-practices)

### Error Handling Pattern {#error-handling-pattern}

Model errors and recovery explicitly

**Demonstrates:** oneof for success/failure, error states

```fizz
# Example 0057: Error Handling Pattern
# Model errors and recovery explicitly
# Demonstrates: oneof for success/failure, error states

ErrorCode = enum('OK', 'TIMEOUT', 'INVALID')

action Init:
    state = "idle"
    error = None
    retry_count = 0

action ProcessRequest:
    require state == "idle"

    state = "processing"

    # Nondeterministically succeed or fail
    oneof:
        # Success path
        state = "completed"
        error = ErrorCode.OK

        # Timeout path
        state = "error"
        error = ErrorCode.TIMEOUT

        # Invalid input path
        state = "error"
        error = ErrorCode.INVALID

action Retry:
    require state == "error"

    if retry_count >= 2:
        state = "failed"
        return

    retry_count = retry_count + 1
    state = "idle"
    error = None

# Verify error handling invariant
always assertion NoInfiniteRetries:
    return retry_count <= 2

atomic action NoOp:
    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: 240, queued: 0
Valid Nodes: 240 Unique states: 213
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/12-05-error-handling-pattern)