Best Practices

State Space Management

Always bound your state:

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

counter = (counter + 1) % MAX_VALUE

Guard Clauses

Use early returns for enabling conditions:

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:

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

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

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

# ✅ GOOD: Cohesive role
role Account:
    action Init:
        self.balance = 0
        self.transactions = []

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

Mark ephemeral state explicitly:

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

Assertions

Write clear invariants:

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

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

# 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

Always bound your state variables to prevent explosion

Demonstrates: modulo arithmetic, guard clauses, bounded ranges

Run in playground

 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


# 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

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

Error Handling Pattern

Model errors and recovery explicitly

Demonstrates: oneof for success/failure, error states

Run in playground

 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


# 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

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