# quickcheck-dynamic

A library for testing stateful programs using [QuickCheck](https://hackage.haskell.org/package/QuickCheck) and [dynamic logic](https://en.wikipedia.org/wiki/Dynamic_logic_(modal_logic)).

## Background

This library was initially designed by [QuviQ](http://www.quviq.com/) in collaboration with
[IOG](https://iohk.io/) to provide a dedicated test framework for [Plutus](https://docs.cardano.org/plutus/learn-about-plutus) "Smart
contracts". As the need of a _Model-Based Testing_ framework arises in
quite a lot of contexts, it was deemed useful to extract the most
generic part as a standalone package with no strings attached to
Plutus or Cardano.

## Usage

* Documentation is currenly mostly provided inline as Haddock
  comments. Checkout [StateModel](src/Test/QuickCheck/StateModel.hs)
  and [DynamicLogic](src/Test/QuickCheck/DynamicLogic.hs) modules for
  some usage instructions.
* For a concrete standalone example, have a look at [Registry](../quickcheck-io-sim-compat/test/Spec/DynamicLogic/Registry.hs), a multithreaded Thread registry.
* For more documentation on how to quickcheck-dynamic is used to test
  Plutus DApps, check this
  [tutorial](https://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-models.html).
* Apart from Plutus, this library is now in use in the
  [Hydra](https://github.com/input-output-hk/hydra-poc) project to
  verify the _Head Protocol_ implementation with respect to the
  original research paper.