State Management

Global State Variables

Variables defined in top-level Init action are automatically global:

action Init:
    # These are global state variables
    counter = 0
    items = []
    config = {}

atomic action Increment:
    # Access global state directly
    counter = counter + 1

No global keyword needed - state variables are automatically accessible everywhere.

Top-Level Constants

Variables defined at the top level (outside actions) are read-only constants:

# Constants (read-only)
MAX_VALUE = 100
TIMEOUT = 30

action Init:
    # State variables (read-write)
    counter = 0

Local Variables

Variables in functions/actions (not in Init) are local:

atomic func process():
    temp = 100  # Local variable (not in state)
    return temp * 2

Role State

Only self.* variables in roles are part of state:

role Example:
    action Init:
        self.state_var = 0  # Part of state
        local_var = 100     # NOT in state

Examples

Global Variables

State variables and top-level constants

Demonstrates: automatic global state, top-level constants

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 0058: Global Variables
# State variables and top-level constants
# Demonstrates: automatic global state, top-level constants

# Top-level constants (read-only, available everywhere)
MAX_ITEMS = 5
MIN_VALUE = 0

action Init:
    # State variables (automatically global, accessible everywhere)
    counter = MIN_VALUE
    items = []
    config_value = MAX_ITEMS

atomic func CheckLimit():
    # State variables accessible in functions automatically
    return len(items) < MAX_ITEMS

atomic action AddItem:
    require len(items) < MAX_ITEMS

    # State variables accessible in actions automatically
    items.append(counter)
    counter = counter + 1

# Top-level constants accessible everywhere
atomic func GetMaxItems():
    return MAX_ITEMS

# State variables accessible in all functions/actions
atomic func GetItemCount():
    return len(items)

atomic action NoOp:
    if counter >= MAX_ITEMS:
        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