# Actions

> FizzBee actions: how the model checker invokes them, the Init action, enabling conditions with require, and the pass statement, with runnable examples.

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


## Definition

Actions are the entry points for the model checker. They are automatically invoked by the model checker to explore the state space.

```python
action Init:
    # Initialize state variables
    counter = 0
    items = []

atomic action Increment:
    if counter >= 10:
        return
    counter = counter + 1
```

## Action Syntax

Actions can have optional modifiers that control execution flow and fairness:

```
[flow_modifier] [fairness_modifier] action ActionName:
```

**Modifier Order** (both optional):
1. **Flow modifier**: `atomic` or `serial` (default: `serial`)
2. **Fairness modifier**: `fair`, `fair<weak>`, or `fair<strong>` (default: unfair)
3. **`action` keyword**
4. **Action name**

**Examples**:

```python
# No modifiers - serial, unfair
action Process:
    counter = counter + 1

# Flow only - atomic, unfair
atomic action AtomicUpdate:
    x = x + 1
    y = y + 1

# Fairness only - serial, weakly fair
fair action Progress:
    done = True

# Both modifiers - atomic, weakly fair
atomic fair action ProduceMessage:
    require len(queue) < MAX_SIZE
    queue.append(message)

# Both modifiers - atomic, strongly fair
atomic fair<strong> action SelectValue:
    value = fair<strong> oneof options
```

**Common mistake**: Using `fair atomic action` instead of `atomic fair action` (syntax error)

## Characteristics

1. **No parameters**: Actions cannot take parameters (no parentheses)
2. **Automatic invocation**: Model checker calls actions automatically
3. **Special Init action**: Called once at the start
4. **Default flow**: Serial (yields between statements)
5. **State scope**: Variables in `Init` become global state

## Init Action

The `Init` action is special:
- Called exactly once at the beginning
- Initializes global state variables
- All variables defined in `Init` scope are part of the state
- Must be named exactly `Init`

```python
action Init:
    # These become state variables
    x = 0
    items = []
    config = {"key": "value"}
```

## Enabling Conditions

Actions can be conditionally enabled:

```python
action DoSomething:
    # Option 1: if-return pattern
    if not condition:
        return
    # Action body

action DoSomethingElse:
    # Option 2: require statement
    require condition
    # Action body
```

**Difference**:
- `if-return`: Action executes but does nothing
- `require`: Action is disabled (not executed at all)

## Action Enabling Semantics

**How actions become enabled**:

1. **Start disabled**: Every action starts with `enabled=False`
2. **Enabled by execution**: Action becomes enabled when it executes a simple Python statement (assignment, method call)
3. **Control flow doesn't enable**: `if`, `for`, `while`, `require` alone don't enable
4. **Disabled by require**: `require False` disables and exits immediately

**Examples**:

```python
action Example1:
    if condition:
        x = 1  # This enables the action
    # Action is enabled if condition is True

action Example2:
    require condition  # Disables if False
    # Action never becomes enabled if condition is False

action Example3:
    for i in range(10):
        pass  # for loop doesn't enable, but pass does
    # Action is enabled

action Example4:
    if False:
        x = 1  # Never executed
    # Action stays disabled (no statement executed)
```

**Simple Python statements** that enable actions:
- Assignments: `x = 1`, `list.append(2)`
- Function calls with assignment: `result = func()`
- `pass` statement

**Statements that DON'T enable**:
- Control flow: `if`, `elif`, `else`, `for`, `while`
- Flow control: `break`, `continue`, `return`
- Guards: `require`
- Non-determinism: `oneof` / `any` (but the assignment `x = oneof ...` does enable)

**Critical pitfall**:

```python
# ⚠️ This action is ALWAYS enabled (even when condition is False)
action Pitfall:
    is_ready = (condition == True)  # Assignment enables!
    if is_ready:
        process()

# ✅ Correct version - only enabled when condition is True
action Fixed:
    require condition
    process()
```

**Advanced pattern**: `require` in the middle of an action (after a yield point) can coordinate with other actions. See "Action Coordination with Require and Yield" in Quick Reference.

## Pass Statement

Use `pass` to explicitly enable an action without changing state:

```python
atomic action NoOp:
    pass  # Unconditionally enabled, does nothing
```

## Examples

### No-op Action {#noop}

The simplest FizzBee spec with a single action that does nothing meaningful

**Demonstrates:** basic action syntax and minimal state initialization

```fizz
# Example 0001: No-op Action
# The simplest FizzBee spec with a single action that does nothing meaningful
# Demonstrates: basic action syntax and minimal state initialization

action Init:
    counter = 0

atomic action NoOp:
    # pass statement unconditionally enables the action
    # without it, the action would be disabled (no state change)
    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: 1, queued: 0
Valid Nodes: 1 Unique states: 1
IsLive: true
PASSED: Model checker completed successfully
```

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

### Atomic Action {#atomic-action}

A single atomic action that modifies state

**Demonstrates:** atomic modifier and simple state transitions

```fizz
# Example 0002: Atomic Action
# A single atomic action that modifies state
# Demonstrates: atomic modifier and simple state transitions
#
# WARNING: This creates an INFINITE state space (counter can grow unbounded)
# FizzBee caps exploration at max_actions=100 by default (see output: 101 states)
# In real models, unbounded counters cause state explosion - always use:
# - Bounded ranges (e.g., counter < MAX)
# - Modulo arithmetic (e.g., counter = (counter + 1) % 10)
# - Guard clauses to limit growth

action Init:
    counter = 0

atomic action Increment:
    # This entire block executes as one indivisible step
    counter = counter + 1
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

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

### Multiple Actions {#multiple-actions}

Multiple independent actions operating on the same state

**Demonstrates:** how multiple actions create state transitions

```fizz
# Example 0003: Multiple Actions
# Multiple independent actions operating on the same state
# Demonstrates: how multiple actions create state transitions
# NOTE: Unbounded state space - see 0002 for details on state explosion

action Init:
    counter = 0

atomic action Increment:
    counter = counter + 1

atomic action Decrement:
    counter = counter - 1
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

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

### Init Action Details {#example-init-action}

Demonstrates how Init action initializes state variables All variables defined in Init become part of the state space NOTE: Unbounded state space - see 0002 for details on state explosion

```fizz
# Example 0004: Init Action Details
# Demonstrates how Init action initializes state variables
# All variables defined in Init become part of the state space
# NOTE: Unbounded state space - see 0002 for details on state explosion

action Init:
    # These variables become state variables
    counter = 0
    status = "ready"
    items = []

atomic action AddItem:
    items.append(counter)
    counter = counter + 1
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

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

### Constants and Init {#init-with-constants}

Global constants defined at top level, used in Init

**Demonstrates:** global statements and constant access

```fizz
# Example 0005: Constants and Init
# Global constants defined at top level, used in Init
# Demonstrates: global statements and constant access
#
# NOTE: This spec causes a DEADLOCK when counter reaches limit (3)
# The action is disabled because the if condition is false and no statement executes
# To fix: make the action idempotent by removing the guard, or add a reset action

# Global constants (defined at top level)
MAX_VALUE = 3
MIN_VALUE = 0

action Init:
    # Initialize state using constants
    counter = MIN_VALUE
    limit = MAX_VALUE

atomic action Increment:
    # Guard clause: only increment if below limit
    require counter < limit
    counter = counter + 1

# Uncomment to fix deadlock - allows counter to wrap around
# atomic action Reset:
#     require counter >= limit
#     counter = MIN_VALUE
```
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
DEADLOCK detected
FAILED: Model checker failed
------
Init
--
state: {"counter":0,"limit":3}
------
Increment
--
state: {"counter":1,"limit":3}
------
Increment
--
state: {"counter":2,"limit":3}
------
Increment
--
state: {"counter":3,"limit":3}
------
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/01-05-init-with-constants)

### Require Statement {#require-statement}

Using require for guard clauses

**Demonstrates:** require statement, explicit enabling conditions

```fizz
# Example 0026: Require Statement
# Using require for guard clauses
# Demonstrates: require statement, explicit enabling conditions

action Init:
    state = "OFF"

atomic action TurnOn:
    # Require acts as guard - action disabled if false
    require state == "OFF"
    state = "ON"

atomic action TurnOff:
    require state == "ON"
    state = "OFF"

# Require immediately disables action if condition is false
# More explicit than using if with return
```
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/07-01-require-statement)

### Pass for Deadlock Prevention {#example-pass-statement}

Using pass to prevent deadlocks at terminal states

**Demonstrates:** pass statement prevents stuttering deadlock

```fizz
# Example 0027: Pass for Deadlock Prevention
# Using pass to prevent deadlocks at terminal states
# Demonstrates: pass statement prevents stuttering deadlock

action Init:
    counter = 0

atomic action Increment:
    if counter >= 5:
        return
    counter = counter + 1

# Without this action, model checker would report deadlock at counter=5
# because no action can execute (Increment is disabled)
atomic action Stabilize:
    if counter >= 5:
        pass  # Enables action without changing state

# Pass allows the action to be enabled even though no state changes
# This prevents "stuttering deadlock" where all actions are disabled
# Common pattern: add pass action for terminal/stable states
```
Run it in the FizzBee playground: https://fizzbee.io/play


**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](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/07-02-pass-statement)

### Guard Clauses - if-return vs require {#guard-clauses}

Comparing implicit and explicit guard patterns

**Demonstrates:** if-return vs require for enabling conditions

```fizz
# Example 0028: Guard Clauses - if-return vs require
# Comparing implicit and explicit guard patterns
# Demonstrates: if-return vs require for enabling conditions

action Init:
    value = 0
    mode = "increment"

# Pattern 1: Implicit guard with if-return
atomic action IncrementWithIf:
    if value >= 3:
        return

    # Action enabled only if value < 3
    value = value + 1

# Pattern 2: Explicit guard with require
atomic action IncrementWithRequire:
    # Require makes the guard explicit at the start
    require value < 3
    value = value + 1

# Both patterns achieve the same result:
# - if-return: guard is implicit in control flow
# - require: guard is explicit and declarative
#
# Use require for: simple enabling conditions
# Use if-return for: complex conditional logic with multiple paths

atomic action NoOp:
    if value >= 3:
        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/07-03-guard-clauses)

### Require with Parallel Blocks {#require-with-parallel}

Where require can and cannot appear around a parallel block, and the clean model error for the unsupported form

**Demonstrates:** require, parallel block, guards, model error

> Uses a `fizz.yaml` config file (shown below); run locally with `fizz`.

```python
# Example 0095: Require with Parallel Blocks
# Where require can and cannot appear around a parallel block, and the clean model error for the unsupported form
# Demonstrates: require, parallel block, guards, model error

# require cannot be a DIRECT statement of a parallel block (the model
# checker reports a clean error): parallel statements are unordered, so
# there is no defined point at which the condition would be checked.
# The two supported patterns, both exercised here:
#   1. require above the parallel block - guards the whole action
#   2. require wrapped with its dependent statements in an atomic/serial
#      branch - guards just that branch

action Init:
    a = 0
    b = 0
    ready = False

atomic action MakeReady:
    ready = True

action NoOp:
    pass

# Pattern 1: guard the whole action
action GuardedAction:
    require ready and a < 2
    parallel:
        a = a + 1
        b = (b + 1) % 3

# Pattern 2: guard one branch
parallel action BranchGuard:
    atomic:
        require b > 0
        a = (a + 1) % 3
    serial:
        b = (b + 1) % 3
```

`fizz.yaml`:

```yaml
# The branch guard (require b > 0) has await semantics after a yield:
# when b cycles back to 0, in-flight threads hold until it becomes true
# again, and two held threads fill max_concurrent_actions - a genuine
# await-starvation deadlock, orthogonal to the require-placement patterns
# this example demonstrates.
deadlock_detection: false
```

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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/07-04-require-with-parallel)