Control Flow

if condition1:
    # Branch 1
elif condition2:
    # Branch 2
else:
    # Default branch

# Atomic: all iterations together
atomic for i in range(10):
    counter = counter + 1

# Serial: yield between iterations
serial for item in items:
    process(item)

# Parallel: concurrent iterations
parallel for i in range(3):
    results[i] = compute(i)

while counter < 10:
    counter = counter + 1
    # Yields after each iteration (if serial context)

for i in range(10):
    if i == 5:
        break  # Exit loop
    if i % 2 == 0:
        continue  # Skip to next iteration
    process(i)

action Process:
    step1 = prepare()
    `checkpoint`  # Explicit breakpoint
    step2 = execute()
    `checkpoint`  # Another breakpoint
    step3 = finalize()

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

# Example 0010: If-Else Statement
# Basic conditional branching
# Demonstrates: if/else control flow

MAX = 5

action Init:
    counter = 0

atomic action Toggle:
    if counter >= MAX:
        return

    if counter % 2 == 0:
        counter = counter + 1
    else:
        counter = counter + 2

# Counter follows pattern: 0 -> 1 -> 3 -> 4 -> 6 (stops at 6 > MAX)

atomic action NoOp:
    if counter >= MAX:
        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 0011: If-Elif-Else Statement
# Multiple conditional branches
# Demonstrates: if/elif/else control flow

action Init:
    value = 0
    status = "init"

atomic action UpdateStatus:
    if status == "done":
        return

    value = value + 1

    if value < 3:
        status = "low"
    elif value < 6:
        status = "medium"
    elif value < 10:
        status = "high"
    else:
        status = "done"

# Status progresses: init -> low -> medium -> high -> done

atomic action NoOp:
    if status == "done":
        pass

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

 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

# Example 0012: Nested If Statements
# Nested conditional logic
# Demonstrates: nested if/else structures

MAX = 3

action Init:
    x = 0
    y = 0
    category = "none"

atomic action Categorize:
    if x >= MAX and y >= MAX:
        return

    if x < MAX:
        x = x + 1

    if y < MAX:
        y = y + 1

    # Nested conditionals for categorization
    if x > y:
        if x > 2:
            category = "high-x"
        else:
            category = "mid-x"
    else:
        if y > 2:
            category = "high-y"
        else:
            category = "mid-y"

# Categories change based on x and y values

atomic action NoOp:
    if x >= MAX and y >= MAX:
        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

# Example 0013: For Loop (Atomic)
# Atomic for loop executes all iterations as one step
# Demonstrates: atomic for loop, no yielding between iterations

action Init:
    items = []
    total = 0

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

    # Atomic for loop - all iterations execute together
    atomic for i in range(3):
        items.append(i)
        total = total + i

    # After this action: items = [0, 1, 2], total = 3

always assertion ValidState:
    # In atomic for, we never see partial lists
    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

# Example 0014: For Loop (Serial)
# Serial for loop yields after each iteration
# Demonstrates: serial for loop, interleaving between iterations

MAX = 2

action Init:
    items = []
    total = 0

action ProcessItems:
    require len(items) < MAX

    # Serial for loop - yields after each iteration
    serial for i in range(MAX):
        items.append(i)
        total = total + i

# NOTE: Unbounded state space - see 0002 for details

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

# Example 0015: For Loop (Parallel)
# Parallel for loop executes iterations concurrently
# Demonstrates: parallel for loop, all interleavings explored

action Init:
    results = {}
    counter = 0

action ProcessParallel:
    require counter < 2

    counter = counter + 1

    # Parallel for loop - iterations can interleave
    parallel for i in range(2):
        results[i] = i * 2

# Results can be populated in any order: {0:0, 1:2} or {1:2, 0:0} etc.

atomic action NoOp:
    if counter >= 2:
        pass

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

# Example 0016: While Loop
# While loop continues until condition is false
# Demonstrates: while loop with guard condition

MAX = 3

action Init:
    counter = 0
    accumulator = 0

atomic action Accumulate:
    require counter < MAX

    counter = counter + 1

    # While loop with bounded condition
    temp = 0
    atomic while temp < counter:
        accumulator = accumulator + 1
        temp = temp + 1

# After 3 calls: accumulator = 1 + 2 + 3 = 6

atomic action NoOp:
    if counter >= MAX:
        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
29
30
31
32

# Example 0017: Break and Continue
# Loop control statements
# Demonstrates: break and continue in loops

MAX = 3

action Init:
    evens = []
    stopped_at = -1

atomic action ProcessWithBreak:
    require len(evens) == 0

    for i in range(10):
        if i >= MAX:
            stopped_at = i
            break  # Exit loop early

        if i % 2 == 1:
            continue  # Skip odd numbers

        evens.append(i)

    # Result: evens = [0, 2], stopped_at = 3

always assertion ValidState:
    # Break ensures we stop at MAX
    return stopped_at == -1 or stopped_at == MAX

atomic action NoOp:
    if len(evens) > 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
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97

# Example 0088: Checkpoints (Visualization Labels)
# Using backtick labels to create visualization breakpoints
# Demonstrates: checkpoint syntax, visualization aids, debugging workflow

---
options:
    max_actions: 3
---

Status = enum('IDLE', 'PREPARING', 'READY', 'PROCESSING', 'DONE')

role Worker:
    action Init:
        self.status = Status.IDLE
        self.data = None

    action ProcessTask:
        require self.status == Status.IDLE

        # Checkpoint: Mark the start of preparation phase
        `start_preparation`
        self.status = Status.PREPARING
        self.data = "loading..."

        # Checkpoint: Preparation complete
        `preparation_complete`
        self.status = Status.READY
        self.data = "ready"

        # Checkpoint: Start processing
        `start_processing`
        self.status = Status.PROCESSING

        # Checkpoint: Processing complete
        `processing_complete`
        self.status = Status.DONE
        self.data = "result"

        # Checkpoint: Final cleanup
        `cleanup`
        self.status = Status.IDLE

role Coordinator:
    action Init:
        self.decision = None

    atomic action Decide:
        # Checkpoints work in atomic actions too
        # They don't create yield points, just visualization markers
        `evaluating`
        choice = oneof ["approve", "reject"]

        `decision_made`
        self.decision = choice

action Init:
    worker = Worker()
    coordinator = Coordinator()

# What are checkpoints?
# ======================
# Checkpoints are visualization labels marked with backticks: `label_name`
#
# Purpose:
# - Create meaningful breakpoints in the explorer/visualizer
# - Help understand multi-step processes
# - Debug complex actions by seeing intermediate states
# - Document important transitions in sequence diagrams
#
# Key properties:
# 1. Don't affect execution semantics
# 2. Don't create yield points (even in atomic blocks)
# 3. Only affect visualization/debugging
# 4. Can have any descriptive name
#
# Default checkpoints (created automatically):
# - Start of each action
# - At nondeterministic choices (any, oneof)
# - At yield points
#
# When to use explicit checkpoints:
# - Multi-step workflows (like ProcessTask above)
# - To highlight important state transitions
# - For sequence diagram clarity
# - When debugging complex actions
#
# Syntax:
# `checkpoint_name` - just a name in backticks
#
# Examples:
# `prepared`
# `sent_request`
# `waiting_for_response`
# `committed`
# `aborted`
#
# Note: Checkpoints are optional - use them when they add clarity!

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

gdoc_arrow_left_alt Data Structures Nondeterminism gdoc_arrow_right_alt