FizzBee Specification Language and Model Checker

The examples/references/ directory contains a comprehensive collection of 100 examples organized by topic to help developers learn the FizzBee specification language and provide reference for AI coding agents. Examples use a hierarchical numbering system (e.g., 01-01, 13-02-01) to categorize features from basic syntax to complex distributed systems patterns.

Key documentation resources available alongside these examples include:

• FizzBee Language Reference Guide: Complete specification of syntax and semantics.
• Performance Guide: Strategies for reducing state space and runtime.
• Gotchas and Common Issues: Known pitfalls and workarounds.
• Verification Guide: Methods for sanity-checking specifications using simulation and guided traces.

Rotational symmetry is used for values that wrap around a ring (integers mod limit). Arithmetic like p + 1 will wrap from limit-1 back to 0. Note that ordering operators like < or > are not supported because the domain is circular.

RING = symmetry.rotational(name="pos", limit=5)

atomic action Advance:
    p = oneof positions
    next_p = p + 1  # wraps: 4 + 1 = 0 on ring of 5

The following patterns are commonly implemented in FizzBee to verify distributed protocols:

• Mutual Exclusion: Using Mutex patterns with lock/unlock actions and critical sections.
• Consensus: Implementing protocols like Two-Phase Commit (2PC), Paxos-style proposals, or simple quorum-based acceptance.
• Concurrency Control: Implementing Optimistic Locking (version-based), Read-Write Locks, or Compare-And-Swap (CAS).
• Reliability Patterns: Implementing Circuit Breakers, Idempotent Operations (using request IDs), and Saga patterns (with compensating transactions).
• Data Consistency: Modeling Eventual Consistency (replica synchronization) and Cache Coherence (invalidation/write-through).

Symmetry reduction collapses equivalent states. Choosing the correct type for your domain is critical for performance:

Note on symmetric role: When using symmetric role with bag(), removed-then-recreated actors map to the same canonical states, which avoids the need for a maximum creation cap.

symmetric role Employee:
    action Init:
        self.status = "active"

FizzBee has built-in mechanisms to simulate real-world unreliability:

• Implicit Fault Injection (crash_on_yield): By default, FizzBee automatically injects crashes at yield points (anywhere the execution might pause, such as between statements in a serial block or between loop iterations). This is a key differentiator for testing system resilience.
• Disabling Crashes: To test the 'happy path' or liveness properties without automatic crashes, set crash_on_yield: false in your configuration.
• Role Crashes: You can simulate process crashes with state loss by using ephemeral state in roles. When a role crashes, its ephemeral state is lost, while durable state persists.
• Message Loss: FizzBee automatically simulates message loss in RPC calls to model network unreliability.

Unlike TLA+, Fizz does not strictly separate guard clauses (preconditions) from state transitions. Instead, Fizz uses standard programming constructs like if blocks to handle preconditions within an action. This approach is designed to be more intuitive for programmers and simplifies the implementation of the model checker.

When writing an action, if a condition must be met for the action to be enabled, you should use an if statement at the top of the action block. For example, to implement a TLA+ action that only increments a counter if it is less than 10, you would write:

action Count:
  if count < 10:
    count = count + 1

Fizz provides three ways to express state transitions, making them more readable for programmers than TLA+ primed notation:

1. Simplified Notation (Recommended): Use standard assignment. count = count + 1 represents the transition.
2. Explicit Notation: Use this for the current state and next for the next state. next.count = this.count + 1.
3. Implicit UNCHANGED: Unlike TLA+, if a variable is not mentioned in a transition, Fizz assumes it remains unchanged. You do not need to explicitly declare UNCHANGED.

# Simplified Fizz notation
count = count + 1

# Fizz explicit notation
next.count = this.count + 1

Interval Arithmetic

Interval symmetry supports arithmetic. val + int and val - int produce new symmetric values. The model checker normalizes by subtracting the minimum value (zero-shifting).

Divergence

Use the divergence parameter to bound the spread (max - min). Transitions that would exceed this bound are automatically pruned.

Reflection

Setting reflection=True makes mirror-image states equivalent (e.g., {t1=0, t2=3} is equivalent to {t1=3, t2=0}).

# Bounding spread to 3
SEQ = symmetry.interval(name="s", divergence=3)

# Interval with reflection
TICKS = symmetry.interval(name="t", limit=6, reflection=True)

The library is designed for programmatic, in-memory use within Go applications. It differs from the CLI tool in several key ways:

You can synchronize actions by using the require keyword in the middle of an action. When require fails, the current action's continuation is disabled (it yields), allowing the model checker to schedule other actions. Once the condition in require is met by another action, the original action is rescheduled and continues.

action Step1:
    require a == 0     # Wait for precondition
    a = 1              # Update state, then yield
    require a == 2     # Wait for Step2 to update 'a'
    a = 3              # Continue when condition met

action Step2:
    require a == 1     # Only enabled when Step1 sets a=1
    a = 2              # Unblocks Step1