quickcheck-state-machine 0.7.0 → 0.7.1
raw patch · 4 files changed
+170/−156 lines, 4 filesdep ~HTTPdep ~QuickCheckdep ~aeson
Dependency ranges changed: HTTP, QuickCheck, aeson, array, base, bifunctors, bytestring, containers, directory, doctest, filelock, filepath, hashable, hashtables, http-client, monad-logger, mtl, network, persistent-postgresql, persistent-sqlite, persistent-template, postgresql-simple, pretty-show, process, quickcheck-instances, random, resource-pool, resourcet, servant, servant-client, servant-server, sop-core, split, stm, strict, string-conversions, tasty, tasty-hunit, tasty-quickcheck, text, time, tree-diff, unliftio, unliftio-core, wai, warp
Files
- CHANGELOG.md +6/−0
- README.md +14/−18
- quickcheck-state-machine.cabal +148/−138
- src/Test/StateMachine/Lockstep/NAry.hs +2/−0
CHANGELOG.md view
@@ -1,3 +1,9 @@+#### 0.7.1 (2021-8-17)++ * Update links and references from the old archived repo at the+ `advancedtelematic` Github organisation to the active fork of the repo at+ the Github user `stevana`.+ #### 0.7.0 (2020-3-17) * Add Stack resolver lts-15 and drop lts-11;
README.md view
@@ -1,9 +1,6 @@ ## quickcheck-state-machine [](https://hackage.haskell.org/package/quickcheck-state-machine)-[](http://stackage.org/nightly/package/quickcheck-state-machine)-[](http://stackage.org/lts/package/quickcheck-state-machine)-[](https://travis-ci.org/advancedtelematic/quickcheck-state-machine) `quickcheck-state-machine` is a Haskell library, based on [QuickCheck](https://hackage.haskell.org/package/QuickCheck), for testing@@ -307,7 +304,7 @@ We shall come back to this example below, but if your are impatient you can find the full source code-[here](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MemoryReference.hs).+[here](https://github.com/stevana/quickcheck-state-machine/blob/master/test/MemoryReference.hs). ### How it works @@ -372,7 +369,7 @@ * The water jug problem from *Die Hard 3* -- this is a simple- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/DieHard.hs) of+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/DieHard.hs) of a specification where we use the sequential property to find a solution (counterexample) to a puzzle from an action movie. Note that this example has no meaningful semantics, we merely model-check. It might be helpful to@@ -384,19 +381,19 @@ [solution](https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla); * The Tower of Hanoi puzzle -- this- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/Hanoi.hs) uses+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/Hanoi.hs) uses property based testing in a very similar manner to the- Die Hard [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/DieHard.hs)+ Die Hard [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/DieHard.hs) to find a solution to the classic [Tower of Hanoi puzzle](https://en.wikipedia.org/wiki/Tower_of_Hanoi); * Mutable reference- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MemoryReference.hs) --+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/MemoryReference.hs) -- this is a bigger example that shows both how the sequential property can find normal bugs, and how the parallel property can find race conditions; * Circular buffer- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/CircularBuffer.hs)+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CircularBuffer.hs) -- another example that shows how the sequential property can find help find different kind of bugs. This example is borrowed from the paper *Testing the Hard Stuff and Staying Sane*@@ -406,7 +403,7 @@ [variant](https://github.com/polux/qsm-ffi-demo) which uses the C FFI; * The union-find- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/UnionFind.hs)+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/UnionFind.hs) -- an imperative implementation of the union-find algorithm. It could be useful to compare the solution to the one that appears in the paper *Testing Monadic Code with QuickCheck*@@ -416,7 +413,7 @@ * Ticket dispenser- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/TicketDispenser.hs) --+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/TicketDispenser.hs) -- a simple example where the parallel property is used once again to find a race condition. The semantics in this example uses a simple database file that needs to be setup and cleaned up. This example also appears in the@@ -428,7 +425,7 @@ * CRUD webserver where create returns unique ids- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/CrudWebserverDb.hs) --+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CrudWebserverDb.hs) -- create, read, update and delete users in a postgres database on a webserver using an API written using [Servant](https://github.com/haskell-servant/servant). Creating a user@@ -436,7 +433,7 @@ to use. In this example, unlike in the last one, the server is setup and torn down once per property rather than generate program; - * Bookstore [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/Bookstore.hs)+ * Bookstore [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/Bookstore.hs) -- another database application, that uses simple SQL queries to manage a bookstore. It is based on a [case study](https://propertesting.com/book_case_study_stateful_properties_with_a_bookstore.html)@@ -444,7 +441,7 @@ book; * Process registry- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/ProcessRegistry.hs)+ [example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/ProcessRegistry.hs) -- an example often featured in the Erlang QuickCheck papers. This example shows how one can tag the specification with which requirements are covered and then generate (minimal) examples of test cases that cover each@@ -455,11 +452,10 @@ [video](https://www.youtube.com/watch?v=w2fin2V83e8)] papers. All properties from the examples can be found in the-[`Spec`](https://github.com/advancedtelematic/quickcheck-state-machine/tree/master/test/Spec.hs)+[`Spec`](https://github.com/stevana/quickcheck-state-machine/tree/master/test/Spec.hs) module located in the-[`test`](https://github.com/advancedtelematic/quickcheck-state-machine/tree/master/test)-directory. The properties from the examples get tested as part of [Travis-CI](https://travis-ci.org/advancedtelematic/quickcheck-state-machine).+[`test`](https://github.com/stevana/quickcheck-state-machine/tree/master/test)+directory. To get a better feel for the examples it might be helpful to `git clone` this repo, `cd` into it, fire up `stack ghci --test`, load the different examples,
quickcheck-state-machine.cabal view
@@ -1,60 +1,58 @@-cabal-version: >=1.10-name: quickcheck-state-machine-version: 0.7.0-license: BSD3-license-file: LICENSE-copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;- 2018-2019, HERE Europe B.V.;- 2019-2020, Stevan Andjelkovic.-maintainer: Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>-author: Stevan Andjelkovic-tested-with: ghc ==8.4.3 ghc ==8.6.5 ghc ==8.8.3-homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme-synopsis: Test monadic programs using state machine based models-description:- See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>-category: Testing-build-type: Simple-extra-source-files:- README.md- CHANGELOG.md- CONTRIBUTING.md--source-repository head- type: git- location: https://github.com/advancedtelematic/quickcheck-state-machine+name: quickcheck-state-machine+version: 0.7.1+synopsis: Test monadic programs using state machine based models+description: See README at <https://github.com/stevana/quickcheck-state-machine#readme>+homepage: https://github.com/stevana/quickcheck-state-machine#readme+license: BSD3+license-file: LICENSE+author: Stevan Andjelkovic+maintainer: Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>+copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;+ 2018-2019, HERE Europe B.V.;+ 2019-2021, Stevan Andjelkovic.+category: Testing+build-type: Simple+extra-source-files: README.md+ , CHANGELOG.md+ , CONTRIBUTING.md+cabal-version: >=1.10+tested-with: GHC == 8.4.3, GHC == 8.6.5, GHC == 8.8.3 library- exposed-modules:- Test.StateMachine- Test.StateMachine.BoxDrawer- Test.StateMachine.ConstructorName- Test.StateMachine.DotDrawing- Test.StateMachine.Labelling- Test.StateMachine.Lockstep.Auxiliary- Test.StateMachine.Lockstep.NAry- Test.StateMachine.Lockstep.Simple- Test.StateMachine.Logic- Test.StateMachine.Markov- Test.StateMachine.Parallel- Test.StateMachine.Sequential- Test.StateMachine.Types- Test.StateMachine.Types.Environment- Test.StateMachine.Types.GenSym- Test.StateMachine.Types.History- Test.StateMachine.Types.Rank2- Test.StateMachine.Types.References- Test.StateMachine.Utils- Test.StateMachine.Z- hs-source-dirs: src- other-modules:- Paths_quickcheck_state_machine- default-language: Haskell2010- ghc-options: -Weverything -Wno-missing-exported-signatures- -Wno-missing-import-lists -Wno-missed-specialisations- -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe- -Wno-missing-local-signatures -Wno-monomorphism-restriction- build-depends:+ hs-source-dirs: src+ ghc-options:+ -Weverything+ -Wno-missing-exported-signatures+ -Wno-missing-import-lists+ -Wno-missed-specialisations+ -Wno-all-missed-specialisations+ -Wno-unsafe+ -Wno-safe+ -Wno-missing-local-signatures+ -Wno-monomorphism-restriction+ exposed-modules: Test.StateMachine+ , Test.StateMachine.BoxDrawer+ , Test.StateMachine.ConstructorName+ , Test.StateMachine.DotDrawing+ , Test.StateMachine.Labelling+ , Test.StateMachine.Lockstep.Auxiliary+ , Test.StateMachine.Lockstep.NAry+ , Test.StateMachine.Lockstep.Simple+ , Test.StateMachine.Logic+ , Test.StateMachine.Markov+ , Test.StateMachine.Parallel+ , Test.StateMachine.Sequential+ , Test.StateMachine.Types+ , Test.StateMachine.Types.Environment+ , Test.StateMachine.Types.GenSym+ , Test.StateMachine.Types.History+ , Test.StateMachine.Types.Rank2+ , Test.StateMachine.Types.References+ , Test.StateMachine.Utils+ , Test.StateMachine.Z+ other-modules:+ Paths_quickcheck_state_machine+ build-depends: ansi-wl-pprint >=0.6.7.3, base >=4.10 && <5, containers >=0.5.7.1,@@ -62,7 +60,7 @@ exceptions >=0.8.3, filepath >=1.0, generic-data >=0.3.0.0,- graphviz >=2999.20.0.3,+ graphviz >= 2999.20.0.3, markov-chain-usage-model >=0.0.0, matrix >=0.3.5.0, mtl >=2.2.1,@@ -71,89 +69,101 @@ process >=1.2.0.0, QuickCheck >=2.12, random >=1.1,- sop-core >=0.5.0.0,- split >=0.2.3.4,- text >=1.2.4.0,+ sop-core,+ split,+ text, tree-diff >=0.0.2.1, unliftio >=0.2.7.0+ default-language: Haskell2010 test-suite quickcheck-state-machine-test- type: exitcode-stdio-1.0- main-is: Spec.hs- hs-source-dirs: test- other-modules:- Bookstore- CircularBuffer- Cleanup- CrudWebserverDb- DieHard- Echo- ErrorEncountered- Hanoi- IORefs- MemoryReference- Mock- Overflow- ProcessRegistry- Schema- RQlite- ShrinkingProps- SQLite- TicketDispenser- UnionFind- default-language: Haskell2010- ghc-options: -threaded -rtsopts -with-rtsopts=-N- -fno-ignore-asserts -Weverything -Wno-missing-exported-signatures- -Wno-missing-import-lists -Wno-missed-specialisations- -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe- -Wno-missing-local-signatures -Wno-monomorphism-restriction- build-depends:- aeson >=1.4.6.0,- array >=0.5.4.0,- base >=4.13.0.0,- bifunctors >=5.5.7,- bytestring >=0.10.10.0,- containers >=0.6.2.1,- directory >=1.3.6.0,- doctest >=0.16.2,- filelock >=0.1.1.4,- filepath >=1.4.2.1,- hashable >=1.3.0.0,- hashtables >=1.2.3.4,- hs-rqlite >=0.1.2.0,- HTTP >=4000.3.14,- http-client >=0.6.4.1,- monad-logger >=0.3.32,- mtl >=2.2.2,- network >=3.1.1.1,- persistent >=2.10.3,- persistent-postgresql >=2.10.1,- persistent-sqlite >=2.10.2,- persistent-template >=2.8.2.3,- postgresql-simple >=0.6.2,- pretty-show >=1.10,- process >=1.6.8.0,- QuickCheck >=2.13.2,- quickcheck-instances >=0.3.22,- quickcheck-state-machine -any,- random >=1.1,- resourcet >=1.2.3,- resource-pool >=0.2.3.2,- servant >=0.16.2,- servant-client >=0.16.0.1,- servant-server >=0.16.2,- split >=0.2.3.4,- stm >=2.5.0.0,- strict >=0.3.2,- string-conversions >=0.4.0.1,- tasty >=1.2.3,- tasty-hunit >=0.10.0.2,- tasty-quickcheck >=0.10.1.1,- text >=1.2.4.0,- tree-diff >=0.0.2.1,- time >=1.9.3,- vector >=0.12.0.1,- wai >=3.2.2.1,- warp >=3.3.9,- unliftio >=0.2.12.1,- unliftio-core >=0.1.2.0+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends: aeson,+ array,+ base,+ bifunctors,+ bytestring,+ containers,+ directory,+ doctest,+ filelock,+ filepath,+ hashable,+ hashtables,+ hs-rqlite >= 0.1.2.0,+ HTTP,+ http-client,+ monad-logger,+ mtl,+ network,+ persistent >= 2.10.3,+ persistent-postgresql,+ persistent-sqlite,+ persistent-template,+ postgresql-simple,+ pretty-show,+ process,+ QuickCheck,+ quickcheck-instances,+ quickcheck-state-machine,+ random,+ resourcet,+ resource-pool,+ servant,+ servant-client,+ servant-server,+ split,+ stm,+ strict,+ string-conversions,+ tasty,+ tasty-hunit,+ tasty-quickcheck,+ text,+ tree-diff,+ time,+ vector >=0.12.0.1,+ wai,+ warp,+ unliftio,+ unliftio-core++ other-modules: Bookstore,+ CircularBuffer,+ Cleanup,+ CrudWebserverDb,+ DieHard,+ Echo,+ ErrorEncountered,+ Hanoi,+ IORefs,+ MemoryReference,+ Mock,+ Overflow,+ ProcessRegistry,+ Schema,+ RQlite,+ ShrinkingProps,+ SQLite,+ TicketDispenser,+ UnionFind++ ghc-options:+ -threaded -rtsopts -with-rtsopts=-N+ -fno-ignore-asserts+ -Weverything+ -Wno-missing-exported-signatures+ -Wno-missing-import-lists+ -Wno-missed-specialisations+ -Wno-all-missed-specialisations+ -Wno-unsafe+ -Wno-safe+ -Wno-missing-local-signatures+ -Wno-monomorphism-restriction+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/stevana/quickcheck-state-machine
src/Test/StateMachine/Lockstep/NAry.hs view
@@ -39,6 +39,8 @@ -- * Running the tests , prop_sequential , prop_parallel+ -- * Translate to state machine model+ , toStateMachine ) where import Data.Functor.Classes