Actions

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

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

[flow_modifier] [fairness_modifier] action ActionName:

# 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

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

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

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

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)

# ⚠️ 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()

atomic action NoOp:
    pass  # Unconditionally enabled, does nothing

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

# 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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

# 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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

# 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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

# 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

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

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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

# 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

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

# 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

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

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

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

# Example: require with Parallel Blocks
# 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

# 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

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

gdoc_arrow_left_alt Keywords and Reserved Words Functions gdoc_arrow_right_alt