Property-Based Testing with PropEr in Elixir/

...

/

Writing FSM Properties

Writing FSM Properties

Get started with FSM properties and take a look at the structure of the properties, the states, and the callbacks.

We'll cover the following...

The property structure

The standard test suite is used, and the created test suite will have two parts:

  1. The state machine property.
  2. The model, which is a mix of callbacks and generators.

Let’s take a look at what the test suite would look like:

Press + to interact
defmodule FSMTest do 
  use ExUnit.Case 
  use PropCheck
  use PropCheck.FSM
  property "FSM property", [:verbose] do 
    forall cmds <- commands(__MODULE__) do #(1)
      ActualSystem.start_link()
      {history, state, result} = run_commands(__MODULE__, cmds) #(2)
      ActualSystem.stop() 
      (result == :ok) 
      |> aggregate( 
        :proper_statem.zip(state_names(history), command_names(cmds)) #(3)
      )
      |> when_fail(
        IO.puts("""
        History: #{inspect(history)} 
        State: #{inspect(state)} 
        Result: #{inspect(result)} 
        """)
      )
  end 
end

At line 7 and line 9, special variations of stateful properties’ command generators and runners are used. The rest of the property is mostly similar, aside from line 14, where a special zip/2 function along with state_names generates readable output in case of a test failure. The rest works as usual.

Note: zip is a specialized ...