Functions

atomic func add(x, y):
    return x + y

serial func process_items():
    for item in items:
        # Process each item
        result = transform(item)

# ✅ Calling from atomic action
atomic action FromAtomic:
    result = some_function()

# ✅ Calling from serial action (default flow)
action FromSerial:
    result = some_function()  # function body yields between statements

# ✅ Calling from a parallel block — each call is one parallel statement;
# the function bodies interleave with the other parallel statements
action FromParallel:
    parallel:
        some_function()
        other_function()

# ✅ Calling from a oneof block
action FromOneof:
    oneof:
        some_function()
        other_function()

# ✅ Calling from role actions
role MyRole:
    action DoWork:
        result = some_function()

[variable =] [role.]function([parameters])

# ❌ WRONG: Function call in conditional
if replica.get_state() == State.ACTIVE:
    process()

# ✅ CORRECT: Extract to variable first
state = replica.get_state()
if state == State.ACTIVE:
    process()

# ❌ WRONG: Function call in arithmetic
result = compute() + 10

# ✅ CORRECT: Extract first
value = compute()
result = value + 10

always assertion AllDone:
    return all([c.done() for c in consumers]) or total_received() < MAX

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

# Example 0021: Simple Function
# Basic function definition and calls
# Demonstrates: func keyword, function calls

action Init:
    result = 0
    counter = 0

func add_one(x):
    return x + 1

atomic action Calculate:
    require counter < 3

    counter = counter + 1
    # Call function and use return value
    result = add_one(result)

# Result progresses: 0 -> 1 -> 2 -> 3

atomic action NoOp:
    if counter >= 3:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 4, queued: 0
Valid Nodes: 4 Unique states: 4
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

# Example 0022: Function with Parameters
# Functions with multiple parameters
# Demonstrates: multiple parameters, parameter order

action Init:
    x = 0
    y = 0

func add(a, b):
    return a + b

func multiply(a, b):
    return a * b

atomic action Compute:
    require x < 2

    x = x + 1
    # Functions with multiple parameters
    y = add(x, 2)
    y = multiply(y, 2)

# After first call: x=1, y=add(1,2)*2=6
# After second call: x=2, y=add(2,2)*2=8

atomic action NoOp:
    if x >= 2:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
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

# Example 0023: Function Return Values
# Functions with conditional returns
# Demonstrates: early return, conditional logic in functions

action Init:
    value = 0
    is_valid = False

func validate(x):
    if x < 0:
        return False
    if x > 10:
        return False
    return True

atomic action CheckValue:
    if value >= 12:
        return

    value = value + 3
    is_valid = validate(value)

# value: 0->3->6->9->12
# is_valid: True, True, True, False

atomic action NoOp:
    if value >= 12:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 21, queued: 0
Valid Nodes: 21 Unique states: 17
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

# Example 0024: Atomic Function
# Atomic functions execute without yielding
# Demonstrates: atomic func modifier

action Init:
    items = []
    total = 0

atomic func process_batch():
    # Atomic function - all statements execute together
    for i in range(3):
        items.append(i)
        total = total + i
    return total

atomic action ProcessData:
    require len(items) == 0

    # Call atomic function
    result = process_batch()

# After ProcessData: items=[0,1,2], total=3, result=3

always assertion ValidState:
    # Atomic function ensures we never see partial state
    return len(items) == 0 or len(items) == 3

atomic action NoOp:
    if len(items) > 0:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 2, queued: 0
Valid Nodes: 2 Unique states: 2
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

# Example 0025: Function with Serial For Loop
# Functions can contain serial blocks/loops that yield
# Demonstrates: atomic function with serial for loop inside
# NOTE: Functions can be called from any flow context (atomic, serial,
#       parallel, oneof), at the top level or within roles

MAX = 2

action Init:
    items = []
    total = 0

# Atomic function with serial for loop inside
# Function itself is atomic, but for loop yields between iterations
atomic func process_items():
    serial for i in range(MAX):
        items.append(i)
        total = total + i
    return total

atomic action ProcessData:
    require len(items) < MAX

    # Call function from atomic action
    result = process_items()

# Function is atomic overall, but serial for yields internally
# Creates intermediate states during loop execution

atomic action NoOp:
    if len(items) >= MAX:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 40, queued: 0
Valid Nodes: 40 Unique states: 39
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

# Example 0090: Function Called from a Serial Action
# A top-level function called from a serial action yields between statements and interleaves with other actions
# Demonstrates: functions, serial actions, yield points, interleaving

# Top-level (non-role) functions can be called from serial actions.
# The function body yields between statements like any serial code,
# so other actions (and crashes) interleave with it.

MAX = 2

action Init:
    counter = 0
    last = 0

func Incr(amount):
    counter = counter + amount
    return counter

atomic action Reset:
    counter = 0
    last = 0

serial action Add:
    require counter < MAX
    last = Incr(1)

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 15, queued: 0
Valid Nodes: 15 Unique states: 12
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

# Example 0091: Functions Called from a Parallel Block
# Function calls as parallel statements interleave with the other branches of the parallel block
# Demonstrates: functions, parallel block, interleaving

# Function calls are supported inside parallel blocks. Each call is one
# parallel statement; the function body executes with its own flow
# (serial by default) and interleaves with the other parallel statements.
# The reachable states are identical to writing the function bodies inline.
# MOD keeps the counters bounded without require (a `require` directly
# inside a parallel block is a separate known issue).

MOD = 3

action Init:
    a = 0
    b = 0

action NoOp:
    pass

func IncrTwiceA():
    a = (a + 1) % MOD
    a = (a + 1) % MOD

func IncrB():
    b = (b + 1) % MOD

parallel action Both:
    IncrTwiceA()
    IncrB()

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 252, queued: 0
Skipping dotfile generation. Too many Nodes: 252
Valid Nodes: 252 Unique states: 207
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

# Example 0092: Role Functions Called from a Parallel Block
# Role methods called as parallel statements inside a parallel action
# Demonstrates: roles, role functions, parallel block

# Role methods can be called from parallel blocks too. (Before the
# executeEndOfBlock fork-propagation fix this crashed the model checker
# even though role calls passed the old call-site guard.)

MOD = 3

role Node:
    action Init:
        self.a = 0
        self.b = 0

    func IncrA():
        self.a = (self.a + 1) % MOD

    func IncrB():
        self.b = (self.b + 1) % MOD

    parallel action Both:
        self.IncrA()
        self.IncrB()

action Init:
    n = Node()

action NoOp:
    pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 108, queued: 0
Valid Nodes: 108 Unique states: 81
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

# Example 0093: Function Calls in Nested Blocks Inside a Parallel Block
# Function calls wrapped in atomic or serial blocks within a parallel block
# Demonstrates: functions, nested blocks, atomic, serial, parallel block

# A function call nested inside an atomic: or serial: block within a
# parallel block works: when the call returns, the block ends advance
# through the parallel scope and fork the remaining parallel statements
# (the executeEndOfBlock scope-climbing path).
# MOD keeps the counters bounded without require (a `require` directly
# inside a parallel block is a separate known issue).

MOD = 3

action Init:
    a = 0
    b = 0

action NoOp:
    pass

func IncrA():
    a = (a + 1) % MOD

func IncrB():
    b = (b + 1) % MOD

parallel action Both:
    atomic:
        IncrA()
    serial:
        IncrB()

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 108, queued: 0
Valid Nodes: 108 Unique states: 81
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

# Example 0094: Function Calls Inside Nested Parallel Blocks
# A parallel block nested within a parallel block, with function calls at both levels
# Demonstrates: functions, nested parallel blocks

# A parallel block nested within a parallel block, with function calls
# at both levels. A function return inside the inner block must fork the
# inner block's remaining statements; the inner block's end must advance
# through the outer parallel scope (recursive executeEndOfBlock climbing).
# MOD keeps the counters bounded without require (a `require` directly
# inside a parallel block is a separate known issue).

MOD = 2

action Init:
    a = 0
    b = 0
    c = 0

action NoOp:
    pass

func IncrA():
    a = (a + 1) % MOD

func IncrB():
    b = (b + 1) % MOD

func IncrC():
    c = (c + 1) % MOD

parallel action Trio:
    IncrA()
    parallel:
        IncrB()
        IncrC()

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 560, queued: 0
Skipping dotfile generation. Too many Nodes: 560
Valid Nodes: 560 Unique states: 392
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

---
deadlock_detection: false
---

# Example: Name Resolution
# Which binding a name refers to when locals, function parameters, role
# fields, state and comprehension variables share a name.
# Demonstrates: shadowing, comprehensions, lambdas, nested blocks, role
# methods reading globals. Every check runs inside the actions, so a wrong
# lookup fails an assertion.

LIMIT = 2

role Counter:
    action Init:
        self.n = 0

    func bump(n):
        # The parameter n shadows the field self.n.
        self.n = self.n + n
        return n

    atomic action Step:
        require self.n < LIMIT
        got = self.bump(1)
        ok = ok and got == 1


action Init:
    count = 0
    x = 10
    ok = True
    counter = Counter()


func shadow(x):
    # The parameter x shadows the state variable x.
    return x * 2


atomic action Shadowing:
    require count < 2
    count = count + 1
    # Inside shadow, x is the parameter, not the state variable.
    doubled = shadow(3)
    ok = ok and doubled == 6 and x == 10
    # A comprehension variable named like a state variable does not leak.
    squares = [x * x for x in range(3)]
    ok = ok and squares == [0, 1, 4] and x == 10
    # A lambda parameter shadows too.
    add = lambda x, y: x + y
    ok = ok and add(1, 2) == 3 and x == 10


atomic action NestedBlocks:
    require count < 2
    total = 0
    for i in range(2):
        for j in range(2):
            if i == j:
                total = total + 1
    # A local set in a nested block is visible after it.
    ok = ok and total == 2
    count = count + 1


always assertion AllLookupsCorrect:
    return ok

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

gdoc_arrow_left_alt Actions Roles gdoc_arrow_right_alt