Nondeterminism

Any Statement

Nondeterministically chooses from a collection:

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

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

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

# ✅ 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:

# 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

Any statement for nondeterministic choice from a collection

Demonstrates: any statement, exploring all possibilities

Run in playground

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


# 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

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

Any with Condition

Nondeterministic choice with filtering

Demonstrates: any with if condition syntax

Run in playground

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


# 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

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

Any with Fairness

Fair choice ensures all values eventually selected

Demonstrates: fair any with liveness assertion

Run in playground

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


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

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

Combining Any with Fairness and Conditions

Demonstrates: combining any features together

Run in playground

 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


# 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

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