...

/

Writing Stateful Properties

Writing Stateful Properties

Get started with stateful properties and their file structure and generators.

Getting started

We’ve seen that stateless properties all follow a pretty similar structure. The layout of code may vary from project to project, but overall, most test suites do share a separation between properties, generators, and helper functions. When it comes to stateful properties, there is far less of a standard. Some people put properties in one file, models in another one, with helper functions and wrappers around the actual system in a third module. Other developers prefer to have everything in one spot.

We’ll stick to keeping the properties and model in one file. With basic properties, we can make use of the rebar3 plugin’s templating facilities to get the file we need within any standard Elixir project. The command is:

rebar3 new proper_statem base

File structure

The generated file contains the prop_base module, a test suite that is divided into two sections:

  1. Section for the stateful property we’ll want to execute.
  2. Section for the model, which is a mix of callbacks and generators.

Properties

Let’s start by looking at the property.

Press + to interact
defmodule PbtTest do
use ExUnit.Case
use PropCheck
use PropCheck.StateM # <-- this is a new one to use
property "stateful property" do
forall cmds <- commands(__MODULE__) do #1
ActualSystem.start_link() #2
{history, state, result} = run_commands(__MODULE__, cmds) #3
ActualSystem.stop() #4
(result == :ok)
|> aggregate(command_names(cmds))
|> when_fail(
IO.puts("""
History: #{inspect(history)}
State: #{inspect(state)}
Result: #{inspect(result)}
""")
)
end
end

This looks similar to standard properties, but ...