Search⌘ K
AI Features
Home
Courses
Property-Based Testing with PropEr in Elixir

Writing FSM Properties

Explore how to write finite state machine (FSM) properties in PropEr for Elixir. Understand the structure of state machine tests, generators, and callbacks used to model state transitions. Learn to work with initial states, nested states, and weighting transitions to create robust, stateful property tests.

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:

C++
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 adaptation of ...