# `ExTLA.Invariant.Test`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/invariant/test.ex#L1)

ExUnit helpers for testing Layer 1 declarations in isolation.

    defmodule AccountTest do
      use ExUnit.Case
      use ExTLA.Invariant.Test

      test "a withdrawal keeps the account whole" do
        old = %{balance: 100, deposits: 0}
        new = %{balance: 50, deposits: 0}

        assert_invariants(Account, new)
        assert_action_properties(Account, old, new)
      end

      test "and the invariant can actually fail" do
        refute_invariant(Account, :never_negative, %{balance: -1, deposits: 0})
      end
    end

These check a *state*, not a running process. That is the point: a state a process can
only reach through a sequence of calls is a value here, so the negative cases — the ones
that prove a declaration is not vacuously true — can be written down directly.

## Why `refute_invariant/3` earns its place

An invariant no test has ever seen return `false` is indistinguishable from `true`, and
a `true` invariant is checked on every transition forever while proving nothing. It is
the same vacuity `mix extla.check` reports at Layer 2 (see "Reading the coverage report"
in `guides/reference.md`), one layer down, and it is not detectable from the passing side.

## A module compiled `:disabled` cannot be asserted about

Under `mode: :disabled` the `@before_compile` hook emits no predicates — that is what
makes the mode free. Every helper here says so by name rather than failing as though the
declaration were false.

# `__using__`
*macro* 

Imports the helpers. `use ExUnit.Case` first.

# `assert_action_properties`
*macro* 

Assert that the transition from `old_state` to `new_state` satisfies every action
property of `module`. Names every one that failed.

# `assert_invariants`
*macro* 

Assert that `state` satisfies every invariant of `module`.

Names *every* invariant that failed, not the first: a state that breaks three of them is
three separate facts about the state, and reporting one hides the other two behind
another test run.

# `refute_invariant`
*macro* 

Assert that `state` VIOLATES the named invariant of `module`.

Fails when the invariant holds, and fails differently when `module` declares no
invariant by that name — a renamed declaration would otherwise turn this test green by
making it check nothing.

# `valid_states`

A generator of states satisfying `module`'s named type invariant.

`base_generator` produces candidate states and this keeps the ones the invariant
admits, so a property test over the result never has to state the type constraint a
second time — a restatement is a second place for it to drift.

Filtering rather than constructing is deliberate: the invariant is the only definition
of the type the module actually enforces, and a generator built to mirror it would be
a copy that can disagree with it.

## The base generator should already be close to the type

Each candidate the invariant rejects is redrawn, and 25 rejections in a row raise
`StreamData.FilterTooNarrowError`. So the cost of a broad `base_generator` is not a
slower test but a test that fails on some seeds and not others. Measured on a
three-colour type invariant, over 100-run properties:

| the invariant accepts | properties that raise |
|---|---|
| about half the candidates | none seen in 2,000 |
| about 30% | about 1 in 90 |
| about 15% | about 3 in 4 |

The middle row is the one to fear: it passes locally and goes red on a rare seed in
someone else's merge request. Aim for a base generator the invariant accepts at least
half the time. Get the *shape* right (the keys, the tags, the members of a closed set)
and leave the invariant to decide the conditions between fields:

    # good: the right colours and a right-shaped map; only the sign of cycles is filtered
    StreamData.tuple({
      StreamData.member_of([:red, :yellow, :green]),
      StreamData.map(StreamData.integer(), &%{cycles: &1})
    })

    # bad: almost every atom is the wrong colour, so nearly every candidate is rejected
    StreamData.tuple({
      StreamData.atom(:alphanumeric),
      StreamData.map(StreamData.integer(), &%{cycles: &1})
    })

---

*Consult [api-reference.md](api-reference.md) for complete listing*