# Module proper_fsm

- Description
- Data Types
- Function Index
- Function Details

This module defines the `proper_fsm` behaviour, useful for testing systems that can be modeled as finite state machines.

Copyright © 2010-2016 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas

Version: Jan 2 2021 16:13:05

Authors: Eirini Arvaniti.

## Description

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. `proper_fsm` is closely related to `proper_statem` and is, in fact, implemented in terms of that. Testcases generated using `proper_fsm` will be on precisely the same form as testcases generated using `proper_statem`. The difference lies in the way the callback modules are specified. The relation between `proper_statem` and `proper_fsm` is similar to the one between `gen_server` and `gen_fsm` in OTP libraries.

Due to name conflicts with functions automatically imported from `proper_statem`, a fully qualified call is needed in order to use the API functions of `proper_fsm`.

#### The states of the finite state machine

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

`StateName` 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 `StateName` for each floor could be `{floor,K}, 1 <= K <= N`.
`StateData` can be an arbitrary term, but is usually a record.

#### Transitions between states

A transition (`transition()`) is represented as a tuple `{TargetState, {call,M,F,A}}`. This means that performing the specified symbolic call at the current state of the fsm will lead to `TargetState`. The atom `history` can be used as `TargetState` 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:

- `initial_state() ->` `state_name()`

  Specifies the initial state of the finite state machine. As with `proper_statem:initial_state/0`, its result should be deterministic.

- `initial_state_data() ::` `state_data()`

  Specifies what the state data should initially contain. Its result should be deterministic

- `StateName(S::``state_data()``) ::` `[``transition()``]`

  There should be one instance of this function for each reachable state `StateName` of the finite state machine. In case `StateName` is a tuple the function takes a different form, described just below. The function returns a list of possible transitions (`transition()`) 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 `StateData` 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 `StateData`.

- `StateName(Attr1::term(), ..., AttrN::term(), S::``state_data()``) ::` `[``transition()``]`

  There should be one instance of this function for each reachable state `{StateName,Attr1,...,AttrN}` of the finite state machine. The function has similar beaviour to `StateName/1`, described above.

- `weight(From::``state_name()``, Target::``state_name()``, Call::``symbolic_call()``) -> integer()`

  This is an optional callback. When it is not defined (or not exported), transitions are chosen with equal probability. When it is defined, it assigns an integer weight to transitions from `From` to `Target` triggered by symbolic call `Call`. In this case, each transition is chosen with probability proportional to the weight assigned.

- `precondition(From::``state_name()``, Target::``state_name()``, StateData::``state_data()``, Call::``symbolic_call()``) -> boolean()`

  Similar to `proper_statem:precondition/2`. Specifies the precondition that should hold about `StateData` so that `Call` can be included in the command sequence. In case precondition doesn't hold, a new transition is chosen using the appropriate `StateName/1` generator. It is possible for more than one transitions to be triggered by the same symbolic call and lead to different target states. In this case, at most one of the target states may have a true precondition. Otherwise, PropEr will not be able to detect which transition was chosen and an exception will be raised.

- `postcondition(From::``state_name()``, Target::``state_name()``, StateData::``state_data()``, Call::``symbolic_call()``, Res::``cmd_result()``) -> boolean()`

  Similar to `proper_statem:postcondition/3`. Specifies the postcondition that should hold about the result `Res` of the evaluation of `Call`.

- `next_state_data(From::``state_name()``, Target::``state_name()``, StateData::``state_data()``, Res::``cmd_result()``, Call::``symbolic_call()``) ->` `state_data()`

  Similar to `proper_statem:next_state/3`. Specifies how the transition from `FromState` to `Target` triggered by `Call` affects the `StateData`. `Res` refers to the result of `Call` and can be either symbolic or dynamic.

#### The property used

This is an example of a property that can be used to test a finite state machine specification:

          prop_fsm() ->
              ?FORALL(Cmds, proper_fsm:commands(?MODULE),
                      begin
                          {_History, _State, Result} = proper_fsm:run_commands(?MODULE, Cmds),
                          cleanup(),
                          Result =:= ok
                      end).

## Data Types

### cmd_result()

abstract datatype: `cmd_result()`

### command()

    command() =
        {set, symbolic_var(), symbolic_call()} | {init, fsm_state()}

### command_list()

    command_list() = [command()]

### fsm_result()

    fsm_result() = proper_statem:statem_result()

### fsm_state()

    fsm_state() = {state_name(), state_data()}

### history()

    history() = [{fsm_state(), cmd_result()}]

### mod_name()

    mod_name() = atom()

### state_data()

abstract datatype: `state_data()`

### state_name()

    state_name() = atom() | tuple()

### symbolic_call()

    symbolic_call() = proper_statem:symbolic_call()

### symbolic_var()

    symbolic_var() = proper_statem:symbolic_var()

## Function Index

commands/1 | A special PropEr type which generates random command sequences, according to a finite state machine specification.
commands/2 | Similar to `commands/1`, but generated command sequences always start at a given state.
run_commands/2 | Evaluates a given symbolic command sequence `Cmds` according to the finite state machine specified in `Mod`.
run_commands/3 | Similar to `run_commands/2`, but also accepts an environment used for symbolic variable evaluation, exactly as described in `proper_statem:run_commands/3`.
state_names/1 | Extracts the names of the states from a given command execution history.

## Function Details

### commands/1

    commands(Mod :: mod_name()) -> proper_types:type()

A special PropEr type which generates random command sequences, according to a finite state machine specification. The function takes as input the name of a callback module, which contains the fsm specification. The initial state is computed by
`{Mod:initial_state/0, Mod:initial_state_data/0}`.

### commands/2

    commands(Mod :: mod_name(), InitialState :: fsm_state()) ->
                proper_types:type()

Similar to `commands/1`, but generated command sequences always start at a given state. In this case, the first command is always
`{init, InitialState = {Name,Data}}` and is used to correctly initialize the state every time the command sequence is run (i.e. during normal execution, while shrinking and when checking a counterexample).

### run_commands/2

    run_commands(Mod :: mod_name(), Cmds :: command_list()) ->
                    {history(), fsm_state(), fsm_result()}

Evaluates a given symbolic command sequence `Cmds` according to the finite state machine specified in `Mod`. The result is a triple of the form
`{History, FsmState, Result}`, similar to `proper_statem:run_commands/2`.

### run_commands/3

    run_commands(Mod :: mod_name(),
                 Cmds :: command_list(),
                 Env :: proper_symb:var_values()) ->
                    {history(), fsm_state(), fsm_result()}

Similar to `run_commands/2`, but also accepts an environment used for symbolic variable evaluation, exactly as described in `proper_statem:run_commands/3`.

### state_names/1

    state_names(History :: history()) -> [state_name()]

Extracts the names of the states from a given command execution history. It is useful in combination with functions such as `proper:aggregate/2` in order to collect statistics about state transitions during command execution.

Generated by EDoc