# Configuration

> Configuring the FizzBee model checker: options in YAML frontmatter or fizz.yaml, per-action options, and which setting takes precedence.

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


## Options

Global configuration in YAML frontmatter:

```yaml
---
# Global options
options:
  max_actions: 100              # Max total action executions
  max_concurrent_actions: 2     # Max actions running in parallel
  crash_on_yield: true          # Enable crash fault injection (default: true)

# Deadlock detection
deadlock_detection: true        # Enable deadlock checking (default: true)
                                # Set to false if deadlock is expected/acceptable

# Liveness checking
liveness: "false"               # Disable liveness checking
# liveness: "strict"            # Enable strict liveness checking
# liveness: true                # Enable liveness checking

# Custom seed for reproducibility
seed: 12345                     # Optional: for reproducing specific runs
---
```

**Available global options**:

| Option | Type | Default | Description |
|--------|------|---------|-------------|
| `max_actions` | int | unlimited | Total action executions before stopping |
| `max_concurrent_actions` | int | unlimited | Maximum actions running in parallel |
| `crash_on_yield` | bool | `true` | Enable automatic crash injection at yield points |
| `deadlock_detection` | bool | `true` | Check for deadlock states |
| `liveness` | string/bool | `false` | Liveness checking mode: `"false"`, `true`, `"strict"` |
| `seed` | int | random | Random seed for reproducible runs |

**Common configurations**:

```yaml
# Fast exploration (no crashes)
---
options:
  crash_on_yield: false
  max_concurrent_actions: 1
---

# Thorough testing
---
options:
  crash_on_yield: true
  max_concurrent_actions: 3
liveness: "strict"
deadlock_detection: true
---

# Debugging specific scenario
---
options:
  max_actions: 50
seed: 12345
---
```

## Action-Level Options

Override options per action:

```yaml
---
action_options:
  HighFrequency:
    max_actions: 50             # Limit this action

  CriticalPath:
    crash_on_yield: false       # No crashes for this

  BackgroundTask:
    max_concurrent_actions: 1   # Only one at a time
---
```

**For role actions**, use special notation:

```yaml
---
action_options:
  # Limit across ALL Server instances combined
  "Server.Process":
    max_actions: 10

  # Limit PER Server instance
  "Server#.Process":
    max_concurrent_actions: 1   # Each instance runs at most 1

  # Thread example: disable crashes, limit concurrency per thread
  "Thread.Run":
    crash_on_yield: false
  "Thread#.Run":
    max_concurrent_actions: 1   # Only 1 Run per Thread instance
---
```

**Notation**:
- `"Role.Action"` - Limits apply **across all instances** of the role
- `"Role#.Action"` - Limits apply **per individual instance** of the role
- Top-level actions - Use action name directly (no quotes needed)

**Example**:

```python
role Worker:
    action Process:
        # Do work
        pass

action Init:
    workers = [Worker(), Worker(), Worker()]

# With "Worker.Process": max_actions: 5
# → Total of 5 Process actions across all 3 workers

# With "Worker#.Process": max_actions: 5
# → Each worker can execute Process 5 times (15 total possible)
```

## Configuration Precedence

1. Action-specific options (highest priority)
2. Global options
3. Default values (lowest priority)

## Examples

### YAML Frontmatter Configuration {#yaml-frontmatter}

Configure model checker behavior

**Demonstrates:** options with max_actions, deadlock_detection

```fizz
---
# Example 0054: YAML Frontmatter Configuration
# Configure model checker behavior
# Demonstrates: options with max_actions, deadlock_detection

options:
  max_actions: 20

deadlock_detection: false
---

# This spec intentionally hits max_actions limit
action Init:
    counter = 0

atomic action Increment:
    # No guard - runs forever (until max_actions)
    counter = counter + 1

# Demonstrates hitting the configured limit
# With max_actions: 20, this will stop at 20 instead of default 100
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:20 max_concurrent_actions:2} deadlock_detection:false
Nodes: 21, queued: 0
Valid Nodes: 21 Unique states: 21
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/12-02-yaml-frontmatter)

### Action-Level Configuration {#action-level-config}

Per-action limits and crash settings

**Demonstrates:** action_options, per-action max_actions, crash_on_yield

```fizz
---
# Example 0082: Action-Level Configuration
# Per-action limits and crash settings
# Demonstrates: action_options, per-action max_actions, crash_on_yield

# Global options
options:
  max_actions: 100
  crash_on_yield: true

# Per-action overrides
action_options:
  HighFrequency:
    max_actions: 5  # Limit this action to 5 executions

  CriticalPath:
    crash_on_yield: false  # Disable crashes for this action

  BackgroundTask:
    max_concurrent_actions: 1  # Only one instance at a time
---

action Init:
    high_freq_count = 0
    critical_count = 0
    background_count = 0

# Limited to 5 executions by action_options
action HighFrequency:
    require high_freq_count < 10

    high_freq_count = high_freq_count + 1

# No crash injection (crash_on_yield: false)
action CriticalPath:
    require critical_count < 3

    # These steps run without crash injection
    critical_count = critical_count + 1
    # More work here...

# Only runs once at a time (max_concurrent_actions: 1)
action BackgroundTask:
    require background_count < 2

    background_count = background_count + 1

# Safety: high frequency action respects limit
always assertion HighFreqWithinLimit:
    return high_freq_count <= 5

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 crash_on_yield:true} action_options:{key:"BackgroundTask" value:{max_concurrent_actions:1}} action_options:{key:"CriticalPath" value:{crash_on_yield:false}} action_options:{key:"HighFrequency" value:{max_actions:5}}
Nodes: 72, queued: 0
Valid Nodes: 72 Unique states: 72
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/15-01-action-level-config)

### Action Coordination {#action-coordination}

Using require mid-action with yield points for synchronization

**Demonstrates:** require as wait mechanism, action coordination

```fizz
# Example 0083: Action Coordination
# Using require mid-action with yield points for synchronization
# Demonstrates: require as wait mechanism, action coordination

---
deadlock_detection: false
options:
    crash_on_yield: false
---

action Init:
    stage = 0

# First action: does work in stages, waits for second action
action Step1:
    require stage == 0     # Only start when stage is 0
    stage = 1              # Set to stage 1, then yield

    # After yield, this require acts as a "wait"
    # Step1 continuation disabled until stage becomes 2
    require stage == 2     # Wait for Step2 to advance stage
    stage = 3              # Continue when condition met

# Second action: advances stage when ready
action Step2:
    require stage == 1     # Only enabled when Step1 sets stage to 1
    stage = 2              # Advance to stage 2, unblocking Step1

# Execution flow:
# 1. Step1 starts (stage == 0), sets stage = 1
# 2. Yield point after stage = 1
# 3. Step1 tries to continue, hits require stage == 2, fails
# 4. Step1 continuation disabled
# 5. Step2 becomes enabled (stage == 1), runs, sets stage = 2
# 6. Step1 can be rescheduled, require passes
# 7. Step1 continues, sets stage = 3

# This pattern is equivalent to:
# - Step1 "waits" for Step2
# - Handshake/synchronization between actions
# - Multi-phase coordination without busy-waiting

always assertion StageMonotonic:
    return stage >= 0 and stage <= 3

transition assertion StageIncrementsOneAtATime(before, after):
    # Stutter step allowed (no change)
    if after.stage == before.stage:
        return True
    # When stage changes, must increment by exactly 1
    return after.stage == before.stage + 1

exists assertion ReachesStage3:
    return stage == 3
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/15-02-action-coordination)