Property-Based Testing with PropEr in Erlang/

...

/

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

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.

Press + to interact
-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
...