Symmetry Reduction

 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
44
45
46
47
48
49
50
51
52
53
54
55
56
57

# Example 0084: Symmetric Values for IDs
# Using symmetric_values() to reduce state space by treating permutations as equivalent
# Demonstrates: symmetric_values(), state space optimization, interchangeable IDs
#
# NOTE: Prefer the symmetry module API for new models. This is equivalent to:
#   KEYS = symmetry.nominal(name="k", limit=3, materialize=True).values()
# The symmetry module offers more types (ordinal, interval, rotational)
# and features (reflection, divergence, segments). See 16-05 through 16-12.

# Define symmetric values instead of regular numbers or strings
# symmetric_values('prefix', count) creates prefix0, prefix1, prefix2, ...
KEYS = symmetric_values('k', 3)  # Creates k0, k1, k2

action Init:
    # Use symmetric keys in a dictionary
    switches = {}
    for k in KEYS:
        switches[k] = 'OFF'

atomic action TurnOn:
    # Model checker explores all possible choices
    # With symmetric values: states where k0=ON,k1=OFF,k2=OFF
    # are equivalent to k1=ON,k0=OFF,k2=OFF
    key = oneof KEYS
    if switches[key] == 'OFF':
        switches[key] = 'ON'

atomic action TurnOff:
    key = oneof KEYS
    if switches[key] == 'ON':
        switches[key] = 'OFF'

# Verify at least one switch can be on
exists assertion SomeOn:
    return any([switches[k] == 'ON' for k in KEYS])

# Why use symmetric_values?
# ============================
# Without symmetry: KEYS = range(3) or KEYS = ['k0', 'k1', 'k2']
#   - State (k0=ON, k1=OFF, k2=OFF) is different from (k1=ON, k0=OFF, k2=OFF)
#   - Model checker explores all permutations
#   - State space: MUCH LARGER
#
# With symmetry: KEYS = symmetric_values('k', 3)
#   - These states are recognized as equivalent (just permutations)
#   - Model checker only explores one representative state
#   - State space: SIGNIFICANTLY REDUCED
#
# When to use:
# - Process IDs, Node IDs, Client IDs that are truly interchangeable
# - Keys/IDs where order and identity don't matter
# - All instances start in identical states
#
# When NOT to use:
# - IDs have different initial states
# - Identity matters (e.g., "master" vs "replica")
# - Order is semantically meaningful

 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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

# Example 0085: Symmetric Roles
# Using 'symmetric role' keyword for indistinguishable role instances
# Demonstrates: symmetric role, automatic symmetry reduction, __id__ field

---
deadlock_detection: false
liveness: "false"
---

Status = enum('INIT', 'WORKING', 'DONE')

NUM_WORKERS = 3

# Mark role as symmetric - tells model checker instances are interchangeable
symmetric role Worker:
    action Init:
        self.status = Status.INIT
        self.result = None

    atomic action StartWork:
        require self.status == Status.INIT
        self.status = Status.WORKING

    atomic action FinishWork:
        require self.status == Status.WORKING
        self.status = Status.DONE
        self.result = 'OK'
        # Add this worker's ID to the done set
        completed.add(self.__id__)

action Init:
    # CRITICAL: Use bag() or set(), NOT list()
    # Lists are order-dependent and break symmetry reduction
    workers = bag()
    for i in range(NUM_WORKERS):
        workers.add(Worker())

    completed = set()

# Safety: all workers eventually complete
eventually always assertion AllWorkersComplete:
    for w in workers:
        if w.status != Status.DONE:
            return False
    return True

# Why use symmetric role?
# ============================
# Without 'symmetric' keyword:
#   - State (w0=DONE, w1=INIT, w2=INIT) is different from (w1=DONE, w0=INIT, w2=INIT)
#   - Model checker explores all permutations
#   - For N workers, explores N! times more states
#
# With 'symmetric' keyword:
#   - Model checker recognizes these as equivalent
#   - Only explores one representative permutation
#   - State space: N! times smaller
#
# Example with 3 workers:
#   - Without symmetry: explores 3! = 6x more states
#   - With symmetry: only explores canonical representative
#
# When to use symmetric role:
# - All instances start in identical states
# - Instances are truly indistinguishable
# - Identity doesn't matter for correctness
#
# When NOT to use:
# - Instances have different initial states
# - Some instances have special roles (leader, coordinator)
# - Instance identity is semantically meaningful
#
# IMPORTANT: Must use bag() or set() for workers collection
# Using list() defeats symmetry because lists are order-dependent!

 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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

# Example 0086: Common Pitfall - Using List with Symmetric Roles
# Demonstrates why you MUST use bag() or set() with symmetric roles, not list()
# Shows: symmetry broken by order-dependent collections

---
# Limit to show the pitfall quickly
options:
    max_actions: 10
---

Status = enum('READY', 'DONE')

NUM_NODES = 2

# This role is marked as symmetric
symmetric role Node:
    action Init:
        self.status = Status.READY

    atomic action Process:
        require self.status == Status.READY
        self.status = Status.DONE

# WRONG APPROACH: Using list() defeats symmetry reduction
action Init:
    # Lists are ORDER-DEPENDENT
    # State [Node(id=0), Node(id=1)] is different from [Node(id=1), Node(id=0)]
    # Even though the role is symmetric, the list ordering creates distinct states
    # Result: NO state space reduction, symmetry is broken
    nodes = []
    for i in range(NUM_NODES):
        nodes.append(Node())

# CORRECT APPROACH: Using bag() preserves symmetry
# To see the correct version, comment out the Init above and uncomment below:
# action Init:
#     # Bags are ORDER-INDEPENDENT (multiset)
#     # Bag{Node(id=0), Node(id=1)} is same as Bag{Node(id=1), Node(id=0)}
#     # Model checker can exploit symmetry
#     # Result: State space reduction works correctly
#     nodes = bag()
#     for i in range(NUM_NODES):
#         nodes.add(Node())

# The Pitfall Explained:
# ======================
# Common mistake when migrating to symmetric roles:
#
# 1. Start with: participants = []  (list of participants)
# 2. Add: symmetric role Participant
# 3. Expect: automatic state space reduction
# 4. Reality: NO reduction because list preserves order!
#
# Fix: Change to participants = bag() or participants = set()
#
# Why this matters:
# - With 2 symmetric nodes and list: explores both orderings
# - With 2 symmetric nodes and bag: explores only one canonical state
# - With N nodes: difference is N! (factorial) states
#
# When to use each collection with symmetric roles:
# - bag(): When duplicates are possible/meaningful
# - set(): When duplicates are impossible/don't matter
# - list(): NEVER with symmetric roles (breaks symmetry)
# - dict: OK if keys are symmetric_values() or other symmetric types

always assertion BothNodesReady:
    # This will fail once a node processes
    # Demonstrates that the model is running
    for n in nodes:
        if n.status != Status.READY:
            return False
    return True

 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
44
45
46
47
48
49
50
51
52
53
54
55

# Example 0087b: State Space WITH Symmetry Reduction
# Run this to see reduced state space
# Compare state count with WithoutSymmetry.fizz

---
options:
    max_actions: 6
---

Status = enum('IDLE', 'BUSY')

NUM_PROCESSES = 2

# Symmetric role - instances are interchangeable
symmetric role Process:
    action Init:
        self.status = Status.IDLE
        self.counter = 0

    atomic action Work:
        require self.status == Status.IDLE
        self.status = Status.BUSY
        self.counter = self.counter + 1

    atomic action Rest:
        require self.status == Status.BUSY
        self.status = Status.IDLE

action Init:
    # CRITICAL: Use bag() not list() for symmetry to work
    processes = bag()
    for i in range(NUM_PROCESSES):
        processes.add(Process())

# Example state space exploration (approximate):
# With 2 processes marked symmetric in a bag:
#
# States like:
#   Bag{p0:(IDLE,0), p1:(BUSY,1)} and Bag{p0:(BUSY,1), p1:(IDLE,0)}
# are SAME state (explores only one)
#
# Expected: ~20-30 unique states (50% reduction from WithoutSymmetry.fizz)
#
# State space reduction:
# - 2 processes: ~50% reduction
# - 3 processes: ~6x reduction (3! = 6)
# - 4 processes: ~24x reduction (4! = 24)
# - N processes: N! reduction factor
#
# How to verify:
# 1. Run: fizz WithoutSymmetry.fizz
#    Note: X states, Y nodes
# 2. Run: fizz WithSymmetry.fizz
#    Note: Much smaller state count
# 3. Compare the state graphs in explorer

 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

# Example 0087a: State Space WITHOUT Symmetry Reduction
# Run this to see baseline state space
# Then compare with WithSymmetry.fizz to see the reduction

---
options:
    max_actions: 6
---

Status = enum('IDLE', 'BUSY')

NUM_PROCESSES = 2

# Regular role (NOT symmetric)
role Process:
    action Init:
        self.status = Status.IDLE
        self.counter = 0

    atomic action Work:
        require self.status == Status.IDLE
        self.status = Status.BUSY
        self.counter = self.counter + 1

    atomic action Rest:
        require self.status == Status.BUSY
        self.status = Status.IDLE

action Init:
    processes = []
    for i in range(NUM_PROCESSES):
        processes.append(Process())

# Example state space exploration (approximate):
# With 2 processes, each can be (IDLE,c=0), (BUSY,c=1), (IDLE,c=1), etc.
#
# States like:
#   [p0:(IDLE,0), p1:(BUSY,1)] and [p0:(BUSY,1), p1:(IDLE,0)]
# are DIFFERENT states (explores both)
#
# Expected: ~40-60 unique states (varies by max_actions)

 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

# Nominal Symmetry: Unordered, interchangeable identifiers.
# Operations: == and != only. No ordering, no arithmetic.
# Reduction: permutations of active set are equivalent.
# Use cases: user IDs, session tokens, cache keys.
#
# Key methods:
#   fresh()   - allocate a new unique value (deterministic, canonical)
#   values()  - list all active values
#   choices() - values() + one fresh (if limit allows)
#   choose()  - deterministic default value (like TLA+ CHOOSE); for initial values

IDS = symmetry.nominal(name="id", limit=3)

action Init:
    cache = {}

atomic action Put:
    # choices() returns existing IDs + one fresh ID (if under limit).
    # Use with `any` for nondeterministic selection.
    id = oneof IDS.choices()
    cache[id] = "data"

atomic action Evict:
    # `oneof` on an empty list disables the transition, so no guard needed.
    id = oneof IDS.values()
    if id in cache:
        cache.pop(id)

always assertion BoundedSize:
    return len(cache) <= 3

 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

# Ordinal Symmetry: Ordered values where only relative rank matters.
# Operations: ==, !=, <, <=, >, >=. No arithmetic.
# Reduction: values are squeezed to dense ranks (0,1,2,...).
# Use cases: logical timestamps, priority levels, version numbers.
#
# Key methods:
#   fresh()  - allocate value greater than all existing (appends to end)
#   min()    - smallest active value (or fresh if empty)
#   max()    - largest active value (or fresh if empty)
#   values() - all active values, sorted ascending
#
# The model checker treats states with the same relative ordering
# as equivalent. E.g., timestamps {10,20,30} and {1,5,99} are
# equivalent because both have the same rank order.

TIMES = symmetry.ordinal(name="ts", limit=4)

action Init:
    events = []

atomic action RecordEvent:
    # fresh() appends after max; min()/max() return the extremes.
    t = TIMES.fresh()
    events = events + [t]

atomic action ProcessEvent:
    # Consuming the oldest event frees a slot, allowing fresh()
    # to allocate again -- enabling infinite traces without deadlock.
    require len(events) > 0
    events = events[1:]

always assertion EventsOrdered:
    # fresh() always appends, so events are in order
    for i in range(len(events) - 1):
        if not (events[i] < events[i + 1]):
            return False
    return True

 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
44

# Ordinal Segments: Inserting values between existing ordinal values.
# segments() returns gap objects between active values. Each gap
# has a fresh() method to allocate a value within that gap.
#
# With 2 values [a, b], segments() returns 3 gaps:
#   (-inf, a)  -- head: values less than a
#   (a, b)     -- body: values between a and b
#   (b, +inf)  -- tail: values greater than b
#
# Filtering: segments(after=v) excludes gaps before v.
#            segments(before=v) excludes gaps after v.
#
# Use cases: inserting events in a timeline, priority insertion.

TIMES = symmetry.ordinal(name="ts", limit=6)

action Init:
    t_start = TIMES.fresh()
    t_end = TIMES.fresh()

atomic action InsertAnywhere:
    # Get all gaps between existing timestamps
    gaps = TIMES.segments()
    gap = oneof gaps
    t = gap.fresh()

atomic action InsertBetween:
    # Insert strictly between t_start and t_end.
    # Ordinal gaps are always non-empty (the domain is dense).
    gaps = TIMES.segments(after=t_start, before=t_end)
    gap = oneof gaps
    t = gap.fresh()
    # Guaranteed: t_start < t < t_end

atomic action InsertBeforeEarliest:
    # Insert before the minimum existing value.
    # (Inserting after max is just fresh(), but before min needs segments.)
    earliest = TIMES.min()
    gaps = TIMES.segments(before=earliest)
    gap = oneof gaps
    t = gap.fresh()

# Note: domain methods like values() cannot be called from assertions
# (no symmetry context in invariant scope). Use stored state instead.

 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

# Interval Symmetry: Ordered values where distance is meaningful.
# Operations: ==, !=, <, <=, >, >=, +int, -int, val-val.
# Reduction: zero-shifting (subtract minimum to normalize).
# Use cases: sequence numbers, log indices, counters.
#
# Key differences from ordinal:
#   - Supports arithmetic: val + 1, val - 1
#   - Value difference: val1 - val2 returns a plain int
#   - fresh() allocates max+1 (pessimistic, sequential)
#   - `divergence` parameter bounds the max spread (max - min)
#
# Key methods:
#   fresh()  - allocate max+1 (or start value if empty)
#   min()    - smallest active value (or fresh if empty)
#   max()    - largest active value (or fresh if empty)
#   values() - all active values, sorted ascending
#
# The model checker normalizes by shifting min to 0.
# E.g., {5,7,8} and {0,2,3} are equivalent (same distances).

LIMIT = 6
TICKS = symmetry.interval(name="t", limit=LIMIT)

action Init:
    t1 = TICKS.min()
    t2 = TICKS.min()

atomic fair action Tick1:
    t1 = t1 + 1

atomic fair action Tick2:
    t2 = t2 + 1

# With interval symmetry, only the *distances* between t1 and t2
# matter. States {t1=0,t2=0}, {t1=5,t2=5}, {t1=100,t2=100}
# are all equivalent (distance = 0).
# Total unique states: O(LIMIT^2) instead of unbounded.

 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

# Interval Divergence: Bounding the spread of interval values.
#
# The `divergence` parameter limits (max - min) across all active
# values in the domain. This prevents unbounded state growth.
#
# Parameter rules:
#   - divergence only:  limit = divergence + 1 (auto-derived)
#   - limit only:       divergence = limit - 1 (auto-derived)
#   - both:             must satisfy limit <= divergence + 1
#   - at least one of divergence or limit is required
#
# When a fresh() or arithmetic would exceed the divergence bound,
# the transition is disabled (pruned from state space).
#
# Use case: modeling sliding windows where values can't drift
# too far apart (e.g., TCP window, Raft log gap).

# divergence=3 means max - min <= 3 at all times.
# limit is auto-derived to 4 (divergence + 1).
SEQ = symmetry.interval(name="s", divergence=3)

action Init:
    head = SEQ.fresh()     # s0
    tail = SEQ.fresh()     # s1

atomic fair action AdvanceHead:
    head = head + 1
    # If head - tail > 3, this transition is pruned.

atomic fair action AdvanceTail:
    require tail < head
    tail = tail + 1

# Note: domain methods (values(), max(), min()) cannot be called
# from assertions. The divergence bound is enforced automatically
# by the symmetry engine — transitions that would violate it
# are pruned from the state space.

 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

# Rotational Symmetry: Integers mod N (ring positions).
# Operations: ==, !=, +int, -int, val-val (all mod limit).
# No ordering (<, >, etc.) since the domain wraps around.
# Reduction: rotate all values to lexicographically smallest set.
# Use cases: ring topologies, clock arithmetic, hash ring slots.
#
# Key methods:
#   fresh()   - next unused position (sequential, wrapping)
#   values()  - all active values
#   choices() - values() + one fresh (if under limit)
#   choose()  - min active value (or fresh if empty)
#
# Arithmetic wraps: on a ring of size 5, position 4 + 1 = 0.
# Difference returns plain int: (a - b) % limit.
#
# With rotational symmetry, the model checker recognizes that
# {0,2} and {1,3} and {3,0} are all equivalent (same gap pattern).

RING = symmetry.rotational(name="pos", limit=5)

action Init:
    positions = set()

atomic action Place:
    require len(positions) < 3
    p = RING.fresh()
    positions.add(p)

atomic action Advance:
    require len(positions) > 0
    p = oneof positions
    next_p = p + 1   # wraps mod 5
    if next_p not in positions:
        positions.remove(p)
        positions.add(next_p)

atomic action ComputeGap:
    require len(positions) == 2
    pair = RING.values()
    gap = pair[1] - pair[0]  # plain int, mod 5

 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

# Reflection Symmetry (Interval): Mirror states are equivalent.
#
# With reflection=True, the model checker also considers the
# "mirror image" of each state. For interval symmetry, this means
# {a, b} with distances [0, d] is equivalent to [d, 0] (reversed).
#
# Concretely: state (t1=0, t2=3) is equivalent to (t1=3, t2=0)
# because reflecting maps v -> (max - v), turning {0,3} into {3,0}
# which normalizes back to {0,3} with swapped variable bindings.
#
# This is useful when two processes are truly interchangeable and
# "t1 ahead of t2 by 3" is equivalent to "t2 ahead of t1 by 3".
#
# Compare: Run this file vs IntervalNoReflection.fizz to see
# the state space reduction from reflection.

LIMIT = 6
TICKS = symmetry.interval(name="t", limit=LIMIT, reflection=True)

action Init:
    t1 = TICKS.min()
    t2 = TICKS.min()

atomic fair action Tick1:
    t1 = t1 + 1

atomic fair action Tick2:
    t2 = t2 + 1

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

# Interval WITHOUT reflection (for comparison with ReflectionInterval.fizz).
# Run both and compare state/node counts to see the reduction.

LIMIT = 6
TICKS = symmetry.interval(name="t", limit=LIMIT, reflection=False)

action Init:
    t1 = TICKS.min()
    t2 = TICKS.min()

atomic fair action Tick1:
    t1 = t1 + 1

atomic fair action Tick2:
    t2 = t2 + 1

 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

# Reflection Symmetry (Rotational): Clockwise = counterclockwise.
#
# With reflection=True on a rotational domain, the model checker
# treats clockwise and counterclockwise orientations as equivalent.
# On a ring of size 6: {0,1} (gap=1) and {0,5} (gap=5, i.e. -1)
# are equivalent because one is the mirror of the other.
#
# Without reflection: {0,1} and {0,5} are distinct states.
# With reflection: they collapse to one canonical state.
#
# Use case: undirected ring networks where message direction
# doesn't matter, or symmetric physical arrangements.

RING = symmetry.rotational(name="pos", limit=6, reflection=True)

action Init:
    positions = set()

atomic action Place:
    require len(positions) < 3
    p = RING.fresh()
    positions.add(p)

atomic action Step:
    require len(positions) > 0
    p = any positions
    next_p = p + 1
    if next_p not in positions:
        positions.remove(p)
        positions.add(next_p)

 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

# Materialize: Pre-populate all domain values at declaration.
#
# With materialize=True, all `limit` values exist from the start.
# - values() immediately returns all values
# - fresh() is NOT allowed (raises error)
# - Useful when the set of values is fixed and known upfront
#
# Works with all symmetry types:
#   nominal:    values 0, 1, ..., limit-1
#   ordinal:    values 0, 1, ..., limit-1
#   interval:   values start, start+1, ..., start+limit-1
#   rotational: values 0, 1, ..., limit-1
#
# Use cases: fixed-size process rings, known node sets,
#            enumerated configurations.

NODES = symmetry.rotational(name="n", limit=4, materialize=True)

action Init:
    # All 4 values exist immediately
    status = {}
    for n in NODES.values():
        status[n] = "idle"

atomic action Activate:
    n = oneof NODES.values()
    require status[n] == "idle"
    status[n] = "active"

atomic action Deactivate:
    n = oneof NODES.values()
    require status[n] == "active"
    status[n] = "idle"

atomic action PassToken:
    n = oneof NODES.values()
    require status[n] == "active"
    next_n = n + 1  # wraps mod 4
    status[n] = "idle"
    status[next_n] = "active"