Assertions

always assertion Invariant:
    return counter >= 0

exists assertion Reachability:
    return counter == 10

transition assertion MonotonicIncrease(before, after):
    if after.counter != before.counter:
        return after.counter > before.counter
    return True  # Stutter step

# ✅ CORRECT: Allows stuttering
transition assertion NoDecrease(before, after):
    if after.value != before.value:
        return after.value >= before.value
    return True  # Stutter allowed

# ❌ WRONG: Requires change every step
transition assertion AlwaysIncreases(before, after):
    return after.value > before.value
    # Fails on stutter steps!

always assertion EveryTrashItemRestorable:
    for k in items:
        if items[k] == "trash":
            if len([n for n in next_states() if n.state.items[k] == "active"]) == 0:
                return False
    return True

always assertion EveryIdleWorkerCanWork:
    for w in workers:
        if w.status == "idle":
            if len([n for n in next_states() if n.action_name == "Work" and n.role_id == w.__id__]) == 0:
                return False
    return True

eventually always assertion EventuallyStable:
    return done == True

always eventually assertion AlwaysProgresses:
    return processed_count > 0

 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

# Example 0038: Always Assertion (Safety Property)
# Safety invariants that must hold in every state
# Demonstrates: always assertion, safety properties

MAX = 5

action Init:
    counter = 0
    total = 0

atomic action Increment:
    require counter < MAX

    counter = counter + 1
    total = total + counter

# Safety property: must be true in ALL states
always assertion CounterBounded:
    return counter <= MAX

always assertion TotalCorrect:
    # Total should be sum of 1..counter
    expected = (counter * (counter + 1)) / 2
    return total == expected

# If either assertion fails, model checker reports violation

atomic action NoOp:
    if counter >= MAX:
        pass

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

# Example 0039: Exists Assertion
# Existential properties - at least one state must satisfy
# Demonstrates: exists assertion

action Init:
    value = 0
    reached_five = False

atomic action Increment:
    require value < 10

    value = value + 1

    if value == 5:
        reached_five = True

# Existential property: must be true in AT LEAST ONE state
exists assertion ReachesFive:
    return reached_five == True

# Model checker verifies that some execution path reaches this state

atomic action NoOp:
    if value >= 10:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 11, queued: 0
Valid Nodes: 11 Unique states: 11
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

# Example 0040: Transition Assertion
# Properties about state transitions
# Demonstrates: transition assertion with before/after states

action Init:
    counter = 0

atomic action Increment:
    require counter < 5

    counter = counter + 1

atomic action BigIncrement:
    require counter < 5

    counter = counter + 3

# Transition assertion: checks state changes
# Parameters are before and after states
transition assertion NoLargeJumps(before, after):
    # Counter should not increase by more than 3 in one step
    delta = after.counter - before.counter
    return delta <= 3

# This checks the transition, not individual states
# Stutter-invariant: if state doesn't change, assertion passes

atomic action NoOp:
    if counter >= 5:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 8, queued: 0
Valid Nodes: 8 Unique states: 8
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

# Example 0041: Eventually Always (Liveness)
# Eventually the system reaches a stable state
# Demonstrates: eventually always assertion (liveness property)

action Init:
    counter = 0
    stable = False

fair action Increment:
    if counter >= 5:
        stable = True
        return

    counter = counter + 1

# Liveness property: eventually reaches a state where it stays true
eventually always assertion BecomesStable:
    return stable == True

# "Eventually always" means:
# - Eventually: at some point in the future
# - Always: from that point onward, stays true
# This requires fairness to prevent infinite incrementing

atomic action NoOp:
    if stable:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 9, queued: 0
Valid Nodes: 9 Unique states: 9
Checking eventually always BecomesStable
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

# Example 0042: Always Eventually (Progress)
# System always makes progress eventually
# Demonstrates: always eventually assertion (strong fairness)

action Init:
    counter = 0

fair action Process:
    require counter < 3

    counter = counter + 1

# Progress property: eventually the counter reaches target
always eventually assertion AlwaysMakesProgress:
    # Eventually counter reaches 3
    return counter >= 3

# "Always eventually" means:
# - Always: in every state
# - Eventually: progress happens within finite steps
# With fairness, Process will eventually run enough times

atomic action NoOp:
    if counter >= 3:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 4, queued: 0
Valid Nodes: 4 Unique states: 4
Checking always eventually AlwaysMakesProgress
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
33
34

---
deadlock_detection: false
options:
    max_actions: 8
---

# Soft-delete CRUDL: any trashed item can be restored directly.
# EveryTrashItemRestorable must PASS.

NUM_ITEMS = 3

action Init:
    items = {}
    next_id = 0

atomic action Create:
    require next_id < NUM_ITEMS
    items[next_id] = "active"
    next_id += 1

atomic action Delete:
    id = oneof [k for k in items if items[k] == "active"]
    items[id] = "trash"

atomic action Restore:
    id = oneof [k for k in items if items[k] == "trash"]
    items[id] = "active"

always assertion EveryTrashItemRestorable:
    for k in items:
        if items[k] == "trash":
            if len([n for n in next_states() if n.state.items[k] == "active"]) == 0:
                return False
    return True

StateSpaceOptions: options:{max_actions:8 max_concurrent_actions:2} deadlock_detection:false
Nodes: 37, queued: 0
Valid Nodes: 37 Unique states: 15
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
33
34
35
36
37
38
39
40
41

---
deadlock_detection: false
options:
    max_actions: 8
---

# Soft-delete CRUDL where the trash is a STACK: only the most recently
# deleted item can be restored. With two items in the trash, the bottom
# one is not restorable in one step, so EveryTrashItemRestorable must
# FAIL. This is the case a global-reachability (`exists`) formulation
# cannot catch.

NUM_ITEMS = 3

action Init:
    items = {}
    trash_stack = []
    next_id = 0

atomic action Create:
    require next_id < NUM_ITEMS
    items[next_id] = "active"
    next_id += 1

atomic action Delete:
    id = oneof [k for k in items if items[k] == "active"]
    items[id] = "trash"
    trash_stack = trash_stack + [id]

atomic action Restore:
    require len(trash_stack) > 0
    id = trash_stack[-1]
    trash_stack = trash_stack[:-1]
    items[id] = "active"

always assertion EveryTrashItemRestorable:
    for k in items:
        if items[k] == "trash":
            if len([n for n in next_states() if n.state.items[k] == "active"]) == 0:
                return False
    return True

StateSpaceOptions: options:{max_actions:8 max_concurrent_actions:2} deadlock_detection:false
FAILED: Model checker failed. Invariant: EveryTrashItemRestorable
------
Init
--
state: {"items":{},"next_id":0,"trash_stack":[]}
------
Create
--
state: {"items":{"0":"active"},"next_id":1,"trash_stack":[]}
------
Create
--
state: {"items":{"0":"active","1":"active"},"next_id":2,"trash_stack":[]}
------
Delete
--
state: {"items":{"0":"active","1":"active"},"next_id":2,"trash_stack":[]}
------
Any:id=0
--
state: {"items":{"0":"trash","1":"active"},"next_id":2,"trash_stack":[0]}
------
Delete
--
state: {"items":{"0":"trash","1":"active"},"next_id":2,"trash_stack":[0]}
------
Any:id=1
--
state: {"items":{"0":"trash","1":"trash"},"next_id":2,"trash_stack":[0,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
31
32
33

---
deadlock_detection: false
options:
    max_actions: 6
    max_concurrent_actions: 1
---

# Regression guard for the concurrency-cap false positive: Churn is a
# serial (non-atomic) action. At its mid-action yield, the one in-flight
# thread exhausts max_concurrent_actions=1, so the real explorer cannot
# schedule Restore from that state. The next_states() probe must ignore
# the cap (ENABLED is a property of the state, not the scheduler), so
# TrashRestorable must PASS. If the probe respected the cap, this spec
# would FAIL at every mid-Churn yield.

action Init:
    items = {0: "trash"}
    counter = 0

action Churn:
    counter = counter + 1
    counter = counter + 1

atomic action Restore:
    id = oneof [k for k in items if items[k] == "trash"]
    items[id] = "active"

always assertion TrashRestorable:
    for k in items:
        if items[k] == "trash":
            if len([n for n in next_states() if n.state.items[k] == "active"]) == 0:
                return False
    return True

StateSpaceOptions: options:{max_actions:6 max_concurrent_actions:1} deadlock_detection:false
Nodes: 55, queued: 0
Valid Nodes: 55 Unique states: 43
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46

---
deadlock_detection: false
options:
    max_actions: 6
---

# next_states() with symmetric roles: transitions carry structured fields
# (kind, role_ref, role_id, action_name) alongside the flat name. role_id
# is the role's identity value (same as the role's __id__) and compares by
# VALUE, so `n.role_id == w.__id__` works across the assertion/probe clone
# boundary. Comparing Role objects directly would silently be False —
# roles compare by pointer. See GOTCHAS.
# (The fields are named action_name/role_ref because `action` and `role`
# are fizz keywords and cannot appear as attribute names.)
#
# Also exercises the id component attrs: id.name ("Worker") and id.index.

NUM_WORKERS = 2

symmetric role Worker:
    action Init:
        self.status = "idle"

    atomic action Work:
        require self.status == "idle"
        self.status = "done"

action Init:
    workers = bag()
    for i in range(NUM_WORKERS):
        workers.add(Worker())

always assertion EveryIdleWorkerCanWork:
    for w in workers:
        if w.status == "idle":
            witnesses = [n for n in next_states() if n.kind == "action" and n.action_name == "Work" and n.role_id == w.__id__]
            # Exactly one: each worker has exactly one Work transition of its
            # own. If role_id failed to discriminate between instances, both
            # workers' transitions would match and this would be 2.
            if len(witnesses) != 1:
                return False
            if w.__id__.name != "Worker":
                return False
            if w.__id__.index < 0:
                return False
    return True

StateSpaceOptions: options:{max_actions:6 max_concurrent_actions:2} deadlock_detection:false
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
IsLive: true
PASSED: Model checker completed successfully

---
deadlock_detection: false
options:
    max_actions: 6
    crash_on_yield: false
---

# Regression pin for the no_graph exists bug: an unsatisfiable `exists`
# must FAIL under --experimental_no_graph (flags.txt) exactly as it does
# with the full graph. Before the fix, exists assertions were silently
# skipped in no_graph mode and this spec reported PASSED.

action Init:
    counter = 0

atomic action Inc:
    require counter < 3
    counter = counter + 1

exists assertion ImpossibleProbe:
    return counter > 999

exists assertion ReachableProbe:
    return counter == 2

StateSpaceOptions: options:{max_actions:6 max_concurrent_actions:2 crash_on_yield:false} deadlock_detection:false
Nodes: 4, queued: 0
FAILED: Expected states never reached
Invariant 0: ImpossibleProbe

---
deadlock_detection: false
options:
    max_actions: 6
    crash_on_yield: false
---

# Companion to 09-10: a satisfiable `exists` must PASS under
# --experimental_no_graph (flags.txt) — the witness accumulator must
# actually detect witnesses, not just fail everything.

action Init:
    counter = 0

atomic action Inc:
    require counter < 3
    counter = counter + 1

exists assertion ReachableProbe:
    return counter == 2

StateSpaceOptions: options:{max_actions:6 max_concurrent_actions:2 crash_on_yield:false} deadlock_detection:false
Nodes: 4, queued: 0
PASSED: Model checker completed successfully

---
deadlock_detection: false
options:
    max_actions: 6
---

# Simulation-mode exists coverage warning: with a fixed seed (flags.txt,
# forces a single deterministic run), the unsatisfiable exists must
# produce a named WARNING — not a failure, since simulation is not
# exhaustive. The reachable probe must not be warned about if this
# seed's trace witnesses it; the impossible one always warns.

action Init:
    counter = 0

atomic action Inc:
    require counter < 3
    counter = counter + 1

exists assertion ImpossibleProbe:
    return counter > 999

StateSpaceOptions: options:{max_actions:6 max_concurrent_actions:2} deadlock_detection:false
WARNING: 1 exists assertion(s) never satisfied in 1 simulation run(s):
exists assertion ImpossibleProbe
Simulation is not exhaustive: this may be a coverage gap rather than unreachability. Model check to verify.

gdoc_arrow_left_alt Fairness Data Structures gdoc_arrow_right_alt