Roles

Definition

Roles are class-like structures representing actors, processes, or components in a distributed system.

role Server:
    action Init:
        self.data = {}
        self.version = 0

    action Process:
        self.version = self.version + 1

    func get_data(key):
        return self.data.get(key, None)

Characteristics

Instance-based: Create multiple instances
State encapsulation: Each instance has independent state
Implicit self: Like Java’s this, no need to pass self
Role Init: Constructor-like initialization
Actions and functions: Can have both

Role Init Action

The Init action in a role acts like a constructor:

role Account:
    action Init:
        # Initialize instance state
        self.balance = 0
        self.owner = None

# Create instance with parameters
action Init:
    account = Account(INITIAL_BALANCE=100, ACCOUNT_ID=1)

State Variables

Only self.* variables are part of role state:

role Example:
    action Init:
        self.persisted = 0  # Part of state
        temp = 100          # NOT part of state (local variable)

Special Role Fields

self.__id__ - Auto-generated unique identifier:

role Server:
    action Init:
        self.name = "server"
        # self.__id__ is automatically set by FizzBee

    action LogStatus:
        print(f"Server {self.__id__}: {self.status}")

action Init:
    servers = []
    for i in range(3):
        servers.append(Server())
    # servers[0].__id__ != servers[1].__id__ != servers[2].__id__

Use cases:

Distinguishing role instances in logs
Using instance ID in message routing
Debugging and visualization

Note: __id__ is read-only and unique across all role instances

Durable vs Ephemeral State

Use @state decorator to mark ephemeral fields:

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

Alternatively, mark durable fields:

@state(durable=['disk_data'])
role Server:
    action Init:
        self.disk_data = 0  # Durable
        self.cache = 0      # Ephemeral (not in durable list)

Rules:

Cannot specify both durable and ephemeral
Default: all state is durable
On crash: ephemeral fields reset to Init values

Role Communication

Roles communicate by calling each other’s functions:

role Client:
    action SendRequest:
        response = server.process()  # RPC call

role Server:
    func process():
        return "OK"

Automatic fault injection: Message can be lost (see Fault Injection section)

Examples

Simple Role

Basic role definition (like a class)

Demonstrates: role keyword, role structure

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


# Example 0046: Simple Role
# Basic role definition (like a class)
# Demonstrates: role keyword, role structure

role Account:
    action Init:
        # self prefix makes it part of role state
        self.balance = 0
        self.owner = "alice"

    action Deposit:
        require self.balance < 100

        self.balance = self.balance + 10

# Create role instance
action Init:
    account = Account()

# Role instances can have their own state
# Multiple instances would have independent state

atomic action NoOp:
    if account.balance >= 100:
        pass

Expected result (from fizz):

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

Source on GitHub

Role Init

Role Init action is like a constructor

Demonstrates: role initialization with parameters

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


# Example 0047: Role Init
# Role Init action is like a constructor
# Demonstrates: role initialization with parameters

role Account:
    # Init is called when role is instantiated
    action Init:
        # self.OWNER comes from constructor parameter
        self.balance = 0
        self.name = self.OWNER  # Use parameter

    action Deposit:
        require self.balance < 50

        self.balance = self.balance + 10

# Create role instances with parameters
action Init:
    alice_account = Account(OWNER="alice")
    bob_account = Account(OWNER="bob")
    counter = 0

atomic action IncrementCounter:
    require counter < 2
    counter = counter + 1

# Each instance has its own state
# alice_account.name = "alice"
# bob_account.name = "bob"

atomic action NoOp:
    if counter >= 2:
        pass

Expected result (from fizz):

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

Source on GitHub

Role Actions

Actions within roles

Demonstrates: role actions, implicit self

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


# Example 0048: Role Actions
# Actions within roles
# Demonstrates: role actions, implicit self

role Account:
    action Init:
        self.balance = 0

    # Role actions don't take parameters (like top-level actions)
    # self is implicit (no need to declare)
    action Deposit:
        require self.balance < 50

        self.balance = self.balance + 10

    action Withdraw:
        require self.balance >= 10

        self.balance = self.balance - 10

action Init:
    account = Account()

# Role actions are called by the model checker
# Just like top-level actions
# The model checker explores all enabled role actions

atomic action NoOp:
    pass

Expected result (from fizz):

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

Source on GitHub

Role Functions

Functions within roles

Demonstrates: role functions, implicit self

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


# Example 0049: Role Functions
# Functions within roles
# Demonstrates: role functions, implicit self

role Calculator:
    action Init:
        self.total = 0

    # Functions in roles - self is implicit
    # No self parameter needed (like Java/C++)
    func add(x, y):
        return x + y

    func accumulate(value):
        self.total = self.total + value
        return self.total

    atomic action Compute:
        require self.total < 10

        # Call role functions
        sum = self.add(2, 3)
        self.accumulate(sum)

action Init:
    calc = Calculator()

atomic action NoOp:
    if calc.total >= 10:
        pass

Expected result (from fizz):

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

Source on GitHub

Role State

Only self.* variables are part of role state

Demonstrates: role state variables vs local variables

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


# Example 0050: Role State
# Only self.* variables are part of role state
# Demonstrates: role state variables vs local variables

role Account:
    action Init:
        # State variables (persisted)
        self.balance = 0
        self.transactions = 0

        # Local variable (not persisted)
        temp = 100  # This is NOT part of state

    action Deposit:
        require self.balance < 50

        # Local variables don't affect state
        amount = 10

        # Only self.* updates are persisted
        self.balance = self.balance + amount
        self.transactions = self.transactions + 1

action Init:
    account = Account()

# Only self.balance and self.transactions are part of state
# Local variables like temp, amount are not tracked

atomic action NoOp:
    if account.balance >= 50:
        pass

Expected result (from fizz):

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

Source on GitHub

Role Decorators

@state decorator marks durable vs ephemeral fields

Demonstrates: @state(durable=[…]) and @state(ephemeral=[…])

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


# Example 0051: Role Decorators
# @state decorator marks durable vs ephemeral fields
# Demonstrates: @state(durable=[...]) and @state(ephemeral=[...])

# Mark cache as ephemeral (lost on crash)
@state(ephemeral=['cache'])
role Storage:
    action Init:
        # Durable state (persists across crashes)
        self.data = {}

        # Ephemeral state (lost on crash)
        self.cache = {}

    atomic action Write:
        require len(self.data) < 2

        key = "key_" + str(len(self.data))
        self.data[key] = "value"
        self.cache[key] = "cached_value"

# Can also mark durable explicitly:
# @state(durable=['data'])
# This makes everything else ephemeral

action Init:
    storage = Storage()

atomic action NoOp:
    if len(storage.data) >= 2:
        pass

Expected result (from fizz):

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

Source on GitHub

Role Instances

Creating and managing multiple role instances

Demonstrates: multiple instances with independent state

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


# Example 0052: Role Instances
# Creating and managing multiple role instances
# Demonstrates: multiple instances with independent state

role Account:
    action Init:
        self.balance = self.INITIAL_BALANCE
        self.id = self.ACCOUNT_ID

    action Deposit:
        require self.balance < 100

        self.balance = self.balance + 10

action Init:
    # Create multiple independent instances
    accounts = []

    for i in range(2):
        account = Account(INITIAL_BALANCE=i*10, ACCOUNT_ID=i)
        accounts.append(account)

    total_processed = 0

atomic action CheckTotal:
    require total_processed < 2

    total_processed = total_processed + 1

# Each account has independent state
# accounts[0].balance starts at 0
# accounts[1].balance starts at 10

atomic action NoOp:
    if total_processed >= 2:
        pass

Expected result (from fizz):

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 330, queued: 0
Skipping dotfile generation. Too many Nodes: 330
Valid Nodes: 330 Unique states: 330
IsLive: true
PASSED: Model checker completed successfully

Source on GitHub

Roles

Definition

Characteristics

Role Init Action

State Variables

Special Role Fields

Durable vs Ephemeral State

Role Communication

Examples

Simple Role

Role Init

Role Actions

Role Functions

Role State

Role Decorators

Role Instances

Patterns that use this