The finite state machine approach for stateful systems, which is closer to Erlangs gen_fsm model.

This module defines the proper_fsm behaviour, useful for testing systems that can be modeled as finite state machines. That is, a finite collection of named states and transitions between them. PropCheck.FSM is closely related to PropCheck.StateM and is, in fact, implemented in terms of that. Testcases generated using PropCheck.FSM will be on precisely the same form as testcases generated using PropCheck.StateM. The difference lies in the way the callback modules are specified. The relation between PropCheck.StateM and PropCheck.FSM is similar to the one between gen_server and gen_fsm in OTP libraries.

Due to name conflicts with functions automatically imported from PropCheck.StateM, a fully qualified call is needed in order to use the API functions of PropCheck.FSM.

The states of the finite state machine

Following the convention used in gen_fsm behaviour, the state is separated into types t:state_name/0 and some t:state_data/0. state_name is used to denote a state of the finite state machine and state_data is any relevant information that has to be stored in the model state. States are fully represented as tuples {state_name, state_data}.

state_name is usually an atom (i.e. the name of the state), but can also be a tuple. In the latter case, the first element of the tuple must be an atom specifying the name of the state, whereas the rest of the elements can be arbitrary terms specifying state attributes. For example, when implementing the fsm of an elevator which can reach n different floors, the state_name for each floor could be {:floor, k}, 1 <= k <= n.
state_data can be an arbitrary term, but is usually a record.

Transitions between states

A transition t:transition/0 is represented as a tuple {target_state, {:call, m, f, a}}. This means that performing the specified symbolic call at the current state of the fsm will lead to target_state. The atom :history can be used as target_state to denote that a transition does not change the current state of the fsm.

The callback functions

The following functions must be exported from the callback module implementing the finite state machine:

• c:initial_state/0
• c:initial_data/0
• c:precondition/4
• c:postcondition/5
• c:next_state_data/5
• c:weight/3

In addition to these functions, we also need functions for each state:

• state_name(s::state_data) ::[transition]
  There should be one instance of this function for each reachable state state_name of the finite state machine. In case state_name is a tuple the function takes a different form, described just below. The function returns a list of possible transitions (t:transition/0 ) from the current state.

  At command generation time, the instance of this function with the same name as the current state’s name is called to return the list of possible transitions. Then, PropEr will randomly choose a transition and, according to that, generate the next symbolic call to be included in the command sequence. However, before the call is actually included, a precondition that might impose constraints on state_data is checked.

  Note also that PropEr detects transitions that would raise an exception of class <error> at generation time (not earlier) and does not choose them. This feature can be used to include conditional transitions that depend on the t:state_data/0.

• state_name(attr1::any, ..., attrN::any, s::type state_data) :: [transition]
  There should be one instance of this function for each reachable state {state_name, attr1, ..., attrN} of the finite state machine. The function has similar beaviour to state_name/1, described above.

The property used

This is an example of a property that can be used to test a finite state machine specification. It expects a cleanup function that takes care of removing all artifacts created during tests to enable a clean start for each test case execution.

property "fsm" do
   forall cmds <- commands(__MODULE__) do
     {_history, _state, result} = run_commands(__MODULE__, cmds)
     cleanup()
     result == :ok
  end
end