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
endThese 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.
Summary
Functions
Imports the helpers. use ExUnit.Case first.
Assert that the transition from old_state to new_state satisfies every action
property of module. Names every one that failed.
Assert that state satisfies every invariant of module.
Assert that state VIOLATES the named invariant of module.
A generator of states satisfying module's named type invariant.
Functions
Imports the helpers. use ExUnit.Case first.
Assert that the transition from old_state to new_state satisfies every action
property of module. Names every one that failed.
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.
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.
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})
})