# Fault Injection

> Implicit fault injection in FizzBee: crashes at yield points, message loss in RPC, and how ephemeral vs durable state behaves after a crash.

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


**FizzBee's key differentiator**: Automatic fault injection at yield points.

## Crash on Yield

By default, crashes can happen at any yield point:

```python
action MultiStep:
    step1 = True  # Yield - crash possible
    step2 = True  # Yield - crash possible
    step3 = True  # Yield - crash possible
```

**Model checker explores**:
- Normal execution (all steps complete)
- Crash after step1
- Crash after step2
- All combinations

## Enabling Crash Injection

```yaml
---
options:
  crash_on_yield: true  # Default
---
```

## Disabling Crash Injection

**Globally**:
```yaml
---
options:
  crash_on_yield: false
---
```

**Per-action**:
```yaml
---
action_options:
  CriticalPath:
    crash_on_yield: false
---
```

## Message Loss in RPC

When roles call each other, messages can be lost:

```python
role Client:
    action SendRequest:
        response = server.process()
        # Message can be lost:
        # 1. Request never sent
        # 2. Request sent, server processes, response lost
        # 3. Success (both ways)
```

**Automatic simulation** of:
- Network failures
- Process crashes
- Timeouts

## Ephemeral vs Durable State

```python
@state(ephemeral=['cache'])
role Server:
    action Init:
        self.disk_data = 0  # Durable
        self.cache = 0      # Ephemeral

    action Process:
        self.disk_data = self.disk_data + 1
        self.cache = self.cache + 1
        # If crash here:
        # - disk_data preserved
        # - cache reset to 0
```

## When Faults Are Injected

**Injected automatically**:
1. Message loss (role-to-role communication)
2. Thread crash (at yield points)
3. Process crash (ephemeral state loss)

**NOT injected (model explicitly)**:
1. Byzantine faults
2. Message duplication
3. Disk corruption
4. Message reordering

## Examples

### Crash on Yield (Implicit Fault Injection) {#example-crash-on-yield}

FizzBee's key differentiator - automatic crash fault injection

**Demonstrates:** crash_on_yield, implicit fault injection at yield points

```fizz
---
# Example 0078: Crash on Yield (Implicit Fault Injection)
# FizzBee's key differentiator - automatic crash fault injection
# Demonstrates: crash_on_yield, implicit fault injection at yield points

# Default is true - crashes can happen at yield points
options:
  max_actions: 3
  crash_on_yield: true
---

# This example shows FizzBee's automatic fault injection
# At each yield point (between statements in serial blocks),
# the model checker explores the possibility of a crash

action Init:
    step1_done = False
    step2_done = False
    step3_done = False

# Serial action has yield points between statements
action MultiStepOperation:
    require not step3_done

    # Yield point 1 (after this statement)
    step1_done = True

    # Yield point 2 (after this statement)
    step2_done = True

    # Yield point 3 (after this statement)
    step3_done = True

# Model checker automatically explores:
# - Normal execution (all steps complete)
# - Crash after step1 (step1_done=True, others False)
# - Crash after step2 (step1&2 done, step3 False)
# - etc.

# Safety: if step3 done, earlier steps must be done
always assertion StepsOrdered:
    if step3_done:
        return step1_done and step2_done
    if step2_done:
        return step1_done
    return True

atomic action NoOp:
    pass
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/14-01-crash-on-yield)

### Disable Crash on Yield {#disable-crash-on-yield}

Turning off implicit fault injection

**Demonstrates:** crash_on_yield: false, comparing with/without crashes

```fizz
---
# Example 0079: Disable Crash on Yield
# Turning off implicit fault injection
# Demonstrates: crash_on_yield: false, comparing with/without crashes

# Disable crash fault injection
options:
  max_actions: 3
  crash_on_yield: false
---

# With crash_on_yield: false, the model checker does NOT
# explore crash scenarios at yield points.
# Useful for: testing happy path, performance modeling,
# or when crashes are explicitly modeled

action Init:
    step1_done = False
    step2_done = False
    step3_done = False
    completed = False

fair action MultiStepOperation:
    require not completed

    # No crash injected after this
    step1_done = True

    # No crash injected after this
    step2_done = True

    # No crash injected after this
    step3_done = True

    completed = True

# With crash_on_yield: false and fair action,
# the operation will eventually complete
eventually always assertion EventuallyCompletes:
    return completed

atomic action NoOp:
    pass
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:3 max_concurrent_actions:2 crash_on_yield:false}
Nodes: 17, queued: 0
Valid Nodes: 17 Unique states: 17
Checking eventually always EventuallyCompletes
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/14-02-disable-crash-on-yield)

### Role Crash with Ephemeral State {#role-crash-ephemeral}

Simulating process crashes with state loss

**Demonstrates:** role crashes, ephemeral vs durable state, recovery

```fizz
# Example 0080: Role Crash with Ephemeral State
# Simulating process crashes with state loss
# Demonstrates: role crashes, ephemeral vs durable state, recovery

# Cache is ephemeral (lost on crash), disk_data is durable
@state(ephemeral=['cache'])
role Server:
    action Init:
        self.disk_data = 0  # Durable (persists across crashes)
        self.cache = 0      # Ephemeral (lost on crash)
        self.requests = 0

    action ProcessRequest:
        require self.requests < 2

        # Update disk first, then cache
        self.disk_data = self.disk_data + 1
        self.requests = self.requests + 1

        # Update cache after disk
        self.cache = self.cache + 1

        # If crash happens between disk and cache updates,
        # cache is reset to 0 (ephemeral)
        # but disk_data is preserved (durable)

action Init:
    server = Server()

# Safety: disk_data reflects durable state
always assertion DiskDataPersists:
    return server.disk_data >= 0

# Safety: cache can be behind disk_data after crash
always assertion CacheMayBeBehind:
    return server.cache <= server.disk_data

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/14-03-role-crash-ephemeral)

### Message Loss in Role Communication {#message-loss-rpc}

Automatic message loss simulation in RPC calls

**Demonstrates:** message loss, RPC failures, network unreliability

```fizz
---
# Example 0081: Message Loss in Role Communication
# Automatic message loss simulation in RPC calls
# Demonstrates: message loss, RPC failures, network unreliability

options:
  max_actions: 2
---

# When one role calls another role's function,
# FizzBee automatically explores message loss scenarios

role Client:
    action Init:
        self.state = 'init'
        self.result = None

    action SendRequest:
        require self.state == 'init'

        self.state = 'calling'
        # RPC call - can fail in multiple ways
        response = server.Process()
        self.result = response
        self.state = 'done'

role Server:
    action Init:
        self.processed = 0

    func Process():
        self.processed = self.processed + 1
        return 'OK'

action Init:
    client = Client()
    server = Server()

# Model checker explores:
# 1. Request message lost (server never receives)
# 2. Request received, response message lost (client hangs)
# 3. Successful round-trip

# Safety: if client got result, server must have processed
always assertion ResponseImpliesProcessing:
    if client.result == 'OK':
        return server.processed > 0
    return True

atomic action NoOp:
    pass
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/14-04-message-loss-rpc)