Fault Injection

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

---
options:
  crash_on_yield: true  # Default
---

---
options:
  crash_on_yield: false
---

---
action_options:
  CriticalPath:
    crash_on_yield: false
---

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)

@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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

---
# 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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

---
# 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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

# 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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51

---
# 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

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

gdoc_arrow_left_alt State Management Configuration gdoc_arrow_right_alt