# Nondeterminism

> Nondeterministic choice in FizzBee: the any statement, oneof blocks, fairness on choices, and the concise vs block forms, with runnable examples.

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


## Any Statement

Nondeterministically chooses from a collection:

```python
# Choose one value
value = oneof [1, 2, 3, 4, 5]

# Choose with condition
value = oneof [x for x in options if x != previous]

# Choose from range
index = oneof range(10)
```

**Behavior**: Model checker explores all possible choices

**Important**: If no elements match the condition, the action is **disabled**:

```python
atomic action ProcessLargeValues:
    # If all values are <= 10, this action is disabled
    x = oneof [1, 2, 3, 4, 5] if x > 10
    # This line never executes
```

**Use case**: Conditional action enabling based on available choices

## Fairness with Oneof

```python
# Fair choice (eventually tries all)
fair action Choose:
    value = fair oneof options
```

## Concise vs Block Form

`oneof` has two forms. **Prefer the concise form** — it keeps code flat and readable:

```python
# ✅ Concise form (preferred): assigns and continues
n = oneof nodes
require status[n] == "active"
status[n] = "done"

# Block form: runs indented block for chosen value
oneof n in nodes:
    require status[n] == "active"
    status[n] = "done"
```

Both are semantically equivalent. The block form is the older pattern; the concise form avoids unnecessary indentation.

## Oneof: Two Meanings

`oneof` is used in two distinct but related ways:

```python
# 1. Choose a value from a collection (∃ — existential)
x = oneof [1, 2, 3]          # picks one value, assigns it

# 2. Choose a branch to execute (∨ — disjunction)
oneof:
    x = 1
    x = 2
    x = 3
```

Both mean "nondeterministically pick one". The syntax makes the semantics clear:
- `x = oneof collection` → pick an element (existential choice)
- `oneof:` block → pick a branch (disjunctive choice)

**Note**: `any` is a deprecated alias for the existential form (`x = oneof collection`).
It still works but emits a `DeprecationWarning`. Prefer `oneof`.

## Examples

### Any Statement {#example-any-statement}

Any statement for nondeterministic choice from a collection

**Demonstrates:** any statement, exploring all possibilities

```fizz
# Example 0018: Any Statement
# Any statement for nondeterministic choice from a collection
# Demonstrates: any statement, exploring all possibilities

action Init:
    options = [1, 2, 3]
    chosen = 0
    count = 0

atomic action ChooseOne:
    require count < 2

    count = count + 1

    # Any picks one element nondeterministically
    # Model checker explores all possibilities
    chosen = oneof options

# Creates branches for each option: chosen=1, chosen=2, chosen=3

atomic action NoOp:
    if count >= 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: 11, queued: 0
Valid Nodes: 11 Unique states: 7
IsLive: true
PASSED: Model checker completed successfully
```

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

### Any with Condition {#any-with-condition}

Nondeterministic choice with filtering

**Demonstrates:** any with if condition syntax

```fizz
# Example 0019: Any with Condition
# Nondeterministic choice with filtering
# Demonstrates: any with if condition syntax

action Init:
    options = [1, 2, 3]
    first = 0
    second = 0

atomic action ChoosePair:
    require first == 0 or second == 0

    # Choose two different values from options
    first = oneof options
    second = oneof options if second != first

# Safety: first and second must be different (unless both 0)
always assertion DifferentValues:
    return (first == 0 and second == 0) or (first != second)

atomic action NoOp:
    if first > 0 and second > 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: 11, queued: 0
Valid Nodes: 11 Unique states: 7
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/05-02-any-with-condition)

### Any with Fairness {#any-fairness}

Fair choice ensures all values eventually selected

**Demonstrates:** fair any with liveness assertion

```fizz
# Example 0020: Any with Fairness
# Fair choice ensures all values eventually selected
# Demonstrates: fair any with liveness assertion

action Init:
    values = [False, False, False]

atomic fair<strong> action SelectValue:
    # Fair any ensures all indices eventually chosen
    idx = fair oneof range(len(values))
    values[idx] = True

# Liveness: all values eventually become True
always eventually assertion AllValuesSelected:
    return all(values)
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 16, queued: 0
Valid Nodes: 16 Unique states: 8
Checking always eventually AllValuesSelected
IsLive: true
PASSED: Model checker completed successfully
```

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

### Combining Any with Fairness and Conditions {#advanced-any-patterns}

**Demonstrates:** combining any features together

```fizz
# Example 0055: Combining Any with Fairness and Conditions
# Demonstrates: combining any features together

action Init:
    options = [1, 2, 3]
    first = 0
    second = 0
    fair_choice = 0

# Combine any with condition
atomic action ChooseDifferentPair:
    require first == 0 or second == 0

    first = oneof options
    # Choose different value using condition
    second = oneof options if second != first

# Combine fair any with range
atomic fair<strong> action FairChoice:
    require fair_choice == 0

    # Ensures all values eventually chosen
    fair_choice = fair oneof options

# Can also combine fair any with filtering by using separate variables
atomic fair<strong> action FairFilteredChoice:
    require len(options) > 0

    # Fair choice from available options
    idx = fair oneof range(len(options))
    chosen = options[idx]

# Safety: first and second are different
always assertion DifferentValues:
    return (first == 0 and second == 0) or (first != second)

# Liveness: fair choices eventually selected
always eventually assertion FairChoiceMade:
    return fair_choice > 0

atomic action NoOp:
    if first > 0 and second > 0 and fair_choice > 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: 79, queued: 0
Valid Nodes: 79 Unique states: 28
Checking always eventually FairChoiceMade
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/12-03-advanced-any-patterns)