This module defines the :proper_statem behaviour, useful for testing stateful reactive systems whose internal state and side-effects are specified via an abstract state machine. Given a callback module implementing the :proper_statem behaviour (i.e. defining an abstract state machine of the system under test), PropEr can generate random symbolic sequences of calls to that system.

As a next step, generated symbolic calls are actually performed, while monitoring the system’s responses to ensure it behaves as expected. Upon failure, the shrinking mechanism attempts to find a minimal sequence of calls provoking the same error.

The role of commands

Testcases generated for testing a stateful system are lists of symbolic API calls to that system. Symbolic representation has several benefits, which are listed here in increasing order of importance:

• Generated testcases are easier to read and understand.
• Failing testcases are easier to shrink.
• The generation phase is side-effect free and this results in repeatable testcases, which is essential for correct shrinking.

Since the actual results of symbolic calls are not known at generation time, we use symbolic variables of type t:symb_var/0 to refer to them. A command of type t:command/0 is a symbolic term, used to bind a symbolic variable to the result of a symbolic call. For example:

[{:set, {:var, 1}, {:call, :erlang, :put, [:a, 42]}},
{:set, {:var, 2}, {:call, :erlang, :erase, [:a]}},
{:set, {:var, 3}, {:call, :erlang, :put, [:b, {:var, 2}]}}]

is a command sequence that could be used to test the process dictionary. In this example, the first call stores the pair {:a, 42} in the process dictionary, while the second one deletes it. Then, a new pair {:b, {:var, 2}} is stored. {:var, 2} is a symbolic variable bound to the result of :erlang.erase/1. This result is not known at generation time, since none of these operations is performed at that time. After evaluating the command sequence at runtime, the process dictionary will eventually contain the pair {:b, 42}.

The abstract model-state

In order to be able to test impure code, we need a way to track its internal state (at least the useful part of it). To this end, we use an abstract state machine representing the possible configurations of the system under test. When referring to the model state, we mean the state of the abstract state machine. The model state can be either symbolic or dynamic:

• During command generation, we use symbolic variables to bind the results of symbolic calls. Therefore, the model state might (and usually does) contain symbolic variables and/or symbolic calls, which are necessary to operate on symbolic variables. Thus, we refer to it as symbolic state. For example, assuming that the internal state of the process dictionary is modeled as a proplist, the model state after generating the previous command sequence will be [b: {:var, 2}}].
• During runtime, symbolic calls are evaluated and symbolic variables are replaced by their corresponding real values. Now we refer to the state as dynamic state. After running the previous command sequence, the model state will be [b: 42].

The callback functions

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

• c:initial_state/0
• c:command/1
• c:precondition/2
• c:postcondition/3
• c:next_state/3

The property used

Each test consists of two phases:

• As a first step, PropEr generates random symbolic command sequences deriving information from the callback module implementing the abstract state machine. This is the role of commands/1 generator.
• As a second step, command sequences are executed so as to check that the system behaves as expected. This is the role of run_commands/2, a function that evaluates a symbolic command sequence according to an abstract state machine specification.

These two phases are encapsulated in the following property, which can be used for testing the process dictionary:

def prop_pdict() do
  forall cmds <- commands(__MODULE__) do
    {_history, _state, result} = run_commands(__MODULE__, cmds)
    cleanup()
    result == ok
  end
end

When testing impure code, it is very important to keep each test self-contained. For this reason, almost every property for testing stateful systems contains some clean-up code. Such code is necessary to put the system in a known state, so that the next test can be executed independently from previous ones.

Parallel testing

After ensuring that a system’s behaviour can be described via an abstract state machine when commands are executed sequentially, it is possible to move to parallel testing. The same state machine can be used to generate command sequences that will be executed in parallel to test for race conditions. A parallel testcase (t:parallel_testcase/0 ) consists of a sequential and a parallel component. The sequential component is a command sequence that is run first to put the system in a random state. The parallel component is a list containing 2 command sequences to be executed in parallel, each of them in a separate newly-spawned process.

Generating parallel test cases involves the following actions. Initially, we generate a command sequence deriving information from the abstract state machine specification, as in the case of sequential statem testing. Then, we parallelize a random suffix (up to 12 commands) of the initial sequence by splitting it into 2 subsequences that will be executed concurrently. Limitations arise from the fact that each subsequence should be a valid command sequence (i.e. all commands should satisfy preconditions and use only symbolic variables bound to the results of preceding calls in the same sequence). Furthermore, we apply an additional check: we have to ensure that preconditions are satisfied in all possible interleavings of the concurrent tasks. Otherwise, an exception might be raised during parallel execution and lead to unexpected (and unwanted) test failure. In case these constraints cannot be satisfied for a specific test case, the test case will be executed sequentially. Then an f is printed on screen to inform the user. This usually means that preconditions need to become less strict for parallel testing to work.

After running a parallel testcase, PropEr uses the state machine specification to check if the results observed could have been produced by a possible serialization of the parallel component. If no such serialization is possible, then an atomicity violation has been detected. In this case, the shrinking mechanism attempts to produce a counterexample that is minimal in terms of concurrent operations. Properties for parallel testing are very similar to those used for sequential testing.

def prop_parallel_testing() do
   forall testcase <- parallel_commands(__MODULE__) do
      {_sequential, _parallel, result} = run_parallel_commands(__MODULE__, testcase),
      cleanup(),
      result == :ok
   end
end

Please note that the actual interleaving of commands of the parallel component depends on the Erlang scheduler, which is too deterministic. For PropEr to be able to detect race conditions, the code of the system under test should be instrumented with erlang:yield/0 calls to the scheduler.

Acknowldgements

Very much of the documentation is immediately taken from the proper API documentation.