Advanced tutorial for targeted property-based testingBy Andreas Löscher and Kostis Sagonas
This task is about writing a neighborhood function, a component needed for the search strategy simulated annealing. The neighborhood function is critical for the performance of simulated annealing.
Let’s say we want to design a role-play game (RPG) where our character has some attributes like strength and intelligence (see Wikipedia) that effect how good actions are performed. A strong character will typically be better at fighting and an intelligent character will be better at using magic. Furthermore we want our RPG to have a spell-based system that allows us to customize these these attributes. The player can cast a spell that will reduce some of these attributes to increase others.
The stats can be implemented as a record:
Spells are represented with the same record and the record fields specifies how much an attribute goes up or down when the spell is cast.
Our spell attribute API contains only one function
that calculates the resulting attributes if a list of spells is cast. It can
happen that a spell in the list cannot be casts because the character does not
have the required attributes left. In such a case the spell does not have any
Now we only need some spells:
With the spells in place, how can we make sure, that a player cannot exploit our spell system and get lets say an twice the amount of attributes? We can specify a property to test for this type of exploit as follows:
We define some initial attributes and then cast a random list of spells.
Then we calculate the total number of attributes with
and check if the spells somehow managed to double them compared to the initial
attributes. The generator
list_of_spells() looks like this:
Note that we don’t want PropEr to shrink the values inside the spell records.
We can prevent that by wrapping the generator with
If we test this property now with PropEr, we will see that the property holds for all randomly generated inputs even if the number of tests is very high:
Unfortunately there is are list of spells but PropEr is unable to find it by
list_of_spells() generator. To find them we want to use PropEr’s
targeted PBT extension.
We can change
prop_spells() to make use of the search strategy as follows:
We added the following elements:
FORALL_SAspecifies simulated annealing as search strategy
?TARGETtells the strategy that it should generate input according to
?MAXIMIZEspecifies the search goal. In this case we want to maximize the attributes our character has after casting the spells.
Now we just need to tell simulated annealing how to generate the first element and which neighborhood function it should use:
We can use the random generator
list_of_spells() for the first element.
The task is to implement
list_of_spells_next() so that it returns a
neighborhood function. When writing the function you can make full use of
PropEr’s language for defining custom generators:
The first element of the neighborhood function is the base input. The
neighborhood function should generate a new instance of the input that is
similar to this base input (in the neighborhood of). The second parameter is the
temperature. This is a
float() parameter that typically decreases during
(see Simulated Annealing).
It is possible to use the temperature to scale the size of the neighborhood in which the neighborhood function generates new input:
- If the neighborhood is very large the input space can be traversed fast (global search), but the search might degrade to random testing. With a large neighborhood it can also take many steps to narrow down to a good input that is otherwise close in the input space of an already accepted input (local search).
- If the neighborhood is very small, the search can usually narrow down fast input that is close. However, it might require many steps to reach other parts of the input space or to escape a local optima.
The temperature makes it possible to reduce the size of the neighborhood during the search, transitioning from global search to local search. This can sometimes be useful. In many cases it is sufficient to keep the neighborhood size constant.
- All of the input space must be reachable by consecutive calls of
list_of_spells_next(). This means that lists should be able to grow and shrink in size.
- Use the temperature argument only if necessary.
- Even with targeted PBT the amount of tests needed can be in the few thousands but a counterexample should be found in under
10000tests depending on your neighborhood function.