<commit_before>homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme
changelog-type: markdown
hash: df0bf54c90768255cde54c268b2f9591ff971a4bb865f9b38a56d0e7867c43b6
test-bench-deps:
  base: -any
maintainer: <NAME> <<EMAIL>>
synopsis: Test monadic programs using state machine based models
changelog: ! "#### 0.3.0 (2017-12-15)\n\n  * A propositional logic module was added
  to help provide better\n    counterexamples when pre- and post-conditions don't
  hold;\n\n  * Generation of parallel programs was improved (base on\n    a [comment](https://github.com/Quviq/QuickCheckExamples/issues/2)
  by\n    <NAME> about how Erlang QuickCheck does it);\n\n  * Support for semantics
  that might fail was added;\n\n  * Pretty printing of counterexamples was improved.\n\n####
  0.2.0\n\n  * Z-inspired definition of relations and associated operations were\n
  \   added to help defining concise and showable models;\n\n  * Template Haskell
  derivation of `shrink` and type classes: `Show`,\n    `Constructors`, `HFunctor`,
  `HFoldable`, `HTraversable`;\n\n  * New and more flexible combinators for building
  sequential and\n    parallel properties replaced the old clunky ones;\n\n  * Circular
  buffer example was added;\n\n  * Two examples of how to test CRUD web applications
  were added.\n\n#### 0.1.0\n\n  * The API was simplified, thanks to ideas stolen
  from\n    [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog/commit/385c92f9dd0aa7e748fc677b2eeead5e3572685f).\n\n####
  0.0.0\n\n  * Initial release.\n"
basic-deps:
  ansi-wl-pprint: ! '>=0.6.7.3 && <0.7'
  stm: ! '>=2.4.4.1 && <2.5'
  base: ! '>=4.7 && <5'
  monad-control: ! '>=1.0.2.2 && <1.1'
  async: ! '>=2.1.1.1 && <2.2'
  lifted-base: ! '>=0.2.3.11 && <0.3'
  quickcheck-with-counterexamples: ! '>=1.0 && <2.0'
  th-abstraction: ! '>=0.2.6.0 && <0.3'
  containers: ! '>=0.5.7.1 && <0.6'
  mtl: ! '>=2.2.1 && <2.3'
  lifted-async: ! '>=0.9.3 && <0.10'
  random: ==1.1.*
  QuickCheck: ! '>=2.9.2 && <2.11'
  template-haskell: ! '>=2.11.1.0 && <2.13'
all-versions:
- '0.0.0'
- '0.1.0'
- '0.2.0'
- '0.3.0'
author: <NAME>
latest: '0.3.0'
description-type: markdown
description: ! "## quickcheck-state-machine\n\n[![Hackage](https://img.shields.io/hackage/v/quickcheck-state-machine.svg)](https://hackage.haskell.org/package/quickcheck-state-machine)\n[![Build
  Status](https://api.travis-ci.org/advancedtelematic/quickcheck-state-machine.svg?branch=master)](https://travis-ci.org/advancedtelematic/quickcheck-state-machine)\n\n`quickcheck-state-machine`
  is a Haskell library, based\non [QuickCheck](https://hackage.haskell.org/package/QuickCheck),
  for testing\nstateful programs. The library is different from\nthe\n[`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html)
  approach\nin that it lets the user specify the correctness by means of a state machine\nbased
  model using pre- and post-conditions. The advantage of the state machine\napproach
  is twofold: 1) specifying the correctness of your programs becomes less\nadhoc,
  and 2) you get testing for race conditions for free.\n\nThe combination of state
  machine based model specification and property based\ntesting first appeard in Erlang's
  proprietary QuickCheck. The\n`quickcheck-state-machine` library can be seen as an
  attempt to provide similar\nfunctionality to Haskell's QuickCheck library.\n\n###
  Example\n\nAs a first example, let's implement and test programs using mutable\nreferences.
  Our implementation will be using `IORef`s, but let's start with a\nrepresentation
  of what actions are possible with programs using mutable\nreferences. Our mutable
  references can be created, read from, written to and\nincremented:\n\n```haskell\ndata
  Action (v :: * -> *) :: * -> * where\n  New   ::                                     Action
  v (Opaque (IORef Int))\n  Read  :: Reference v (Opaque (IORef Int)) -> Action v
  Int\n  Write :: Reference v (Opaque (IORef Int)) -> Int -> Action v ()\n  Inc   ::
  Reference v (Opaque (IORef Int)) -> Action v ()\n```\n\nWhen we generate actions
  we won't be able to create arbitrary `IORef`s, that's\nwhy all uses of `IORefs`
  are wrapped in `Reference v`, where the parameter `v`\nwill let us use symbolic
  references while generating (and concrete ones when\nexecuting).\n\nIn order to
  be able to show counterexamples, we need a show instance for our\nactions. `IORef`s
  don't have a show instance, thats why we wrap them in\n`Opaque`; which gives a show
  instance to a type that doesn't have one.\n\nNext, we give the actual implementation
  of our mutable references. To make\nthings more interesting, we parametrise the
  semantics by a possible problem.\n\n```haskell\ndata Problem = None | Bug | RaceCondition\n
  \ deriving Eq\n\nsemantics :: Problem -> Action Concrete resp -> IO resp\nsemantics
  _   New           = Opaque <$> newIORef 0\nsemantics _   (Read  ref)   = readIORef
  \ (opaque ref)\nsemantics prb (Write ref i) = writeIORef (opaque ref) i'\n  where\n
  \ -- One of the problems is a bug that writes a wrong value to the\n  -- reference.\n
  \ i' | i `elem` [5..10] = if prb == Bug then i + 1 else i\n     | otherwise        =
  i\nsemantics prb (Inc   ref)   =\n  -- The other problem is that we introduce a
  possible race condition\n  -- when incrementing.\n  if prb == RaceCondition\n  then
  do\n    i <- readIORef (opaque ref)\n    threadDelay =<< randomRIO (0, 5000)\n    writeIORef
  (opaque ref) (i + 1)\n  else\n    atomicModifyIORef' (opaque ref) (\\i -> (i + 1,
  ()))\n```\n\nNote that above `v` is instantiated to `Concrete`, which is essentially
  the\nidentity type, so while writing the semantics we have access to real `IORef`s.\n\nWe
  now have an implementation, the next step is to define a model for the\nimplementation
  to be tested against. We'll use a simple map between references\nand integers as
  a model.\n\n```haskell\nnewtype Model v = Model [(Reference v (Opaque (IORef Int)),
  Int)]\n\ninitModel :: Model v\ninitModel = Model []\n```\n\nThe pre-condition of
  an action specifies in what context the action is\nwell-defined. For example, we
  can always create a new mutable reference, but\nwe can only read from references
  that already have been created. The\npre-conditions are used while generating programs
  (lists of actions).\n\n```haskell\nprecondition :: Model Symbolic -> Action Symbolic
  resp -> Bool\nprecondition _         New           = True\nprecondition (Model m)
  (Read  ref)   = ref `elem` map fst m\nprecondition (Model m) (Write ref _) = ref
  `elem` map fst m\nprecondition (Model m) (Inc   ref)   = ref `elem` map fst m\n```\n\nThe
  transition function explains how actions change the model. Note that the\ntransition
  function is polymorphic in `v`. The reason for this is that we use\nthe transition
  function both while generating and executing.\n\n```haskell\ntransition :: Model
  v -> Action v resp -> v resp -> Model v\ntransition (Model m) New           ref
  = Model (m ++ [(Reference ref, 0)])\ntransition m         (Read  _)     _   = m\ntransition
  (Model m) (Write ref i) _   = Model (update ref i         m)\ntransition (Model
  m) (Inc   ref)   _   = Model (update ref (old + 1) m)\n  where\n  Just old = lookup
  ref m\n\nupdate :: Eq a => a -> b -> [(a, b)] -> [(a, b)]\nupdate ref i m = (ref,
  i) : filter ((/= ref) . fst) m\n```\n\nPost-conditions are checked after we executed
  an action and got access to the\nresult.\n\n```haskell\npostcondition :: Model Concrete
  -> Action Concrete resp -> resp -> Bool\npostcondition _         New         _    =
  True\npostcondition (Model m) (Read ref)  resp = lookup ref m == Just resp\npostcondition
  _         (Write _ _) _    = True\npostcondition _         (Inc _)     _    = True\n```\n\nFinally,
  we have to explain how to generate and shrink actions.\n\n```haskell\ngenerator
  :: Model Symbolic -> Gen (Untyped Action)\ngenerator (Model m)\n  | null m    =
  pure (Untyped New)\n  | otherwise = frequency\n      [ (1, pure (Untyped New))\n
  \     , (8, Untyped .    Read  <$> elements (map fst m))\n      , (8, Untyped <$>
  (Write <$> elements (map fst m) <*> arbitrary))\n      , (8, Untyped .    Inc   <$>
  elements (map fst m))\n      ]\n\nshrinker :: Action v resp -> [Action v resp]\nshrinker
  (Write ref i) = [ Write ref i' | i' <- shrink i ]\nshrinker _             = []\n```\n\nTo
  be able to fit the code on a line we pack up all of them above into a\nrecord.\n\n```haskell\nsm
  :: Problem -> StateMachine Model Action IO\nsm prb = stateMachine\n  generator shrinker
  precondition transition\n  postcondition initModel (semantics prb) id\n```\n\nWe
  can now define a sequential property as follows.\n\n```haskell\nprop_references
  :: Problem -> PropertyOf (Program Action)\nprop_references prb = monadicSequentialC
  sm' $ \\prog -> do\n  (hist, _, res) <- runProgram sm' prog\n  prettyProgram sm'
  hist $\n    checkActionNames prog (res === Ok)\n  where\n  sm' = sm prb\n```\n\nIf
  we run the sequential property without introducing any problems to the\nsemantics
  function, i.e. `quickCheck (prop_references None)`, then the property\npasses. If
  we however introduce the bug problem, then it will fail with the\nminimal counterexample:\n\n```\n>
  quickCheck (prop_references Bug)\n*** Failed! Falsifiable (after 19 tests and 3
  shrinks):\n\nModel []\n\n    New --> Opaque\n\nModel [(Reference Concrete Opaque,0)]\n\n
  \   Write (Reference (Symbolic (Var 0))) 5 --> ()\n\nModel [(Reference Concrete
  Opaque,5)]\n\n    Read (Reference (Symbolic (Var 0))) --> 6\n\nModel [(Reference
  Concrete Opaque,5)]\n\nPostconditionFailed /= Ok\n```\n\nRecall that the bug problem
  causes the write of values ``i `elem` [5..10]`` to\nactually write `i + 1`.\n\nRunning
  the sequential property with the race condition problem will not uncover\nthe race
  condition.\n\nIf we however define a parallel property as follows.\n\n```haskell\nprop_referencesParallel
  :: Problem -> Property\nprop_referencesParallel prb = monadicParallel (sm prb) $
  \\prog ->\n  prettyParallelProgram prog =<< runParallelProgram (sm prb) prog\n```\n\nAnd
  run it using the race condition problem, then we'll find the race\ncondition:\n\n```\n>
  quickCheck (prop_referencesParallel RaceCondition)\n*** Failed! (after 8 tests and
  6 shrinks):\n\nCouldn't linearise:\n\n┌────────────────────────────────┐\n│ Var
  0 ← New                    │\n│                       → Opaque │\n└────────────────────────────────┘\n┌─────────────┐
  │\n│ Inc (Var 0) │ │\n│             │ │ ┌──────────────┐\n│             │ │ │ Inc
  (Var 0)  │\n│        → () │ │ │              │\n└─────────────┘ │ │              │\n
  \               │ │         → () │\n                │ └──────────────┘\n                │
  ┌──────────────┐\n                │ │ Read (Var 0) │\n                │ │          →
  1 │\n                │ └──────────────┘\nJust 2 /= Just 1\n```\n\nAs we can see
  above, a mutable reference is first created, and then in\nparallel (concurrently)
  we do two increments of said reference, and finally we\nread the value `1` while
  the model expects `2`.\n\nRecall that incrementing is implemented by first reading
  the reference and\nthen writing it, if two such actions are interleaved then one
  of the writes\nmight end up overwriting the other one -- creating the race condition.\n\nWe
  shall come back to this example below, but if your are impatient you can\nfind the
  full source\ncode\n[here](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference.hs).\n\n###
  How it works\n\nThe rough idea is that the user of the library is asked to provide:\n\n
  \ * a datatype of actions;\n  * a datatype model;\n  * pre- and post-conditions
  of the actions on the model;\n  * a state transition function that given a model
  and an action advances the\n    model to its next state;\n  * a way to generate
  and shrink actions;\n  * semantics for executing the actions.\n\nThe library then
  gives back a bunch of combinators that let you define a\nsequential and a parallel
  property.\n\n#### Sequential property\n\nThe *sequential property* checks if the
  model is consistent with respect to the\nsemantics. The way this is done is:\n\n
  \ 1. generate a list of actions;\n\n  2. starting from the initial model, for each
  action do the the following:\n\n       1. check that the pre-condition holds;\n
  \      2. if so, execute the action using the semantics;\n       3. check if the
  the post-condition holds;\n       4. advance the model using the transition function.\n\n
  \ 3. If something goes wrong, shrink the initial list of actions and present a\n
  \    minimal counterexample.\n\n#### Parallel property\n\nThe *parallel property*
  checks if parallel execution of the semantics can be\nexplained in terms of the
  sequential model. This is useful for trying to find\nrace conditions -- which normally
  can be tricky to test for. It works as\nfollows:\n\n  1. generate a list of actions
  that will act as a sequential prefix for the\n     parallel program (think of this
  as an initialisation bit that setups up\n     some state);\n\n  2. generate two
  lists of actions that will act as parallel suffixes;\n\n  3. execute the prefix
  sequentially;\n\n  4. execute the suffixes in parallel and gather the a trace (or
  history) of\n     invocations and responses of each action;\n\n  5. try to find
  a possible sequential interleaving of action invocations and\n     responses that
  respects the post-conditions.\n\nThe last step basically tries to find\na [linearisation](https://en.wikipedia.org/wiki/Linearizability)
  of calls that\ncould have happend on a single thread.\n\n### More examples\n\nHere
  are some more examples to get you started:\n\n  * The water jug problem from *Die
  Hard 3* -- this is a\n    simple\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/DieHard.hs)
  of\n    a specification where we use the sequential property to find a solution\n
  \   (counterexample) to a puzzle from an action movie. Note that this example\n
  \   has no meaningful semantics, we merely model-check. It might be helpful to\n
  \   compare the solution to the\n    Hedgehog\n    [solution](http://clrnd.com.ar/posts/2017-04-21-the-water-jug-problem-in-hedgehog.html)
  and\n    the\n    TLA+\n    [solution](https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla);\n\n
  \ * The\n    union-find\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/UnionFind.hs)
  --\n    another use of the sequential property, this time with a useful semantics\n
  \   (imperative implementation of the union-find algorithm). It could be useful\n
  \   to compare the solution to the one that appears in the paper *Testing\n    Monadic
  Code with\n    QuickCheck* [[PS](http://www.cse.chalmers.se/~rjmh/Papers/QuickCheckST.ps)],\n
  \   which the\n    [`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html)
  module\n    is based on;\n\n  * Mutable\n    reference\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference.hs)
  --\n    this is a bigger example that shows both how the sequential property can\n
  \   find normal bugs, and how the parallel property can find race conditions.\n
  \   Several metaproperties, that for example check if the counterexamples are\n
  \   minimal, are specified in a\n    separate\n    [module](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs);\n\n
  \ * Circular buffer\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/CircularBuffer.hs)\n
  \   -- another example that shows how the sequential property can find help find\n
  \   different kind of bugs. This example is borrowed from the paper *Testing the\n
  \   Hard Stuff and Staying Sane*\n    [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),\n
  \   [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)];\n\n  * Ticket\n    dispenser\n
  \   [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/TicketDispenser.hs)
  --\n    a simple example where the parallel property is used once again to find
  a\n    race condition. The semantics in this example uses a simple database file\n
  \   that needs to be setup and cleaned up. This example also appears in the\n    *Testing
  a Database for Race Conditions with QuickCheck* and *Testing the\n    Hard Stuff
  and Staying\n    Sane*\n    [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),\n
  \   [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)] papers;\n\n  * CRUD webserver
  where create returns unique\n    ids\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/CrudWebserverDb.hs)
  --\n    create, read, update and delete users in a sqlite database on a webserver\n
  \   using an API written\n    using [Servant](https://github.com/haskell-servant/servant).
  Creating a user\n    will return a unique id, which subsequent reads, updates, and
  deletes need\n    to use. In this example, unlike in the last one, the server is
  setup and\n    torn down once per property rather than generate program.\n\n\nAll
  examples have an associated `Spec` module located in\nthe\n[`example/test`](https://github.com/advancedtelematic/quickcheck-state-machine/tree/master/example/test)
  directory.\nThese make use of the properties in the examples, and get tested as
  part\nof\n[Travis CI](https://travis-ci.org/advancedtelematic/quickcheck-state-machine).\n\nTo
  get a better feel for the examples it might be helpful to `git clone` this\nrepo,
  `cd` into the `example/` directory and fire up `stack ghci` and run the\ndifferent
  properties interactively.\n\n### How to contribute\n\nThe `quickcheck-state-machine`
  library is still very experimental.\n\nWe would like to encourage users to try it
  out, and join the discussion of how\nwe can improve it on the issue tracker!\n\n###
  See also\n\n  * The QuickCheck\n    bugtrack [issue](https://github.com/nick8325/quickcheck/issues/139)
  -- where\n    the initial discussion about how how to add state machine based testing
  to\n    QuickCheck started;\n\n  * *Finding Race Conditions in Erlang with QuickCheck
  and\n    PULSE*\n    [[PDF](http://www.cse.chalmers.se/~nicsma/papers/finding-race-conditions.pdf),\n
  \   [video](https://vimeo.com/6638041)] -- this is the first paper to describe\n
  \   how Erlang's QuickCheck works (including the parallel testing);\n\n  * *Linearizability:
  a correctness condition for concurrent\n    objects* [[PDF](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)],
  this\n    is a classic paper that describes the main technique of the parallel\n
  \   property;\n\n  * Aphyr's blogposts about [Jepsen](https://github.com/jepsen-io/jepsen),
  which\n    also uses the linearisability technique, and has found bugs in many\n
  \   distributed systems:\n\n    - [Knossos: Redis and linearizability](https://aphyr.com/posts/309-knossos-redis-and-linearizability);\n
  \   - [Strong consistency models](https://aphyr.com/posts/313-strong-consistency-models);\n
  \   - [Computational techniques in Knossos](https://aphyr.com/posts/314-computational-techniques-in-knossos);\n
  \   - [Serializability, linearizability, and locality](https://aphyr.com/posts/333-serializability-linearizability-and-locality).\n\n
  \ * The use of state machines to model and verify properties about programs is\n
  \   quite well-established, as witnessed by several books on the subject:\n\n      -
  [Specifying\n        Systems](https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/):\n
  \       The TLA+ Language and Tools for Hardware and Software Engineers.\n        Parts
  of this book are also presented by the author, <NAME>, in the following
  video\n        [course](https://lamport.azurewebsites.net/video/videos.html);\n\n
  \     - [Modeling in Event-B](http://www.event-b.org/abook.html): System\n        and
  Software Engineering. Parts of this book are covered in the\n        following (video)
  course given at Microsoft Research by the\n        author, <NAME>,
  himself:\n\n          + [Lecture 1](https://www.youtube.com/watch?v=2GP1pJINVT4):\n
  \           introduction to modeling and Event-B (chapter 1 of the\n            book)
  and start of \"controlling cars on bridge\" example\n            (chapter 2);\n\n
  \         + [Lecture 2](https://www.youtube.com/watch?v=M8nvVaZ74wA):\n            refining
  the \"controlling cars on a bridge\" example\n            (sections 2.6 and 2.7);\n\n
  \         + [Lecture 3](https://www.youtube.com/watch?v=Y5OUtq8cdV8):\n            design
  patterns and the \"mechanical press controller\"\n            example (chapter 3);\n\n
  \         + [Lecture 4](https://www.youtube.com/watch?v=ku-lfjxM4WI):\n            sorting
  algorithm example (chapter 15);\n\n          + [Lecture 5](https://www.youtube.com/watch?v=C0tpgPOKAyg):\n
  \           designing sequential programs (chapter 15);\n\n          + [Lecture
  6](https://www.youtube.com/watch?v=i-GKHZAWWjU):\n            status report of the
  hypervisor that Microsoft Research are\n            developing using Event-B.\n\n
  \     - [Abstract State Machines](http://www.di.unipi.it/~boerger/AsmBook/): A\n
  \       Method for High-Level System Design and Analysis.\n\n    The books contain
  general advice how to model systems using state machines,\n    and are hence relevant
  to us. For shorter texts on why state machines are\n    important for modeling,
  see:\n\n      - Lamport's\n        [*Computation and State Machines*](https://www.microsoft.com/en-us/research/publication/computation-state-machines/);\n\n
  \     - Gurevich's\n        [*Evolving Algebras 1993: Lipari Guide*](https://www.microsoft.com/en-us/research/publication/103-evolving-algebras-1993-lipari-guide/)
  and\n        *Sequential Abstract State Machines Capture Sequential\n        Algorithms*\n
  \       [[PDF](http://delta-apache-vm.cs.tau.ac.il/~nachumd/models/gurevich.pdf)].\n\n
  \ * Other similar libraries:\n\n      - Erlang QuickCheck, [eqc](http://quviq.com/documentation/eqc/),
  the first\n        property based testing library to have support for state machines\n
  \       (closed source);\n\n      - The Erlang library [PropEr](https://github.com/manopapad/proper)
  is\n        *eqc*-inspired, open source, and has support for state\n        machine
  [testing](http://propertesting.com/);\n\n      - The Haskell\n        library [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog),
  also\n        has support for state machine based testing;\n\n      - [ScalaCheck](http://www.scalacheck.org/),
  likewise has support for state\n        machine\n        based\n        [testing](https://github.com/rickynils/scalacheck/blob/master/doc/UserGuide.md#stateful-testing)
  (no\n        parallel property);\n\n      - The Python\n        library [Hypothesis](https://hypothesis.readthedocs.io/en/latest/),
  also\n        has support for state machine\n        based\n        [testing](https://hypothesis.readthedocs.io/en/latest/stateful.html)
  (no\n        parallel property).\n\n### License\n\nBSD-style (see the file LICENSE).\n"
license-name: BSD3
<commit_msg>Update from Hackage at 2018-01-15T13:45:39Z<commit_after>homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme
changelog-type: markdown
hash: 7424fb14c9824898a6b68f640b919447b87b09a3ad06aa04763984f87dcdd57a
test-bench-deps:
  base: -any
maintainer: <NAME> <<EMAIL>>
synopsis: Test monadic programs using state machine based models
changelog: ! "#### 0.3.1 (2018-1-15)\n\n  * Remove upper bounds for dependencies,
  to easier keep up with\n    Stackage nightly.\n\n#### 0.3.0 (2017-12-15)\n\n  *
  A propositional logic module was added to help provide better\n    counterexamples
  when pre- and post-conditions don't hold;\n\n  * Generation of parallel programs
  was improved (base on\n    a [comment](https://github.com/Quviq/QuickCheckExamples/issues/2)
  by\n    <NAME> about how Erlang QuickCheck does it);\n\n  * Support for semantics
  that might fail was added;\n\n  * Pretty printing of counterexamples was improved.\n\n####
  0.2.0\n\n  * Z-inspired definition of relations and associated operations were\n
  \   added to help defining concise and showable models;\n\n  * Template Haskell
  derivation of `shrink` and type classes: `Show`,\n    `Constructors`, `HFunctor`,
  `HFoldable`, `HTraversable`;\n\n  * New and more flexible combinators for building
  sequential and\n    parallel properties replaced the old clunky ones;\n\n  * Circular
  buffer example was added;\n\n  * Two examples of how to test CRUD web applications
  were added.\n\n#### 0.1.0\n\n  * The API was simplified, thanks to ideas stolen
  from\n    [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog/commit/385c92f9dd0aa7e748fc677b2eeead5e3572685f).\n\n####
  0.0.0\n\n  * Initial release.\n"
basic-deps:
  ansi-wl-pprint: ! '>=0.6.7.3'
  stm: ! '>=2.4.4.1'
  base: ! '>=4.7 && <5'
  monad-control: ! '>=1.0.2.2'
  async: ! '>=2.1.1.1'
  lifted-base: ! '>=0.2.3.11'
  quickcheck-with-counterexamples: ! '>=1.0'
  th-abstraction: ! '>=0.2.6.0'
  containers: ! '>=0.5.7.1'
  mtl: ! '>=2.2.1'
  lifted-async: ! '>=0.9.3'
  random: ! '>=1.1'
  QuickCheck: ! '>=2.9.2'
  template-haskell: ! '>=2.11.1.0'
all-versions:
- '0.0.0'
- '0.1.0'
- '0.2.0'
- '0.3.0'
- '0.3.1'
author: <NAME>
latest: '0.3.1'
description-type: markdown
description: ! "## quickcheck-state-machine\n\n[![Hackage](https://img.shields.io/hackage/v/quickcheck-state-machine.svg)](https://hackage.haskell.org/package/quickcheck-state-machine)\n[![Stackage
  Nightly](http://stackage.org/package/quickcheck-state-machine/badge/nightly)](http://stackage.org/nightly/package/quickcheck-state-machine)\n[![Stackage
  LTS](http://stackage.org/package/quickcheck-state-machine/badge/lts)](http://stackage.org/lts/package/quickcheck-state-machine)\n[![Build
  Status](https://api.travis-ci.org/advancedtelematic/quickcheck-state-machine.svg?branch=master)](https://travis-ci.org/advancedtelematic/quickcheck-state-machine)\n\n`quickcheck-state-machine`
  is a Haskell library, based\non [QuickCheck](https://hackage.haskell.org/package/QuickCheck),
  for testing\nstateful programs. The library is different from\nthe\n[`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html)
  approach\nin that it lets the user specify the correctness by means of a state machine\nbased
  model using pre- and post-conditions. The advantage of the state machine\napproach
  is twofold: 1) specifying the correctness of your programs becomes less\nadhoc,
  and 2) you get testing for race conditions for free.\n\nThe combination of state
  machine based model specification and property based\ntesting first appeard in Erlang's
  proprietary QuickCheck. The\n`quickcheck-state-machine` library can be seen as an
  attempt to provide similar\nfunctionality to Haskell's QuickCheck library.\n\n###
  Example\n\nAs a first example, let's implement and test programs using mutable\nreferences.
  Our implementation will be using `IORef`s, but let's start with a\nrepresentation
  of what actions are possible with programs using mutable\nreferences. Our mutable
  references can be created, read from, written to and\nincremented:\n\n```haskell\ndata
  Action (v :: * -> *) :: * -> * where\n  New   ::                                     Action
  v (Opaque (IORef Int))\n  Read  :: Reference v (Opaque (IORef Int)) -> Action v
  Int\n  Write :: Reference v (Opaque (IORef Int)) -> Int -> Action v ()\n  Inc   ::
  Reference v (Opaque (IORef Int)) -> Action v ()\n```\n\nWhen we generate actions
  we won't be able to create arbitrary `IORef`s, that's\nwhy all uses of `IORefs`
  are wrapped in `Reference v`, where the parameter `v`\nwill let us use symbolic
  references while generating (and concrete ones when\nexecuting).\n\nIn order to
  be able to show counterexamples, we need a show instance for our\nactions. `IORef`s
  don't have a show instance, thats why we wrap them in\n`Opaque`; which gives a show
  instance to a type that doesn't have one.\n\nNext, we give the actual implementation
  of our mutable references. To make\nthings more interesting, we parametrise the
  semantics by a possible problem.\n\n```haskell\ndata Problem = None | Bug | RaceCondition\n
  \ deriving Eq\n\nsemantics :: Problem -> Action Concrete resp -> IO resp\nsemantics
  _   New           = Opaque <$> newIORef 0\nsemantics _   (Read  ref)   = readIORef
  \ (opaque ref)\nsemantics prb (Write ref i) = writeIORef (opaque ref) i'\n  where\n
  \ -- One of the problems is a bug that writes a wrong value to the\n  -- reference.\n
  \ i' | i `elem` [5..10] = if prb == Bug then i + 1 else i\n     | otherwise        =
  i\nsemantics prb (Inc   ref)   =\n  -- The other problem is that we introduce a
  possible race condition\n  -- when incrementing.\n  if prb == RaceCondition\n  then
  do\n    i <- readIORef (opaque ref)\n    threadDelay =<< randomRIO (0, 5000)\n    writeIORef
  (opaque ref) (i + 1)\n  else\n    atomicModifyIORef' (opaque ref) (\\i -> (i + 1,
  ()))\n```\n\nNote that above `v` is instantiated to `Concrete`, which is essentially
  the\nidentity type, so while writing the semantics we have access to real `IORef`s.\n\nWe
  now have an implementation, the next step is to define a model for the\nimplementation
  to be tested against. We'll use a simple map between references\nand integers as
  a model.\n\n```haskell\nnewtype Model v = Model [(Reference v (Opaque (IORef Int)),
  Int)]\n\ninitModel :: Model v\ninitModel = Model []\n```\n\nThe pre-condition of
  an action specifies in what context the action is\nwell-defined. For example, we
  can always create a new mutable reference, but\nwe can only read from references
  that already have been created. The\npre-conditions are used while generating programs
  (lists of actions).\n\n```haskell\nprecondition :: Model Symbolic -> Action Symbolic
  resp -> Bool\nprecondition _         New           = True\nprecondition (Model m)
  (Read  ref)   = ref `elem` map fst m\nprecondition (Model m) (Write ref _) = ref
  `elem` map fst m\nprecondition (Model m) (Inc   ref)   = ref `elem` map fst m\n```\n\nThe
  transition function explains how actions change the model. Note that the\ntransition
  function is polymorphic in `v`. The reason for this is that we use\nthe transition
  function both while generating and executing.\n\n```haskell\ntransition :: Model
  v -> Action v resp -> v resp -> Model v\ntransition (Model m) New           ref
  = Model (m ++ [(Reference ref, 0)])\ntransition m         (Read  _)     _   = m\ntransition
  (Model m) (Write ref i) _   = Model (update ref i         m)\ntransition (Model
  m) (Inc   ref)   _   = Model (update ref (old + 1) m)\n  where\n  Just old = lookup
  ref m\n\nupdate :: Eq a => a -> b -> [(a, b)] -> [(a, b)]\nupdate ref i m = (ref,
  i) : filter ((/= ref) . fst) m\n```\n\nPost-conditions are checked after we executed
  an action and got access to the\nresult.\n\n```haskell\npostcondition :: Model Concrete
  -> Action Concrete resp -> resp -> Bool\npostcondition _         New         _    =
  True\npostcondition (Model m) (Read ref)  resp = lookup ref m == Just resp\npostcondition
  _         (Write _ _) _    = True\npostcondition _         (Inc _)     _    = True\n```\n\nFinally,
  we have to explain how to generate and shrink actions.\n\n```haskell\ngenerator
  :: Model Symbolic -> Gen (Untyped Action)\ngenerator (Model m)\n  | null m    =
  pure (Untyped New)\n  | otherwise = frequency\n      [ (1, pure (Untyped New))\n
  \     , (8, Untyped .    Read  <$> elements (map fst m))\n      , (8, Untyped <$>
  (Write <$> elements (map fst m) <*> arbitrary))\n      , (8, Untyped .    Inc   <$>
  elements (map fst m))\n      ]\n\nshrinker :: Action v resp -> [Action v resp]\nshrinker
  (Write ref i) = [ Write ref i' | i' <- shrink i ]\nshrinker _             = []\n```\n\nTo
  be able to fit the code on a line we pack up all of them above into a\nrecord.\n\n```haskell\nsm
  :: Problem -> StateMachine Model Action IO\nsm prb = stateMachine\n  generator shrinker
  precondition transition\n  postcondition initModel (semantics prb) id\n```\n\nWe
  can now define a sequential property as follows.\n\n```haskell\nprop_references
  :: Problem -> PropertyOf (Program Action)\nprop_references prb = monadicSequentialC
  sm' $ \\prog -> do\n  (hist, _, res) <- runProgram sm' prog\n  prettyProgram sm'
  hist $\n    checkActionNames prog (res === Ok)\n  where\n  sm' = sm prb\n```\n\nIf
  we run the sequential property without introducing any problems to the\nsemantics
  function, i.e. `quickCheck (prop_references None)`, then the property\npasses. If
  we however introduce the bug problem, then it will fail with the\nminimal counterexample:\n\n```\n>
  quickCheck (prop_references Bug)\n*** Failed! Falsifiable (after 19 tests and 3
  shrinks):\n\nModel []\n\n    New --> Opaque\n\nModel [(Reference Concrete Opaque,0)]\n\n
  \   Write (Reference (Symbolic (Var 0))) 5 --> ()\n\nModel [(Reference Concrete
  Opaque,5)]\n\n    Read (Reference (Symbolic (Var 0))) --> 6\n\nModel [(Reference
  Concrete Opaque,5)]\n\nPostconditionFailed /= Ok\n```\n\nRecall that the bug problem
  causes the write of values ``i `elem` [5..10]`` to\nactually write `i + 1`.\n\nRunning
  the sequential property with the race condition problem will not uncover\nthe race
  condition.\n\nIf we however define a parallel property as follows.\n\n```haskell\nprop_referencesParallel
  :: Problem -> Property\nprop_referencesParallel prb = monadicParallel (sm prb) $
  \\prog ->\n  prettyParallelProgram prog =<< runParallelProgram (sm prb) prog\n```\n\nAnd
  run it using the race condition problem, then we'll find the race\ncondition:\n\n```\n>
  quickCheck (prop_referencesParallel RaceCondition)\n*** Failed! (after 8 tests and
  6 shrinks):\n\nCouldn't linearise:\n\n┌────────────────────────────────┐\n│ Var
  0 ← New                    │\n│                       → Opaque │\n└────────────────────────────────┘\n┌─────────────┐
  │\n│ Inc (Var 0) │ │\n│             │ │ ┌──────────────┐\n│             │ │ │ Inc
  (Var 0)  │\n│        → () │ │ │              │\n└─────────────┘ │ │              │\n
  \               │ │         → () │\n                │ └──────────────┘\n                │
  ┌──────────────┐\n                │ │ Read (Var 0) │\n                │ │          →
  1 │\n                │ └──────────────┘\nJust 2 /= Just 1\n```\n\nAs we can see
  above, a mutable reference is first created, and then in\nparallel (concurrently)
  we do two increments of said reference, and finally we\nread the value `1` while
  the model expects `2`.\n\nRecall that incrementing is implemented by first reading
  the reference and\nthen writing it, if two such actions are interleaved then one
  of the writes\nmight end up overwriting the other one -- creating the race condition.\n\nWe
  shall come back to this example below, but if your are impatient you can\nfind the
  full source\ncode\n[here](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference.hs).\n\n###
  How it works\n\nThe rough idea is that the user of the library is asked to provide:\n\n
  \ * a datatype of actions;\n  * a datatype model;\n  * pre- and post-conditions
  of the actions on the model;\n  * a state transition function that given a model
  and an action advances the\n    model to its next state;\n  * a way to generate
  and shrink actions;\n  * semantics for executing the actions.\n\nThe library then
  gives back a bunch of combinators that let you define a\nsequential and a parallel
  property.\n\n#### Sequential property\n\nThe *sequential property* checks if the
  model is consistent with respect to the\nsemantics. The way this is done is:\n\n
  \ 1. generate a list of actions;\n\n  2. starting from the initial model, for each
  action do the the following:\n\n       1. check that the pre-condition holds;\n
  \      2. if so, execute the action using the semantics;\n       3. check if the
  the post-condition holds;\n       4. advance the model using the transition function.\n\n
  \ 3. If something goes wrong, shrink the initial list of actions and present a\n
  \    minimal counterexample.\n\n#### Parallel property\n\nThe *parallel property*
  checks if parallel execution of the semantics can be\nexplained in terms of the
  sequential model. This is useful for trying to find\nrace conditions -- which normally
  can be tricky to test for. It works as\nfollows:\n\n  1. generate a list of actions
  that will act as a sequential prefix for the\n     parallel program (think of this
  as an initialisation bit that setups up\n     some state);\n\n  2. generate two
  lists of actions that will act as parallel suffixes;\n\n  3. execute the prefix
  sequentially;\n\n  4. execute the suffixes in parallel and gather the a trace (or
  history) of\n     invocations and responses of each action;\n\n  5. try to find
  a possible sequential interleaving of action invocations and\n     responses that
  respects the post-conditions.\n\nThe last step basically tries to find\na [linearisation](https://en.wikipedia.org/wiki/Linearizability)
  of calls that\ncould have happend on a single thread.\n\n### More examples\n\nHere
  are some more examples to get you started:\n\n  * The water jug problem from *Die
  Hard 3* -- this is a\n    simple\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/DieHard.hs)
  of\n    a specification where we use the sequential property to find a solution\n
  \   (counterexample) to a puzzle from an action movie. Note that this example\n
  \   has no meaningful semantics, we merely model-check. It might be helpful to\n
  \   compare the solution to the\n    Hedgehog\n    [solution](http://clrnd.com.ar/posts/2017-04-21-the-water-jug-problem-in-hedgehog.html)
  and\n    the\n    TLA+\n    [solution](https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla);\n\n
  \ * The\n    union-find\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/UnionFind.hs)
  --\n    another use of the sequential property, this time with a useful semantics\n
  \   (imperative implementation of the union-find algorithm). It could be useful\n
  \   to compare the solution to the one that appears in the paper *Testing\n    Monadic
  Code with\n    QuickCheck* [[PS](http://www.cse.chalmers.se/~rjmh/Papers/QuickCheckST.ps)],\n
  \   which the\n    [`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html)
  module\n    is based on;\n\n  * Mutable\n    reference\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference.hs)
  --\n    this is a bigger example that shows both how the sequential property can\n
  \   find normal bugs, and how the parallel property can find race conditions.\n
  \   Several metaproperties, that for example check if the counterexamples are\n
  \   minimal, are specified in a\n    separate\n    [module](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs);\n\n
  \ * Circular buffer\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/CircularBuffer.hs)\n
  \   -- another example that shows how the sequential property can find help find\n
  \   different kind of bugs. This example is borrowed from the paper *Testing the\n
  \   Hard Stuff and Staying Sane*\n    [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),\n
  \   [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)];\n\n  * Ticket\n    dispenser\n
  \   [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/TicketDispenser.hs)
  --\n    a simple example where the parallel property is used once again to find
  a\n    race condition. The semantics in this example uses a simple database file\n
  \   that needs to be setup and cleaned up. This example also appears in the\n    *Testing
  a Database for Race Conditions with QuickCheck* and *Testing the\n    Hard Stuff
  and Staying\n    Sane*\n    [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),\n
  \   [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)] papers;\n\n  * CRUD webserver
  where create returns unique\n    ids\n    [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/CrudWebserverDb.hs)
  --\n    create, read, update and delete users in a sqlite database on a webserver\n
  \   using an API written\n    using [Servant](https://github.com/haskell-servant/servant).
  Creating a user\n    will return a unique id, which subsequent reads, updates, and
  deletes need\n    to use. In this example, unlike in the last one, the server is
  setup and\n    torn down once per property rather than generate program.\n\n\nAll
  examples have an associated `Spec` module located in\nthe\n[`example/test`](https://github.com/advancedtelematic/quickcheck-state-machine/tree/master/example/test)
  directory.\nThese make use of the properties in the examples, and get tested as
  part\nof\n[Travis CI](https://travis-ci.org/advancedtelematic/quickcheck-state-machine).\n\nTo
  get a better feel for the examples it might be helpful to `git clone` this\nrepo,
  `cd` into the `example/` directory and fire up `stack ghci` and run the\ndifferent
  properties interactively.\n\n### How to contribute\n\nThe `quickcheck-state-machine`
  library is still very experimental.\n\nWe would like to encourage users to try it
  out, and join the discussion of how\nwe can improve it on the issue tracker!\n\n###
  See also\n\n  * The QuickCheck\n    bugtrack [issue](https://github.com/nick8325/quickcheck/issues/139)
  -- where\n    the initial discussion about how how to add state machine based testing
  to\n    QuickCheck started;\n\n  * *Finding Race Conditions in Erlang with QuickCheck
  and\n    PULSE*\n    [[PDF](http://www.cse.chalmers.se/~nicsma/papers/finding-race-conditions.pdf),\n
  \   [video](https://vimeo.com/6638041)] -- this is the first paper to describe\n
  \   how Erlang's QuickCheck works (including the parallel testing);\n\n  * *Linearizability:
  a correctness condition for concurrent\n    objects* [[PDF](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)],
  this\n    is a classic paper that describes the main technique of the parallel\n
  \   property;\n\n  * Aphyr's blogposts about [Jepsen](https://github.com/jepsen-io/jepsen),
  which\n    also uses the linearisability technique, and has found bugs in many\n
  \   distributed systems:\n\n    - [Knossos: Redis and linearizability](https://aphyr.com/posts/309-knossos-redis-and-linearizability);\n
  \   - [Strong consistency models](https://aphyr.com/posts/313-strong-consistency-models);\n
  \   - [Computational techniques in Knossos](https://aphyr.com/posts/314-computational-techniques-in-knossos);\n
  \   - [Serializability, linearizability, and locality](https://aphyr.com/posts/333-serializability-linearizability-and-locality).\n\n
  \ * The use of state machines to model and verify properties about programs is\n
  \   quite well-established, as witnessed by several books on the subject:\n\n      -
  [Specifying\n        Systems](https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/):\n
  \       The TLA+ Language and Tools for Hardware and Software Engineers.\n        Parts
  of this book are also presented by the author, Leslie\n        Lamport, in the following
  video\n        [course](https://lamport.azurewebsites.net/video/videos.html);\n\n
  \     - [Modeling in Event-B](http://www.event-b.org/abook.html): System\n        and
  Software Engineering. Parts of this book are covered in the\n        following (video)
  course given at Microsoft Research by the\n        author, <NAME>,
  himself:\n\n          + [Lecture 1](https://www.youtube.com/watch?v=2GP1pJINVT4):\n
  \           introduction to modeling and Event-B (chapter 1 of the\n            book)
  and start of \"controlling cars on bridge\" example\n            (chapter 2);\n\n
  \         + [Lecture 2](https://www.youtube.com/watch?v=M8nvVaZ74wA):\n            refining
  the \"controlling cars on a bridge\" example\n            (sections 2.6 and 2.7);\n\n
  \         + [Lecture 3](https://www.youtube.com/watch?v=Y5OUtq8cdV8):\n            design
  patterns and the \"mechanical press controller\"\n            example (chapter 3);\n\n
  \         + [Lecture 4](https://www.youtube.com/watch?v=ku-lfjxM4WI):\n            sorting
  algorithm example (chapter 15);\n\n          + [Lecture 5](https://www.youtube.com/watch?v=C0tpgPOKAyg):\n
  \           designing sequential programs (chapter 15);\n\n          + [Lecture
  6](https://www.youtube.com/watch?v=i-GKHZAWWjU):\n            status report of the
  hypervisor that Microsoft Research are\n            developing using Event-B.\n\n
  \     - [Abstract State Machines](http://www.di.unipi.it/~boerger/AsmBook/): A\n
  \       Method for High-Level System Design and Analysis.\n\n    The books contain
  general advice how to model systems using state machines,\n    and are hence relevant
  to us. For shorter texts on why state machines are\n    important for modeling,
  see:\n\n      - Lamport's\n        [*Computation and State Machines*](https://www.microsoft.com/en-us/research/publication/computation-state-machines/);\n\n
  \     - Gurevich's\n        [*Evolving Algebras 1993: Lipari Guide*](https://www.microsoft.com/en-us/research/publication/103-evolving-algebras-1993-lipari-guide/)
  and\n        *Sequential Abstract State Machines Capture Sequential\n        Algorithms*\n
  \       [[PDF](http://delta-apache-vm.cs.tau.ac.il/~nachumd/models/gurevich.pdf)].\n\n
  \ * Other similar libraries:\n\n      - Erlang QuickCheck, [eqc](http://quviq.com/documentation/eqc/),
  the first\n        property based testing library to have support for state machines\n
  \       (closed source);\n\n      - The Erlang library [PropEr](https://github.com/manopapad/proper)
  is\n        *eqc*-inspired, open source, and has support for state\n        machine
  [testing](http://propertesting.com/);\n\n      - The Haskell\n        library [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog),
  also\n        has support for state machine based testing;\n\n      - [ScalaCheck](http://www.scalacheck.org/),
  likewise has support for state\n        machine\n        based\n        [testing](https://github.com/rickynils/scalacheck/blob/master/doc/UserGuide.md#stateful-testing)
  (no\n        parallel property);\n\n      - The Python\n        library [Hypothesis](https://hypothesis.readthedocs.io/en/latest/),
  also\n        has support for state machine\n        based\n        [testing](https://hypothesis.readthedocs.io/en/latest/stateful.html)
  (no\n        parallel property).\n\n### License\n\nBSD-style (see the file LICENSE).\n"
license-name: BSD3

{'fraction_non_alphanumeric': 0.12651017214397495, 'fraction_numerical': 0.01433489827856025, 'mean_word_length': 3.1180615225983845, 'pattern_counts': {'":': 0, '<': 56, '<?xml version=': 0, '>': 121, 'https://': 96, 'lorem ipsum': 0, 'www.': 32, 'xml': 0}, 'pii_count': 16, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6332961', 'n_tokens_mistral': 16314, 'n_tokens_neox': 15321, 'n_words': 4768}