Notes on Erlang QuickCheck

A few days ago I had the chance to spend some time with John Hughes, one of the creators of the Erlang Quickcheck. We looked at some of our APIs and went through some of our QuickCheck models. It has been an incredibly helpful learning experience, so I thought to share some of the highlights from our discussions to a broader public.

The following notes are listed in a more or less random order and they assume that you are already familiar with QuickCheck (EQC) and QuickCheck abstract state machines.

Generating sublists

Given a list of items - say, atoms - you want to extract random sublists from the original list.

One way of doing this is to pair each element of the list with a boolean generator and to filter out false values:

sublist(L0) ->
  ?LET(L, [{E, eqc_gen:bool()} || E <- L0], [X || {X, true} <- L]).

Since the boolean generator shrinks towards the false value, your sublist shrinks towards the empty list, which is what you want in most cases. If you need to invert this behaviour and you want to shrink - or should I say grow - towards the entire list, you can simply toggle the true boolean and set it to false:

sublist(L0) ->
  ?LET(L, [{E, eqc_gen:bool()} || E <- L0], [X || {X, false} <- L]).

Use elements/1 or oneof/1?

In QuickCheck two similar functions are available: elements/1 and oneof/1. They look similar at a first glance, so you may wonder which one to use.

The main difference between the two functions stands in the input arguments. The elements/1 takes a list of terms as input and it generates an element from it, whilst oneof/1 takes a list of generators and it picks one of them.

The above is important for how the two functions shrink. elements/1 shrinks towards the first element of the list, whilst oneof/1 shrinks towards the failing one.

Verify your generators

Whenever you implement a new generator or even if you simply use a built-in one, you may want to verify that the generator works as you expect. You can use eqc_gen:sample/1 for the purpose.

> eqc_gen:sample(eqc_gen:list(eqc_gen:nat())).

This is also useful to verify the sequence of commands that your abstract state machine can generate:

> eqc_gen:sample(eqc_statem:commands(my_eqc)).
> eqc_gen:sample(eqc_statem:parallel_commands(my_eqc)).

Where my_eqc is the module where your eqc_statem is defined.

Think shrinking

The elements/1 generator shrinks towards the beginning of the list. Keep that in mind when implementing your QuickCheck abstract state machines. If you keep a list of elements - say, pids - in your model state and you plan to use elements/1 on them, ensure that whenever a new element is added to the state, it is always appended at the end of a list, even if you are a seasoned Erlang developer and it feels a bit unnatural to you. This will give you better shrinking in most cases.

### DO
add_next(S, Res, [Pid]) ->
  S#state{pids = S#state.pids ++ [Pid]}

### DON'T
add_next(S, Res, [Pid]) ->
  S#state{pids = [Pid | S#state.pids]}

Don’t bother about quadratic complexity here, since you will only run this code during tests and you will probably have only a few elements in your state at any given time.

Living in the Erlang shell

Sometimes the feedback loop for executing QuickCheck tests is long and/or the way properties are verified is inflexible. As an example, you may be wrapping your QuickCheck properties in EUnit suites to get code coverage information, or you may run QuickCheck via rebar.

When implementing a new property or debugging an abstract state machine, try to run QuickCheck from the Erlang shell as much as possible. Being able to run eqc:check/1 on your latest counterexample, to verify the list of generated commands using the sample/1 function (as explained above) and to re-run a property in seconds after a quick fix is a great win in the long term.

How long will my commands take?

In your QuickCheck abstract state machine, you could have operations which take long time, so you may want to set a timeout for the entire test suite. You don’t want to set the timeout too small, to avoid incurring into occasionaly failing test cases (due to the timeout being hit, in case long sequences of commands are generated). On the other hand, you don’t want to set the timeout too long, since you don’t want your tests to run forever. So, what’s a good value for a timeout?

Well, since the sequence of command is available in your property, you could calculate a timeout value from the sequence of commands itself. The following snippet should give you a better idea of what I mean here.

prop_bar() ->
   ?FORALL(Cmds, commands(),

my_timeout(Cmds) ->
  lists:sum([expected_time(Cmd) || Cmd <- Cmds]).

expected_time({call, ?MODULE, op1, _Args}) ->
expected_time({call, ?MODULE, op2, _Args}) ->

Non derministic test outcomes

In certain situations test outcomes are non-deterministic. In such cases, have a look to the ?SOMETIMES/2 macro. An extract from the QuickCheck documentation follows.


A property which tests Prop repeatedly N times, failing only if all of the
tests fail. In other words, the property passes if Prop sometimes passes.
This is used in situations where test outcomes are non-deterministic,
to search for test cases that consistently fail.
A property such as ?FORALL(X,...,?SOMETIMES(10,...)) will find test cases X for
which the property inside ?SOMETIMES is very likely to fail.

More compacted State Machines

The most recent versions of QuickCheck have a new format for defining an abstract state machine, which is more readable and concise and which requires much less boilerplate than before. You can find extensive documentation about the new statem format by looking at the documentation in the eqc_group_commands module. Not easy to find, which is why I’m mentioning it here.

Failing is good

Too often your QuickCheck tests pass and your properties are successful. In many occasions it’s useful to ensure that your tests are meaningful by testing properties that should not succeed. You can perform negative testing by wrapping a property using the eqc:fails/1 function.


Testing race conditions

In QuickCheck, going from sequential testing to parallel testing is a snap in most cases. As an example, the following property:

prop_registry() ->
  ?FORALL(Cmds, commands(?MODULE),
      {H, S, Res} = run_commands(?MODULE, Cmds),
      pretty_commands(?MODULE, Cmds, {H, S, Res},
                      Res == ok))

Would become:

prop_registry() ->
  ?FORALL(Cmds, parallel_commands(?MODULE),
      {H, S, Res} = run_parallel_commands(?MODULE, Cmds),
      pretty_commands(?MODULE, Cmds, {H, S, Res},
                      Res == ok))

You can use preconditions to ensure logical precedence between operations.

Running on multicore

If you are testing race conditions and you are using parallel_cmds as above, ensure you are running on a multicore system. Do not underestimate this requisite since, even if your machine has at least 4 or 8 cores, your application could be running in a VM or in a Jenkins slave with limited cores. In such a situation, in fact, the Erlang scheduler will try as hard as possible to prevent context switches between processes and your parallel tests may be less useful than you think.

About check/1 and check/2

It’s possible to test a property for a given case (usually the current counterexample) by using the check/1 and check/2 functions exported by the eqc module. An interesting application of the check functions is in a system where plenty of log information are produced by the system under test while running QuickCheck. By using the following pattern, it will be possible to replay a failing test case and to display only relevant logs.

case eqc:quickcheck(Property) of
        true -> true;
        _    -> io:format(user, "Repeating failing test~n", []),
                true = eqc:check(Prop)

As a plus, the check/2 function can be used without a QuickCheck licence, allowing anyone to run tests that a licenced user has generated.