# Assertions

> FizzBee assertions: always (safety), exists, transition, eventually always and always eventually (liveness), plus next_states() lookahead, with examples.

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


Assertions specify properties the model checker should verify.

## Always (Safety)

Must hold in all reachable states:

```python
always assertion Invariant:
    return counter >= 0
```

**Use cases**: Invariants, safety properties

## Exists

Must hold in at least one reachable state:

```python
exists assertion Reachability:
    return counter == 10
```

**Use cases**: Reachability, possibility

## Transition

Must hold for all state transitions:

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

**Stutter Invariance** (critical requirement):

Transition assertions **must allow stutter steps** (transitions where state doesn't change):

```python
# ✅ 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!
```

**Why stutter invariance matters**:
- Model checker may have steps where only thread-local variables change
- Some actions may execute without changing state variables
- FizzBee automatically passes assertion if no state variables changed

**Automatic handling**: If no state variables changed, assertion assumed satisfied (even if thread-local variables changed)

**Pattern**: Always check `before != after` before asserting a property about the change

## next_states() — One-Step Lookahead (ENABLED-style properties)

Inside an `always assertion`, `next_states()` returns the list of successor
transitions from the state under check — one entry per enabled transition,
each executed to its first yield point. This expresses TLA+ ENABLED-style
safety properties with arbitrary quantifier nesting, e.g. "every item in the
trash must be restorable *right now*":

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

Each transition is a struct:

| Field | Type | Example | Notes |
|---|---|---|---|
| `name` | string | `"Customer#0.PlaceOrder"` | Flat label; also `"thread-0"`, `"channel-0-message-1"` |
| `kind` | string | `"action"` | `"action"`, `"thread"`, or `"channel"` |
| `role_ref` | string / None | `"Customer#0"` | None for non-role transitions |
| `role_id` | id value / None | `Customer0` | Same value as the role's `__id__`; compares by value |
| `action_name` | string / None | `"PlaceOrder"` | Bare action name; None for thread/channel |
| `state` | struct | `n.state.items` | Successor state vars — same shape as `before`/`after` in transition assertions |

(`action_name`/`role_ref` — not `action`/`role` — because `action` and `role`
are fizz keywords and cannot appear as attribute names.)

To scope a check to a specific role instance, compare ids — never role
objects (roles compare by pointer and never match across states; see
GOTCHAS):

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

Id values also expose their components: `w.__id__.name` → `"Worker"`,
`w.__id__.index` → `0`.

**Semantics**:
- Successors **ignore exploration bounds** (`max_actions` depth,
  `max_concurrent_actions`, per-action caps). Enabledness is a property of
  the state, not the scheduler — so the check does not false-fail at the
  depth frontier or when in-flight actions exhaust the concurrency cap.
- Crash variants are excluded.
- For **non-atomic (serial) actions**, the successor is the action's *first
  yield point* — effects later in the body are not yet visible. Use
  effect predicates (`n.state.x == ...`) with atomic witness actions; use
  name filtering (`n.action_name == ...`) to check a serial action can start.
- Computed lazily, once per checked state. Works in model checking (BFS/DFS),
  simulation, and no-graph modes. Not available in composition specs.
- Reference examples: `09-06` through `09-09`.

## Eventually Always (Liveness)

Eventually reaches a stable state:

```python
eventually always assertion EventuallyStable:
    return done == True
```

**Requires**: Fairness on relevant actions

## Always Eventually (Progress)

Always makes progress:

```python
always eventually assertion AlwaysProgresses:
    return processed_count > 0
```

**Requires**: Strong fairness typically

## Temporal Formulas

An assertion without a prefix returns a temporal formula. The body may
compute locals first, as any assertion can, and must end with a single
`return`:

```python
assertion Answered:
    waiting = [c for c in range(NUM_CLIENTS) if pending[c]]
    return len(waiting) > 0 leadsto len(waiting) == 0

assertion NoRequestsBeforeStart:
    return no_requests() until started

assertion StaysStarted:
    return always (started implies always started)
```

| FizzBee | LTL | TLA+ | Holds on a run when |
|---|---|---|---|
| `always P` | □P or G P | `[]P` | P holds in every state |
| `eventually P` | ◇P or F P | `<>P` | P holds in some state, now or later |
| `P until Q` | P U Q | none built in | Q holds in some state, and P in every state before it |
| `P unless Q` | P W Q | none built in | P holds in every state before the first where Q holds; if Q never holds, in every state |
| `P leadsto Q` | □(P → ◇Q) | `P ~> Q` | every state where P holds is followed, now or later, by one where Q holds |
| `P implies Q` | P → Q | `P => Q` | P is false or Q holds |
| `not`, `and`, `or` | ¬, ∧, ∨ | `~`, `/\`, `\/` | as usual |
| `possibly P` | none; CTL's EF P | none built in | some path from the current state reaches a state where P holds (see Possibility below) |

There is no next operator (LTL X, TLA+ primes): a formula can't tell a
state from a repeat of it.

Operator precedence, from tightest to loosest binding:

| Level | Operators | Meaning |
|---|---|---|
| 1 | any expression | evaluated in a state |
| 2 | `not P`, `always P`, `eventually P`, `possibly P` | prefix |
| 3 | `P and Q` | |
| 4 | `P or Q` | |
| 5 | `P implies Q`, `P until Q`, `P unless Q`, `P leadsto Q` | need parentheses to combine |

`and` and `or` chain (`P and Q and R`). The level 5 operators don't: write
`(P until Q) until R` or `P until (Q until R)`; `P until Q until R` is an
error, and so is mixing two of them without parentheses.

- `P until Q`: Q eventually holds, and P holds in every state before it
  (strong until).
- `P unless Q`: weak until. `P until Q` requires Q to happen. `P unless Q`
  does not: if Q never happens, P must hold forever. Once Q happens,
  neither operator constrains P afterward. It is not "P if not Q": in
  `x == 0 unless done`, a state with `x == 1` before `done` fails it.
- `P leadsto Q`: `always (P implies eventually Q)`.
- `implies`, `until`, `unless`, `leadsto` and `possibly` are keywords only in
  an assertion's return, so they can still be used as names elsewhere.

**Atoms.** Each largest part of the formula with no temporal operator is an
ordinary expression (it may call funcs), evaluated in every state.
**Locals are recomputed in every state**: they are definitions, not
snapshots. So `v = x` then `return eventually x > v` compares `x` with
itself and is always false.

**Parentheses.** Prefix operators bind tightest, so
`always x >= 0 and y >= 0` would mean `(always x >= 0) and y >= 0`. That is
an error; write `always (x >= 0 and y >= 0)`. The same holds for
`eventually`, `possibly` and `not always` on the left of any binary
operator.

**One formula per value.** A `for` clause on the header checks one instance
per value, named like `Answered[0]`. Iterables and filters may use only
constants and builtins, and are evaluated once, before `Init`. The targets
are names; with several, like `for a, b in PAIRS`, each value must be a
tuple or list of that length. Several clauses nest in order, and a later
clause can use an earlier one's names. Inside the assertion (its filters,
later clauses and body), a header name shadows a constant with the same
name, as a loop variable would:

```python
assertion Answered for c in range(NUM_CLIENTS):
    return pending[c] leadsto not pending[c]

assertion Replicated for k in KEYS for r in REPLICAS if r != PRIMARY:
    return written[k] leadsto r in copies[k]
```

A `for` clause also works on prefixed assertions:

```python
always eventually assertion Copied for k in KEYS for r in REPLICAS if r != PRIMARY:
    return r in copies[k]
```

`return always P`, `return always eventually P` and
`return eventually always P` (with P free of temporal operators) are the
same checks as the prefixed `always`, `always eventually` and
`eventually always` assertions.

**One return.** The body computes locals, then returns one formula. A
formula can't be chosen with `if`:

```python
assertion Progress:
    if MODE == 1:                 # error: a single return, as the last statement
        return always x >= 0
    return eventually x == 2
```

Instead, use one of these:

```python
# Separate assertions, when the cases are separate properties.
assertion Bounded:
    return always x >= 0

assertion Reaches:
    return eventually x == 2

# A local for the non-temporal part.
assertion Progress:
    ready = MODE == 1 and x >= 0
    return ready leadsto x == 2

# Connectives. An atom outside every temporal operator, such as MODE == 1
# here, is evaluated in the first state only.
assertion ByMode:
    return (MODE == 1 and always x >= 0) or (MODE != 1 and eventually x == 2)
```

**Common patterns.** For a request that is made and then served:

| Pattern | Formula | Meaning |
|---|---|---|
| Invariance | `always (served implies requested)` | never served without being requested |
| Absence | `always not (served and not requested)` | the bad state never occurs |
| Existence | `eventually served` | served at some point |
| Response | `requested leadsto served` | every request is eventually served |
| Precedence | `(not served) unless requested` | not served before it's requested; it may never be requested |
| Strict precedence | `(not served) until requested` | requested at some point, and not served before then |
| Stays true | `always (served implies always served)` | once served, served forever |
| Stability | `eventually always served` | eventually settles with served true |
| Recurrence | `always eventually served` | served infinitely often |
| Constrained response | `always (requested implies (requested until served))` | once requested, stays requested until served |
| Held until released | `always (held implies (held unless released))` | once held, stays held until released, or forever |
| Conditional | `(always eventually requested) implies (always eventually served)` | if requested infinitely often, served infinitely often |
| Absence after | `always (basic implies always not refunded)` | once basic, never refunded, whatever happens next |

**Properties that start from a condition.** `always (P implies F)` checks
the formula F from every state where P holds: a precondition for the
property. It replaces a history variable in the model. For example, a basic
ticket can't be refunded, but it can be upgraded to premium, which can. The
invariant `not (cabin == "basic" and refunded)` misses the
upgrade-then-cancel loophole, because the ticket is premium by the time it
is refunded. The formula talks about every basic ticket's future instead:

```python
assertion BasicNeverRefunded:
    return always (cabin == "basic" implies always not refunded)
```

It fails, and the counterexample is the loophole: buy basic, `Upgrade`,
`Cancel`. F can be any formula: `always Q` (safety after P),
`eventually Q` (that is `P leadsto Q`), `possibly Q`, or `Q unless R`.
See `09-20`.

`until` is strong and `unless` is weak: `P unless Q` means
`(P until Q) or always P`. Like any formula, a bare `P unless Q` is judged
from the first state only; to check it from every state where P starts,
write `always (start implies (P unless Q))`, as in the held-until-released
pattern.

**Possibility.** The other operators are linear-time, as in LTL: they
describe each fair run. `possibly` is the one branching-time operator,
CTL's EF: `possibly P` holds in a state when some path from it, of zero or
more steps, reaches a state where P holds. It says P *can* happen,
never that it *will*: the path may take any action, fair or not. The
operators around it keep their meaning over fair runs:

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

# The system can always get back to idle.
assertion CanReset:
    return always possibly status == "idle"
```

```python
action Init:
    x = 0

atomic action Leave:        # not fair
    x = 1

atomic fair action Stay:
    x = 0

assertion CanLeave:
    return always possibly (x == 1)   # passes: Leave is a path to x == 1

assertion WillLeave:
    return eventually (x == 1)        # fails: a fair run can repeat Stay forever
```

- What follows `possibly` is a condition on a state: expressions combined
  with `and`, `or`, `not`, `implies` and nested `possibly`. Temporal
  operators can't appear inside it, so `possibly (always P)` is an error,
  and `possibly (eventually P)` is written `possibly P`.
- The path never takes a crash: recovery that needs a fault isn't something
  a user can count on. States reached after a crash are still checked by an
  enclosing `always`.
- `exists eventually P` is another spelling of `possibly P`. An
  `exists assertion` is close to `possibly` checked in the initial state,
  except that it also counts states reached by a crash.
- `next_states()` looks one step ahead; `possibly` looks any number of
  steps ahead.
- When a formula with `possibly` fails, a note under the assertion's name
  gives the step of the counterexample after which that `possibly` is
  false.
- An assertion has at most 64 atoms. Each distinct condition counts once,
  and each use of `possibly` adds one, so
  `always (possibly ready and possibly recovered)` uses four.

**Limitations.**
- Formulas are checked by the default (strict) liveness checker only, not
  with `liveness: eventual`, simulation or `--experimental_no_graph`.
- Only one `return`, at the end (see below).
- Temporal operators and `implies` can't be stored in locals.
- `for` clauses can't iterate over symmetric domains yet.
- There is no release operator (LTL R). `P R Q` is `Q unless (P and Q)`.
- Reference examples: `09-14` (passing) and `09-15` (a violation);
  for `possibly`, `09-16` (passing) and `09-17` (a violation); for
  `unless`, `09-18`; for a property that starts from a condition, `09-20`;
  for `for` clauses, `09-21`.

## Incremental Liveness Checking (experimental)

By default, liveness assertions and formulas are checked once the whole
state space is explored. With `--experimental_incremental_liveness`, the
checker also checks the part explored so far each time the explored node
count doubles, and stops at the first violation:

```bash
./fizz --experimental_incremental_liveness spec.fizz
```

- It never changes a verdict. A violation found early is a real one, and a
  run with no violation still ends with the usual full check. Only *when* a
  failure is reported changes.
- It helps most on large models where the bad run sits close to `Init`.
- Formulas with `possibly` are checked at the end only.
- It needs the default BFS exploration and strict liveness. It is refused
  with simulation, an explicit `--experimental_processed_queue` and
  `--experimental_no_graph`, and has no effect with `liveness: eventual`.
  It turns off the default processed queue.
- Reference example: `09-19` (the flag is in its `flags.txt`).

## Examples

### Always Assertion (Safety Property) {#always-assertion}

Safety invariants that must hold in every state

**Demonstrates:** always assertion, safety properties

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-01-always-assertion)

### Exists Assertion {#exists-assertion}

Existential properties - at least one state must satisfy

**Demonstrates:** exists assertion

```fizz
# 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
```
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: 11
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-02-exists-assertion)

### Transition Assertion {#transition-assertion}

Properties about state transitions

**Demonstrates:** transition assertion with before/after states

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-03-transition-assertion)

### Eventually Always (Liveness) {#eventually-always}

Eventually the system reaches a stable state

**Demonstrates:** eventually always assertion (liveness property)

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-04-eventually-always)

### Always Eventually (Progress) {#always-eventually}

System always makes progress eventually

**Demonstrates:** always eventually assertion (strong fairness)

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-05-always-eventually)

### One-Step Reachability with next_states() {#next-states-restorable}

Assert that every trashed item can be restored in one step using next_states()

**Demonstrates:** next_states(), one-step reachability, always assertion

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-06-next-states-restorable)

### Detecting Unrestorable States with next_states() {#next-states-violation}

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

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
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]}
------
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-07-next-states-violation)

### next_states() Ignores the Concurrency Cap {#next-states-concurrency-cap}

The next_states() probe sees enabled transitions even when max_concurrent_actions is exhausted

**Demonstrates:** next_states(), max_concurrent_actions, serial actions

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-08-next-states-concurrency-cap)

### Matching next_states() Transitions to Roles {#next-states-role-id}

Use role_id and action_name to match next_states() transitions to a specific role instance

**Demonstrates:** next_states(), role_id, symmetric roles

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-09-next-states-role-id)

### Exists Assertion in No-Graph Mode (Unsatisfiable) {#exists-no-graph-unreachable}

An unsatisfiable exists assertion must fail under --experimental_no_graph, matching full-graph mode

**Demonstrates:** exists assertion, --experimental_no_graph

> Needs command-line flags (`--experimental_no_graph`); run locally with `fizz`.

```python
# Example 0100: Exists Assertion in No-Graph Mode (Unsatisfiable)
# An unsatisfiable exists assertion must fail under --experimental_no_graph, matching full-graph mode
# Demonstrates: exists assertion, --experimental_no_graph

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

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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-10-exists-no-graph-unreachable)

### Exists Assertion in No-Graph Mode (Satisfiable) {#exists-no-graph-reachable}

A satisfiable exists assertion passes under --experimental_no_graph by detecting a witness

**Demonstrates:** exists assertion, --experimental_no_graph, witness detection

> Needs command-line flags (`--experimental_no_graph`); run locally with `fizz`.

```python
# Example 0101: Exists Assertion in No-Graph Mode (Satisfiable)
# A satisfiable exists assertion passes under --experimental_no_graph by detecting a witness
# Demonstrates: exists assertion, --experimental_no_graph, witness detection

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

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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-11-exists-no-graph-reachable)

### Exists Coverage Warning in Simulation Mode {#exists-simulation-warning}

In simulation mode an unwitnessed exists assertion produces a warning instead of a failure

**Demonstrates:** exists assertion, simulation mode, coverage warning

> Needs command-line flags (`-x --seed 42`); run locally with `fizz`.

```python
# Example 0102: Exists Coverage Warning in Simulation Mode
# In simulation mode an unwitnessed exists assertion produces a warning instead of a failure
# Demonstrates: exists assertion, simulation mode, coverage warning

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

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

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-12-exists-simulation-warning)

### Func Calls in Assertions {#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

```fizz
# 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()
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 9, queued: 0
Valid Nodes: 9 Unique states: 9
Checking eventually always AllDone
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-13-func-calls-in-assertions)

### Temporal Formulas {#example-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

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 58, queued: 0
Valid Nodes: 58 Unique states: 26
Checking formula NoRequestsBeforeStart
Checking formula Answered[0]
Checking formula Answered[1]
Checking formula StaysStarted
Checking always eventually EventuallyIdle
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-14-temporal-formulas)

### Temporal Formula Violation {#temporal-formula-violation}

A temporal formula that fails, with a counterexample run that violates it

**Demonstrates:** temporal formulas, assertion failure, counterexample

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 58, queued: 0
Valid Nodes: 58 Unique states: 26
Checking formula NoRequestsBeforeStart
Checking formula Answered[0]
IsLive: false
FAILED: Liveness check failed
Invariant: Answered[0]
------
Init
--
state: {"answered":[0,0],"pending":[false,false],"started":false}
------
Start
--
state: {"answered":[0,0],"pending":[false,false],"started":true}
------
Request
--
state: {"answered":[0,0],"pending":[false,false],"started":true}
------
Any:c=0
--
state: {"answered":[0,0],"pending":[true,false],"started":true}
------
stutter
--
state: {"answered":[0,0],"pending":[true,false],"started":true}
------
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-15-temporal-formula-violation)

### Possibility {#possibly}

possibly P: some path from this state reaches a state where P holds

**Demonstrates:** possibly, can happen versus will happen, nested possibly, exists eventually

```fizz
# 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"
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 8, queued: 0
Valid Nodes: 8 Unique states: 8
Checking formula CanCancel
Checking formula CanUpgrade
Checking formula CanBookThenFly
Checking formula FlyingIsFinal
Checking formula EventuallyDone
Checking formula CanFly
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-16-possibly)

### Possibility Violation {#possibly-violation}

A possibly property that fails: from some state, no path reaches the condition

**Demonstrates:** possibly, recoverability, counterexample note

```fizz
# 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"
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
Checking formula Restorable
Checking formula Recoverable
IsLive: false
FAILED: Liveness check failed
Invariant: Recoverable
Note: the possibly at line 37, column 19 is false in the state after Purge (step 2; Init is step 0): no path from there, without a crash, reaches its condition
------
Init
--
state: {"status":"active"}
------
Delete
--
state: {"status":"trash"}
------
Purge
--
state: {"status":"purged"}
------
stutter
--
state: {"status":"purged"}
------
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-17-possibly-violation)

### Weak Until {#weak-until}

P unless Q: P holds until Q happens, or forever if Q never happens

**Demonstrates:** unless, unless versus until, unless under always

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 7, queued: 0
Valid Nodes: 7 Unique states: 7
Checking formula HeldUntilReturned
Checking formula NotReturnedBeforeTaken
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-18-weak-until)

### Incremental liveness checking {#incremental-liveness}

Find a liveness violation without exploring every state first

**Demonstrates:** --experimental_incremental_liveness (see flags.txt)

> Needs command-line flags (`--experimental_incremental_liveness`); run locally with `fizz`.

```python
# Example 0121: Incremental liveness checking
# Find a liveness violation without exploring every state first
# Demonstrates: --experimental_incremental_liveness (see flags.txt)

---
deadlock_detection: false
options:
  max_actions: 200
---
# A producer may send up to 60 messages and a consumer acknowledges them.
# The consumer is weakly fair, so every message sent is acknowledged. The
# producer isn't fair, so nothing makes it send them all: a run may only
# ever exchange heartbeats. AllSent is false on that run.
#
# Normally liveness is checked once the whole state space is explored.
# With --experimental_incremental_liveness the checker also checks the part
# explored so far, each time the node count doubles, and stops at the
# first violation. Here the run of heartbeats sits next to Init, so the
# first partial check finds it, long before all 3,782 states are
# explored. A run with no violation still ends with the full check, so the
# option never changes a verdict, only when a failure is reported.

action Init:
    sent = 0
    acked = 0
    beat = False

atomic action Send:
    require sent < 60
    sent += 1

atomic fair action Ack:
    require acked < sent
    acked += 1

atomic fair action Heartbeat:
    beat = not beat

always eventually assertion AllAcked:
    return acked == sent

always eventually assertion AllSent:
    return sent == 60
```

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

```
StateSpaceOptions: options:{max_actions:200 max_concurrent_actions:2} deadlock_detection:false
Checking liveness on 953 closed nodes of 1000
FAILED: Liveness check failed
Invariant: AllSent
------
Init
--
state: {"acked":0,"beat":false,"sent":0}
------
Heartbeat
--
state: {"acked":0,"beat":true,"sent":0}
------
Heartbeat
--
state: {"acked":0,"beat":false,"sent":0}
------
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-19-incremental-liveness)

### Scoped Absence Violation {#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

```fizz
# 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)
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 7, queued: 0
Valid Nodes: 7 Unique states: 6
Checking formula BasicNeverRefunded
IsLive: false
FAILED: Liveness check failed
Invariant: BasicNeverRefunded
------
Init
--
state: {}
------
Any:cabin="basic"
--
state: {"cabin":"basic","refunded":false,"status":"booked"}
------
Upgrade
--
state: {"cabin":"premium","refunded":false,"status":"booked"}
------
Cancel
--
state: {"cabin":"premium","refunded":true,"status":"cancelled"}
------
stutter
--
state: {"cabin":"premium","refunded":true,"status":"cancelled"}
------
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-20-scoped-absence-violation)

### Assertion For Clauses {#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

```fizz
# 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])
```
Run it in the FizzBee playground: https://fizzbee.io/play


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

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 80, queued: 0
Valid Nodes: 76 Unique states: 25
Checking always eventually Copied[a, 1]
Checking always eventually Copied[a, 2]
Checking always eventually Copied[b, 1]
Checking always eventually Copied[b, 2]
Checking formula StaysCopied[a, 1]
Checking formula StaysCopied[b, 2]
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/09-21-assertion-for-clauses)


## Patterns that use this

- [Mutex Pattern](/design/patterns/mutex/)
- [Read-Write Lock Pattern](/design/patterns/read-write-lock/)
- [Distributed Lock Pattern](/design/patterns/distributed-lock/)
- [Optimistic Locking Pattern](/design/patterns/optimistic-locking/)
- [Saga Pattern](/design/patterns/saga-pattern/)
- [Snapshot Isolation Pattern](/design/patterns/snapshot-isolation/)
- [Leader Election (Simplified Raft)](/design/patterns/leader-election/)
- [Compare-And-Swap Pattern](/design/patterns/compare-and-swap/)
- [Producer-Consumer Pattern](/design/patterns/producer-consumer/)
- [Message Queue Pattern](/design/patterns/message-queue/)
- [Cache Coherence Pattern](/design/patterns/cache-coherence/)
- [Eventual Consistency Pattern](/design/patterns/eventual-consistency/)
- [Idempotent Operations Pattern](/design/patterns/idempotent-operations/)
- [Circuit Breaker Pattern](/design/patterns/circuit-breaker/)
- [Rate Limiting Pattern](/design/patterns/rate-limiting/)
- [Write-Ahead Log Pattern](/design/patterns/write-ahead-log/)
- [Event Sourcing Pattern](/design/patterns/event-sourcing/)