Writing FSM Properties

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.