quickcheck-state-machine: Test monadic programs using state machine based models

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


See README at https://github.com/advancedtelematic/quickcheck-state-machine#readme

[Skip to ReadMe]


Versions0.0.0, 0.0.0, 0.1.0, 0.2.0, 0.3.0, 0.3.1, 0.4.0, 0.4.1, 0.4.2
Change logCHANGELOG.md
Dependenciesansi-wl-pprint (>= && <0.7), base (>=4.7 && <5), constraints (>=0.9.1 && <0.10), containers (>= && <0.6), mtl (>=2.2.1 && <2.3), parallel-io (>=0.3.3 && <0.4), QuickCheck (>=2.9.2 && <2.10), random (==1.1.*), singletons (==2.2.*), stm (>= && <2.5) [details]
CopyrightCopyright (C) 2017, ATS Advanced Telematic Systems GmbH
AuthorStevan Andjelkovic
MaintainerStevan Andjelkovic <stevan@advancedtelematic.com>
Home pagehttps://github.com/advancedtelematic/quickcheck-state-machine#readme
Source repositoryhead: git clone https://github.com/advancedtelematic/quickcheck-state-machine
UploadedWed Jun 7 08:27:27 UTC 2017 by stevana




Maintainers' corner

For package maintainers and hackage trustees

Readme for quickcheck-state-machine-0.0.0

[back to package description]


Hackage Build Status

quickcheck-state-machine is a Haskell library, based on QuickCheck, for testing stateful programs. The library is different from the Test.QuickCheck.Monadic approach in that it lets the user specify the correctness by means of a state machine based model using pre- and post-conditions. The advantage of the state machine approach is twofold: 1) specifying the correctness of your programs becomes less adhoc, and 2) you get testing for race conditions for free.

The combination of state machine based model specification and property based testing first appeard in Erlang's proprietary QuickCheck. The quickcheck-state-machine library can be seen as an attempt to provide similar functionality to Haskell's QuickCheck library.

Sample run (teaser)

Here's a sample output from when we look for race conditions in the mutable reference example:

> quickCheck (MutableReference.prop_parallel RaceCondition)
*** Failed! (after 5 tests and 6 shrinks):

Couldn't linearise:

│ New                  │
│                 ⟶ $0 │
            │ ┌────────┐
            │ │ Inc $0 │
┌─────────┐ │ │        │
│ Inc $0  │ │ │        │
│         │ │ │   ⟶ () │
│         │ │ └────────┘
│    ⟶ () │ │
└─────────┘ │
┌─────────┐ │
│ Read $0 │ │
│     ⟶ 1 │ │
└─────────┘ │

Clearly, if we increment a mutable reference in parallel we can end up with a race condition. We shall come back to this example below, but if your are impatient you can find the full source code here.

How it works

The rought idea is that the user of the library is asked to provide:

The library then gives back a sequential and a parallel property.

Sequential property

The sequential property checks if the model is consistent with respect to the semantics. The way this is done is:

  1. generate a list of commands;

  2. starting from the initial model, for each command do the the following:

    1. check that the pre-condition holds;
    2. if so, execute the command using the semantics;
    3. check if the the post-condition holds;
    4. advance the model using the transition function.
  3. If something goes wrong, shrink the initial list of commands and present a minimal counter example.

Parallel property

The parallel property checks if parallel execution of the semantics can be explained in terms of the sequential model. This is useful for trying to find race conditions -- which normally can be tricky to test for. It works as follows:

  1. generate a list of commands that will act as a sequential prefix for the parallel program (think of this as an initialisation bit that setups up some state);

  2. generate two lists of commands that will act as parallel suffixes;

  3. execute the prefix sequentially;

  4. execute the suffixes in parallel and gather the a trace (or history) of invocations and responses of each command;

  5. try to find a possible sequential interleaving of command invocations and responses that respects the post-conditions.

The last step basically tries to find a linearisation of calls that could have happend on a single thread.


To get started it is perhaps easiest to have a look at one of the several examples:

All examples have an associated Spec module located in the example/test directory. These make use of the properties in the examples, and get tested as part of Travis CI.

To get a better feel for the examples it might be helpful to git clone this repo, cd into the example/ directory and fire up stack ghci and run the different properties interactively.

How to contribute

The quickcheck-state-machine library is still very experimental.

We would like to encourage users to try it out, and join the discussion of how we can improve it on the issue tracker!

See also


BSD-style (see the file LICENSE).