# A PropEr finite state machine tutorial

By Eirini Arvaniti and Kostis Sagonas

In this tutorial we will use PropEr to test a finite state machine specification. The testcases produced using the PropEr fsm library (`proper_fsm`) are of exactly the same form as the testcases produced using the PropEr statem library (`proper_statem`). The difference lies in the way the callback modules are specified. Before reading this tutorial, please make sure you have understood the basic concepts of testing stateful systems with PropEr, as described here and here.

PropEr fsm offers a convenient way to test systems exhibiting a finite state machine behaviour. That is, systems that can be modeled as a finite collection of named states and transitions between them. A typical finite state machine representation of a system is the state diagram. PropEr fsm is designed to bring the callback module specification very close to a state diagram.

## A finite state machine example

Consider the following state diagram that describes the life of a strange creature that feeds on cheese, grapes and lettuce but never eats the same kind of food on two consecutive days.

As we can see from the state diagram, days are categorized into `cheese_days`, `lettuce_days` and `grapes_days`. On a `cheese_day` the creature eats only cheese, on a `lettuce_day` only lettuce and so on. When it gets hungry, it consumes a fixed portion of the daily food, which is kept in the food storage. To make life less boring and, more importantly, to bring food to the storage, the creature goes shopping from time to time. Finally, every night it decides what to eat the next day. There is only one rule regarding this decision: “never eat the same food for two days in a row”.

Being a huge fan of Erlang, this creature has implemented a finite state machine describing its daily routine using the OTP `gen_fsm` behaviour. The internal state of the finite state machine is a record that represents the food storage. The record fields contain the quantity of food that is currently stored.

Let us now describe the API of the finite state machine:

• We can start the finite state machine by specifying the kind of day on which it will be started.
• We can simulate the condition when the creature is hungry. The function `hungry/0` will return us the quantity of available food at the moment when the creature is ready to start eating.
• We can simulate the situation when the creature goes shopping to buy some new food.

Note that we will add more clauses to these functions (see below) hence the semicolons at the end of these clauses.

• Last but not least, we can simulate the beginning of a new day by specifying the creature’s food for that day.

### The property to test

Properties for testing finite state machine specifications are very similar to those we have seen in the PropEr statem tutorials. The difference is that the functions `commands/1` and `run_commands/2` are now imported from `proper_fsm` module. These functions behave similarly to their `proper_statem` counterparts, only now commands are generated and executed according to a finite state machine specification.

As a first example, we would like to test that the creature never runs out of food in the storage.

## Defining the PropEr finite state machine

### State representation

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

Splitting the model state into state name and state data makes the states of the fsm more explicit and allows the specification to be closer to a state diagram of the system under test. The `proper_statem:command/1` generator is replaced by a collection of callback functions, one for each reachable state of the fsm. Each callback function is named after the state it represents and takes the state data as argument.

The state is initialized via the `initial_state/0` and `initial_state_data/0` callbacks. The former specifies the initial state of the finite state machine, while the latter specifies what the state data should initially contain. Let us start on a `cheese_day` with the default portions of each kind of food available in the storage, since the initial state of our model should coincide with the initial state of the system under test.

### Specifying transitions

In our specification, we will define a separate callback function for each state in the state diagram (i.e. `cheese_day/1`, `lettuce_day/1`, `grapes_day/1`). Each of these callbacks should specify a list of possible transitions from that state. A transition is a pair consisting of the target state and the symbolic call that triggers the transition. The atom `history` can be used as target state to denote that a transition does not change the current state of the fsm.

As we mentioned before, the state callbacks take as argument the state data. In our case, the state data is a record containing the quantity of cheese, lettuce and grapes in the food storage.

A `store_transition` is triggered every time the creature buys some food, whereas an `eat_transition` is triggered every time it is hungry. Both of these transitions do not change the current state of the fsm and this is specified by having `history` as the target state.

We also need to define the generators `food()` and `quantity()`. A possible definition of them is given below:

Note that we could have defined `quantity()` more simply as `range(1,4)`. Actually, this would have been a better choice here but, just so as to show how to deal with some possible error situations, let us stick to this definition for the rest of this tutorial.

At command generation time, the callback function corresponding to the current state of the finite state machine will be called to return the list of possible transitions from that state. Then, PropEr will randomly choose a transition and, according to that, generate the next symbolic call to be included in the command sequence. By default transitions are chosen with equal probability, but this behaviour can be fine-tuned, as we will see later.

### The other callback functions

Preconditions and postconditions are also imposed on the finite state machine specification. Only now these callbacks take a slightly different form. Instead of the State argument that was provided in `proper_statem` callbacks, the callbacks in `proper_fsm` take into account the origin of a transition (From state), the target of a transition (Target state) and the state data.

Initially, let’s not have any preconditions.

However, postconditions are needed.

The set of callback functions corresponding to the states of the fsm update part of the model state, since they specify the target state of a transition. In order to update the state data, we have to define a separate callback function.

## PropEr in action

Let us run the first test on our property. It states that the creature never runs out of food in the storage.

Well, we didn’t see that coming! It seems that some part of our specification is not proper enough.

PropEr allows more than one transitions to be triggered by the same symbolic call and lead to different target states. As in this case:

However, the precondition callback may return true for at most one of these target states. Otherwise, PropEr will not be able to detect which transition was chosen and an exception will be raised. In our case, we have to specify the following preconditions to associate each possible argument of `new_day/1` with the correct target state.

We run the test one more time:

Ooops! Now we have triggered another kind of error. This error suggests that a `?SUCHTHAT` constraint could not be satisfied with the default value of ‘constraint_tries’. At this point there are two options. We can either increase the `constraint_tries` limit to e.g. 100 tries by running

or we can modify the generator that is responsible for this error. We choose to take the second option so as to eliminate the error permanently. A `?SUCHTHAT` constraint occurs in the `quantity/0` generator. It was introduced to control the quantity of food that can be bought in one transaction. The modified generator may return any positive integer after 50 failing attempts to produce a positive integer less than five.

And again we run the test:

Finally some results! It seems that there is always some food in the storage. But… wait a minute! We cannot be sure of what was tested unless we have a look at the testcase distribution.

The property is now instrumented to collect statistics about how often each transition was tested. Let’s try it:

It seems that the creature doesn’t get hungry very often in our tests. Thus, our previous conclusion about everlasting food supplies cannot be really trusted. We can instruct PropEr to choose `hungry/0` calls more often by assigning weights to transitions. The optional callback `weight/3` serves exactly this purpose.

`weight(From, Target, Call)` assigns an integer weight to transitions from `From` state to `Target` state triggered by `Call`. Each transition is now chosen with probability proportional to the weight assigned.

Running the test with weighted transitions:

As we can see now, in case of non-stop eating the creature eventually runs out of food. What is more, the content of the `State` variable reveals that the quantity of available food starts getting negative values. We will correct the code to prevent this from happening.

Let us now assume that the creature is wise enough to take care of buying food before it gets hungry. This can be modeled by adding the following precondition.

At this point, we would like to mention another, less obvious cause of `cant_generate` errors: difficult-to-satisfy preconditions. After failing `constraint_tries` times to generate a symbolic call with a true precondition, PropEr will report a `cant_generate` error. In our specification, this is not the case. Nevertheless, we can instruct PropEr to choose an `eat_transition` only when there is food available.

The property now successfully passes 1000 tests.

You can get the complete final code of this tutorial by clicking on the following link: food_fsm.erl.