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

Writing FSM Properties

Explore how to create and structure finite state machine (FSM) properties in PropEr for Erlang projects. Understand the use of state transitions, command generators, and callbacks to model stateful systems. Learn to implement on, off, and nested states along with probabilistic weighting for transitions. Gain the skills to write preconditions, postconditions, and state update logic needed to validate complex FSM behavior through property-based testing.

We'll cover the following...

The property structure

As with stateful properties, we can make use of the rebar3 plugin’s templates to get a property suite within any standard Erlang project. The command to use for creating a new FSM property suite is:

rebar3 new proper_fsm name=fsm

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

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

Let’s start by taking a look at the property.

Erlang
-module(prop_fsm). 
-include_lib("proper/include/proper.hrl").
-export([initial_state/0, initial_state_data/0,
        on/1, off/1, service/3, % State generators
        weight/3, precondition/4, postcondition/5, next_state_data/5]).
prop_test() ->
    ?FORALL(Cmds, proper_fsm:commands(?MODULE), %(1)
        begin
            actual_system:start_link(),
            {History,State,Result} = proper_fsm:run_commands(?MODULE, Cmds), %(2)
            actual_system:stop(),
            ?WHENFAIL(io:format("History: ~p\nState: ~p\nResult: ~p\n",
                                [History,State,Result]), 
                        aggregate(zip(proper_fsm:state_names(History), %(3)
                                command_names(Cmds)), 
                            Result =:= ok))
        end).

This property has a lot of exports. Many of them are variations on those for stateful properties, and we’ll revisit them soon. Functions such as on/1, off/1, and service/3 are state-machine–specific and represent individual states:

  1. On
...