Assertions

 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

 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

 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

 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

 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

 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

# Example 0096: One-Step Reachability with next_states()
# Assert that every trashed item can be restored in one step using next_states()
# Demonstrates: next_states(), one-step reachability, always assertion

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

 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

# Example 0097: Detecting Unrestorable States with next_states()
# A stack-based trash means only the most recent item is restorable, so the next_states() assertion fails with a counterexample
# Demonstrates: next_states(), assertion failure, counterexample

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

 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

# Example 0098: next_states() Ignores the Concurrency Cap
# The next_states() probe sees enabled transitions even when max_concurrent_actions is exhausted
# Demonstrates: next_states(), max_concurrent_actions, serial actions

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

 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

# Example 0099: Matching next_states() Transitions to Roles
# Use role_id and action_name to match next_states() transitions to a specific role instance
# Demonstrates: next_states(), role_id, symmetric roles

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

 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

# Example 0115: Func Calls in Assertions
# Fizz funcs can be called anywhere in an assertion expression, each on its own copy of the state
# Demonstrates: role funcs and top-level funcs called inside expressions

---
deadlock_detection: false
---

# Inside an assertion, fizz funcs can be called anywhere in an expression:
# in a return, in a condition, in a list comprehension, or on an
# invariants line. Each call runs on its own copy of the state, so a func
# can't change the model. It must be deterministic: no oneof, any or
# parallel blocks.

MAX_MESSAGES = 2

role Consumer:
    action Init:
        self.received = 0

    atomic fair action Receive:
        require self.received < MAX_MESSAGES
        self.received = self.received + 1

    func done():
        return self.received == MAX_MESSAGES

func total_received():
    total = 0
    for c in consumers:
        total = total + c.received
    return total

func all_done():
    return all([c.done() for c in consumers])

action Init:
    consumers = []
    for i in range(2):
        consumers.append(Consumer())

invariants:
    always total_received() <= MAX_MESSAGES * len(consumers)

always assertion DoneMeansAllReceived:
    return not all_done() or total_received() == MAX_MESSAGES * len(consumers)

always assertion SomeDoneCount:
    return len([c for c in consumers if c.done()]) <= len(consumers)

eventually always assertion AllDone:
    return all_done()

 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

# Example 0116: Temporal Formulas
# An assertion without a prefix returns a temporal formula built from always, eventually, until, leadsto and implies
# Demonstrates: temporal formulas, until, leadsto, for clauses on an assertion header

---
deadlock_detection: false
---
# An assertion can return a formula built from always, eventually, until,
# leadsto, implies, and, or and not. Each maximal non-temporal part of the
# formula (an atom) is an ordinary expression, evaluated in every state.
# Locals before the return are recomputed in every state too.
#
# A server starts, then answers its clients' requests. Each client sends at
# most two requests, one at a time. Start and Respond are fair, so each
# pending request is eventually answered.
# Respond's oneof isn't fair, but the bound keeps it from serving one client
# forever: once a client is done, only the other is left to pick.

NUM_CLIENTS = 2

action Init:
    started = False
    pending = [False] * NUM_CLIENTS
    answered = [0] * NUM_CLIENTS

atomic fair action Start:
    require not started
    started = True

atomic action Request:
    require started
    c = oneof [i for i in range(NUM_CLIENTS) if not pending[i] and answered[i] < 2]
    pending[c] = True

atomic fair action Respond:
    c = oneof [i for i in range(NUM_CLIENTS) if pending[i]]
    pending[c] = False
    answered[c] += 1

func no_requests():
    return True not in pending

# No request arrives before the server starts, and it does start (strong until).
assertion NoRequestsBeforeStart:
    return no_requests() until started

# A `for` clause on the header checks one formula per client: Answered[0]
# and Answered[1]. The iterable may use only constants.
assertion Answered for c in range(NUM_CLIENTS):
    return pending[c] leadsto not pending[c]

# Once started, the server stays started.
assertion StaysStarted:
    return always (started implies always started)

# `return always eventually P` is the same check as the prefixed
# `always eventually assertion`, with the local recomputed in each state.
assertion EventuallyIdle:
    busy = len([c for c in range(NUM_CLIENTS) if pending[c]])
    return always eventually busy == 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
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 0117: Temporal Formula Violation
# A temporal formula that fails, with a counterexample run that violates it
# Demonstrates: temporal formulas, assertion failure, counterexample

---
deadlock_detection: false
---
# A temporal formula that fails. The checker reports the first failing
# assertion and a counterexample: a run that violates it.
#
# A server starts, then answers its clients' requests. Each client sends at
# most two requests. Respond is not fair, so a request may never be answered.

NUM_CLIENTS = 2

action Init:
    started = False
    pending = [False] * NUM_CLIENTS
    answered = [0] * NUM_CLIENTS

atomic fair action Start:
    require not started
    started = True

atomic action Request:
    require started
    c = oneof [i for i in range(NUM_CLIENTS) if not pending[i] and answered[i] < 2]
    pending[c] = True

atomic action Respond:
    c = oneof [i for i in range(NUM_CLIENTS) if pending[i]]
    pending[c] = False
    answered[c] += 1

func no_requests():
    return True not in pending

# No request arrives before the server starts, and it does start (strong until).
assertion NoRequestsBeforeStart:
    return no_requests() until started

# A `for` clause on the header checks one formula per client: Answered[0]
# and Answered[1]. The iterable may use only constants.
assertion Answered for c in range(NUM_CLIENTS):
    return pending[c] leadsto not pending[c]

# Once started, the server stays started.
assertion StaysStarted:
    return always (started implies always started)

# `return always eventually P` is the same check as the prefixed
# `always eventually assertion`, with the local recomputed in each state.
assertion EventuallyIdle:
    busy = len([c for c in range(NUM_CLIENTS) if pending[c]])
    return always eventually busy == 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
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

# Example 0118: Possibility
# possibly P: some path from this state reaches a state where P holds
# Demonstrates: possibly, can happen versus will happen, nested possibly, exists eventually

---
deadlock_detection: false
---
# `possibly P` holds in a state when some path from it, of zero or more
# steps, reaches a state where P holds. It asks what *can* happen, so it
# follows every action, fair or not (but never a crash). The operators
# around it keep their usual meaning over fair runs.
#
# A ticket is booked, then flown or cancelled. A cancelled ticket can be
# booked again, and flying ends it. Upgrade is not fair: it may happen, but
# no run has to take it.

action Init:
    status = "none"
    upgraded = False

atomic fair action Book:
    require status == "none"
    status = "booked"

atomic fair action Cancel:
    require status == "booked"
    status = "cancelled"

atomic fair action Rebook:
    require status == "cancelled"
    status = "none"

atomic fair<strong> action Fly:
    require status == "booked"
    status = "flown"

atomic action Upgrade:
    require status == "booked" and not upgraded
    upgraded = True

# From every booked state, cancelling is still possible.
assertion CanCancel:
    return always (status == "booked" implies possibly status == "cancelled")

# An upgrade can happen from any booked, not yet upgraded ticket, even
# though Upgrade isn't fair. `eventually upgraded` would fail: a fair run can
# fly without upgrading. possibly says it *can* happen, not that it *will*.
assertion CanUpgrade:
    return always ((status == "booked" and not upgraded) implies possibly upgraded)

# Nested: from the start, the ticket can be booked in a state from which it
# can still fly.
assertion CanBookThenFly:
    return possibly (status == "booked" and possibly status == "flown")

# Once flown, booking is no longer possible.
assertion FlyingIsFinal:
    return always (status == "flown" implies not possibly status == "booked")

# Fly is strongly fair, so every fair run reaches a state from which booking
# is no longer possible.
assertion EventuallyDone:
    return eventually not possibly status == "booked"

# `exists eventually P` is another spelling of `possibly P`.
assertion CanFly:
    return exists eventually status == "flown"

 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

# Example 0119: Possibility Violation
# A possibly property that fails: from some state, no path reaches the condition
# Demonstrates: possibly, recoverability, counterexample note

---
deadlock_detection: false
---
# A document can be moved to the trash and restored, or purged from the
# trash for good. Every trashed document can still be restored, but once
# purged it can't come back, so "the document can always become active
# again" fails.
#
# The counterexample ends in a state where the possibly is false, and a note
# says the step after which no path reaches its condition.

action Init:
    status = "active"

atomic action Delete:
    require status == "active"
    status = "trash"

atomic action Restore:
    require status == "trash"
    status = "active"

atomic action Purge:
    require status == "trash"
    status = "purged"

# Holds: a trashed document can still be restored.
assertion Restorable:
    return always (status == "trash" implies possibly status == "active")

# Fails: after Purge, no path leads back to an active document.
assertion Recoverable:
    return always possibly status == "active"

 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 0120: Weak Until
# P unless Q: P holds until Q happens, or forever if Q never happens
# Demonstrates: unless, unless versus until, unless under always

---
deadlock_detection: false
---
# `P until Q` requires Q to happen. `P unless Q` does not: if Q never
# happens, P must hold forever. Once Q happens, neither says anything more
# about P.
#
# A client may take a lease, and renews it while it works. It may hand the
# lease back, but nothing forces it to, so a run may keep the lease forever.
# Only handing it back ends the lease.

action Init:
    leased = False
    returned = False
    renewals = 0

atomic action Take:
    require not leased and not returned
    leased = True

atomic fair action Renew:
    require leased and renewals < 2
    renewals += 1

atomic action Return:
    require leased
    leased = False
    returned = True

# Once taken, the lease stays held until it is handed back, or forever.
assertion HeldUntilReturned:
    return always (leased implies (leased unless returned))

# The lease is never handed back before it is taken. Taking it isn't fair,
# so a run may never take it, and until would fail here.
assertion NotReturnedBeforeTaken:
    return (not returned) unless leased

 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

# Example 0122: Scoped Absence Violation
# A property about what happens after a condition, which a state invariant can't express
# Demonstrates: always (P implies always Q), why an invariant misses it, counterexample

---
deadlock_detection: false
---
# Basic economy tickets can't be refunded. Premium tickets get a full
# refund on cancel. A basic ticket can be upgraded to premium.
#
# The loophole: buy basic, upgrade, then cancel for a full refund. The
# invariant NoBasicRefund can't see it, because once upgraded the ticket
# is premium, and a refund on a premium ticket is fine. The formula
# BasicNeverRefunded talks about the future of every basic ticket: once
# basic, never refunded, whatever happens after. It fails, and the
# counterexample is the loophole. Without formulas this needs a history
# variable that remembers the original cabin.

action Init:
    cabin = oneof ["basic", "premium"]
    status = "booked"
    refunded = False

atomic action Upgrade:
    require status == "booked" and cabin == "basic"
    cabin = "premium"

atomic action Cancel:
    require status == "booked"
    status = "cancelled"
    if cabin == "premium":
        refunded = True

atomic action Fly:
    require status == "booked"
    status = "flown"

# Passes: no state is both basic and refunded.
always assertion NoBasicRefund:
    return not (cabin == "basic" and refunded)

# Fails: Upgrade then Cancel refunds a ticket that was bought as basic.
assertion BasicNeverRefunded:
    return always (cabin == "basic" implies always not refunded)

 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 0123: Assertion For Clauses
# One assertion header checks one property per value, with filters, nesting and tuples
# Demonstrates: for clauses on prefixed and formula assertions, if filters, several clauses, tuple targets

---
deadlock_detection: false
---
# A primary holds every key, and a fair Copy action copies a key to one
# more replica at a time.
#
# A `for` clause on the assertion header checks one instance per value,
# named like Copied[a, 1]. It works on prefixed assertions (always,
# always eventually, eventually always) as well as on formula assertions.
# Iterables and filters may use only constants and builtins: they are
# evaluated once, before Init.

KEYS = ["a", "b"]
REPLICAS = [0, 1, 2]
PRIMARY = 0
WATCHED = [("a", 1), ("b", 2)]

action Init:
    copies = {k: [PRIMARY] for k in KEYS}

atomic fair action Copy:
    k = oneof KEYS
    r = oneof [r for r in REPLICAS if r not in copies[k]]
    copies[k] = copies[k] + [r]

# One safety check per key: Bounded[a] and Bounded[b].
always assertion Bounded for k in KEYS:
    return len(copies[k]) <= len(REPLICAS)

# Several clauses nest in order, and `if` filters the values: one check
# per key and non-primary replica, four in all.
always eventually assertion Copied for k in KEYS for r in REPLICAS if r != PRIMARY:
    return r in copies[k]

# With several targets, each value is a tuple of that length.
assertion StaysCopied for k, r in WATCHED:
    return always (r in copies[k] implies always r in copies[k])