# Control Flow

> if/elif/else, for and while loops, break and continue, and checkpoints in FizzBee, including how loops behave under atomic, serial and parallel modifiers.

Canonical: https://fizzbee.io/reference/language/control-flow/
Source: https://github.com/fizzbee-io/fizzbee/blob/main/examples/references/LANGUAGE_REFERENCE.md#control-flow


## If-Elif-Else

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

## For Loops

Can be atomic, serial, or parallel:

```python
# 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 Loops

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

## Break and Continue

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

## Checkpoints

Checkpoints are visualization breakpoints for debugging and exploration:

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

**Default checkpoints** (automatically created):
- At the start of each action
- At non-deterministic choices (`any`, `oneof`)
- At yield points

**Use cases**:
- Step-through debugging in explorer
- Creating meaningful visualization points
- Breaking down complex actions into observable steps

**Note**: Checkpoints don't affect execution semantics, only visualization

**Reference**: [Checkpoints (Visualization Labels)](#example-checkpoints) for a complete example

## Examples

### If-Else Statement {#if-else}

Basic conditional branching

**Demonstrates:** if/else control flow

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/03-01-if-else)

### If-Elif-Else Statement {#example-if-elif-else}

Multiple conditional branches

**Demonstrates:** if/elif/else control flow

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**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](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/03-02-if-elif-else)

### Nested If Statements {#nested-if}

Nested conditional logic

**Demonstrates:** nested if/else structures

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/03-03-nested-if)

### For Loop (Atomic) {#for-loop-atomic}

Atomic for loop executes all iterations as one step

**Demonstrates:** atomic for loop, no yielding between iterations

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/04-01-for-loop-atomic)

### For Loop (Serial) {#for-loop-serial}

Serial for loop yields after each iteration

**Demonstrates:** serial for loop, interleaving between iterations

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/04-02-for-loop-serial)

### For Loop (Parallel) {#for-loop-parallel}

Parallel for loop executes iterations concurrently

**Demonstrates:** parallel for loop, all interleavings explored

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/04-03-for-loop-parallel)

### While Loop {#while-loop}

While loop continues until condition is false

**Demonstrates:** while loop with guard condition

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/04-04-while-loop)

### Break and Continue {#break-continue}

Loop control statements

**Demonstrates:** break and continue in loops

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/04-05-break-continue)

### Checkpoints (Visualization Labels) {#example-checkpoints}

Using backtick labels to create visualization breakpoints

**Demonstrates:** checkpoint syntax, visualization aids, debugging workflow

```fizz
# 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!
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/99-01-checkpoints)

