quickcheck-state-machine 0.3.1 → 0.4.0
raw patch · 36 files changed
+3666/−2471 lines, 36 filesdep +bytestringdep +directorydep +exceptionsdep −quickcheck-with-counterexamplesdep −template-haskelldep −th-abstractiondep ~basedep ~mtl
Dependencies added: bytestring, directory, exceptions, filelock, filepath, http-client, matrix, monad-logger, network, persistent, persistent-postgresql, persistent-template, pretty-show, process, quickcheck-instances, quickcheck-state-machine, resourcet, servant, servant-client, servant-server, split, strict, string-conversions, tasty, tasty-quickcheck, text, tree-diff, vector, wai, warp
Dependencies removed: quickcheck-with-counterexamples, template-haskell, th-abstraction
Dependency ranges changed: base, mtl
Files
- CHANGELOG.md +16/−0
- CONTRIBUTING.md +1/−1
- LICENSE +2/−2
- README.md +170/−129
- quickcheck-state-machine.cabal +103/−51
- src/Test/StateMachine.hs +31/−269
- src/Test/StateMachine/BoxDrawer.hs +105/−0
- src/Test/StateMachine/ConstructorName.hs +88/−0
- src/Test/StateMachine/Internal/Parallel.hs +0/−349
- src/Test/StateMachine/Internal/Sequential.hs +0/−217
- src/Test/StateMachine/Internal/Types.hs +0/−138
- src/Test/StateMachine/Internal/Types/Environment.hs +0/−93
- src/Test/StateMachine/Internal/Utils.hs +0/−113
- src/Test/StateMachine/Internal/Utils/BoxDrawer.hs +0/−104
- src/Test/StateMachine/Logic.hs +112/−12
- src/Test/StateMachine/Parallel.hs +383/−0
- src/Test/StateMachine/Sequential.hs +411/−0
- src/Test/StateMachine/TH.hs +0/−51
- src/Test/StateMachine/Types.hs +77/−145
- src/Test/StateMachine/Types/Environment.hs +100/−0
- src/Test/StateMachine/Types/GenSym.hs +49/−0
- src/Test/StateMachine/Types/Generics.hs +0/−33
- src/Test/StateMachine/Types/Generics/TH.hs +0/−276
- src/Test/StateMachine/Types/HFunctor.hs +0/−56
- src/Test/StateMachine/Types/HFunctor/TH.hs +0/−209
- src/Test/StateMachine/Types/History.hs +43/−90
- src/Test/StateMachine/Types/Rank2.hs +135/−0
- src/Test/StateMachine/Types/References.hs +89/−96
- src/Test/StateMachine/Utils.hs +92/−6
- src/Test/StateMachine/Z.hs +73/−29
- test/CircularBuffer.hs +399/−0
- test/CrudWebserverDb.hs +521/−0
- test/DieHard.hs +215/−0
- test/MemoryReference.hs +168/−0
- test/Spec.hs +61/−2
- test/TicketDispenser.hs +222/−0
CHANGELOG.md view
@@ -1,3 +1,19 @@+#### 0.4.0 (2018-8-21)++ * Major rewrite, addressing many issues:++ - The output of sequential runs now shows a diff of how the model changed in+ each step (related to issue #77);++ - The datatype of actions was renamed to commands and no longer is a GADT+ (discussed in issue #170, also makes issue #196 obsolete);++ - Commands can now return multiple references (issue #197);++ - Global invariants can now more easily be expressed (issue #200);++ - Counterexamples are now printed when post-conditions fail (issue #172).+ #### 0.3.1 (2018-1-15) * Remove upper bounds for dependencies, to easier keep up with
CONTRIBUTING.md view
@@ -4,7 +4,7 @@ 1. Update CHANGELOG.md; 2. Bump version in .cabal file and fix bounds;- 3. Make tarball with `stack sdist --pvp-bounds both`;+ 3. Make tarball with `stack sdist --pvp-bounds lower`; 4. Upload tarball as a package [candidate](https://hackage.haskell.org/packages/candidates/upload), and if
LICENSE view
@@ -1,5 +1,5 @@-Copyright (c) 2017 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley,- Xia Li-yao+Copyright (c) 2017-2018 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley,+ Xia Li-yao, Robert Danitz All rights reserved.
README.md view
@@ -29,15 +29,21 @@ incremented: ```haskell-data Action (v :: * -> *) :: * -> * where- New :: Action v (Opaque (IORef Int))- Read :: Reference v (Opaque (IORef Int)) -> Action v Int- Write :: Reference v (Opaque (IORef Int)) -> Int -> Action v ()- Inc :: Reference v (Opaque (IORef Int)) -> Action v ()+data Command r+ = Create+ | Read (Reference (Opaque (IORef Int)) r)+ | Write (Reference (Opaque (IORef Int)) r) Int+ | Increment (Reference (Opaque (IORef Int)) r)++data Response r+ = Created (Reference (Opaque (IORef Int)) r)+ | ReadValue Int+ | Written+ | Incremented ``` When we generate actions we won't be able to create arbitrary `IORef`s, that's-why all uses of `IORefs` are wrapped in `Reference v`, where the parameter `v`+why all uses of `IORef`s are wrapped in `Reference _ r`, where the parameter `r` will let us use symbolic references while generating (and concrete ones when executing). @@ -49,31 +55,33 @@ things more interesting, we parametrise the semantics by a possible problem. ```haskell-data Problem = None | Bug | RaceCondition+data Bug = None | Logic | Race deriving Eq -semantics :: Problem -> Action Concrete resp -> IO resp-semantics _ New = Opaque <$> newIORef 0-semantics _ (Read ref) = readIORef (opaque ref)-semantics prb (Write ref i) = writeIORef (opaque ref) i'- where- -- One of the problems is a bug that writes a wrong value to the- -- reference.- i' | i `elem` [5..10] = if prb == Bug then i + 1 else i- | otherwise = i-semantics prb (Inc ref) =- -- The other problem is that we introduce a possible race condition- -- when incrementing.- if prb == RaceCondition- then do- i <- readIORef (opaque ref)- threadDelay =<< randomRIO (0, 5000)- writeIORef (opaque ref) (i + 1)- else- atomicModifyIORef' (opaque ref) (\i -> (i + 1, ()))+semantics :: Bug -> Command Concrete -> IO (Response Concrete)+semantics bug cmd = case cmd of+ Create -> Created <$> (reference . Opaque <$> newIORef 0)+ Read ref -> ReadValue <$> readIORef (opaque ref)+ Write ref i -> Written <$ writeIORef (opaque ref) i'+ where+ -- One of the problems is a bug that writes a wrong value to the+ -- reference.+ i' | i `Prelude.elem` [5..10] = if bug == Logic then i + 1 else i+ | otherwise = i+ Increment ref -> do+ -- The other problem is that we introduce a possible race condition+ -- when incrementing.+ if bug == Race+ then do+ i <- readIORef (opaque ref)+ threadDelay =<< randomRIO (0, 5000)+ writeIORef (opaque ref) (i + 1)+ else+ atomicModifyIORef' (opaque ref) (\i -> (i + 1, ()))+ return Incremented ``` -Note that above `v` is instantiated to `Concrete`, which is essentially the+Note that above `r` is instantiated to `Concrete`, which is essentially the identity type, so while writing the semantics we have access to real `IORef`s. We now have an implementation, the next step is to define a model for the@@ -81,9 +89,9 @@ and integers as a model. ```haskell-newtype Model v = Model [(Reference v (Opaque (IORef Int)), Int)]+newtype Model r = Model [(Reference (Opaque (IORef Int)) r, Int)] -initModel :: Model v+initModel :: Model r initModel = Model [] ``` @@ -93,19 +101,27 @@ pre-conditions are used while generating programs (lists of actions). ```haskell-precondition :: Model Symbolic -> Action Symbolic resp -> Bool-precondition _ New = True-precondition (Model m) (Read ref) = ref `elem` map fst m-precondition (Model m) (Write ref _) = ref `elem` map fst m-precondition (Model m) (Inc ref) = ref `elem` map fst m+precondition :: Model Symbolic -> Command Symbolic -> Logic+precondition (Model m) cmd = case cmd of+ Create -> Top+ Read ref -> ref `elem` domain m+ Write ref _ -> ref `elem` domain m+ Increment ref -> ref `elem` domain m ``` The transition function explains how actions change the model. Note that the-transition function is polymorphic in `v`. The reason for this is that we use+transition function is polymorphic in `r`. The reason for this is that we use the transition function both while generating and executing. ```haskell-transition :: Model v -> Action v resp -> v resp -> Model v+transition :: Eq1 r => Model r -> Command r -> Response r -> Model r+transition m@(Model model) cmd resp = case (cmd, resp) of+ (Create, Created ref) -> Model ((ref, 0) : model)+ (Read _, ReadValue _) -> m+ (Write ref x, Written) -> Model ((ref, x) : filter ((/= ref) . fst) model)+ (Increment ref, Incremented) -> case lookup ref model of+ Just i -> Model ((ref, succ i) : filter ((/= ref) . fst) model)+transition :: Ord1 v => Model v -> Action v resp -> v resp -> Model v transition (Model m) New ref = Model (m ++ [(Reference ref, 0)]) transition m (Read _) _ = m transition (Model m) (Write ref i) _ = Model (update ref i m)@@ -121,27 +137,36 @@ result. ```haskell-postcondition :: Model Concrete -> Action Concrete resp -> resp -> Bool-postcondition _ New _ = True-postcondition (Model m) (Read ref) resp = lookup ref m == Just resp-postcondition _ (Write _ _) _ = True-postcondition _ (Inc _) _ = True+postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic+postcondition (Model m) cmd resp = case (cmd, resp) of+ (Create, Created ref) -> m' ! ref .== 0 .// "Create"+ where+ Model m' = transition (Model m) cmd resp+ (Read ref, ReadValue v) -> v .== m ! ref .// "Read"+ (Write _ref _x, Written) -> Top+ (Increment _ref, Incremented) -> Top ``` -Finally, we have to explain how to generate and shrink actions.+Finally, we have to explain how to generate, mock responses given a model, and+shrink actions. ```haskell-generator :: Model Symbolic -> Gen (Untyped Action)-generator (Model m)- | null m = pure (Untyped New)- | otherwise = frequency- [ (1, pure (Untyped New))- , (8, Untyped . Read <$> elements (map fst m))- , (8, Untyped <$> (Write <$> elements (map fst m) <*> arbitrary))- , (8, Untyped . Inc <$> elements (map fst m))- ]+generator :: Model Symbolic -> Gen (Command Symbolic)+generator (Model model) = frequency+ [ (1, pure Create)+ , (4, Read <$> elements (domain model))+ , (4, Write <$> elements (domain model) <*> arbitrary)+ , (4, Increment <$> elements (domain model))+ ] -shrinker :: Action v resp -> [Action v resp]+mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)+mock (Model m) cmd = case cmd of+ Create -> Created <$> genSym+ Read ref -> ReadValue <$> pure (m ! ref)+ Write _ _ -> pure Written+ Increment _ -> pure Incremented++shrinker :: Command Symbolic -> [Command Symbolic] shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ] shrinker _ = [] ```@@ -150,52 +175,61 @@ record. ```haskell-sm :: Problem -> StateMachine Model Action IO-sm prb = stateMachine- generator shrinker precondition transition- postcondition initModel (semantics prb) id+sm :: Bug -> StateMachine Model Command IO Response+sm bug = StateMachine initModel transition precondition postcondition+ Nothing Nothing generator Nothing shrinker (semantics bug) id mock ``` We can now define a sequential property as follows. ```haskell-prop_references :: Problem -> PropertyOf (Program Action)-prop_references prb = monadicSequentialC sm' $ \prog -> do- (hist, _, res) <- runProgram sm' prog- prettyProgram sm' hist $- checkActionNames prog (res === Ok)- where- sm' = sm prb+prop_sequential :: Bug -> Property+prop_sequential bug = forAllCommands sm' Nothing $ \cmds -> monadicIO $ do+ (hist, _model, res) <- runCommands sm' cmds+ prettyCommands sm' hist (checkCommandNames cmds (res === Ok))+ where+ sm' = sm bug ``` If we run the sequential property without introducing any problems to the-semantics function, i.e. `quickCheck (prop_references None)`, then the property-passes. If we however introduce the bug problem, then it will fail with the+semantics function, i.e. `quickCheck (prop_sequential None)`, then the property+passes. If we however introduce the logic bug problem, then it will fail with the minimal counterexample: ```-> quickCheck (prop_references Bug)-*** Failed! Falsifiable (after 19 tests and 3 shrinks):+> quickCheck (prop_sequential Logic)+*** Failed! Falsifiable (after 12 tests and 2 shrinks):+Commands+ { unCommands =+ [ Command Create (fromList [ Var 0 ])+ , Command (Write (Reference (Symbolic (Var 0))) 5) (fromList [])+ , Command (Read (Reference (Symbolic (Var 0)))) (fromList [])+ ]+ } Model [] - New --> Opaque+ == Create ==> Created (Reference (Concrete Opaque)) [ 0 ] -Model [(Reference Concrete Opaque,0)]+Model [+_×_ (Reference Opaque)+ 0] - Write (Reference (Symbolic (Var 0))) 5 --> ()+ == Write (Reference (Concrete Opaque)) 5 ==> Written [ 0 ] -Model [(Reference Concrete Opaque,5)]+Model [_×_ (Reference Opaque)+ -0+ +5] - Read (Reference (Symbolic (Var 0))) --> 6+ == Read (Reference (Concrete Opaque)) ==> ReadValue 6 [ 0 ] -Model [(Reference Concrete Opaque,5)]+Model [_×_ (Reference Opaque) 5] -PostconditionFailed /= Ok+PostconditionFailed "AnnotateC \"Read\" (PredicateC (6 :/= 5))" /= Ok ``` Recall that the bug problem causes the write of values ``i `elem` [5..10]`` to-actually write `i + 1`.+actually write `i + 1`. Also notice how the diff of the model is displayed+between each action. Running the sequential property with the race condition problem will not uncover the race condition.@@ -203,37 +237,56 @@ If we however define a parallel property as follows. ```haskell-prop_referencesParallel :: Problem -> Property-prop_referencesParallel prb = monadicParallel (sm prb) $ \prog ->- prettyParallelProgram prog =<< runParallelProgram (sm prb) prog+prop_parallel :: Bug -> Property+prop_parallel bug = forAllParallelCommands sm' $ \cmds -> monadicIO $ do+ prettyParallelCommands cmds =<< runParallelCommands sm' cmds+ where+ sm' = sm bug ``` And run it using the race condition problem, then we'll find the race condition: ```-> quickCheck (prop_referencesParallel RaceCondition)-*** Failed! (after 8 tests and 6 shrinks):--Couldn't linearise:--┌────────────────────────────────┐-│ Var 0 ← New │-│ → Opaque │-└────────────────────────────────┘-┌─────────────┐ │-│ Inc (Var 0) │ │-│ │ │ ┌──────────────┐-│ │ │ │ Inc (Var 0) │-│ → () │ │ │ │-└─────────────┘ │ │ │- │ │ → () │- │ └──────────────┘- │ ┌──────────────┐- │ │ Read (Var 0) │- │ │ → 1 │- │ └──────────────┘-Just 2 /= Just 1+> quickCheck (prop_parallel Race)+*** Failed! Falsifiable (after 26 tests and 6 shrinks):+ParallelCommands+ { prefix =+ Commands { unCommands = [ Command Create (fromList [ Var 0 ]) ] }+ , suffixes =+ [ Pair+ { proj1 =+ Commands+ { unCommands =+ [ Command (Increment (Reference (Symbolic (Var 0)))) (fromList [])+ , Command (Read (Reference (Symbolic (Var 0)))) (fromList [])+ ]+ }+ , proj2 =+ Commands+ { unCommands =+ [ Command (Increment (Reference (Symbolic (Var 0)))) (fromList [])+ ]+ }+ }+ ]+ }+┌─────────────────────────────────────────────────────────────────────────────────────────────────┐+│ [Var 0] ← Create │+│ → Created (Reference (Concrete Opaque)) │+└─────────────────────────────────────────────────────────────────────────────────────────────────┘+┌──────────────────────────────────────────────┐ │+│ [] ← Increment (Reference (Concrete Opaque)) │ │+│ │ │ ┌──────────────────────────────────────────────┐+│ │ │ │ [] ← Increment (Reference (Concrete Opaque)) │+│ │ │ │ → Incremented │+│ │ │ └──────────────────────────────────────────────┘+│ → Incremented │ │+└──────────────────────────────────────────────┘ │+┌──────────────────────────────────────────────┐ │+│ [] ← Read (Reference (Concrete Opaque)) │ │+│ → ReadValue 1 │ │+└──────────────────────────────────────────────┘ │ ``` As we can see above, a mutable reference is first created, and then in@@ -247,7 +300,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/example/src/MutableReference.hs).+[here](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MutableReference.hs). ### How it works @@ -312,7 +365,7 @@ * The water jug problem from *Die Hard 3* -- this is a simple- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/DieHard.hs) of+ [example](https://github.com/advancedtelematic/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@@ -323,30 +376,18 @@ TLA+ [solution](https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla); - * The- union-find- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/UnionFind.hs) --- another use of the sequential property, this time with a useful semantics- (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* [[PS](http://www.cse.chalmers.se/~rjmh/Papers/QuickCheckST.ps)],- which the- [`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html) module- is based on;- * Mutable reference- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference.hs) --+ [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MutableReference.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. Several metaproperties, that for example check if the counterexamples are minimal, are specified in a separate- [module](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs);+ [module](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/test/MutableReference/Prop.hs); * Circular buffer- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/CircularBuffer.hs)+ [example](https://github.com/advancedtelematic/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*@@ -355,7 +396,7 @@ * Ticket dispenser- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/TicketDispenser.hs) --+ [example](https://github.com/advancedtelematic/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@@ -367,25 +408,25 @@ * CRUD webserver where create returns unique ids- [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/CrudWebserverDb.hs) --- create, read, update and delete users in a sqlite database on a webserver+ [example](https://github.com/advancedtelematic/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 will return a unique id, which subsequent reads, updates, and deletes need to use. In this example, unlike in the last one, the server is setup and torn down once per property rather than generate program. --All examples have an associated `Spec` module located in-the-[`example/test`](https://github.com/advancedtelematic/quickcheck-state-machine/tree/master/example/test) directory.-These make use of the properties in the examples, and get tested as part-of-[Travis CI](https://travis-ci.org/advancedtelematic/quickcheck-state-machine).+All properties from the examples can be found in the+[`Spec`](https://github.com/advancedtelematic/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). 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.+repo, `cd` into it, fire up `stack ghci --test`, load the different examples,+e.g. `:l test/CrudWebserverDb.hs`, and run the different properties+interactively. ### How to contribute
quickcheck-state-machine.cabal view
@@ -1,66 +1,118 @@-name: quickcheck-state-machine-version: 0.3.1-synopsis: Test monadic programs using state machine based models-description: See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>-homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme-license: BSD3-license-file: LICENSE-author: Stevan Andjelkovic-maintainer: Stevan Andjelkovic <stevan@advancedtelematic.com>-copyright: Copyright (C) 2017, ATS Advanced Telematic Systems GmbH-category: Testing-build-type: Simple-extra-source-files: README.md- , CHANGELOG.md- , CONTRIBUTING.md-cabal-version: >=1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2+cabal-version: >=1.10+name: quickcheck-state-machine+version: 0.4.0+license: BSD3+license-file: LICENSE+copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;+ 2018, HERE Europe B.V.+maintainer: Stevan Andjelkovic <stevan.andjelkovic@here.com>+author: Stevan Andjelkovic+tested-with: ghc ==8.2.2 ghc ==8.4.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+ library- hs-source-dirs: src- exposed-modules: Test.StateMachine- , Test.StateMachine.Internal.Parallel- , Test.StateMachine.Internal.Sequential- , Test.StateMachine.Internal.Types- , Test.StateMachine.Internal.Types.Environment- , Test.StateMachine.Internal.Utils- , Test.StateMachine.Internal.Utils.BoxDrawer- , Test.StateMachine.Logic- , Test.StateMachine.TH- , Test.StateMachine.Types- , Test.StateMachine.Types.Generics- , Test.StateMachine.Types.Generics.TH- , Test.StateMachine.Types.HFunctor- , Test.StateMachine.Types.HFunctor.TH- , Test.StateMachine.Types.History- , Test.StateMachine.Types.References- , Test.StateMachine.Z- other-modules: Test.StateMachine.Utils- build-depends:+ exposed-modules:+ Test.StateMachine+ Test.StateMachine.BoxDrawer+ Test.StateMachine.ConstructorName+ Test.StateMachine.Logic+ 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: ansi-wl-pprint >=0.6.7.3, async >=2.1.1.1, base >=4.7 && <5, containers >=0.5.7.1,+ exceptions >=0.8.3, lifted-async >=0.9.3, lifted-base >=0.2.3.11,+ matrix >=0.3.5.0, monad-control >=1.0.2.2, mtl >=2.2.1,+ pretty-show >=1.7, QuickCheck >=2.9.2,- quickcheck-with-counterexamples >=1.0, random >=1.1,+ split >=0.2.3.3, stm >=2.4.4.1,- template-haskell >=2.11.1.0,- th-abstraction >=0.2.6.0- default-language: Haskell2010+ tree-diff >=0.0.1,+ vector >=0.12.0.1 test-suite quickcheck-state-machine-test- type: exitcode-stdio-1.0- hs-source-dirs: test- main-is: Spec.hs- build-depends: base- ghc-options: -threaded -rtsopts -with-rtsopts=-N- default-language: Haskell2010--source-repository head- type: git- location: https://github.com/advancedtelematic/quickcheck-state-machine+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ hs-source-dirs: test+ other-modules:+ CircularBuffer+ CrudWebserverDb+ DieHard+ MemoryReference+ TicketDispenser+ default-language: Haskell2010+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -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:+ base >=4.11.1.0,+ bytestring >=0.10.8.2,+ directory >=1.3.1.5,+ filelock >=0.1.1.2,+ filepath >=1.4.2,+ http-client >=0.5.13.1,+ lifted-async >=0.9.3,+ matrix >=0.3.5.0,+ monad-control >=1.0.2.2,+ monad-logger >=0.3.28.5,+ mtl >=2.2.2,+ network >=2.6.3.6,+ persistent >=2.8.2,+ persistent-postgresql >=2.8.2.0,+ persistent-template >=2.5.4,+ process >=1.6.3.0,+ QuickCheck >=2.9.2,+ quickcheck-instances >=0.3.18,+ quickcheck-state-machine -any,+ random >=1.1,+ resourcet >=1.2.1,+ servant >=0.14.1,+ servant-client >=0.14,+ servant-server >=0.14.1,+ strict >=0.3.2,+ string-conversions >=0.4.0.1,+ tasty >=1.1.0.2,+ tasty-quickcheck >=0.10,+ text >=1.2.3.0,+ tree-diff >=0.0.1,+ vector >=0.12.0.1,+ wai >=3.2.1.2,+ warp >=3.2.23
src/Test/StateMachine.hs view
@@ -1,13 +1,3 @@-{-# OPTIONS_GHC -Wno-orphans #-}--{-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}- ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine@@ -26,269 +16,41 @@ module Test.StateMachine ( -- * Sequential property combinators- Program- , programLength- , forAllProgram- , monadicSequential- , runProgram- , prettyProgram- , actionNames- , checkActionNames-- -- * Parallel property combinators- , ParallelProgram- , History- , monadicParallel- , runParallelProgram- , runParallelProgram'- , prettyParallelProgram+ forAllCommands+ , transitionMatrix+ , modelCheck+ , runCommands+ , prettyCommands+ , checkCommandNames+ , commandNames+ , commandNamesInOrder - -- * With counterexamples- , forAllProgramC- , monadicSequentialC- , monadicParallelC+ -- * Parallel property combinators+ , forAllParallelCommands+ , runParallelCommands+ , runParallelCommandsNTimes+ , prettyParallelCommands -- * Types- , module Test.StateMachine.Types+ , StateMachine(StateMachine)+ , Concrete+ , Symbolic+ , Reference+ , concrete+ , reference+ , Opaque(..)+ , opaque+ , Reason(..)+ , GenSym+ , genSym - -- * Reexport- , Test.QuickCheck.quickCheck- ) where+ , module Test.StateMachine.Logic -import Control.Monad.IO.Class- (MonadIO)-import Control.Monad.State- (evalStateT, replicateM)-import Control.Monad.Trans.Control- (MonadBaseControl)-import Data.Functor.Classes- (Show1)-import Data.Map- (Map)-import qualified Data.Map as M-import Data.Typeable- (Typeable)-import Test.QuickCheck- (Property, Testable, collect, cover, ioProperty,- property)-import qualified Test.QuickCheck-import Test.QuickCheck.Counterexamples- ((:&:)(..), PropertyOf)-import qualified Test.QuickCheck.Counterexamples as CE-import Test.QuickCheck.Monadic- (PropertyM, monadic, run)-import Test.QuickCheck.Property- (succeeded)+ ) where -import Test.StateMachine.Internal.Parallel-import Test.StateMachine.Internal.Sequential-import Test.StateMachine.Internal.Types-import Test.StateMachine.Internal.Utils- (forAllShrinkShowC, whenFailM)+import Prelude+ ()+import Test.StateMachine.Logic+import Test.StateMachine.Parallel+import Test.StateMachine.Sequential import Test.StateMachine.Types-import Test.StateMachine.Types.History------------------------------------------------------------------------------ | This function is like a 'forAllShrink' for sequential programs.-forAllProgram- :: HFoldable act- => Generator model act- -> Shrinker act- -> Precondition model act- -> Transition' model act err- -> InitialModel model- -> (Program act -> Property) -- ^ Predicate that should hold for all- -- programs.- -> Property-forAllProgram generator shrinker precondition transition model =- property- . forAllProgramC generator shrinker precondition transition model- . \prop p -> CE.property (prop p)---- | Variant of 'forAllProgram' which returns the generated and shrunk--- program if the property fails.-forAllProgramC- :: HFoldable act- => Generator model act- -> Shrinker act- -> Precondition model act- -> Transition' model act err- -> InitialModel model- -> (Program act -> PropertyOf a) -- ^ Predicate that should hold for all- -- programs.- -> PropertyOf (Program act :&: a)-forAllProgramC generator shrinker precondition transition model =- forAllShrinkShowC- (evalStateT (generateProgram generator precondition transition 0) model)- (shrinkProgram shrinker precondition transition model)- (const "")---- | Wrapper around 'forAllProgram' using the 'StateMachine' specification--- to generate and shrink sequential programs.-monadicSequential- :: Monad m- => HFoldable act- => Testable a- => StateMachine' model act m err- -> (Program act -> PropertyM m a)- -- ^ Predicate that should hold for all programs.- -> Property-monadicSequential sm = property . monadicSequentialC sm---- | Variant of 'monadicSequential' with counterexamples.-monadicSequentialC- :: Monad m- => HFoldable act- => Testable a- => StateMachine' model act m err- -> (Program act -> PropertyM m a)- -- ^ Predicate that should hold for all programs.- -> PropertyOf (Program act)-monadicSequentialC StateMachine {..} predicate- = fmap (\(prog :&: ()) -> prog)- . forAllProgramC generator' shrinker' precondition' transition' model'- $ CE.property- . monadic (ioProperty . runner')- . predicate--#if !MIN_VERSION_QuickCheck(2,10,0)-instance Testable () where- property = property . liftUnit- where- liftUnit () = succeeded-#endif---- | Testable property of sequential programs derived from a--- 'StateMachine' specification.-runProgram- :: Monad m- => Show1 (act Symbolic)- => Show err- => Typeable err- => HTraversable act- => StateMachine' model act m err- -- ^- -> Program act- -> PropertyM m (History act err, model Concrete, Reason)-runProgram sm = run . executeProgram sm---- | Takes the output of running a program and pretty prints a--- counterexample if the run failed.-prettyProgram- :: MonadIO m- => Show (model Concrete)- => Show err- => StateMachine' model act m err- -> History act err- -> Property- -> PropertyM m ()-prettyProgram StateMachine{..} hist prop =- putStrLn (ppHistory model' transition' hist) `whenFailM` prop---- | Print distribution of actions and fail if some actions have not been--- executed.-checkActionNames :: Constructors act => Program act -> Property -> Property-checkActionNames prog- = collect names- . cover (length names == numOfConstructors) 1 "coverage"- where- names = actionNames prog- numOfConstructors = nConstructors prog---- | Returns the frequency of actions in a program.-actionNames :: forall act. Constructors act => Program act -> [(Constructor, Int)]-actionNames = M.toList . foldl go M.empty . unProgram- where- go :: Map Constructor Int -> Internal act -> Map Constructor Int- go ih (Internal act _) = M.insertWith (+) (constructor act) 1 ih------------------------------------------------------------------------------ | This function is like a 'forAllShrink' for parallel programs.-forAllParallelProgramC- :: Show1 (act Symbolic)- => Eq (Untyped act)- => HFoldable act- => Generator model act- -> Shrinker act- -> Precondition model act- -> Transition' model act err- -> InitialModel model- -> (ParallelProgram act -> PropertyOf a) -- ^ Predicate that should hold- -- for all parallel programs.- -> PropertyOf (ParallelProgram act :&: a)-forAllParallelProgramC generator shrinker precondition transition model =- forAllShrinkShowC- (generateParallelProgram generator precondition transition model)- (shrinkParallelProgram shrinker precondition transition model)- (const "")---- | Wrapper around 'forAllParallelProgram using the 'StateMachine'--- specification to generate and shrink parallel programs.-monadicParallel- :: MonadBaseControl IO m- => Eq (Untyped act)- => Show1 (act Symbolic)- => HFoldable act- => StateMachine' model act m err- -> (ParallelProgram act -> PropertyM m ())- -- ^ Predicate that should hold for all parallel programs.- -> Property-monadicParallel sm = property . monadicParallelC sm---- | Variant of 'monadicParallel' with counterexamples.-monadicParallelC- :: MonadBaseControl IO m- => Eq (Untyped act)- => Show1 (act Symbolic)- => HFoldable act- => StateMachine' model act m err- -> (ParallelProgram act -> PropertyM m ())- -- ^ Predicate that should hold for all parallel programs.- -> PropertyOf (ParallelProgram act)-monadicParallelC StateMachine {..} predicate- = fmap (\(prog :&: ()) -> prog)- . forAllParallelProgramC generator' shrinker' precondition' transition' model'- $ CE.property- . monadic (ioProperty . runner')- . predicate---- | Testable property of parallel programs derived from a--- 'StateMachine' specification.-runParallelProgram- :: MonadBaseControl IO m- => Show1 (act Symbolic)- => HTraversable act- => StateMachine' model act m err- -- ^- -> ParallelProgram act- -> PropertyM m [(History act err, Property)]-runParallelProgram = runParallelProgram' 10--runParallelProgram'- :: MonadBaseControl IO m- => Show1 (act Symbolic)- => HTraversable act- => Int -- ^ How many times to execute the parallel program.- -> StateMachine' model act m err- -- ^- -> ParallelProgram act- -> PropertyM m [(History act err, Property)]-runParallelProgram' n StateMachine {..} prog =- replicateM n $ do- hist <- run (executeParallelProgram semantics' prog)- return (hist, linearise transition' postcondition' model' hist)---- | Takes the output of a parallel program runs and pretty prints a--- counter example if any of the runs fail.-prettyParallelProgram- :: MonadIO m- => HFoldable act- => Show (Untyped act)- => ParallelProgram act- -> [(History act err, Property)] -- ^ Output of 'runParallelProgram.- -> PropertyM m ()-prettyParallelProgram prog- = mapM_ (\(hist, prop) ->- print (toBoxDrawings prog hist) `whenFailM` prop)
+ src/Test/StateMachine/BoxDrawer.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE DeriveFunctor #-}++-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.BoxDrawer+-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Mats Daniel Gustafsson <daniel@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains functions for visualing a history of a parallel+-- execution.+--+-----------------------------------------------------------------------------++module Test.StateMachine.BoxDrawer+ ( EventType(..)+ , Fork(..)+ , exec+ ) where++import Prelude+import Text.PrettyPrint.ANSI.Leijen+ (Doc, text, vsep)++import Test.StateMachine.Types+ (Pid(..))++------------------------------------------------------------------------++-- | Event invocation or response.+data EventType = Open | Close+ deriving (Show)++data Event = Event EventType Pid String++data Cmd = Top | Start String | Active | Deactive | Ret String | Bottom++compile :: [Event] -> ([Cmd], [Cmd])+compile = go (Deactive, Deactive)+ where+ infixr 9 `add`+ add :: (a,b) -> ([a], [b]) -> ([a], [b])+ add (x,y) (xs, ys) = (x:xs, y:ys)++ set :: (a, a) -> Pid -> a -> (a, a)+ set (_x, y) (Pid 1) x' = (x', y)+ set (x, _y) (Pid 2) y' = (x, y')+ set _ pid _ = error $ "compile.set: unknown pid " ++ show pid++ go :: (Cmd, Cmd) -> [Event] -> ([Cmd], [Cmd])+ go _ [] = ([], [])+ go st (Event Open pid l : rest) =+ set st pid Top `add` set st pid (Start l) `add` go (set st pid Active) rest+ go st (Event Close pid l : rest) =+ set st pid (Ret l) `add` set st pid Bottom `add` go (set st pid Deactive) rest++size :: Cmd -> Int+size Top = 4+size (Start l) = 6 + length l+size Active = 2+size Deactive = 0+size (Ret l) = 4 + length l+size Bottom = 4++adjust :: Int -> Cmd -> String+adjust n Top = "┌" ++ replicate (n - 4) '─' ++ "┐"+adjust n (Start l) = "│ " ++ l ++ replicate (n - length l - 6) ' ' ++ " │"+adjust n Active = "│" ++ replicate (n - 4) ' ' ++ "│"+adjust n Deactive = replicate (n - 2) ' '+adjust n (Ret l) = "│ " ++ replicate (n - 8 - length l) ' ' ++ "→ " ++ l ++ " │"+adjust n Bottom = "└" ++ replicate (n - 4) '─' ++ "┘"++next :: ([Cmd], [Cmd]) -> [String]+next (left, right) = take (length left `max` length right) $ zipWith merge left' right'+ where+ left' = map (adjust $ maximum $ 0:map size left) (left ++ repeat Deactive)+ right' = map (adjust $ maximum $ 0:map size right) (right ++ repeat Deactive)+ merge x y = x ++ " │ " ++ y++toEvent :: [(EventType, Pid)] -> ([String], [String]) -> [Event]+toEvent [] ([], []) = []+toEvent [] ps = error $ "toEvent: residue inputs: " ++ show ps+toEvent ((e , Pid 1):evT) (x:xs, ys) = Event e (Pid 1) x : toEvent evT (xs, ys)+toEvent ((_e, Pid 1):_evT) ([] , _ys) = error "toEvent: no input from pid 1"+toEvent ((e , Pid 2):evT) (xs , y:ys) = Event e (Pid 2) y : toEvent evT (xs, ys)+toEvent ((_e, Pid 2):_evT) (_xs , []) = error "toEvent: no input from pid 2"+toEvent (e : _) _ = error $ "toEvent: unknown pid " ++ show e++compilePrefix :: [String] -> [Cmd]+compilePrefix [] = []+compilePrefix (cmd:res:prefix) = Top : Start cmd : Ret res : Bottom : compilePrefix prefix+compilePrefix [cmd] = error $ "compilePrefix: doesn't have response for cmd: " ++ cmd++data Fork a = Fork a a a+ deriving Functor++-- | Given a history, and output from processes generate Doc with boxes+exec :: [(EventType, Pid)] -> Fork [String] -> Doc+exec evT (Fork lops pops rops) = vsep $ map text (preBoxes ++ parBoxes)+ where+ preBoxes = map (adjust $ maximum $ 0:map ((2+) . length) (take 1 parBoxes)) $ compilePrefix pops+ parBoxes = next . compile $ toEvent evT (lops, rops)
+ src/Test/StateMachine/ConstructorName.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Test.StateMachine.ConstructorName+ ( GConName+ , gconName+ , gconNames+ , GConName1+ , gconName1+ , gconNames1+ )+ where++import Data.Proxy+ (Proxy(Proxy))+import GHC.Generics+ ((:*:)((:*:)), (:+:)(L1, R1), C, Constructor, D,+ Generic1, K1, M1, Rec1, Rep1, S, U1, conName, from1,+ unM1, unRec1)+import Prelude++import Test.StateMachine.Types+ (Command(..), Reference, Symbolic)++------------------------------------------------------------------------++class GConName a where+ gconName :: a -> String+ gconNames :: Proxy a -> [String]++class GConName1 f where+ gconName1 :: f a -> String+ gconNames1 :: Proxy (f a) -> [String]++instance GConName1 U1 where+ gconName1 _ = ""+ gconNames1 _ = []++instance GConName1 (K1 i c) where+ gconName1 _ = ""+ gconNames1 _ = []++instance Constructor c => GConName1 (M1 C c f) where+ gconName1 = conName+ gconNames1 (_ :: Proxy (M1 C c f p)) = [ conName @c undefined ] -- Can we do+ -- better+ -- here?++instance GConName1 f => GConName1 (M1 D c f) where+ gconName1 = gconName1 . unM1+ gconNames1 (_ :: Proxy (M1 D c f p)) = gconNames1 (Proxy :: Proxy (f p))++instance GConName1 f => GConName1 (M1 S c f) where+ gconName1 = gconName1 . unM1+ gconNames1 (_ :: Proxy (M1 S c f p)) = gconNames1 (Proxy :: Proxy (f p))++instance (GConName1 f, GConName1 g) => GConName1 (f :+: g) where+ gconName1 (L1 x) = gconName1 x+ gconName1 (R1 y) = gconName1 y++ gconNames1 (_ :: Proxy ((f :+: g) a)) =+ gconNames1 (Proxy :: Proxy (f a)) +++ gconNames1 (Proxy :: Proxy (g a))++instance (GConName1 f, GConName1 g) => GConName1 (f :*: g) where+ gconName1 (x :*: y) = gconName1 x ++ gconName1 y+ gconNames1 (_ :: Proxy ((f :*: g) a)) =+ gconNames1 (Proxy :: Proxy (f a)) +++ gconNames1 (Proxy :: Proxy (g a))++instance GConName1 f => GConName1 (Rec1 f) where+ gconName1 = gconName1 . unRec1+ gconNames1 (_ :: Proxy (Rec1 f p)) = gconNames1 (Proxy :: Proxy (f p))++------------------------------------------------------------------------++instance GConName1 (Reference a) where+ gconName1 _ = ""+ gconNames1 _ = []++instance (Generic1 cmd, GConName1 (Rep1 cmd)) => GConName (Command cmd) where+ gconName (Command cmd _) = gconName1 (from1 cmd)+ gconNames _ = gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))
− src/Test/StateMachine/Internal/Parallel.hs
@@ -1,349 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.Parallel--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH--- License : BSD-style (see the file LICENSE)------ Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ This module contains helpers for generating, shrinking, and checking--- parallel programs.-----------------------------------------------------------------------------------module Test.StateMachine.Internal.Parallel- ( generateParallelProgram- , shrinkParallelProgram- , validParallelProgram- , executeParallelProgram- , linearise- , toBoxDrawings- ) where--import Control.Arrow- ((***))-import Control.Concurrent.Async.Lifted- (concurrently)-import Control.Concurrent.Lifted- (threadDelay)-import Control.Concurrent.STM- (atomically)-import Control.Concurrent.STM.TChan- (TChan, newTChanIO, writeTChan)-import Control.Monad- (foldM, forM_)-import Control.Monad.State- (StateT, evalStateT, execStateT, get,- lift, modify)-import Control.Monad.Trans.Control- (MonadBaseControl, liftBaseWith)-import Data.Bifunctor- (bimap)-import Data.Dynamic- (toDyn)-import Data.Functor.Classes- (Show1, showsPrec1)-import Data.List- (partition, permutations)-import Data.Monoid- ((<>))-import Data.Set- (Set)-import qualified Data.Set as S-import Data.Tree- (Tree(Node))-import Test.QuickCheck- (Gen, Property, choose, property, shrinkList, sized,- (.&&.))-import Text.PrettyPrint.ANSI.Leijen- (Doc)--import Test.StateMachine.Internal.Sequential-import Test.StateMachine.Internal.Types-import Test.StateMachine.Internal.Types.Environment-import Test.StateMachine.Internal.Utils-import Test.StateMachine.Internal.Utils.BoxDrawer-import Test.StateMachine.Types hiding- (StateMachine'(..))-import Test.StateMachine.Types.History------------------------------------------------------------------------------ | Generate a parallel program whose actions all respect their--- pre-conditions.-generateParallelProgram- :: Generator model act- -> Precondition model act- -> Transition' model act err- -> model Symbolic- -> Gen (ParallelProgram act)-generateParallelProgram generator precondition transition model = do- Program is <- generateProgram' generator precondition transition model- prefixLength <- sized (\k -> choose (0, k `div` 3))- let (prefix, rest) = bimap Program Program (splitAt prefixLength is)- return (ParallelProgram prefix- (splitProgram precondition transition (advanceModel transition model prefix) rest))---- | Shrink a parallel program in a pre-condition and scope respecting--- way.-shrinkParallelProgram- :: forall act model err- . HFoldable act- => Eq (Untyped act)- => Shrinker act- -> Precondition model act- -> Transition' model act err- -> model Symbolic- -> (ParallelProgram act -> [ParallelProgram act])-shrinkParallelProgram shrinker precondition transition model (ParallelProgram prefix suffixes)- = filter (validParallelProgram precondition transition model)- [ ParallelProgram prefix' suffixes'- | (prefix', suffixes') <- shrinkPair' shrinkProgram' shrinkSuffixes (prefix, suffixes)- ]- ++- shrinkMoveSuffixToPrefix- where- shrinkProgram' :: Program act -> [Program act]- shrinkProgram'- = map Program- . shrinkList (liftShrinkInternal shrinker)- . unProgram-- shrinkSuffixes :: [(Program act, Program act)] -> [[(Program act, Program act)]]- shrinkSuffixes = shrinkList (shrinkPair shrinkProgram')-- shrinkMoveSuffixToPrefix :: [ParallelProgram act]- shrinkMoveSuffixToPrefix = case suffixes of- [] -> []- (suffix : suffixes') ->- [ ParallelProgram (prefix <> Program [prefix'])- (bimap Program Program suffix' : suffixes')- | (prefix', suffix') <- pickOneReturnRest2 (unProgram (fst suffix),- unProgram (snd suffix))- ]-- pickOneReturnRest :: [a] -> [(a, [a])]- pickOneReturnRest [] = []- pickOneReturnRest (x : xs) = (x, xs) : map (id *** (x :)) (pickOneReturnRest xs)-- pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a],[a]))]- pickOneReturnRest2 (xs, ys) =- map (id *** flip (,) ys) (pickOneReturnRest xs) ++- map (id *** (,) xs) (pickOneReturnRest ys)--validParallelProgram- :: HFoldable act- => Precondition model act- -> Transition' model act err- -> model Symbolic- -> ParallelProgram act- -> Bool-validParallelProgram precondition transition model (ParallelProgram prefix suffixes)- = validProgram precondition transition model prefix- && validSuffixes precondition transition prefixModel prefixScope (parallelProgramToList suffixes)- where- prefixModel = advanceModel transition model prefix- prefixScope = boundVars prefix--boundVars :: Program act -> Set Var-boundVars- = foldMap (\(Internal _ (Symbolic var)) -> S.singleton var)- . unProgram--usedVars :: HFoldable act => Program act -> Set Var-usedVars- = foldMap (\(Internal act _) -> hfoldMap (\(Symbolic var) -> S.singleton var) act)- . unProgram--validSuffixes- :: forall act model err- . HFoldable act- => Precondition model act- -> Transition' model act err- -> model Symbolic- -> Set Var- -> [Program act]- -> Bool-validSuffixes precondition transition model0 scope0 = go model0 scope0- where- go :: model Symbolic -> Set Var -> [Program act] -> Bool- go _ _ [] = True- go model scope (prog : progs)- = usedVars prog `S.isSubsetOf` scope' -- This assumes that variables- -- are bound before used in a- -- program.- && parallelSafe precondition transition model prog- && go (advanceModel transition model prog) scope' progs- where- scope' = boundVars prog `S.union` scope--runMany- :: MonadBaseControl IO m- => HTraversable act- => Show1 (act Symbolic)- => Semantics' act m err- -> TChan (HistoryEvent (UntypedConcrete act) err)- -> Pid- -> [Internal act]- -> StateT Environment m ()-runMany semantics hchan pid = flip foldM () $ \_ (Internal act sym@(Symbolic var)) -> do- env <- get- case reify env act of- Left _ -> return () -- The reference that the action uses failed to- -- create.- Right cact -> do- liftBaseWith $ const $ atomically $ writeTChan hchan $- InvocationEvent (UntypedConcrete cact) (showsPrec1 10 act "") var pid- mresp <- lift (semantics cact)- threadDelay 10- case mresp of- Fail err ->- liftBaseWith $ const $- atomically $ writeTChan hchan $ ResponseEvent (Fail err) "<fail>" pid- Success resp -> do- modify (insertConcrete sym (Concrete resp))- liftBaseWith $ const $- atomically $ writeTChan hchan $ ResponseEvent (Success (toDyn resp)) (show resp) pid---- | Run a parallel program, by first executing the prefix sequentially--- and then the suffixes in parallel, and return the history (or--- trace) of the execution.-executeParallelProgram- :: forall m act err- . MonadBaseControl IO m- => HTraversable act- => Show1 (act Symbolic)- => Semantics' act m err- -> ParallelProgram act- -> m (History act err)-executeParallelProgram semantics (ParallelProgram prefix suffixes) = do- hchan <- liftBaseWith (const newTChanIO)- env <- execStateT- (runMany semantics hchan (Pid 0) (unProgram prefix))- emptyEnvironment- forM_ suffixes $ \(prog1, prog2) -> do- _ <- concurrently- (evalStateT (runMany semantics hchan (Pid 1) (unProgram prog1)) env)- (evalStateT (runMany semantics hchan (Pid 2) (unProgram prog2)) env)- return ()-- History <$> liftBaseWith (const (getChanContents hchan))------------------------------------------------------------------------------ | Try to linearise a history of a parallel program execution using a--- sequential model. See the *Linearizability: a correctness condition for--- concurrent objects* paper linked to from the README for more info.-linearise- :: forall model act err- . Transition' model act err- -> Postcondition' model act err- -> InitialModel model- -> History act err- -> Property-linearise transition postcondition model0 = go . unHistory- where- go :: History' act err -> Property- go [] = property True- go es = anyP (step model0) (linearTree es)-- step :: model Concrete -> Tree (Operation act err) -> Property- step model (Node (Operation act _ resp _ _) roses) =- postcondition model act resp .&&.- anyP' (step (transition model act (fmap Concrete resp))) roses--anyP' :: (a -> Property) -> [a] -> Property-anyP' _ [] = property True-anyP' p xs = anyP p xs------------------------------------------------------------------------------ | Draw an ASCII diagram of the history of a parallel program. Useful for--- seeing how a race condition might have occured.-toBoxDrawings :: HFoldable act => ParallelProgram act -> History act err -> Doc-toBoxDrawings (ParallelProgram prefix suffixes) = toBoxDrawings'' allVars- where- allVars = usedVars prefix `S.union` foldMap usedVars (parallelProgramToList suffixes)-- toBoxDrawings'' :: Set Var -> History act err -> Doc- toBoxDrawings'' knownVars (History h) = exec evT (fmap out <$> Fork l p r)- where- (p, h') = partition (\e -> getProcessIdEvent e == Pid 0) h- (l, r) = partition (\e -> getProcessIdEvent e == Pid 1) h'-- out :: HistoryEvent act err -> String- out (InvocationEvent _ str var _)- | var `S.member` knownVars = show var ++ " ← " ++ str- | otherwise = str- out (ResponseEvent _ str _) = str-- toEventType :: [HistoryEvent act err] -> [(EventType, Pid)]- toEventType = map go- where- go e = case e of- InvocationEvent _ _ _ pid -> (Open, pid)- ResponseEvent _ _ pid -> (Close, pid)-- evT :: [(EventType, Pid)]- evT = toEventType (filter (\e -> getProcessIdEvent e `elem` map Pid [1,2]) h)----------------------------------------------------------------------------splitProgram- :: Precondition model act- -> Transition' model act err- -> model Symbolic- -> Program act- -> [(Program act, Program act)]-splitProgram precondition transition model0 = go model0 [] . unProgram- where- go _ acc [] = reverse acc- go model acc iacts = go (advanceModel transition model (Program safe))- ((Program safe1, Program safe2) : acc)- rest- where- (safe, rest) = spanSafe model [] iacts- (safe1, safe2) = splitAt (length safe `div` 2) safe-- spanSafe _ safe [] = (reverse safe, [])- spanSafe model safe (iact@(Internal _ _) : iacts)- | length safe <= 5 && parallelSafe precondition transition model (Program (iact : safe))- = spanSafe model (iact : safe) iacts- | otherwise- = (reverse safe, iact : iacts)--parallelSafe- :: Precondition model act- -> Transition' model act err- -> model Symbolic- -> Program act- -> Bool-parallelSafe precondition transition model0- = and- . map (preconditionsHold model0)- . permutations- . unProgram- where- preconditionsHold _ [] = True- preconditionsHold model (Internal act sym : iacts)- = precondition model act- && preconditionsHold (transition model act (Success sym)) iacts--advanceModel- :: Transition' model act err- -> model Symbolic- -> Program act- -> model Symbolic-advanceModel transition model0 = go model0 . unProgram- where- go model [] = model- go model (Internal act sym : iacts) =- go (transition model act (Success sym)) iacts
− src/Test/StateMachine/Internal/Sequential.hs
@@ -1,217 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE ScopedTypeVariables #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.Sequential--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH--- License : BSD-style (see the file LICENSE)------ Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ This module contains helpers for generating, shrinking, and checking--- sequential programs.-----------------------------------------------------------------------------------module Test.StateMachine.Internal.Sequential- ( generateProgram- , generateProgram'- , filterInvalid- , getUsedVars- , liftShrinkInternal- , validProgram- , shrinkProgram- , executeProgram- )- where--import Control.Monad- (filterM, when)-import Control.Monad.State- (State, StateT, evalStateT, get, lift,- put)-import Data.Dynamic- (toDyn)-import Data.Functor.Classes- (Show1, showsPrec1)-import Data.Monoid- ((<>))-import Data.Set- (Set)-import qualified Data.Set as S-import Data.Typeable- (Typeable)-import Test.QuickCheck- (Gen, choose, shrinkList, sized, suchThat)--import Test.StateMachine.Internal.Types-import Test.StateMachine.Internal.Types.Environment-import Test.StateMachine.Types-import Test.StateMachine.Types.History------------------------------------------------------------------------------ | Generate programs whose actions all respect their pre-conditions.-generateProgram- :: forall model act err- . Generator model act- -> Precondition model act- -> Transition' model act err- -> Int -- ^ Name supply for symbolic variables.- -> StateT (model Symbolic) Gen (Program act)-generateProgram generator precondition transition index = do- size <- lift (sized (\k -> choose (0, k)))- Program <$> go size index- where- go :: Int -> Int -> StateT (model Symbolic) Gen [Internal act]- go 0 _ = return []- go sz ix = do- model <- get- Untyped act <- lift (generator model `suchThat`- \(Untyped act) -> precondition model act)- let sym = Symbolic (Var ix)- put (transition model act (Success sym))- acts <- go (sz - 1) (ix + 1)- return (Internal act sym : acts)--generateProgram'- :: Generator model act- -> Precondition model act- -> Transition' model act err- -> model Symbolic- -> Gen (Program act)-generateProgram' g p t = evalStateT (generateProgram g p t 0)---- | Filter out invalid actions from a program. An action is invalid if--- either its pre-condition doesn't hold, or it uses references that--- are not in scope.-filterInvalid- :: HFoldable act- => Precondition model act- -> Transition' model act err- -> Program act- -> State (model Symbolic, Set Var) (Program act) -- ^ Where @Set Var@- -- is the scope.-filterInvalid precondition transition- = fmap Program- . filterM go- . unProgram- where- go (Internal act sym@(Symbolic var)) = do- (model, scope) <- get- let valid = precondition model act && getUsedVars act `S.isSubsetOf` scope- when valid (put (transition model act (Success sym), S.insert var scope))- return valid---- | Returns the set of references an action uses.-getUsedVars :: HFoldable act => act Symbolic a -> Set Var-getUsedVars = hfoldMap (\(Symbolic v) -> S.singleton v)---- | Given a shrinker of typed actions we can lift it to a shrinker of--- internal actions.-liftShrinkInternal :: Shrinker act -> (Internal act -> [Internal act])-liftShrinkInternal shrinker (Internal act sym) =- [ Internal act' sym | act' <- shrinker act ]--validProgram- :: forall act model err- . HFoldable act- => Precondition model act- -> Transition' model act err- -> model Symbolic- -> Program act- -> Bool-validProgram precondition transition model0 = go model0 S.empty . unProgram- where- go :: model Symbolic -> Set Var -> [Internal act] -> Bool- go _ _ [] = True- go model scope (Internal act sym@(Symbolic var) : is) =- valid && go (transition model act (Success sym)) (S.insert var scope) is- where- valid = precondition model act && getUsedVars act `S.isSubsetOf` scope---- | Shrink a program in a pre-condition and scope respecting way.-shrinkProgram- :: HFoldable act- => Shrinker act- -> Precondition model act- -> Transition' model act err- -> model Symbolic- -> Program act -- ^ Program to shrink.- -> [Program act]-shrinkProgram shrinker precondition transition model- = filter (validProgram precondition transition model)- . map Program- . shrinkList (liftShrinkInternal shrinker)- . unProgram---- | Execute a program and return a history, the final model and a result which--- contains the information of whether the execution respects the state--- machine model or not.-executeProgram- :: forall m act model err- . Monad m- => Typeable err- => Show1 (act Symbolic)- => Show err- => HTraversable act- => StateMachine' model act m err- -> Program act- -> m (History act err, model Concrete, Reason)-executeProgram StateMachine{..}- = fmap (\(hist, _, cmodel, _, reason) -> (hist, cmodel, reason))- . go (mempty, model', model', emptyEnvironment)- . unProgram- where- go :: (History act err, model Symbolic, model Concrete, Environment)- -> [Internal act]- -> m (History act err, model Symbolic, model Concrete, Environment, Reason)- go (hist, smodel, cmodel, env) [] =- return (hist, smodel, cmodel, env, Ok)- go (hist, smodel, cmodel, env) (Internal act sym@(Symbolic var) : acts) =- if not (precondition' smodel act)- then- return ( hist- , smodel- , cmodel- , env- , PreconditionFailed- )- else do- let Right cact = reify env act- resp <- semantics' cact- let hist' = hist <> History- [ InvocationEvent (UntypedConcrete cact) (showsPrec1 10 act "") var (Pid 0)- , ResponseEvent (fmap toDyn resp) (ppResult resp) (Pid 0)- ]- if not (postcondition' cmodel cact resp)- then- return ( hist'- , smodel- , cmodel- , env- , PostconditionFailed- )- else- case resp of-- Fail err ->- go ( hist'- , transition' smodel act (Fail err)- , transition' cmodel cact (Fail err)- , env- )- acts-- Success resp' ->- go ( hist'- , transition' smodel act (Success sym)- , transition' cmodel cact (fmap Concrete resp)- , insertConcrete sym (Concrete resp') env- )- acts
− src/Test/StateMachine/Internal/Types.hs
@@ -1,138 +0,0 @@-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE UndecidableInstances #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.Types--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH--- License : BSD-style (see the file LICENSE)------ Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ This module exports some types that are used internally by the library.-----------------------------------------------------------------------------------module Test.StateMachine.Internal.Types- ( Program(..)- , programLength- , ParallelProgram(..)- , parallelProgramLength- , parallelProgramToList- , parallelProgramFromList- , parallelProgramAsList- , flattenParallelProgram- , Pid(..)- , Internal(..)- ) where--import Data.Bifunctor- (bimap)-import Data.Monoid- ((<>))-import Data.Typeable- (Typeable)-import Text.Read- (Lexeme(Ident), lexP, parens, prec, readPrec, step)--import Test.StateMachine.Types- (Untyped(Untyped))-import Test.StateMachine.Types.References------------------------------------------------------------------------------ | A (sequential) program is an abstract datatype representing a list--- of actions.------ The idea is that the user shows how to generate, shrink, execute and--- modelcheck individual actions, and then the below combinators lift--- those things to whole programs.-newtype Program act = Program { unProgram :: [Internal act] }--instance Eq (Internal act) => Eq (Program act) where- Program acts1 == Program acts2 = acts1 == acts2--instance Monoid (Program act) where- mempty = Program []- Program acts1 `mappend` Program acts2 = Program (acts1 ++ acts2)--deriving instance Show (Untyped act) => Show (Program act)-deriving instance Read (Untyped act) => Read (Program act)---- | Returns the number of actions in a program.-programLength :: Program act -> Int-programLength = length . unProgram----------------------------------------------------------------------------data ParallelProgram act- = ParallelProgram (Program act) [(Program act, Program act)]--deriving instance Eq (Untyped act) => Eq (ParallelProgram act)-deriving instance Show (Untyped act) => Show (ParallelProgram act)-deriving instance Read (Untyped act) => Read (ParallelProgram act)--parallelProgramLength :: ParallelProgram act -> Int-parallelProgramLength (ParallelProgram prefix suffixes) =- programLength prefix +- programLength (mconcat (parallelProgramToList suffixes))--parallelProgramFromList :: [Program act] -> [(Program act, Program act)]-parallelProgramFromList- = map (\prog -> bimap Program Program- (splitAt (programLength prog `div` 2) (unProgram prog)))--parallelProgramToList :: [(Program act, Program act)] -> [Program act]-parallelProgramToList = map (\(prog1, prog2) -> prog1 <> prog2)--parallelProgramAsList- :: ([Program act] -> [Program act])- -> [(Program act, Program act)]- -> [(Program act, Program act)]-parallelProgramAsList f = parallelProgramFromList . f . parallelProgramToList--flattenParallelProgram :: ParallelProgram act -> Program act-flattenParallelProgram (ParallelProgram prefix suffixes)- = prefix <> mconcat (parallelProgramToList suffixes)------------------------------------------------------------------------------ | An internal action is an action together with the symbolic variable--- that will hold its result.-data Internal (act :: (* -> *) -> * -> *) where- Internal :: (Show resp, Typeable resp) =>- act Symbolic resp -> Symbolic resp -> Internal act--instance Eq (Untyped act) => Eq (Internal act) where- Internal a1 _ == Internal a2 _ = Untyped a1 == Untyped a2--instance Show (Untyped act) => Show (Internal act) where- showsPrec p (Internal action v) = showParen (p > appPrec) $- showString "Internal " .- showsPrec (appPrec + 1) (Untyped action) .- showString " " .- showsPrec (appPrec + 1) v- where- appPrec = 10--instance Read (Untyped act) => Read (Internal act) where- readPrec = parens $- prec appPrec $ do- Ident "Internal" <- lexP- Untyped action <- step readPrec- v <- step readPrec- return (Internal action v)- where- appPrec = 10------------------------------------------------------------------------------ | A process id.-newtype Pid = Pid Int- deriving (Eq, Show)
− src/Test/StateMachine/Internal/Types/Environment.hs
@@ -1,93 +0,0 @@-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.Types.Environment--- Copyright : (C) 2017, Jacob Stanley--- License : BSD-style (see the file LICENSE)------ Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ This module contains environments that are used to translate between symbolic--- and concrete references. It's taken verbatim from the Hedgehog--- <https://hackage.haskell.org/package/hedgehog library>.-----------------------------------------------------------------------------------module Test.StateMachine.Internal.Types.Environment- ( Environment(..)- , EnvironmentError(..)- , emptyEnvironment- , insertConcrete- , reifyDynamic- , reifyEnvironment- , reify- ) where--import Data.Dynamic- (Dynamic, Typeable, dynTypeRep, fromDynamic, toDyn)-import Data.Map- (Map)-import qualified Data.Map as M-import Data.Typeable- (Proxy(Proxy), TypeRep, typeRep)--import Test.StateMachine.Types------------------------------------------------------------------------------ | A mapping of symbolic values to concrete values.----newtype Environment =- Environment {- unEnvironment :: Map Var Dynamic- } deriving (Show)---- | Environment errors.----data EnvironmentError =- EnvironmentValueNotFound !Var- | EnvironmentTypeError !TypeRep !TypeRep- deriving (Eq, Ord, Show)---- | Create an empty environment.----emptyEnvironment :: Environment-emptyEnvironment =- Environment M.empty---- | Insert a symbolic / concrete pairing in to the environment.----insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment-insertConcrete (Symbolic k) (Concrete v) =- Environment . M.insert k (toDyn v) . unEnvironment---- | Cast a 'Dynamic' in to a concrete value.----reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a)-reifyDynamic dyn =- case fromDynamic dyn of- Nothing ->- Left $ EnvironmentTypeError (typeRep (Proxy :: Proxy a)) (dynTypeRep dyn)- Just x ->- Right $ Concrete x---- | Turns an environment in to a function for looking up a concrete value from--- a symbolic one.----reifyEnvironment :: Environment -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))-reifyEnvironment (Environment vars) (Symbolic n) =- case M.lookup n vars of- Nothing ->- Left $ EnvironmentValueNotFound n- Just dyn ->- reifyDynamic dyn---- | Convert a symbolic structure to a concrete one, using the provided environment.----reify :: HTraversable t => Environment -> t Symbolic b -> Either EnvironmentError (t Concrete b)-reify vars =- htraverse (reifyEnvironment vars)
− src/Test/StateMachine/Internal/Utils.hs
@@ -1,113 +0,0 @@-{-# LANGUAGE TypeOperators #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.Utils--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH--- License : BSD-style (see the file LICENSE)------ Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)-----------------------------------------------------------------------------------module Test.StateMachine.Internal.Utils where--import Control.Concurrent.STM- (atomically)-import Control.Concurrent.STM.TChan- (TChan, tryReadTChan)-import Data.List- (group, sort)-import Test.QuickCheck- (Gen, Property, Testable, again, chatty,- counterexample, ioProperty, property, shrinking,- stdArgs, whenFail)-import Test.QuickCheck.Counterexamples- ((:&:)(..), Counterexample, PropertyOf)-import qualified Test.QuickCheck.Counterexamples as CE-import Test.QuickCheck.Monadic- (PropertyM(MkPropertyM), run)-import Test.QuickCheck.Property- (Property(MkProperty), unProperty)-import Test.QuickCheck.Property- ((.&&.), (.||.))------------------------------------------------------------------------------ | Lifts 'Prelude.any' to properties.-anyP :: (a -> Property) -> [a] -> Property-anyP p = foldr (\x ih -> p x .||. ih) (property False)---- | Lifts a plain property into a monadic property.-liftProperty :: Monad m => Property -> PropertyM m ()-liftProperty prop = MkPropertyM (\k -> fmap (prop .&&.) <$> k ())---- | Lifts 'whenFail' to 'PropertyM'.-whenFailM :: Monad m => IO () -> Property -> PropertyM m ()-whenFailM m prop = liftProperty (m `whenFail` prop)---- | A property that tests @prop@ repeatedly @n@ times, failing as soon as any--- of the tests of @prop@ fails.-alwaysP :: Int -> Property -> Property-alwaysP n prop- | n <= 0 = error "alwaysP: expected positive integer."- | n == 1 = prop- | otherwise = prop .&&. alwaysP (n - 1) prop---- | Given shrinkers for the components of a pair we can shrink the pair.-shrinkPair' :: (a -> [a]) -> (b -> [b]) -> ((a, b) -> [(a, b)])-shrinkPair' shrinkerA shrinkerB (x, y) =- [ (x', y) | x' <- shrinkerA x ] ++- [ (x, y') | y' <- shrinkerB y ]---- | Same above, but for homogeneous pairs.-shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)])-shrinkPair shrinker = shrinkPair' shrinker shrinker---- | A variant of 'Test.QuickCheck.Monadic.forAllShrink' with an explicit show--- function.-forAllShrinkShow- :: Testable prop- => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property-forAllShrinkShow gen shrinker shower pf =- again $- MkProperty $- gen >>= \x ->- unProperty $- shrinking shrinker x $ \x' ->- counterexample (shower x') (pf x')--forAllShrinkShowC- :: CE.Testable prop- => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> PropertyOf (a :&: Counterexample prop)-forAllShrinkShowC arb shr shower prop =- CE.MkProperty $ \f ->- forAllShrinkShow arb shr shower $ \x ->- CE.unProperty (CE.property (prop x)) (\y -> f (x :&: y))------------------------------------------------------------------------------ | Remove duplicate elements from a list.-nub :: Ord a => [a] -> [a]-nub = fmap head . group . sort---- | Drop last 'n' elements of a list.-dropLast :: Int -> [a] -> [a]-dropLast n xs = zipWith const xs (drop n xs)---- | Indexing starting from the back of a list.-toLast :: Int -> [a] -> a-toLast n = last . dropLast n----------------------------------------------------------------------------getChanContents :: TChan a -> IO [a]-getChanContents chan = reverse <$> atomically (go [])- where- go acc = do- mx <- tryReadTChan chan- case mx of- Just x -> go $ x : acc- Nothing -> return acc
− src/Test/StateMachine/Internal/Utils/BoxDrawer.hs
@@ -1,104 +0,0 @@-{-# LANGUAGE DeriveFunctor #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.Parallel--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH--- License : BSD-style (see the file LICENSE)------ Maintainer : Mats Daniel Gustafsson <daniel@advancedtelematic.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ This module contains functions for visualing a history of a parallel--- execution.-----------------------------------------------------------------------------------module Test.StateMachine.Internal.Utils.BoxDrawer- ( EventType(..)- , Fork(..)- , exec- ) where--import Text.PrettyPrint.ANSI.Leijen- (Doc, text, vsep)--import Test.StateMachine.Internal.Types- (Pid(..))------------------------------------------------------------------------------ | Event invocation or response.-data EventType = Open | Close- deriving (Show)--data Event = Event EventType Pid String--data Cmd = Top | Start String | Active | Deactive | Ret String | Bottom--compile :: [Event] -> ([Cmd], [Cmd])-compile = go (Deactive, Deactive)- where- infixr 9 `add`- add :: (a,b) -> ([a], [b]) -> ([a], [b])- add (x,y) (xs, ys) = (x:xs, y:ys)-- set :: (a, a) -> Pid -> a -> (a, a)- set (_x, y) (Pid 1) x' = (x', y)- set (x, _y) (Pid 2) y' = (x, y')- set _ pid _ = error $ "compile.set: unknown pid " ++ show pid-- go :: (Cmd, Cmd) -> [Event] -> ([Cmd], [Cmd])- go _ [] = ([], [])- go st (Event Open pid l : rest) =- set st pid Top `add` set st pid (Start l) `add` go (set st pid Active) rest- go st (Event Close pid l : rest) =- set st pid (Ret l) `add` set st pid Bottom `add` go (set st pid Deactive) rest--size :: Cmd -> Int-size Top = 4-size (Start l) = 6 + length l-size Active = 2-size Deactive = 0-size (Ret l) = 4 + length l-size Bottom = 4--adjust :: Int -> Cmd -> String-adjust n Top = "┌" ++ replicate (n - 4) '─' ++ "┐"-adjust n (Start l) = "│ " ++ l ++ replicate (n - length l - 6) ' ' ++ " │"-adjust n Active = "│" ++ replicate (n - 4) ' ' ++ "│"-adjust n Deactive = replicate (n - 2) ' '-adjust n (Ret l) = "│ " ++ replicate (n - 8 - length l) ' ' ++ "→ " ++ l ++ " │"-adjust n Bottom = "└" ++ replicate (n - 4) '─' ++ "┘"--next :: ([Cmd], [Cmd]) -> [String]-next (left, right) = take (length left `max` length right) $ zipWith merge left' right'- where- left' = map (adjust $ maximum $ 0:map size left) (left ++ repeat Deactive)- right' = map (adjust $ maximum $ 0:map size right) (right ++ repeat Deactive)- merge x y = x ++ " │ " ++ y--toEvent :: [(EventType, Pid)] -> ([String], [String]) -> [Event]-toEvent [] ([], []) = []-toEvent [] ps = error $ "toEvent: residue inputs: " ++ show ps-toEvent ((e , Pid 1):evT) (x:xs, ys) = Event e (Pid 1) x : toEvent evT (xs, ys)-toEvent ((_e, Pid 1):_evT) ([] , _ys) = error "toEvent: no input from pid 1"-toEvent ((e , Pid 2):evT) (xs , y:ys) = Event e (Pid 2) y : toEvent evT (xs, ys)-toEvent ((_e, Pid 2):_evT) (_xs , []) = error "toEvent: no input from pid 2"-toEvent (e : _) _ = error $ "toEvent: unknown pid " ++ show e--compilePrefix :: [String] -> [Cmd]-compilePrefix [] = []-compilePrefix (cmd:res:prefix) = Top : Start cmd : Ret res : Bottom : compilePrefix prefix-compilePrefix [cmd] = error $ "compilePrefix: doesn't have response for cmd: " ++ cmd--data Fork a = Fork a a a- deriving Functor---- | Given a history, and output from processes generate Doc with boxes-exec :: [(EventType, Pid)] -> Fork [String] -> Doc-exec evT (Fork lops pops rops) = vsep $ map text (preBoxes ++ parBoxes)- where- preBoxes = map (adjust $ maximum $ 0:map ((2+) . length) (take 1 parBoxes)) $ compilePrefix pops- parBoxes = next . compile $ toEvent evT (lops, rops)
src/Test/StateMachine/Logic.hs view
@@ -11,13 +11,41 @@ -- Stability : provisional -- Portability : non-portable (GHC extensions) ----- This module provides a propositional logic which gives counterexamples when--- the proposition is false.+-- This module defines a predicate logic-like language and its counterexample+-- semantics. -- ----------------------------------------------------------------------------- -module Test.StateMachine.Logic where+module Test.StateMachine.Logic+ ( Logic(..)+ , Predicate(..)+ , dual+ , strongNeg+ , Counterexample(..)+ , Value(..)+ , boolean+ , logic+ , predicate+ , (.==)+ , (./=)+ , (.<)+ , (.<=)+ , (.>)+ , (.>=)+ , elem+ , notElem+ , (.//)+ , forall+ , exists+ )+ where +import Prelude hiding+ (elem, notElem)+import qualified Prelude++------------------------------------------------------------------------+ infixr 1 :=> infixr 2 :|| infixr 3 :&&@@ -30,8 +58,10 @@ | Logic :=> Logic | Not Logic | Predicate Predicate+ | forall a. Show a => Forall [a] (a -> Logic)+ | forall a. Show a => Exists [a] (a -> Logic)+ | Boolean Bool | Annotate String Logic- deriving Show data Predicate = forall a. (Eq a, Show a) => a :== a@@ -58,7 +88,7 @@ -- See Yuri Gurevich's "Intuitionistic logic with strong negation" (1977). strongNeg :: Logic -> Logic-strongNeg l = case l of+strongNeg l0 = case l0 of Bot -> Top Top -> Bot l :&& r -> strongNeg l :|| strongNeg r@@ -66,6 +96,9 @@ l :=> r -> l :&& strongNeg r Not l -> l Predicate p -> Predicate (dual p)+ Forall xs p -> Exists xs (strongNeg . p)+ Exists xs p -> Forall xs (strongNeg . p)+ Boolean b -> Boolean (not b) Annotate s l -> Annotate s (strongNeg l) data Counterexample@@ -76,14 +109,23 @@ | ImpliesC Counterexample | NotC Counterexample | PredicateC Predicate+ | forall a. Show a => ForallC a Counterexample+ | forall a. Show a => ExistsC [a] [Counterexample]+ | BooleanC | AnnotateC String Counterexample- deriving Show +deriving instance Show Counterexample+ data Value = VFalse Counterexample | VTrue deriving Show +boolean :: Logic -> Bool+boolean l = case logic l of+ VFalse _ -> False+ VTrue -> True+ logic :: Logic -> Value logic Bot = VFalse BotC logic Top = VTrue@@ -106,21 +148,79 @@ VTrue -> VTrue VFalse ce -> VFalse (NotC ce) logic (Predicate p) = predicate p+logic (Forall xs0 p) = go xs0+ where+ go [] = VTrue+ go (x : xs) = case logic (p x) of+ VTrue -> go xs+ VFalse ce -> VFalse (ForallC x ce)+logic (Exists xs0 p) = go xs0 []+ where+ go [] ces = VFalse (ExistsC xs0 (reverse ces))+ go (x : xs) ces = case logic (p x) of+ VTrue -> VTrue+ VFalse ce -> go xs (ce : ces)+logic (Boolean b) = if b then VTrue else VFalse BooleanC logic (Annotate s l) = case logic l of VTrue -> VTrue VFalse ce -> VFalse (AnnotateC s ce) predicate :: Predicate -> Value-predicate p = let b = boolean p in case p of+predicate p0 = let b = go p0 in case p0 of x :== y -> b (x == y) x :/= y -> b (x /= y) x :< y -> b (x < y) x :<= y -> b (x <= y) x :> y -> b (x > y) x :>= y -> b (x >= y)- x `Elem` xs -> b (x `elem` xs)- x `NotElem` xs -> b (x `notElem` xs)+ x `Elem` xs -> b (x `Prelude.elem` xs)+ x `NotElem` xs -> b (x `Prelude.notElem` xs) where- boolean :: Predicate -> Bool -> Value- boolean p True = VTrue- boolean p False = VFalse (PredicateC (dual p))+ go :: Predicate -> Bool -> Value+ go _ True = VTrue+ go p False = VFalse (PredicateC (dual p))++------------------------------------------------------------------------++infix 5 .==+infix 5 ./=+infix 5 .<+infix 5 .<=+infix 5 .>+infix 5 .>=+infix 5 `elem`+infix 5 `notElem`+infixl 4 .//++(.==) :: (Eq a, Show a) => a -> a -> Logic+x .== y = Predicate (x :== y)++(./=) :: (Eq a, Show a) => a -> a -> Logic+x ./= y = Predicate (x :/= y)++(.<) :: (Ord a, Show a) => a -> a -> Logic+x .< y = Predicate (x :< y)++(.<=) :: (Ord a, Show a) => a -> a -> Logic+x .<= y = Predicate (x :<= y)++(.>) :: (Ord a, Show a) => a -> a -> Logic+x .> y = Predicate (x :> y)++(.>=) :: (Ord a, Show a) => a -> a -> Logic+x .>= y = Predicate (x :>= y)++elem :: (Eq a, Show a) => a -> [a] -> Logic+elem x xs = Predicate (Elem x xs)++notElem :: (Eq a, Show a) => a -> [a] -> Logic+notElem x xs = Predicate (NotElem x xs)++(.//) :: Logic -> String -> Logic+l .// s = Annotate s l++forall :: Show a => [a] -> (a -> Logic) -> Logic+forall = Forall++exists :: Show a => [a] -> (a -> Logic) -> Logic+exists = Exists
+ src/Test/StateMachine/Parallel.hs view
@@ -0,0 +1,383 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Parallel+-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains helpers for generating, shrinking, and checking+-- parallel programs.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Parallel+ ( forAllParallelCommands+ , generateParallelCommands+ , shrinkParallelCommands+ , validParallelCommands+ , prop_splitCombine+ , runParallelCommands+ , runParallelCommandsNTimes+ , linearise+ , toBoxDrawings+ , prettyParallelCommands+ ) where++import Control.Arrow+ ((***))+import Control.Concurrent.Async.Lifted+ (concurrently)+import Control.Concurrent.STM.TChan+ (newTChanIO)+import Control.Monad+ (foldM, replicateM)+import Control.Monad.Catch+ (MonadCatch)+import Control.Monad.State+ (MonadIO, State, evalState, put, runStateT)+import Control.Monad.Trans.Control+ (MonadBaseControl, liftBaseWith)+import Data.Bifunctor+ (bimap)+import Data.List+ (partition, permutations)+import Data.List.Split+ (splitPlacesBlanks)+import Data.Monoid+ ((<>))+import Data.Set+ (Set)+import qualified Data.Set as S+import Data.Tree+ (Tree(Node))+import GHC.Generics+ (Generic1, Rep1)+import Prelude+import Test.QuickCheck+ (Gen, Property, Testable, choose, property,+ shrinkList, sized)+import Test.QuickCheck.Monadic+ (PropertyM, run)+import Text.PrettyPrint.ANSI.Leijen+ (Doc)+import Text.Show.Pretty+ (ppShow)++import Test.StateMachine.BoxDrawer+import Test.StateMachine.ConstructorName+import Test.StateMachine.Logic+ (boolean)+import Test.StateMachine.Sequential+import Test.StateMachine.Types+import qualified Test.StateMachine.Types.Rank2 as Rank2+import Test.StateMachine.Utils++------------------------------------------------------------------------++forAllParallelCommands :: Testable prop+ => (Show (cmd Symbolic), Show (model Symbolic))+ => (Generic1 cmd, GConName1 (Rep1 cmd))+ => (Rank2.Foldable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp+ -> (ParallelCommands cmd -> prop) -- ^ Predicate.+ -> Property+forAllParallelCommands sm =+ forAllShrinkShow (generateParallelCommands sm) (shrinkParallelCommands sm) ppShow++generateParallelCommands :: forall model cmd m resp+ . (Rank2.Foldable resp, Show (model Symbolic))+ => (Generic1 cmd, GConName1 (Rep1 cmd))+ => StateMachine model cmd m resp+ -> Gen (ParallelCommands cmd)+generateParallelCommands sm@StateMachine { initModel } = do+ Commands cmds <- generateCommands sm Nothing+ prefixLength <- sized (\k -> choose (0, k `div` 3))+ let (prefix, rest) = bimap Commands Commands (splitAt prefixLength cmds)+ return (ParallelCommands prefix+ (makeSuffixes (advanceModel sm initModel newCounter prefix) rest))+ where+ makeSuffixes :: (model Symbolic, Counter) -> Commands cmd -> [Pair (Commands cmd)]+ makeSuffixes (model0, counter0) = go (model0, counter0) [] . unCommands+ where+ go _ acc [] = reverse acc+ go (model, counter) acc cmds = go (advanceModel sm model counter (Commands safe))+ (Pair (Commands safe1) (Commands safe2) : acc)+ rest+ where+ (safe, rest) = spanSafe model counter [] cmds+ (safe1, safe2) = splitAt (length safe `div` 2) safe++ suffixLength = 5++ spanSafe :: model Symbolic -> Counter -> [Command cmd] -> [Command cmd]+ -> ([Command cmd], [Command cmd])+ spanSafe _ _ safe [] = (reverse safe, [])+ spanSafe model counter safe (cmd@(Command _ _) : cmds)+ | length safe <= suffixLength &&+ parallelSafe sm model counter (Commands (cmd : safe)) =+ spanSafe model counter (cmd : safe) cmds+ | otherwise = (reverse safe, cmd : cmds)++-- | A list of commands is parallel safe if the pre-conditions for all commands+-- hold in all permutations of the list.+parallelSafe :: StateMachine model cmd m resp -> model Symbolic+ -> Counter -> Commands cmd -> Bool+parallelSafe StateMachine { precondition, transition, mock } model0 counter0+ = and+ . map (preconditionsHold model0 counter0)+ . permutations+ . unCommands+ where+ preconditionsHold _ _ [] = True+ preconditionsHold model counter (Command cmd _vars : cmds) =+ let+ (resp, counter') = runGenSym (mock model cmd) counter+ in+ boolean (precondition model cmd) &&+ preconditionsHold (transition model cmd resp) counter' cmds++-- | Apply the transition of some commands to a model.+advanceModel :: StateMachine model cmd m resp+ -> model Symbolic -- ^ The model.+ -> Counter+ -> Commands cmd -- ^ The commands.+ -> (model Symbolic, Counter)+advanceModel StateMachine { transition, mock } model0 counter0 =+ go model0 counter0 . unCommands+ where+ go model counter [] = (model, counter)+ go model counter (Command cmd _vars : cmds) =+ let+ (resp, counter') = runGenSym (mock model cmd) counter+ in+ go (transition model cmd resp) counter' cmds++------------------------------------------------------------------------++-- | Shrink a parallel program in a pre-condition and scope respecting+-- way.+shrinkParallelCommands+ :: forall cmd model m resp. Rank2.Foldable cmd+ => Rank2.Foldable resp+ => StateMachine model cmd m resp+ -> (ParallelCommands cmd -> [ParallelCommands cmd])+shrinkParallelCommands sm@StateMachine { shrinker, initModel }+ (ParallelCommands prefix suffixes)+ = filterMaybe (flip evalState (initModel, S.empty, newCounter) . validParallelCommands sm)+ [ ParallelCommands prefix' (map toPair suffixes')+ | (prefix', suffixes') <- shrinkPair' shrinkCommands' shrinkSuffixes+ (prefix, map fromPair suffixes)+ ]+ +++ shrinkMoveSuffixToPrefix+ where+ shrinkCommands' :: Commands cmd -> [Commands cmd]+ shrinkCommands'+ = map Commands+ . shrinkList (liftShrinkCommand shrinker)+ . unCommands++ shrinkSuffixes :: [(Commands cmd, Commands cmd)] -> [[(Commands cmd, Commands cmd)]]+ shrinkSuffixes = shrinkList (shrinkPair shrinkCommands')++ shrinkMoveSuffixToPrefix :: [ParallelCommands cmd]+ shrinkMoveSuffixToPrefix = case suffixes of+ [] -> []+ (suffix : suffixes') ->+ [ ParallelCommands (prefix <> Commands [prefix'])+ (fmap Commands (toPair suffix') : suffixes')+ | (prefix', suffix') <- pickOneReturnRest2 (unCommands (proj1 suffix),+ unCommands (proj2 suffix))+ ]++ pickOneReturnRest :: [a] -> [(a, [a])]+ pickOneReturnRest [] = []+ pickOneReturnRest (x : xs) = (x, xs) : map (id *** (x :)) (pickOneReturnRest xs)++ pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a],[a]))]+ pickOneReturnRest2 (xs, ys) =+ map (id *** flip (,) ys) (pickOneReturnRest xs) +++ map (id *** (,) xs) (pickOneReturnRest ys)++validParallelCommands :: forall model cmd m resp. (Rank2.Foldable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp -> ParallelCommands cmd+ -> State (model Symbolic, Set Var, Counter) (Maybe (ParallelCommands cmd))+validParallelCommands sm@StateMachine { initModel } (ParallelCommands prefix suffixes) = do+ let prefixLength = lengthCommands prefix+ leftSuffixes = map (\(Pair l _r) -> l) suffixes+ rightSuffixes = map (\(Pair _l r) -> r) suffixes+ leftSuffixLengths = map lengthCommands leftSuffixes+ rightSuffixLengths = map lengthCommands rightSuffixes+ leftSuffix = mconcat leftSuffixes+ rightSuffix = mconcat rightSuffixes+ mleft <- validCommands sm (prefix <> leftSuffix)+ put (initModel, S.empty, newCounter)+ mright <- validCommands sm (prefix <> rightSuffix)+ case (mleft, mright) of+ (Nothing, Nothing) -> return Nothing+ (Just _, Nothing) -> return Nothing+ (Nothing, Just _) -> return Nothing+ (Just left, Just right) ->+ case (splitPlacesBlanks (prefixLength : leftSuffixLengths) (unCommands left),+ splitPlacesBlanks (prefixLength : rightSuffixLengths) (unCommands right)) of+ ([] , []) -> error "validParallelCommands: impossible"+ ([] , _ : _) -> error "validParallelCommands: impossible"+ (_ : _ , []) -> error "validParallelCommands: impossible"+ (prefix' : leftSuffixes', _ : rightSuffixes') -> do+ let suffixes' = zipWith Pair (map Commands leftSuffixes')+ (map Commands rightSuffixes')+ (model', counter') = advanceModel sm initModel newCounter (Commands prefix')++ if parallelSafeMany sm model' counter' suffixes'+ then return (Just (ParallelCommands (Commands prefix') suffixes'))+ else return Nothing++parallelSafeMany :: StateMachine model cmd m resp -> model Symbolic+ -> Counter -> [Pair (Commands cmd)] -> Bool+parallelSafeMany sm = go+ where+ go _ _ [] = True+ go model counter (Pair cmds1 cmds2 : cmdss) = parallelSafe sm model counter cmds+ && go model' counter' cmdss+ where+ cmds = cmds1 <> cmds2+ (model', counter') = advanceModel sm model counter cmds++prop_splitCombine :: [[Int]] -> Bool+prop_splitCombine xs = splitPlacesBlanks (map length xs) (concat xs) == xs++------------------------------------------------------------------------++runParallelCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)+ => (MonadCatch m, MonadBaseControl IO m)+ => StateMachine model cmd m resp+ -> ParallelCommands cmd+ -> PropertyM m [(History cmd resp, Bool)]+runParallelCommands sm = runParallelCommandsNTimes 10 sm++runParallelCommandsNTimes :: (Rank2.Traversable cmd, Rank2.Foldable resp)+ => (MonadCatch m, MonadBaseControl IO m)+ => Int -- ^ How many times to execute the parallel program.+ -> StateMachine model cmd m resp+ -> ParallelCommands cmd+ -> PropertyM m [(History cmd resp, Bool)]+runParallelCommandsNTimes n sm cmds =+ replicateM n $ do+ (hist, _reason) <- run (executeParallelCommands sm cmds)+ return (hist, linearise sm hist)++executeParallelCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)+ => (MonadCatch m, MonadBaseControl IO m)+ => StateMachine model cmd m resp+ -> ParallelCommands cmd+ -> m (History cmd resp, Reason)+executeParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) = do++ hchan <- liftBaseWith (const newTChanIO)++ (reason0, (env0, _cmodel)) <- runStateT+ (executeCommands sm hchan (Pid 0) True prefix)+ (emptyEnvironment, initModel)++ if reason0 /= Ok+ then do+ hist <- liftBaseWith (const (getChanContents hchan))+ return (History hist, reason0)+ else do+ (reason, _) <- foldM (go hchan) (reason0, env0) suffixes+ hist <- liftBaseWith (const (getChanContents hchan))+ return (History hist, reason)+ where+ go hchan (_, env) (Pair cmds1 cmds2) = do+ ((reason1, (env1, _)), (reason2, (env2, _))) <- concurrently++ -- XXX: Post-conditions not checked, so we can pass in initModel here...+ -- It would be better if we made executeCommands take a Maybe model+ -- instead of the boolean...++ (runStateT (executeCommands sm hchan (Pid 1) False cmds1) (env, initModel))+ (runStateT (executeCommands sm hchan (Pid 2) False cmds2) (env, initModel))+ return ( reason1 `combineReason` reason2+ , env1 <> env2+ )+ where+ combineReason :: Reason -> Reason -> Reason+ combineReason Ok r2 = r2+ combineReason r1 _ = r1++------------------------------------------------------------------------++-- | Try to linearise a history of a parallel program execution using a+-- sequential model. See the *Linearizability: a correctness condition for+-- concurrent objects* paper linked to from the README for more info.+linearise :: forall model cmd m resp. StateMachine model cmd m resp+ -> History cmd resp -> Bool+linearise StateMachine { transition, postcondition, initModel } = go . unHistory+ where+ go :: [(Pid, HistoryEvent cmd resp)] -> Bool+ go [] = True+ go es = any (step initModel) (interleavings es)++ step :: model Concrete -> Tree (Operation cmd resp) -> Bool+ step model (Node (Operation cmd resp _) roses) =+ boolean (postcondition model cmd resp) &&+ any' (step (transition model cmd resp)) roses++any' :: (a -> Bool) -> [a] -> Bool+any' _ [] = True+any' p xs = any p xs++------------------------------------------------------------------------++-- | Takes the output of parallel program runs and pretty prints a+-- counterexample if any of the runs fail.+prettyParallelCommands :: (MonadIO m, Rank2.Foldable cmd)+ => (Show (cmd Concrete), Show (resp Concrete))+ => ParallelCommands cmd+ -> [(History cmd resp, Bool)] -- ^ Output of 'runParallelCommands'.+ -> PropertyM m ()+prettyParallelCommands cmds =+ mapM_ (\(hist, bool) -> print (toBoxDrawings cmds hist) `whenFailM` property bool)++-- | Draw an ASCII diagram of the history of a parallel program. Useful for+-- seeing how a race condition might have occured.+toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd+ => (Show (cmd Concrete), Show (resp Concrete))+ => ParallelCommands cmd -> History cmd resp -> Doc+toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars+ where+ allVars = getAllUsedVars prefix `S.union`+ foldMap (foldMap getAllUsedVars) suffixes++ toBoxDrawings'' :: Set Var -> History cmd resp -> Doc+ toBoxDrawings'' knownVars (History h) = exec evT (fmap (out . snd) <$> Fork l p r)+ where+ (p, h') = partition (\e -> fst e == Pid 0) h+ (l, r) = partition (\e -> fst e == Pid 1) h'++ out :: HistoryEvent cmd resp -> String+ out (Invocation cmd vars)+ | vars `S.isSubsetOf` knownVars = show (S.toList vars) ++ " ← " ++ show cmd+ | otherwise = show cmd+ out (Response resp) = show resp++ toEventType :: History' cmd resp -> [(EventType, Pid)]+ toEventType = map go+ where+ go e = case e of+ (pid, Invocation _ _) -> (Open, pid)+ (pid, Response _) -> (Close, pid)++ evT :: [(EventType, Pid)]+ evT = toEventType (filter (\e -> fst e `elem` map Pid [1, 2]) h)++getAllUsedVars :: Rank2.Foldable cmd => Commands cmd -> Set Var+getAllUsedVars = foldMap (\(Command cmd _) -> getUsedVars cmd) . unCommands
+ src/Test/StateMachine/Sequential.hs view
@@ -0,0 +1,411 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Sequential+-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains helpers for generating, shrinking, and checking+-- sequential programs.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Sequential+ ( forAllCommands+ , generateCommands+ , generateCommandsState+ , measureFrequency+ , calculateFrequency+ , getUsedVars+ , shrinkCommands+ , liftShrinkCommand+ , validCommands+ , filterMaybe+ , modelCheck+ , runCommands+ , getChanContents+ , executeCommands+ , prettyPrintHistory+ , prettyCommands+ , commandNames+ , commandNamesInOrder+ , checkCommandNames+ , transitionMatrix+ )+ where++import Control.Concurrent.STM+ (atomically)+import Control.Concurrent.STM.TChan+ (TChan, newTChanIO, tryReadTChan, writeTChan)+import Control.Exception+ (ErrorCall, IOException, displayException)+import Control.Monad.Catch+ (MonadCatch, catch)+import Control.Monad.State+ (MonadIO, State, StateT, evalState, evalStateT, get,+ lift, put, runStateT)+import Control.Monad.Trans.Control+ (MonadBaseControl, liftBaseWith)+import Data.Dynamic+ (Dynamic, toDyn)+import Data.Either+ (fromRight)+import Data.List+ (elemIndex)+import qualified Data.Map as M+import Data.Map.Strict+ (Map)+import Data.Matrix+ (Matrix, getRow, matrix)+import Data.Maybe+ (fromMaybe)+import Data.Monoid+ ((<>))+import Data.Proxy+ (Proxy(..))+import Data.Set+ (Set)+import qualified Data.Set as S+import Data.TreeDiff+ (ToExpr, ansiWlBgEditExpr, ediff)+import qualified Data.Vector as V+import GHC.Generics+ (Generic1, Rep1, from1)+import Prelude+import Test.QuickCheck+ (Gen, Property, Testable, choose, collect, cover,+ generate, resize, shrinkList, sized, suchThat)+import Test.QuickCheck.Monadic+ (PropertyM, run)+import Text.PrettyPrint.ANSI.Leijen+ (Doc)+import qualified Text.PrettyPrint.ANSI.Leijen as PP+import Text.Show.Pretty+ (ppShow)++import Test.StateMachine.ConstructorName+import Test.StateMachine.Logic+import Test.StateMachine.Types+import qualified Test.StateMachine.Types.Rank2 as Rank2+import Test.StateMachine.Utils++------------------------------------------------------------------------++forAllCommands :: Testable prop+ => (Show (cmd Symbolic), Show (model Symbolic))+ => (Generic1 cmd, GConName1 (Rep1 cmd))+ => (Rank2.Foldable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp+ -> Maybe Int -- ^ Minimum number of commands.+ -> (Commands cmd -> prop) -- ^ Predicate.+ -> Property+forAllCommands sm mnum =+ forAllShrinkShow (generateCommands sm mnum) (shrinkCommands sm) ppShow++generateCommands :: (Rank2.Foldable resp, Show (model Symbolic))+ => (Generic1 cmd, GConName1 (Rep1 cmd))+ => StateMachine model cmd m resp+ -> Maybe Int -- ^ Minimum number of commands.+ -> Gen (Commands cmd)+generateCommands sm@StateMachine { initModel } mnum =+ evalStateT (generateCommandsState sm newCounter mnum) (initModel, Nothing)++generateCommandsState :: forall model cmd m resp. Rank2.Foldable resp+ => Show (model Symbolic)+ => (Generic1 cmd, GConName1 (Rep1 cmd))+ => StateMachine model cmd m resp+ -> Counter+ -> Maybe Int -- ^ Minimum number of commands.+ -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd)+generateCommandsState StateMachine { precondition, generator, transition+ , mock, distribution } counter0 mnum = do+ size0 <- lift (sized (\k -> choose (fromMaybe 0 mnum, k)))+ Commands <$> go size0 counter0 []+ where+ go :: Int -> Counter -> [Command cmd]+ -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen [Command cmd]+ go 0 _ cmds = return (reverse cmds)+ go size counter cmds = do+ (model, mprevious) <- get+ mnext <- lift $ commandFrequency (generator model) distribution mprevious+ `suchThatOneOf` (boolean . precondition model)+ case mnext of+ Nothing -> error $ concat+ [ "A deadlock occured while generating commands.\n"+ , "No pre-condition holds in the following model:\n"+ , ppShow model+ -- XXX: show trace of commands generated so far?+ ]+ Just next -> do+ let (resp, counter') = runGenSym (mock model next) counter+ put (transition model next resp, Just next)+ go (size - 1) counter' (Command next (getUsedVars resp) : cmds)++commandFrequency :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))+ => Gen (cmd Symbolic) -> Maybe (Matrix Int) -> Maybe (cmd Symbolic)+ -> [(Int, Gen (cmd Symbolic))]+commandFrequency gen Nothing _ = [ (1, gen) ]+commandFrequency gen (Just distribution) mprevious =+ [ (freq, gen `suchThat` ((== con) . gconName1 . from1)) | (freq, con) <- weights ]+ where+ idx = case mprevious of+ Nothing -> 1+ Just previous ->+ let+ rep = from1 previous+ con = gconName1 rep+ err = "genetateCommandState: no command: " <> con+ in+ fromMaybe (error err) ((+ 2) <$>+ elemIndex con (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))))+ row = V.toList (getRow idx distribution)+ weights = zip row (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic)))++measureFrequency :: (Rank2.Foldable resp, Show (model Symbolic))+ => (Generic1 cmd, GConName1 (Rep1 cmd))+ => StateMachine model cmd m resp+ -> Maybe Int -- ^ Minimum number of commands.+ -> Int -- ^ Maximum number of commands.+ -> IO (Map (String, Maybe String) Int)+measureFrequency sm min0 size = do+ cmds <- generate (sequence [ resize n (generateCommands sm min0) | n <- [0, 2..size] ])+ return (M.unions (map calculateFrequency cmds))++calculateFrequency :: (Generic1 cmd, GConName1 (Rep1 cmd))+ => Commands cmd -> Map (String, Maybe String) Int+calculateFrequency = go M.empty . unCommands+ where+ go m [] = m+ go m [cmd]+ = M.insertWith (\_ old -> old + 1) (gconName cmd, Nothing) 1 m+ go m (cmd1 : cmd2 : cmds)+ = go (M.insertWith (\_ old -> old + 1) (gconName cmd1,+ Just (gconName cmd2)) 1 m) cmds++getUsedVars :: Rank2.Foldable f => f Symbolic -> Set Var+getUsedVars = Rank2.foldMap (\(Symbolic v) -> S.singleton v)++-- | Shrink commands in a pre-condition and scope respecting way.+shrinkCommands :: (Rank2.Foldable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp -> Commands cmd+ -> [Commands cmd]+shrinkCommands sm@StateMachine { initModel, shrinker }+ = filterMaybe ( flip evalState (initModel, S.empty, newCounter)+ . validCommands sm+ . Commands)+ . shrinkList (liftShrinkCommand shrinker)+ . unCommands++liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic])+ -> (Command cmd -> [Command cmd])+liftShrinkCommand shrinker (Command cmd resp) =+ [ Command cmd' resp | cmd' <- shrinker cmd ]++filterMaybe :: (a -> Maybe b) -> [a] -> [b]+filterMaybe _ [] = []+filterMaybe f (x : xs) = case f x of+ Nothing -> filterMaybe f xs+ Just y -> y : filterMaybe f xs++validCommands :: forall model cmd m resp. (Rank2.Foldable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp -> Commands cmd+ -> State (model Symbolic, Set Var, Counter) (Maybe (Commands cmd))+validCommands StateMachine { precondition, transition, mock } =+ fmap (fmap Commands) . go . unCommands+ where+ go :: [Command cmd] -> State (model Symbolic, Set Var, Counter) (Maybe [Command cmd])+ go [] = return (Just [])+ go (Command cmd _vars : cmds) = do+ (model, scope, counter) <- get+ if boolean (precondition model cmd) && getUsedVars cmd `S.isSubsetOf` scope+ then do+ let (resp, counter') = runGenSym (mock model cmd) counter+ vars = getUsedVars resp+ put ( transition model cmd resp+ , vars `S.union` scope+ , counter')+ mih <- go cmds+ case mih of+ Nothing -> return Nothing+ Just ih -> return (Just (Command cmd vars : ih))+ else+ return Nothing++modelCheck :: forall model cmd resp m. Monad m => StateMachine model cmd m resp+ -> Commands cmd+ -> PropertyM m Reason -- XXX: (History cmd, model Symbolic, Reason)+modelCheck StateMachine { initModel, transition, precondition, spostcondition, mock }+ = run . return . go initModel newCounter . unCommands+ where+ go :: model Symbolic -> Counter -> [Command cmd] -> Reason+ go _ _ [] = Ok+ go m counter (Command cmd _vars : cmds)+ | not (boolean (precondition m cmd)) = PreconditionFailed+ | otherwise =+ let (resp, counter') = runGenSym (mock m cmd) counter in+ case logic (fromMaybe err spostcondition m cmd resp) of+ VTrue -> go (transition m cmd resp) counter' cmds+ VFalse ce -> PostconditionFailed (show ce)+ where+ err = error "modelCheck: Symbolic post-condition must be \+ \ specificed in state machine in order to do model checking."++runCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)+ => (MonadCatch m, MonadBaseControl IO m)+ => StateMachine model cmd m resp+ -> Commands cmd+ -> PropertyM m (History cmd resp, model Concrete, Reason)+runCommands sm@StateMachine { initModel } = run . go+ where+ go cmds = do+ hchan <- liftBaseWith (const newTChanIO)+ (reason, (_, model)) <- runStateT (executeCommands sm hchan (Pid 0) True cmds)+ (emptyEnvironment, initModel)+ hist <- liftBaseWith (const (getChanContents hchan))+ return (History hist, model, reason)++getChanContents :: TChan a -> IO [a]+getChanContents chan = reverse <$> atomically (go' [])+ where+ go' acc = do+ mx <- tryReadTChan chan+ case mx of+ Just x -> go' (x : acc)+ Nothing -> return acc++executeCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)+ => (MonadCatch m, MonadBaseControl IO m)+ => StateMachine model cmd m resp+ -> TChan (Pid, HistoryEvent cmd resp)+ -> Pid+ -> Bool -- ^ Check invariant and post-condition?+ -> Commands cmd+ -> StateT (Environment, model Concrete) m Reason+executeCommands StateMachine { transition, postcondition, invariant, semantics } hchan pid check =+ go . unCommands+ where+ go [] = return Ok+ go (Command scmd vars : cmds) = do+ (env, model) <- get+ let ccmd = fromRight (error "executeCommands: impossible") (reify env scmd)+ liftBaseWith (const (atomically (writeTChan hchan (pid, Invocation ccmd vars))))+ !ecresp <- lift (fmap Right (semantics ccmd))+ `catch` (\(err :: IOException) ->+ return (Left (ExceptionThrown (displayException err))))+ `catch` (\(err :: ErrorCall) ->+ return (Left (ExceptionThrown (displayException err))))+ case ecresp of+ Left err -> return err+ Right cresp -> do+ liftBaseWith (const (atomically (writeTChan hchan (pid, Response cresp))))+ if check+ then case logic (postcondition model ccmd cresp) of+ VFalse ce -> return (PostconditionFailed (show ce))+ VTrue -> case logic (fromMaybe (const Top) invariant model) of+ VFalse ce' -> return (InvariantBroken (show ce'))+ VTrue -> do+ put ( insertConcretes (S.toList vars) (getUsedConcrete cresp) env+ , transition model ccmd cresp+ )+ go cmds+ else do+ put ( insertConcretes (S.toList vars) (getUsedConcrete cresp) env+ , transition model ccmd cresp+ )+ go cmds++getUsedConcrete :: Rank2.Foldable f => f Concrete -> [Dynamic]+getUsedConcrete = Rank2.foldMap (\(Concrete x) -> [toDyn x])++modelDiff :: ToExpr (model r) => model r -> Maybe (model r) -> Doc+modelDiff model = ansiWlBgEditExpr . flip ediff model . fromMaybe model++prettyPrintHistory :: forall model cmd m resp. ToExpr (model Concrete)+ => (Show (cmd Concrete), Show (resp Concrete))+ => StateMachine model cmd m resp+ -> History cmd resp+ -> IO ()+prettyPrintHistory StateMachine { initModel, transition }+ = PP.putDoc+ . go initModel Nothing+ . makeOperations+ . unHistory+ where+ go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc+ go current previous [] =+ PP.line <> modelDiff current previous <> PP.line <> PP.line+ go current previous (Operation cmd resp pid : ops) =+ mconcat+ [ PP.line+ , modelDiff current previous+ , PP.line, PP.line+ , PP.string " == "+ , PP.string (show cmd)+ , PP.string " ==> "+ , PP.string (show resp)+ , PP.string " [ "+ , PP.int (unPid pid)+ , PP.string " ]"+ , PP.line+ , go (transition current cmd resp) (Just current) ops+ ]++prettyCommands :: (MonadIO m, ToExpr (model Concrete))+ => (Show (cmd Concrete), Show (resp Concrete))+ => StateMachine model cmd m resp+ -> History cmd resp+ -> Property+ -> PropertyM m ()+prettyCommands sm hist prop = prettyPrintHistory sm hist `whenFailM` prop++------------------------------------------------------------------------+++-- | Print distribution of commands and fail if some commands have not+-- been executed.+checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))+ => Commands cmd -> Property -> Property+checkCommandNames cmds+ = collect names+ . cover (length names == numOfConstructors) 1 "coverage"+ where+ names = commandNames cmds+ numOfConstructors = length (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic)))++commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))+ => Commands cmd -> [(String, Int)]+commandNames = M.toList . foldl go M.empty . unCommands+ where+ go :: Map String Int -> Command cmd -> Map String Int+ go ih cmd = M.insertWith (+) (gconName cmd) 1 ih++commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))+ => Commands cmd -> [String]+commandNamesInOrder = reverse . foldl go [] . unCommands+ where+ go :: [String] -> Command cmd -> [String]+ go ih cmd = gconName cmd : ih+++transitionMatrix :: forall cmd. GConName1 (Rep1 cmd)+ => Proxy (cmd Symbolic)+ -> (String -> String -> Int) -> Matrix Int+transitionMatrix _ f =+ let cons = gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))+ n = length cons+ m = succ n+ in matrix m n $ \case+ (1, j) -> f "<START>" (cons !! pred j)+ (i, j) -> f (cons !! pred (pred i)) (cons !! pred j)
− src/Test/StateMachine/TH.hs
@@ -1,51 +0,0 @@--------------------------------------------------------------------------------- |--- Module : Test.StateMachine.TH--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia--- License : BSD-style (see the file LICENSE)------ Maintainer : Li-yao Xia <lysxia@gmail.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ Template Haskell functions to derive common type classes for--- testing with quickcheck-state-machine.-----------------------------------------------------------------------------------module Test.StateMachine.TH- ( -- * Special classes for @Action@ types- deriveTestClasses-- -- ** Components- , deriveHClasses- , deriveHFunctor- , deriveHFoldable- , deriveHTraversable- , deriveConstructors-- -- * Show- , deriveShows- , deriveShow- , deriveShowUntyped-- -- * Shrink- , mkShrinker- ) where--import Language.Haskell.TH- (Dec, Name, Q)--import Test.StateMachine.Types.Generics.TH-import Test.StateMachine.Types.HFunctor.TH---- | Derive instances of--- 'Test.StateMachine.Types.HFunctor.HFunctor',--- 'Test.StateMachine.Types.HFunctor.HFoldable',--- 'Test.StateMachine.Types.HFunctor.HTraversable',--- 'Test.StateMachine.Types.Generics.Constructor'.-deriveTestClasses :: Name -> Q [Dec]-deriveTestClasses = (fmap (fmap concat . sequence) . sequence)- [ deriveHClasses- , deriveConstructors- ]
src/Test/StateMachine/Types.hs view
@@ -1,9 +1,12 @@-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MonoLocalBinds #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |@@ -15,170 +18,99 @@ -- Stability : provisional -- Portability : non-portable (GHC extensions) ----- This module contains the main types exposed to the user. The module--- is perhaps best read indirectly, on a per need basis, via the main--- module "Test.StateMachine".--- ----------------------------------------------------------------------------- module Test.StateMachine.Types- ( -- * Untyped actions- Untyped(..)-- -- * Type aliases- , StateMachine- , stateMachine- , okTransition- , okPostcondition- , okSemantics- , StateMachine'(..)- , Generator- , Shrinker- , Precondition- , Transition- , Transition'- , Postcondition- , Postcondition'- , InitialModel- , Result(..)- , ppResult- , Semantics- , Semantics'- , Runner+ ( StateMachine(..)+ , Command(..)+ , Commands(..)+ , lengthCommands+ , ParallelCommandsF(..)+ , ParallelCommands+ , Pair(..)+ , fromPair+ , toPair , Reason(..)-- -- * Data type generic operations- , module Test.StateMachine.Types.Generics-- -- * Higher-order functors, foldables and traversables- , module Test.StateMachine.Types.HFunctor-- -- * References+ , module Test.StateMachine.Types.Environment+ , module Test.StateMachine.Types.GenSym+ , module Test.StateMachine.Types.History , module Test.StateMachine.Types.References- )- where+ ) where import Data.Functor.Classes (Ord1, Show1)-import Data.Typeable- (Typeable)-import Data.Void- (Void, absurd)+import Data.Matrix+ (Matrix)+import Data.Semigroup+ (Semigroup)+import Data.Set+ (Set)+import Prelude import Test.QuickCheck (Gen, Property) -import Test.StateMachine.Types.Generics-import Test.StateMachine.Types.HFunctor+import Test.StateMachine.Logic+import Test.StateMachine.Types.Environment+import Test.StateMachine.Types.GenSym+import Test.StateMachine.Types.History import Test.StateMachine.Types.References ------------------------------------------------------------------------ --- | An untyped action is an action where the response type is hidden--- away using an existential type.------ We need to hide the response type when generating actions, because--- in general the actions we want to generate will have different--- response types; and thus we can only type the generating function--- if we hide the response type.-data Untyped (act :: (* -> *) -> * -> *) where- Untyped :: (Show resp, Typeable resp) => act Symbolic resp -> Untyped act------------------------------------------------------------------------------ | A (non-failing) state machine record bundles up all functionality--- needed to perform our tests.-type StateMachine model act m = StateMachine' model act m Void---- | Same as above, but with possibly failing semantics.-data StateMachine' model act m err = StateMachine- { generator' :: Generator model act- , shrinker' :: Shrinker act- , precondition' :: Precondition model act- , transition' :: Transition' model act err- , postcondition' :: Postcondition' model act err- , model' :: InitialModel model- , semantics' :: Semantics' act m err- , runner' :: Runner m+data StateMachine model cmd m resp = StateMachine+ { initModel :: forall r. model r+ , transition :: forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r+ , precondition :: model Symbolic -> cmd Symbolic -> Logic+ , postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic+ , spostcondition :: Maybe (model Symbolic -> cmd Symbolic -> resp Symbolic -> Logic)+ , invariant :: Maybe (model Concrete -> Logic)+ , generator :: model Symbolic -> Gen (cmd Symbolic)+ , distribution :: Maybe (Matrix Int)+ , shrinker :: cmd Symbolic -> [cmd Symbolic]+ , semantics :: cmd Concrete -> m (resp Concrete)+ , runner :: m Property -> IO Property+ , mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) } --- | Helper for lifting non-failing semantics to a possibly failing--- state machine record.-stateMachine- :: forall m model act- . Functor m- => Generator model act- -> Shrinker act- -> Precondition model act- -> Transition model act- -> Postcondition model act- -> InitialModel model- -> Semantics act m- -> Runner m- -> StateMachine' model act m Void-stateMachine gen shr precond trans post model sem run =- StateMachine gen shr precond (okTransition trans)- (okPostcondition post) model (okSemantics sem) run--okTransition :: Transition model act -> Transition' model act Void-okTransition transition model act (Success resp) = transition model act resp-okTransition _ _ _ (Fail false) = absurd false--okPostcondition :: Postcondition model act -> Postcondition' model act Void-okPostcondition postcondition model act (Success resp) = postcondition model act resp-okPostcondition _ _ _ (Fail false) = absurd false--okSemantics :: Functor m => Semantics act m -> Semantics' act m Void-okSemantics sem = fmap Success . sem---- | When generating actions we have access to a model containing--- symbolic references.-type Generator model act = model Symbolic -> Gen (Untyped act)---- | Shrinking should preserve the response type of the action.-type Shrinker act = forall (v :: * -> *) resp.- act v resp -> [act v resp]---- | Pre-conditions are checked while generating, at this stage we do--- not yet have access to concrete references.-type Precondition model act = forall resp.- model Symbolic -> act Symbolic resp -> Bool+data Command cmd = Command !(cmd Symbolic) !(Set Var) --- | The transition function must be polymorphic in the type of--- variables used, as it is used both while generating and executing.-type Transition model act = forall resp v. (Ord1 v, Show1 v) =>- model v -> act v resp -> v resp -> model v+deriving instance Show (cmd Symbolic) => Show (Command cmd) -type Transition' model act err = forall resp v. (Ord1 v, Show1 v) =>- model v -> act v resp -> Result err (v resp) -> model v+newtype Commands cmd = Commands+ { unCommands :: [Command cmd] }+ deriving (Semigroup, Monoid) --- | Post-conditions are checked after the actions have been executed--- and we got a response.-type Postcondition model act = forall resp.- model Concrete -> act Concrete resp -> resp -> Bool+deriving instance Show (cmd Symbolic) => Show (Commands cmd) -type Postcondition' model act err = forall resp.- model Concrete -> act Concrete resp -> Result err resp -> Bool+lengthCommands :: Commands cmd -> Int+lengthCommands = length . unCommands --- | The initial model is polymorphic in the type of references it uses,--- so that it can be used both in the pre- and the post-condition--- check.-type InitialModel m = forall (v :: * -> *). m v+data Reason+ = Ok+ | PreconditionFailed+ | PostconditionFailed String+ | InvariantBroken String+ | ExceptionThrown String+ deriving (Eq, Show) --- | When we execute our actions we have access to concrete references.-type Semantics act m = forall resp. act Concrete resp -> m resp+data ParallelCommandsF t cmd = ParallelCommands+ { prefix :: !(Commands cmd)+ , suffixes :: [t (Commands cmd)]+ } --- | The result of executing an action.-data Result err resp = Success resp | Fail err- deriving Functor+deriving instance (Show (cmd Symbolic), Show (t (Commands cmd))) =>+ Show (ParallelCommandsF t cmd) -ppResult :: (Show err, Show resp) => Result err resp -> String-ppResult (Success resp) = show resp-ppResult (Fail err) = show err+data Pair a = Pair+ { proj1 :: !a+ , proj2 :: !a+ }+ deriving (Eq, Ord, Show, Functor, Foldable, Traversable) -type Semantics' act m err = forall resp. act Concrete resp -> m (Result err resp)+fromPair :: Pair a -> (a, a)+fromPair (Pair x y) = (x, y) --- | How to run the monad used by the semantics.-type Runner m = m Property -> IO Property+toPair :: (a, a) -> Pair a+toPair (x, y) = Pair x y -data Reason = Ok | PreconditionFailed | PostconditionFailed- deriving (Eq, Show)+type ParallelCommands = ParallelCommandsF Pair
+ src/Test/StateMachine/Types/Environment.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Types.Environment+-- Copyright : (C) 2017, Jacob Stanley+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains environments that are used to translate between+-- symbolic and concrete references. It's taken from the Hedgehog+-- <https://hackage.haskell.org/package/hedgehog library>.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Types.Environment+ ( Environment(..)+ , EnvironmentError(..)+ , emptyEnvironment+ , insertConcrete+ , insertConcretes+ , reifyDynamic+ , reifyEnvironment+ , reify+ ) where++import Data.Dynamic+ (Dynamic, Typeable, dynTypeRep, fromDynamic)+import Data.Map+ (Map)+import qualified Data.Map as M+import Data.Semigroup+ (Semigroup)+import Data.Typeable+ (Proxy(Proxy), TypeRep, typeRep)+import Prelude++import qualified Test.StateMachine.Types.Rank2 as Rank2+import Test.StateMachine.Types.References++------------------------------------------------------------------------++-- | A mapping of symbolic values to concrete values.+newtype Environment = Environment+ { unEnvironment :: Map Var Dynamic+ }+ deriving (Semigroup, Monoid, Show)++-- | Environment errors.+data EnvironmentError+ = EnvironmentValueNotFound !Var+ | EnvironmentTypeError !TypeRep !TypeRep+ deriving (Eq, Ord, Show)++-- | Create an empty environment.+emptyEnvironment :: Environment+emptyEnvironment = Environment M.empty++-- | Insert a symbolic / concrete pairing in to the environment.+insertConcrete :: Var -> Dynamic -> Environment -> Environment+insertConcrete var dyn = Environment . M.insert var dyn . unEnvironment++insertConcretes :: [Var] -> [Dynamic] -> Environment -> Environment+insertConcretes [] [] env = env+insertConcretes (var : vars) (dyn : dyns) env =+ insertConcretes vars dyns (insertConcrete var dyn env)+insertConcretes _ _ _ =+ error "insertConcrets: impossible."++-- | Cast a 'Dynamic' in to a concrete value.+reifyDynamic :: forall a. Typeable a => Dynamic+ -> Either EnvironmentError (Concrete a)+reifyDynamic dyn =+ case fromDynamic dyn of+ Nothing ->+ Left (EnvironmentTypeError (typeRep (Proxy :: Proxy a)) (dynTypeRep dyn))+ Just x ->+ Right (Concrete x)++-- | Turns an environment in to a function for looking up a concrete value from+-- a symbolic one.+reifyEnvironment :: Environment+ -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))+reifyEnvironment (Environment vars) (Symbolic n) =+ case M.lookup n vars of+ Nothing ->+ Left (EnvironmentValueNotFound n)+ Just dyn ->+ reifyDynamic dyn++-- | Convert a symbolic structure to a concrete one, using the provided+-- environment.+reify :: Rank2.Traversable t+ => Environment -> t Symbolic -> Either EnvironmentError (t Concrete)+reify vars = Rank2.traverse (reifyEnvironment vars)
+ src/Test/StateMachine/Types/GenSym.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Types.GenSym+-- Copyright : (C) 2018, HERE Europe B.V.+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-----------------------------------------------------------------------------++module Test.StateMachine.Types.GenSym+ ( GenSym+ , runGenSym+ , genSym+ , Counter+ , newCounter+ )+ where++import Control.Monad.State+ (State, get, put, runState)+import Data.Typeable+ (Typeable)+import Prelude++import Test.StateMachine.Types.References++------------------------------------------------------------------------++newtype GenSym a = GenSym (State Counter a)+ deriving (Functor, Applicative, Monad)++runGenSym :: GenSym a -> Counter -> (a, Counter)+runGenSym (GenSym m) counter = runState m counter++genSym :: Typeable a => GenSym (Reference a Symbolic)+genSym = GenSym $ do+ Counter i <- get+ put (Counter (i + 1))+ return (Reference (Symbolic (Var i)))++newtype Counter = Counter Int++newCounter :: Counter+newCounter = Counter 0
− src/Test/StateMachine/Types/Generics.hs
@@ -1,33 +0,0 @@-{-# LANGUAGE KindSignatures #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Types.Generics--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia--- License : BSD-style (see the file LICENSE)------ Maintainer : Li-yao Xia <lysxia@gmail.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ Datatype-generic utilities.-----------------------------------------------------------------------------------module Test.StateMachine.Types.Generics where---- | A constructor name is a string.-newtype Constructor = Constructor String- deriving (Eq, Ord)--instance Show Constructor where- show (Constructor c) = c---- | Extracting constructors from actions.-class Constructors (act :: (* -> *) -> * -> *) where-- -- | Constructor of a given action.- constructor :: act v a -> Constructor-- -- | Total number of constructors in the action type.- nConstructors :: proxy act -> Int
− src/Test/StateMachine/Types/Generics/TH.hs
@@ -1,276 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Types.Generics.TH--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia--- License : BSD-style (see the file LICENSE)------ Maintainer : Li-yao Xia <lysxia@gmail.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ Template Haskell functions to derive some general-purpose functionalities.-----------------------------------------------------------------------------------module Test.StateMachine.Types.Generics.TH- ( deriveShows- , deriveShow- , deriveShowUntyped- , mkShrinker- , deriveConstructors- ) where--import Control.Applicative- (liftA3)-import Control.Monad- (filterM, (>=>))-import Data.Foldable- (asum, foldl')-import Data.Functor.Classes- (Show1, liftShowsPrec)-import Data.Maybe- (maybeToList)-import Language.Haskell.TH- (Body(NormalB), Clause(Clause), Cxt,- Dec(FunD, InstanceD), Exp(AppE, ConE, LitE, VarE),- ExpQ, Lit(IntegerL, StringL), Match, Name,- Pat(RecP, VarP, WildP), PatQ, Q,- Type(AppT, ConT, SigT, VarT), appE, caseE, conE,- conP, lamE, listE, match, mkName, nameBase, newName,- normalB, standaloneDerivD, tupE, tupP,- tupleDataName, varE, varP, wildP)-import Language.Haskell.TH.Datatype- (ConstructorInfo, DatatypeInfo, constructorFields,- constructorName, datatypeCons, datatypeName,- datatypeVars, reifyDatatype, resolveTypeSynonyms)-import Test.QuickCheck- (shrink)--import Test.StateMachine.Internal.Utils- (dropLast, nub, toLast)-import Test.StateMachine.Types- (Symbolic, Untyped)-import Test.StateMachine.Types.Generics-import Test.StateMachine.Types.References- (Reference)---- * Show of actions---- | Given a name @''Action@, derive 'Show' for @(Action v a)@ and @('Untyped'--- Action)@, and 'Show1' @(Action Symbolic)@. See 'deriveShow',--- 'deriveShowUntyped', and 'deriveShow1'.-deriveShows :: Name -> Q [Dec]-deriveShows = (liftA3 . liftA3)- (\xs ys zs -> xs ++ ys ++ zs) deriveShow deriveShowUntyped deriveShow1---- |------ @--- 'deriveShow' ''Action--- ===>--- deriving instance 'Show1' v => 'Show' (Action v a).--- @-deriveShow :: Name -> Q [Dec]-deriveShow = reifyDatatype >=> deriveShow'--deriveShow' :: DatatypeInfo -> Q [Dec]-deriveShow' info = do- (v_, ts) <- showConstraints info- let show1v = maybeToList (fmap (AppT (ConT ''Show1)) v_)- cxt_ = show1v ++ fmap (AppT (ConT ''Show)) ts- instanceHead_ = AppT- (ConT ''Show)- (foldl' AppT (ConT (datatypeName info)) (datatypeVars info))- standaloneDerivD' cxt_ instanceHead_--standaloneDerivD' :: Cxt -> Type -> Q [Dec]-standaloneDerivD' cxt ty = (:[]) <$> standaloneDerivD (return cxt) (return ty)---- |--- @--- 'deriveShowUntyped' ''Action--- ===>--- deriving instance 'Show' ('Untyped' Action)--- @-deriveShowUntyped :: Name -> Q [Dec]-deriveShowUntyped = reifyDatatype >=> deriveShowUntyped'--deriveShowUntyped' :: DatatypeInfo -> Q [Dec]-deriveShowUntyped' info = do- (_, ts) <- showConstraints info- let cxt_ = fmap (AppT (ConT ''Show)) ts- instanceHead_ = AppT- (ConT ''Show)- (AppT- (ConT ''Untyped)- (foldl' AppT (ConT (datatypeName info)) (dropLast 2 (datatypeVars info))))- standaloneDerivD' cxt_ instanceHead_---- |--- @ 'derivingShow1' ''Action--- ===>--- instance Show1 (Action Symbolic) where--- liftShowsPrec _ _ _ act _ = show act--- @-deriveShow1 :: Name -> Q [Dec]-deriveShow1 = (fmap . fmap) deriveShow1' reifyDatatype--deriveShow1' :: DatatypeInfo -> [Dec]-deriveShow1' info0 = pure $- InstanceD Nothing [] (instanceHead' info0)- [ deriveLiftShows ]- where- instanceHead' :: DatatypeInfo -> Type- instanceHead' info =- ConT ''Show1 `AppT`- (ConT (datatypeName info) `AppT` ConT ''Symbolic)-- deriveLiftShows :: Dec- deriveLiftShows =- let- act = mkName "act"- body = VarE 'show `AppE` VarE act- in- FunD 'liftShowsPrec- [Clause [WildP, WildP, WildP, VarP act, WildP] (NormalB body) []]---- | Gather types of fields with parametric types to form @Show@ constraints--- for a derived instance.------ - @(Show1 v, Show a)@ for fields of type @Reference v a@--- - @Show a@ for fields of type @a@------ The @Show1 v@ constraint is separated so that we can easily remove--- it from the list.-showConstraints :: DatatypeInfo -> Q (Maybe Type, [Type])-showConstraints info = do- let SigT v _ = toLast 1 (datatypeVars info)- fmap gatherShowConstraints- (traverse (showConstraintsByCon v) (datatypeCons info))--showConstraintsByCon :: Type -> ConstructorInfo -> Q (Maybe Type, [Type])-showConstraintsByCon v info =- fmap gatherShowConstraints- (traverse (showConstraintsByField v) (constructorFields info))--showConstraintsByField :: Type -> Type -> Q (Maybe Type, [Type])-showConstraintsByField v t' = do- t <- resolveTypeSynonyms t'- return $ case t of- AppT (AppT (ConT _ref) v') a- | _ref == ''Reference && v == v' -> (Just v, singleton a)- _ -> (Nothing, singleton t)- where- singleton t | variableHead t = [t]- | otherwise = []--gatherShowConstraints :: [(Maybe Type, [Type])] -> (Maybe Type, [Type])-gatherShowConstraints vts =- let (vs', ts') = unzip vts- v = asum vs'- ts = nub (concat ts')- in (v, ts)--variableHead :: Type -> Bool-variableHead (AppT u _) = variableHead u-variableHead (VarT _) = True-variableHead _ = False---- * Shrinkers---- | @$('mkShrinker' ''Action)@--- creates a generic shrinker of type @(Action v a -> [Action v a])@--- which ignores 'Reference' fields.-mkShrinker :: Name -> Q Exp-mkShrinker = reifyDatatype >=> mkShrinker'--mkShrinker' :: DatatypeInfo -> Q Exp-mkShrinker' info = do- x <- newName "x"- tms <- traverse shrinkerMatches (datatypeCons info)- let (_ts, ms) = unzip tms- lamE [varP x] (caseE (varE x) ms)--shrinkerMatches :: ConstructorInfo -> Q ([Type], Q Match)-shrinkerMatches info = do- xts <- traverse (\t -> (,) <$> newName "x" <*> pure t) (constructorFields info)- yts <- filterM (\(_, t) -> shrinkable t) xts- let (ys, ts) = unzip yts- fieldPats | [] <- ys = [wildP | _ <- xts]- | otherwise = [varP x | (x, _) <- xts]- m = match (conP (constructorName info) fieldPats) (normalB body) []- e = foldl' appE (conE (constructorName info)) [varE x | (x, _) <- xts]- body | [] <- ys = listE [] -- No field is shrinkable- | otherwise = [|fmap|]- `appE` lamE [listTupleP ys] e- `appE` [|shrink $(listTupleE ys)|]- return (nub ts, m)--listTupleP :: [Name] -> PatQ-listTupleP = listTuple unit cons . fmap varP- where- unit = conP (tupleDataName 0) []- cons a b = tupP [a, b]--listTupleE :: [Name] -> ExpQ-listTupleE = listTuple unit cons . fmap varE- where- unit = conE (tupleDataName 0)- cons a b = tupE [a, b]--listTuple :: a -> (a -> a -> a) -> [a] -> a-listTuple nil cons = go- where- go [] = nil- go [a] = a- go (a : as) = cons a (go as)--shrinkable :: Type -> Q Bool-shrinkable =- fmap (not . isReference) . resolveTypeSynonyms--isReference :: Type -> Bool-isReference (AppT (AppT (ConT r) _) _) = r == ''Reference-isReference _ = False---- * Constructor class---- |--- @--- 'deriveConstructors' ''Action--- ===>--- instance 'Constructors' Action where ...--- @-deriveConstructors :: Name -> Q [Dec]-deriveConstructors = (fmap . fmap) deriveConstructors' reifyDatatype--deriveConstructors' :: DatatypeInfo -> [Dec]-deriveConstructors' info = pure $- InstanceD Nothing [] (instanceHead info)- [ deriveconstructor info- , derivenConstructors info- ]--instanceHead :: DatatypeInfo -> Type-instanceHead info =- ConT ''Constructors `AppT`- foldl' AppT (ConT (datatypeName info)) (dropLast 2 (datatypeVars info))---- |--- > constructor Foo{} = Constructor "Foo"--- > constructor Bar{} = Constructor "Bar"-deriveconstructor :: DatatypeInfo -> Dec-deriveconstructor info =- FunD 'constructor (fmap constructorClause (datatypeCons info))--constructorClause :: ConstructorInfo -> Clause-constructorClause info =- let body = ConE 'Constructor `AppE` LitE (StringL (nameBase (constructorName info)))- in Clause [RecP (constructorName info) []] (NormalB body) []--derivenConstructors :: DatatypeInfo -> Dec-derivenConstructors info =- let nCons = fromIntegral (length (datatypeCons info))- in FunD 'nConstructors [Clause [WildP] (NormalB (LitE (IntegerL nCons))) []]
− src/Test/StateMachine/Types/HFunctor.hs
@@ -1,56 +0,0 @@-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Rank2Types #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Types.HFunctor--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH, Jacob Stanley--- License : BSD-style (see the file LICENSE)------ Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ This module exports a higher-order version of functors, foldable functors,--- and traversable functors.-----------------------------------------------------------------------------------module Test.StateMachine.Types.HFunctor- ( HFunctor- , hfmap- , HFoldable- , hfoldMap- , HTraversable- , htraverse- )- where--import Control.Monad.Identity- (Identity(..), runIdentity)-import Data.Functor.Const- (Const(..))------------------------------------------------------------------------------ | Higher-order functors.-class HFunctor (f :: (* -> *) -> * -> *) where- -- | Higher-order version of 'fmap'.- hfmap :: (forall a. g a -> h a) -> f g b -> f h b-- default hfmap :: HTraversable f => (forall a. g a -> h a) -> f g b -> f h b- hfmap f = runIdentity . htraverse (Identity . f)---- | Higher-order foldable functors.-class HFunctor t => HFoldable (t :: (* -> *) -> * -> *) where- -- | Higher-order version of 'foldMap'.- hfoldMap :: Monoid m => (forall a. v a -> m) -> t v b -> m-- default hfoldMap :: (HTraversable t, Monoid m) => (forall a. v a -> m) -> t v b -> m- hfoldMap f = getConst . htraverse (Const . f)---- | Higher-order traversable functors.-class (HFunctor t, HFoldable t) => HTraversable (t :: (* -> *) -> * -> *) where- -- | Higher-order version of 'traverse'.- htraverse :: Applicative f => (forall a. g a -> f (h a)) -> t g b -> f (t h b)
− src/Test/StateMachine/Types/HFunctor/TH.hs
@@ -1,209 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Types.HFunctor.TH--- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia--- License : BSD-style (see the file LICENSE)------ Maintainer : Li-yao Xia <lysxia@gmail.com>--- Stability : provisional--- Portability : non-portable (GHC extensions)------ Template Haskell functions to derive higher-order structures.-----------------------------------------------------------------------------------module Test.StateMachine.Types.HFunctor.TH- ( deriveHClasses- , deriveHTraversable- , mkhtraverse- , deriveHFoldable- , mkhfoldMap- , deriveHFunctor- , mkhfmap- ) where--import Control.Applicative- (liftA3)-import Control.Monad- (when, (>=>))-import Data.Foldable- (foldl')-import Data.Monoid- (mempty, (<>))-import qualified Data.Set as Set-import Data.Traversable- (for)-import Language.Haskell.TH-import Language.Haskell.TH.Datatype--import Test.StateMachine.Internal.Utils- (dropLast, nub, toLast)-import Test.StateMachine.Types.HFunctor---- | Derive 'HFunctor', 'HFoldable', 'HTraversable'.-deriveHClasses :: Name -> Q [Dec]-deriveHClasses =- (liftA3 . liftA3) (\a b c -> a ++ b ++ c)- deriveHFunctor- deriveHFoldable- deriveHTraversable---- |--- @--- 'deriveHTraversable' ''Action--- ===>--- instance 'HTraversable' Action where ...--- @-deriveHTraversable :: Name -> Q [Dec]-deriveHTraversable = reifying deriveIFor dictHTraversable---- | Derive the body of 'htraverse'.-mkhtraverse :: Name -> Q Exp-mkhtraverse = reifying mkFFor dictHTraversable---- |--- @--- 'deriveHFoldable' ''Action--- ===>--- instance 'HFoldable' Action where ...--- @-deriveHFoldable :: Name -> Q [Dec]-deriveHFoldable = reifying deriveIFor dictHFoldable---- | Derive the body of 'hfoldMap'.-mkhfoldMap :: Name -> Q Exp-mkhfoldMap = reifying mkFFor dictHFoldable---- |--- @--- 'deriveHFunctor' ''Action--- ===>--- instance 'HFunctor' Action where ...--- @-deriveHFunctor :: Name -> Q [Dec]-deriveHFunctor = reifying deriveIFor dictHFunctor---- | Derive the body of 'hfmap'.-mkhfmap :: Name -> Q Exp-mkhfmap = reifying mkFFor dictHFunctor--data Dictionary = Dictionary- { className :: Name- , funName :: Name- , pureE :: Exp -> Exp- , apE :: Exp -> Exp -> Exp- }--dictHFunctor :: Dictionary-dictHFunctor = Dictionary- { className = ''HFunctor- , funName = 'hfmap- , pureE = id- , apE = AppE- }--dictHFoldable :: Dictionary-dictHFoldable = Dictionary- { className = ''HFoldable- , funName = 'hfoldMap- , pureE = const (VarE 'mempty)- , apE = apE'- } where- -- mempty <> e = e- -- e <> mempty = e- apE' (VarE m) e | m == 'mempty = e- apE' e (VarE m) | m == 'mempty = e- apE' e1 e2 = infixE_ e1 '(<>) e2--dictHTraversable :: Dictionary-dictHTraversable = Dictionary- { className = ''HTraversable- , funName = 'htraverse- , pureE = AppE (VarE 'pure)- , apE = apE'- } where- -- pure f <*> v = f <$> v- apE' (AppE (VarE pure_) f) v | pure_ == 'pure = infixE_ f '(<$>) v- apE' u v = infixE_ u '(<*>) v--reifying :: (Dictionary -> DatatypeInfo -> Q r) -> Dictionary -> Name -> Q r-reifying derive dict = reifyDatatype >=> derive dict--deriveIFor :: Dictionary -> DatatypeInfo -> Q [Dec]-deriveIFor dict info = fmap (: []) $ do- when (length (datatypeVars info) < 2)- (fail $ "Type " ++ show (datatypeName info) ++ " should have arity >= 2")- (cxt_, htraversalDec) <- htraversalWithCxtFor dict info- let instanceHead = AppT- (ConT (className dict))- (foldl' AppT (ConT (datatypeName info)) (dropLast 2 (datatypeVars info)))- return- (InstanceD Nothing cxt_ instanceHead [htraversalDec])--mkFFor :: Dictionary -> DatatypeInfo -> Q Exp-mkFFor dict info =- fmap mkF (htraversalBodyFor dict info)- where- mkF (_, pats, body) = LamE pats body--htraversalWithCxtFor :: Dictionary -> DatatypeInfo -> Q (Cxt, Dec)-htraversalWithCxtFor dict info =- fmap mkFunD (htraversalBodyFor dict info)- where- mkFunD (cxt_, pats, body) =- (cxt_, FunD (funName dict) [Clause pats (NormalB body) []])--htraversalBodyFor :: Dictionary -> DatatypeInfo -> Q (Cxt, [Pat], Exp)-htraversalBodyFor dict info = do- fN <- newName "f"- aN <- newName "a"- let SigT v _ = toLast 1 (datatypeVars info)- tucs <- traverse (htraversalMatchFor dict v (VarE fN)) (datatypeCons info)- let (ts, usedF', matches) = unzip3 tucs- usedF = or usedF'- fP = if usedF then VarP fN else WildP- pats = [fP, VarP aN]- cxt_ = fmap (AppT (ConT (className dict))) (nub (concat ts))- return (cxt_, pats, CaseE (VarE aN) matches)--htraversalMatchFor :: Dictionary -> Type -> Exp -> ConstructorInfo -> Q ([Type], Bool, Match)-htraversalMatchFor dict v f info = do- xts <- for (constructorFields info) (\t -> fmap (\x -> (x, t)) (newName "x"))- cyfs <- for xts (uncurry (htraversalFieldFor dict v f))- let conPattern = ConP (constructorName info) [mkVarP x | (x, _) <- xts]- -- HFoldable instances may have unused fields, replaced with wildcards.- mkVarP x | className dict == ''HFoldable && x `Set.member` ys = WildP- | otherwise = VarP x- c = ConE (constructorName info)- (cnstrnts', ys', fields) = unzip3 cyfs- -- f gets used if at least one field did not use pure- usedF = any null ys'- cnstrnts = concat cnstrnts'- ys = Set.fromList (concat ys')- body = foldl' (apE dict) (pureE dict c) fields- return- (cnstrnts, usedF, Match conPattern (NormalB body) [])--infixE_ :: Exp -> Name -> Exp -> Exp-infixE_ x (+.) y = InfixE (Just x) (VarE (+.)) (Just y)--htraversalFieldFor :: Dictionary -> Type -> Exp -> Name -> Type -> Q ([Type], [Name], Exp)-htraversalFieldFor dict v f x' t' = do- let x = VarE x'- t <- resolveTypeSynonyms t'- return $ case t of- AppT (AppT u v') _ | v == v' ->- ( [u | variableHead u]- , []- , VarE (funName dict) `AppE` f `AppE` x)- AppT v' _ | v == v' ->- ([], [], f `AppE` x)- _ ->- ([], [x'], pureE dict x)--variableHead :: Type -> Bool-variableHead (AppT u _) = variableHead u-variableHead (VarT _) = True-variableHead _ = False
src/Test/StateMachine/Types/History.hs view
@@ -1,10 +1,3 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}- ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Types.History@@ -23,116 +16,76 @@ module Test.StateMachine.Types.History ( History(..) , History'- , ppHistory+ , Pid(..) , HistoryEvent(..)- , getProcessIdEvent- , UntypedConcrete(..) , Operation(..)- , linearTree+ , makeOperations+ , interleavings ) where -import Data.Dynamic- (Dynamic)+import Data.Set+ (Set) import Data.Tree- (Tree(Node))-import Data.Typeable- (Typeable)+ (Forest, Tree(Node))+import Prelude -import Test.StateMachine.Internal.Types-import Test.StateMachine.Internal.Types.Environment-import Test.StateMachine.Types+import Test.StateMachine.Types.References ------------------------------------------------------------------------ --- | A history is a trace of a program execution.-newtype History act err = History- { unHistory :: History' act err }- deriving Monoid---- | A trace is a list of events.-type History' act err = [HistoryEvent (UntypedConcrete act) err]+newtype History cmd resp = History+ { unHistory :: History' cmd resp } --- | An event is either an invocation or a response.-data HistoryEvent act err- = InvocationEvent act String Var Pid- | ResponseEvent (Result err Dynamic) String Pid+type History' cmd resp = [(Pid, HistoryEvent cmd resp)] --- | Untyped concrete actions.-data UntypedConcrete (act :: (* -> *) -> * -> *) where- UntypedConcrete :: (Show resp, Typeable resp) =>- act Concrete resp -> UntypedConcrete act+newtype Pid = Pid { unPid :: Int }+ deriving (Eq, Show) --- | Pretty print a history.-ppHistory- :: forall model act err- . Show (model Concrete)- => Show err- => model Concrete -> Transition' model act err -> History act err -> String-ppHistory model0 transition- = showsPrec 10 model0- . go model0- . makeOperations- . unHistory- where- go :: model Concrete -> [Operation act err] -> String- go _ [] = "\n"- go model (Operation act astr resp rstr _ : ops) =- let model1 = transition model act (fmap Concrete resp) in- "\n\n " ++ astr ++ (case resp of- Success _ -> " --> "- Fail _ -> " -/-> ") ++ rstr ++ "\n\n" ++ show model1 ++ go model1 ops+data HistoryEvent cmd resp+ = Invocation !(cmd Concrete) !(Set Var)+ | Response !(resp Concrete) --- | Get the process id of an event.-getProcessIdEvent :: HistoryEvent act err -> Pid-getProcessIdEvent (InvocationEvent _ _ _ pid) = pid-getProcessIdEvent (ResponseEvent _ _ pid) = pid+------------------------------------------------------------------------ -takeInvocations :: [HistoryEvent a b] -> [HistoryEvent a b]-takeInvocations = takeWhile $ \h -> case h of- InvocationEvent {} -> True- _ -> False+takeInvocations :: History' cmd resp -> [(Pid, cmd Concrete)]+takeInvocations [] = []+takeInvocations ((pid, Invocation cmd _) : hist) = (pid, cmd) : takeInvocations hist+takeInvocations ((_, Response _) : _) = [] -findCorrespondingResp :: Pid -> History' act err -> [(Result err Dynamic, History' act err)]-findCorrespondingResp _ [] = []-findCorrespondingResp pid (ResponseEvent resp _ pid' : es) | pid == pid' = [(resp, es)]-findCorrespondingResp pid (e : es) =- [ (resp, e : es') | (resp, es') <- findCorrespondingResp pid es ]+findResponse :: Pid -> History' cmd resp -> [(resp Concrete, History' cmd resp)]+findResponse _ [] = []+findResponse pid ((pid', Response resp) : es) | pid == pid' = [(resp, es)]+findResponse pid (e : es) =+ [ (resp, e : es') | (resp, es') <- findResponse pid es ] ------------------------------------------------------------------------ -- | An operation packs up an invocation event with its corresponding -- response event.-data Operation act err = forall resp. Typeable resp =>- Operation (act Concrete resp) String (Result err resp) String Pid--dynResp :: forall err resp. Typeable resp => Result err Dynamic -> Result err resp-dynResp (Success resp) = Success- (either (error . show) (\(Concrete resp') -> resp') (reifyDynamic resp))-dynResp (Fail err) = Fail err+data Operation cmd resp = Operation (cmd Concrete) (resp Concrete) Pid -makeOperations :: History' act err -> [Operation act err]+makeOperations :: History' cmd resp -> [Operation cmd resp] makeOperations [] = []-makeOperations (InvocationEvent (UntypedConcrete act) astr _ pid :- ResponseEvent resp rstr _ : hist) =- Operation act astr (dynResp resp) rstr pid : makeOperations hist+makeOperations ((pid1, Invocation cmd _) : (pid2, Response resp) : hist)+ | pid1 == pid2 = Operation cmd resp pid1 : makeOperations hist+ | otherwise = error "makeOperations: pid mismatch." makeOperations _ = error "makeOperations: impossible." -- | Given a history, return all possible interleavings of invocations -- and corresponding response events.-linearTree :: History' act err -> [Tree (Operation act err)]-linearTree [] = []-linearTree es =- [ Node (Operation act str (dynResp resp) "<resp>" pid) (linearTree es')- | InvocationEvent (UntypedConcrete act) str _ pid <- takeInvocations es- , (resp, es') <- findCorrespondingResp pid $ filter1 (not . matchInv pid) es+interleavings :: [(Pid, HistoryEvent cmd resp)] -> Forest (Operation cmd resp)+interleavings [] = []+interleavings es =+ [ Node (Operation cmd resp pid) (interleavings es')+ | (pid, cmd) <- takeInvocations es+ , (resp, es') <- findResponse pid (filter1 (not . matchInvocation pid) es) ] where- filter1 :: (a -> Bool) -> [a] -> [a]- filter1 _ [] = []- filter1 p (x : xs) | p x = x : filter1 p xs- | otherwise = xs+ matchInvocation pid (pid', Invocation _ _) = pid == pid'+ matchInvocation _ _ = False - -- Hmm, is this enough?- matchInv pid (InvocationEvent _ _ _ pid') = pid == pid'- matchInv _ _ = False+ filter1 :: (a -> Bool) -> [a] -> [a]+ filter1 _ [] = []+ filter1 p (x : xs) | p x = x : filter1 p xs+ | otherwise = xs
+ src/Test/StateMachine/Types/Rank2.hs view
@@ -0,0 +1,135 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TypeOperators #-}++module Test.StateMachine.Types.Rank2+ ( Functor+ , fmap+ , gfmap+ , (<$>)+ , Foldable+ , foldMap+ , gfoldMap+ , Traversable+ , traverse+ , gtraverse+ )+ where++import qualified Control.Applicative as Rank1+import qualified Control.Monad as Rank1+import qualified Data.Foldable as Rank1+import qualified Data.Traversable as Rank1+import GHC.Generics+ ((:*:)((:*:)), (:+:)(L1, R1), Generic1, K1(K1),+ M1(M1), Rec1(Rec1), Rep1, U1(U1), from1, to1, (:.:)(Comp1))+import Prelude hiding+ (Applicative(..), Foldable(..), Functor(..),+ Traversable(..), (<$>))++------------------------------------------------------------------------++class Functor (f :: (k -> *) -> *) where+ fmap :: (forall x. p x -> q x) -> f p -> f q+ default fmap :: (Generic1 f, Functor (Rep1 f))+ => (forall x. p x -> q x) -> f p -> f q+ fmap = gfmap++gfmap :: (Generic1 f, Functor (Rep1 f)) => (forall a. p a -> q a) -> f p -> f q+gfmap f = to1 . fmap f . from1++(<$>) :: Functor f => (forall x. p x -> q x) -> f p -> f q+(<$>) = fmap+{-# INLINE (<$>) #-}++instance Functor U1 where+ fmap _ U1 = U1++instance Functor (K1 i c) where+ fmap _ (K1 c) = K1 c++instance (Functor f, Functor g) => Functor (f :+: g) where+ fmap f (L1 x) = L1 (fmap f x)+ fmap f (R1 y) = R1 (fmap f y)++instance (Functor f, Functor g) => Functor (f :*: g) where+ fmap f (x :*: y) = fmap f x :*: fmap f y++instance (Rank1.Functor f, Functor g) => Functor (f :.: g) where+ fmap f (Comp1 fg) = Comp1 (Rank1.fmap (fmap f) fg)++instance Functor f => Functor (M1 i c f) where+ fmap f (M1 x) = M1 (fmap f x)++instance Functor f => Functor (Rec1 f) where+ fmap f (Rec1 x) = Rec1 (fmap f x)++------------------------------------------------------------------------++class Foldable (f :: (k -> *) -> *) where+ foldMap :: Monoid m => (forall x. p x -> m) -> f p -> m+ default foldMap :: (Generic1 f, Foldable (Rep1 f), Monoid m)+ => (forall a. p a -> m) -> f p -> m+ foldMap = gfoldMap++gfoldMap :: (Generic1 f, Foldable (Rep1 f), Monoid m)+ => (forall a. p a -> m) -> f p -> m+gfoldMap f = foldMap f . from1++instance Foldable U1 where+ foldMap _ U1 = mempty++instance Foldable (K1 i c) where+ foldMap _ (K1 _) = mempty++instance (Foldable f, Foldable g) => Foldable (f :+: g) where+ foldMap f (L1 x) = foldMap f x+ foldMap f (R1 y) = foldMap f y++instance (Foldable f, Foldable g) => Foldable (f :*: g) where+ foldMap f (x :*: y) = foldMap f x `mappend` foldMap f y++instance (Rank1.Foldable f, Foldable g) => Foldable (f :.: g) where+ foldMap f (Comp1 fg) = Rank1.foldMap (foldMap f) fg++instance Foldable f => Foldable (M1 i c f) where+ foldMap f (M1 x) = foldMap f x++instance Foldable f => Foldable (Rec1 f) where+ foldMap f (Rec1 x) = foldMap f x++------------------------------------------------------------------------++class (Functor t, Foldable t) => Traversable (t :: (k -> *) -> *) where+ traverse :: Rank1.Applicative f => (forall a. p a -> f (q a)) -> t p -> f (t q)+ default traverse :: (Generic1 t, Traversable (Rep1 t), Rank1.Applicative f)+ => (forall a. p a -> f (q a)) -> t p -> f (t q)+ traverse = gtraverse++gtraverse :: (Generic1 t, Traversable (Rep1 t), Rank1.Applicative f)+ => (forall a. p a -> f (q a)) -> t p -> f (t q)+gtraverse f = Rank1.fmap to1 . traverse f . from1++instance Traversable U1 where+ traverse _ U1 = Rank1.pure U1++instance Traversable (K1 i c) where+ traverse _ (K1 c) = Rank1.pure (K1 c)++instance (Traversable f, Traversable g) => Traversable (f :+: g) where+ traverse f (L1 x) = L1 Rank1.<$> traverse f x+ traverse f (R1 y) = R1 Rank1.<$> traverse f y++instance (Traversable f, Traversable g) => Traversable (f :*: g) where+ traverse f (x :*: y) = (:*:) Rank1.<$> traverse f x Rank1.<*> traverse f y++instance (Rank1.Traversable f, Traversable g) => Traversable (f :.: g) where+ traverse f (Comp1 fg) = Comp1 Rank1.<$> Rank1.traverse (traverse f) fg++instance Traversable f => Traversable (M1 i c f) where+ traverse f (M1 x) = M1 Rank1.<$> traverse f x++instance Traversable f => Traversable (Rec1 f) where+ traverse f (Rec1 x) = Rec1 Rank1.<$> traverse f x
src/Test/StateMachine/Types/References.hs view
@@ -1,6 +1,6 @@-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-}@@ -21,106 +21,42 @@ ----------------------------------------------------------------------------- module Test.StateMachine.Types.References- ( Reference(..)+ ( Var(Var)+ , Symbolic(Symbolic)+ , Concrete(Concrete)+ , Reference(Reference)+ , reference , concrete , opaque- , Opaque(..)- , Symbolic(..)- , Concrete(..)- , Var(..)- ) where+ , Opaque(Opaque)+ , unOpaque+ )+ where import Data.Functor.Classes- (Eq1(..), Ord1(..), Show1(..), compare1, eq1,- showsPrec1)+ (Eq1, Ord1, Show1, compare1, eq1, liftCompare,+ liftEq, liftShowsPrec, showsPrec1)+import Data.TreeDiff+ (Expr(App), ToExpr, toExpr) import Data.Typeable (Typeable)--import Test.StateMachine.Types.HFunctor------------------------------------------------------------------------------ | References are the potential or actual result of executing an action. They--- are parameterised by either `Symbolic` or `Concrete` depending on the--- phase of the test.------ `Symbolic` variables are the potential results of actions. These are used--- when generating the sequence of actions to execute. They allow actions--- which occur later in the sequence to make use of the result of an action--- which came earlier in the sequence.------ `Concrete` variables are the actual results of actions. These are used--- during test execution. They provide access to the actual runtime value of--- a variable.----newtype Reference v a = Reference (v a)---- | Take the value from a concrete variable.----concrete :: Reference Concrete a -> a-concrete (Reference (Concrete x)) = x---- | Take the value from an opaque concrete variable.----opaque :: Reference Concrete (Opaque a) -> a-opaque (Reference (Concrete (Opaque x))) = x--instance (Eq1 v, Eq a) => Eq (Reference v a) where- (==) (Reference x) (Reference y) = eq1 x y--instance (Ord1 v, Ord a) => Ord (Reference v a) where- compare (Reference x) (Reference y) = compare1 x y--instance (Show1 v, Show a) => Show (Reference v a) where- showsPrec p (Reference v) = showParen (p > appPrec) $- showString "Reference " .- showsPrec1 p v- where- appPrec = 10--deriving instance Read (v a) => Read (Reference v a)--instance HTraversable Reference where- htraverse f (Reference v) = fmap Reference (f v)+import GHC.Generics+ (Generic)+import Prelude -instance HFunctor Reference-instance HFoldable Reference+import qualified Test.StateMachine.Types.Rank2 as Rank2 ------------------------------------------------------------------------ --- | Opaque values.------ Useful if you want to put something without a 'Show' instance inside--- something which you'd like to be able to display.----newtype Opaque a = Opaque- { unOpaque :: a- } deriving (Eq, Ord)--instance Show (Opaque a) where- showsPrec _ (Opaque _) = showString "Opaque"---- | Symbolic variable names.--- newtype Var = Var Int- deriving (Eq, Ord, Show, Num, Read)+ deriving (Eq, Ord, Show, Generic, ToExpr) --- | Symbolic values.--- data Symbolic a where Symbolic :: Typeable a => Var -> Symbolic a -deriving instance Eq (Symbolic a)-deriving instance Ord (Symbolic a) deriving instance Show (Symbolic a)-deriving instance Typeable a => Read (Symbolic a)-deriving instance Foldable Symbolic--instance Eq1 Symbolic where- liftEq _ (Symbolic x) (Symbolic y) = x == y--instance Ord1 Symbolic where- liftCompare _ (Symbolic x) (Symbolic y) = compare x y+deriving instance Eq (Symbolic a)+deriving instance Ord (Symbolic a) instance Show1 Symbolic where liftShowsPrec _ _ p (Symbolic x) =@@ -130,18 +66,20 @@ where appPrec = 10 --- | Concrete values.----newtype Concrete a where- Concrete :: a -> Concrete a- deriving (Eq, Ord, Show, Read, Functor, Foldable, Traversable)+instance ToExpr a => ToExpr (Symbolic a) where+ toExpr (Symbolic x) = toExpr x -instance Eq1 Concrete where- liftEq eq (Concrete x) (Concrete y) = eq x y+instance Eq1 Symbolic where+ liftEq _ (Symbolic x) (Symbolic y) = x == y -instance Ord1 Concrete where- liftCompare comp (Concrete x) (Concrete y) = comp x y+instance Ord1 Symbolic where+ liftCompare _ (Symbolic x) (Symbolic y) = compare x y +data Concrete a where+ Concrete :: Typeable a => a -> Concrete a++deriving instance Show a => Show (Concrete a)+ instance Show1 Concrete where liftShowsPrec sp _ p (Concrete x) = showParen (p > appPrec) $@@ -149,3 +87,58 @@ sp (appPrec + 1) x where appPrec = 10++instance Eq1 Concrete where+ liftEq eq (Concrete x) (Concrete y) = eq x y++instance Ord1 Concrete where+ liftCompare comp (Concrete x) (Concrete y) = comp x y++instance ToExpr a => ToExpr (Concrete a) where+ toExpr (Concrete x) = toExpr x++data Reference a r = Reference (r a)+ deriving Generic++instance ToExpr (r a) => ToExpr (Reference a r)++instance Rank2.Functor (Reference a) where+ fmap f (Reference r) = Reference (f r)++instance Rank2.Foldable (Reference a) where+ foldMap f (Reference r) = f r++instance Rank2.Traversable (Reference a) where+ traverse f (Reference r) = Reference <$> f r++instance (Eq a, Eq1 r) => Eq (Reference a r) where+ Reference x == Reference y = eq1 x y++instance (Ord a, Ord1 r) => Ord (Reference a r) where+ compare (Reference x) (Reference y) = compare1 x y++instance (Show1 r, Show a) => Show (Reference a r) where+ showsPrec p (Reference v) = showParen (p > appPrec) $+ showString "Reference " .+ showsPrec1 p v+ where+ appPrec = 10++reference :: Typeable a => a -> Reference a Concrete+reference = Reference . Concrete++concrete :: Reference a Concrete -> a+concrete (Reference (Concrete x)) = x++opaque :: Reference (Opaque a) Concrete -> a+opaque (Reference (Concrete (Opaque x))) = x++newtype Opaque a = Opaque+ { unOpaque :: a }+ deriving (Eq, Ord)++instance Show (Opaque a) where+ showsPrec _ (Opaque _) = showString "Opaque"++instance ToExpr (Opaque a) where+ toExpr _ = App "Opaque" []
src/Test/StateMachine/Utils.hs view
@@ -1,3 +1,7 @@+{-# OPTIONS_GHC -Wno-orphans #-}++{-# LANGUAGE CPP #-}+ ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Utils@@ -14,13 +18,95 @@ ----------------------------------------------------------------------------- module Test.StateMachine.Utils- ( anyP- , liftProperty+ ( liftProperty , whenFailM- , alwaysP+ , forAllShrinkShow+ , anyP , shrinkPair , shrinkPair'- , forAllShrinkShowC- ) where+ , suchThatOneOf+ )+ where -import Test.StateMachine.Internal.Utils+import Prelude+import Test.QuickCheck+ (Gen, Property, Testable, again, counterexample,+ frequency, resize, shrinking, sized, suchThatMaybe,+ whenFail)+import Test.QuickCheck.Monadic+ (PropertyM(MkPropertyM))+import Test.QuickCheck.Property+ (Property(MkProperty), property, unProperty, (.&&.),+ (.||.))+#if !MIN_VERSION_QuickCheck(2,10,0)+import Test.QuickCheck.Property+ (succeeded)+#endif++------------------------------------------------------------------------++-- | Lifts a plain property into a monadic property.+liftProperty :: Monad m => Property -> PropertyM m ()+liftProperty prop = MkPropertyM (\k -> fmap (prop .&&.) <$> k ())++-- | Lifts 'whenFail' to 'PropertyM'.+whenFailM :: Monad m => IO () -> Property -> PropertyM m ()+whenFailM m prop = liftProperty (m `whenFail` prop)++-- | A variant of 'Test.QuickCheck.Monadic.forAllShrink' with an+-- explicit show function.+forAllShrinkShow+ :: Testable prop+ => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property+forAllShrinkShow gen shrinker shower pf =+ again $+ MkProperty $+ gen >>= \x ->+ unProperty $+ shrinking shrinker x $ \x' ->+ counterexample (shower x') (pf x')++-- | Lifts 'Prelude.any' to properties.+anyP :: (a -> Property) -> [a] -> Property+anyP p = foldr (\x ih -> p x .||. ih) (property False)++-- | Given shrinkers for the components of a pair we can shrink the pair.+shrinkPair' :: (a -> [a]) -> (b -> [b]) -> ((a, b) -> [(a, b)])+shrinkPair' shrinkerA shrinkerB (x, y) =+ [ (x', y) | x' <- shrinkerA x ] +++ [ (x, y') | y' <- shrinkerB y ]++-- | Same above, but for homogeneous pairs.+shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)])+shrinkPair shrinker = shrinkPair' shrinker shrinker++#if !MIN_VERSION_QuickCheck(2,10,0)+instance Testable () where+ property = property . liftUnit+ where+ liftUnit () = succeeded+#endif++-- | Like 'Test.QuickCheck.suchThatMaybe', but retries @n@ times.+suchThatMaybeN :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)+suchThatMaybeN 0 _ _ = return Nothing+suchThatMaybeN n gen p = do+ mx <- gen `suchThatMaybe` p+ case mx of+ Just x -> return (Just x)+ Nothing -> sized (\m -> resize (m + 1) (suchThatMaybeN (n - 1) gen p))++suchThatOneOf :: [(Int, Gen a)] -> (a -> Bool) -> Gen (Maybe a)+gens0 `suchThatOneOf` p = go gens0 (length gens0 - 1)+ where+ go [] _ = return Nothing+ go gens n = do+ i <- frequency (zip (map fst gens) (map return [0 .. n]))+ case splitAt i gens of+ (_, []) -> error ("suchThatOneOf: impossible, as we" +++ " split the list on its length - 1.")+ (gens', gen : gens'') -> do+ mx <- suchThatMaybeN 20 (snd gen) p+ case mx of+ Just x -> return (Just x)+ Nothing -> go (gens' ++ gens'') (n - 1)
src/Test/StateMachine/Z.hs view
@@ -14,23 +14,67 @@ -- ----------------------------------------------------------------------------- -module Test.StateMachine.Z where+module Test.StateMachine.Z+ ( union+ , intersect+ , isSubsetOf+ , (~=)+ , Rel+ , Fun+ , empty+ , identity+ , singleton+ , domain+ , codomain+ , compose+ , fcompose+ , inverse+ , lookupDom+ , lookupCod+ , (<|)+ , (|>)+ , (<-|)+ , (|->)+ , image+ , (<+)+ , (<**>)+ , (<||>)+ , isTotalRel+ , isSurjRel+ , isTotalSurjRel+ , isPartialFun+ , isTotalFun+ , isPartialInj+ , isTotalInj+ , isPartialSurj+ , isTotalSurj+ , isBijection+ , (!)+ , (.%)+ , (.!)+ , (.=)+ ) where -import qualified Data.List as List+import qualified Data.List as L+import qualified Prelude as P+import Prelude hiding+ (elem, notElem) +import Test.StateMachine.Logic+ ------------------------------------------------------------------------ union :: Eq a => [a] -> [a] -> [a]-union = List.union+union = L.union intersect :: Eq a => [a] -> [a] -> [a]-intersect = List.intersect+intersect = L.intersect -isSubsetOf :: Eq a => [a] -> [a] -> Bool-r `isSubsetOf` s = r == r `intersect` s+isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic+r `isSubsetOf` s = r .== r `intersect` s -(~=) :: Eq a => [a] -> [a] -> Bool-xs ~= ys = xs `isSubsetOf` ys && ys `isSubsetOf` xs+(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic+xs ~= ys = xs `isSubsetOf` ys :&& ys `isSubsetOf` xs ------------------------------------------------------------------------ @@ -85,7 +129,7 @@ -- [('a',"apa")] -- (<|) :: Eq a => [a] -> Rel a b -> Rel a b-xs <| xys = [ (x, y) | (x, y) <- xys, x `elem` xs ]+xs <| xys = [ (x, y) | (x, y) <- xys, x `P.elem` xs ] -- | Codomain restriction. --@@ -93,7 +137,7 @@ -- [('a',"apa")] -- (|>) :: Eq b => Rel a b -> [b] -> Rel a b-xys |> ys = [ (x, y) | (x, y) <- xys, y `elem` ys ]+xys |> ys = [ (x, y) | (x, y) <- xys, y `P.elem` ys ] -- | Domain substraction. --@@ -101,7 +145,7 @@ -- [('b',"bepa")] -- (<-|) :: Eq a => [a] -> Rel a b -> Rel a b-xs <-| xys = [ (x, y) | (x, y) <- xys, x `notElem` xs ]+xs <-| xys = [ (x, y) | (x, y) <- xys, x `P.notElem` xs ] -- | Codomain substraction. --@@ -109,7 +153,7 @@ -- [('b',"bepa")] -- (|->) :: Eq b => Rel a b -> [b] -> Rel a b-xys |-> ys = [ (x, y) | (x, y) <- xys, y `notElem` ys ]+xys |-> ys = [ (x, y) | (x, y) <- xys, y `P.notElem` ys ] -- | The image of a relation. image :: Eq a => Rel a b -> [a] -> [b]@@ -145,35 +189,35 @@ ------------------------------------------------------------------------ -isTotalRel :: Eq a => Rel a b -> [a] -> Bool+isTotalRel :: (Eq a, Show a) => Rel a b -> [a] -> Logic isTotalRel r xs = domain r ~= xs -isSurjRel :: Eq b => Rel a b -> [b] -> Bool+isSurjRel :: (Eq b, Show b) => Rel a b -> [b] -> Logic isSurjRel r ys = codomain r ~= ys -isTotalSurjRel :: (Eq a, Eq b) => Rel a b -> [a] -> [b] -> Bool-isTotalSurjRel r xs ys = isTotalRel r xs && isSurjRel r ys+isTotalSurjRel :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic+isTotalSurjRel r xs ys = isTotalRel r xs :&& isSurjRel r ys -isPartialFun :: (Eq a, Eq b) => Rel a b -> Bool+isPartialFun :: (Eq a, Eq b, Show b) => Rel a b -> Logic isPartialFun f = (f `compose` inverse f) ~= identity (codomain f) -isTotalFun :: (Eq a, Eq b) => Rel a b -> [a] -> Bool-isTotalFun r xs = isPartialFun r && isTotalRel r xs+isTotalFun :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic+isTotalFun r xs = isPartialFun r :&& isTotalRel r xs -isPartialInj :: (Eq a, Eq b) => Rel a b -> Bool-isPartialInj r = isPartialFun r && isPartialFun (inverse r)+isPartialInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> Logic+isPartialInj r = isPartialFun r :&& isPartialFun (inverse r) -isTotalInj :: (Eq a, Eq b) => Rel a b -> [a] -> Bool-isTotalInj r xs = isTotalFun r xs && isPartialFun (inverse r)+isTotalInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic+isTotalInj r xs = isTotalFun r xs :&& isPartialFun (inverse r) -isPartialSurj :: (Eq a, Eq b) => Rel a b -> [b] -> Bool-isPartialSurj r ys = isPartialFun r && isSurjRel r ys+isPartialSurj :: (Eq a, Eq b, Show b) => Rel a b -> [b] -> Logic+isPartialSurj r ys = isPartialFun r :&& isSurjRel r ys -isTotalSurj :: (Eq a, Eq b) => Rel a b -> [a] -> [b] -> Bool-isTotalSurj r xs ys = isTotalFun r xs && isSurjRel r ys+isTotalSurj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic+isTotalSurj r xs ys = isTotalFun r xs :&& isSurjRel r ys -isBijection :: (Eq a, Eq b) => Rel a b -> [a] -> [b] -> Bool-isBijection r xs ys = isTotalInj r xs && isTotalSurj r xs ys+isBijection :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic+isBijection r xs ys = isTotalInj r xs :&& isTotalSurj r xs ys -- | Application. (!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b
+ test/CircularBuffer.hs view
@@ -0,0 +1,399 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}++-----------------------------------------------------------------------------+-- |+-- Module : CircularBuffer+-- Copyright : (C) 2017, Xia Li-yao+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Xia Li-yao+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains a specification of a circular buffer. Adapted+-- from John Hughes' /Experiences with QuickCheck: Testing the hard+-- stuff and staying sane/.+--+------------------------------------------------------------------------++module CircularBuffer+ ( unpropNoSizeCheck+ , unpropFullIsEmpty+ , unpropBadRem+ , unpropStillBadRem+ , prop_circularBuffer+ )+ where++import Control.Applicative+ (liftA2)+import Control.Monad+ (guard)+import Data.Function+ (on)+import Data.Functor.Classes+ (Eq1)+import Data.IORef+import Data.Maybe+ (isJust)+import Data.TreeDiff+ (ToExpr)+import Data.Vector.Unboxed.Mutable+ (IOVector)+import qualified Data.Vector.Unboxed.Mutable as V+import GHC.Generics+ (Generic, Generic1)+import Prelude hiding+ (elem)+import qualified Prelude as P+import Test.QuickCheck+ (Gen, Positive(..), Property, arbitrary, elements,+ frequency, shrink, (===))+import Test.QuickCheck.Monadic+ (monadicIO)++import Test.StateMachine+import qualified Test.StateMachine.Types.Rank2 as Rank2++------------------------------------------------------------------------++-- | Sets of bugs in the implementation and specification.+type Bugs = [Bug]++-- | Possible bugs.+--+-- See 'unpropNoSizeCheck', 'unpropFullIsEmpty', 'unpropBadRem',+-- and 'unpropStillBadRem'.+data Bug = NoSizeCheck | FullIsEmpty | BadRem | StillBadRem+ deriving (Eq, Enum)++-- | Switch to disable or enable testing of the 'lenBuffer' function.+data Version = NoLen | YesLen+ deriving Eq++------------------------------------------------------------------------++-- | An efficient mutable circular buffer.+data Buffer = Buffer+ { top :: IORef Int -- ^ Index to the top: where to 'Put' the next element+ , bot :: IORef Int -- ^ Index to the bottom: where to 'Get' the next element+ , arr :: IOVector Int -- ^ Array of elements of fixed capacity+ }++-- | Different buffers are assumed to have disjoint memories,+-- so we can use 'V.overlaps' to check equality.+instance Eq Buffer where+ (==) =+ ((==) `on` top) `also`+ ((==) `on` bot) `also`+ (V.overlaps `on` arr)+ where+ also = (liftA2 . liftA2) (&&)++-- | See 'New'.+newBuffer :: Bugs -> Int -> IO Buffer+newBuffer bugs n = Buffer+ <$> newIORef 0+ <*> newIORef 0+ <*> V.new (if FullIsEmpty `P.elem` bugs then n else n + 1)++-- | See 'Put'.+putBuffer :: Int -> Buffer -> IO ()+putBuffer x Buffer{top, arr} = do+ i <- readIORef top+ V.write arr i x+ writeIORef top $! (i + 1) `mod` V.length arr++-- | See 'Get'.+getBuffer :: Buffer -> IO Int+getBuffer Buffer{bot, arr} = do+ j <- readIORef bot+ y <- V.read arr j+ writeIORef bot $! (j + 1) `mod` V.length arr+ return y++-- | See 'Len'.+lenBuffer :: Bugs -> Buffer -> IO Int+lenBuffer bugs Buffer{top, bot, arr} = do+ i <- readIORef top+ j <- readIORef bot+ return $+ if BadRem `P.elem` bugs then+ (i - j) `rem` V.length arr+ else if StillBadRem `P.elem` bugs then+ abs ((i - j) `rem` V.length arr)+ else+ (i - j) `mod` V.length arr++------------------------------------------------------------------------++-- | Buffer actions.+data Action (r :: * -> *)+ -- | Create a new buffer of bounded capacity.+ = New Int++ -- | Put an element at the top of the buffer.+ | Put Int (Reference (Opaque Buffer) r)++ -- | Get an element out of the bottom of the buffer.+ | Get (Reference (Opaque Buffer) r)++ -- | Get the number of elements in the buffer.+ | Len (Reference (Opaque Buffer) r)+ deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)++data Response (r :: * -> *)+ = NewR (Reference (Opaque Buffer) r)+ | PutR+ | GetR Int+ | LenR Int+ deriving (Show, Generic1, Rank2.Foldable)++------------------------------------------------------------------------++-- | A simple, persistent, inefficient buffer.+--+-- The top of the buffer is the head of the list, the bottom is the last+-- element.+data SpecBuffer = SpecBuffer+ { specSize :: Int -- ^ Maximum number of elements+ , specContents :: [Int] -- ^ Contents of the buffer+ }+ deriving (Generic, Show, ToExpr)++emptySpecBuffer :: Int -> SpecBuffer+emptySpecBuffer n = SpecBuffer n []++insertSpecBuffer :: Int -> SpecBuffer -> SpecBuffer+insertSpecBuffer x (SpecBuffer n xs) = SpecBuffer n (x : xs)++removeSpecBuffer :: SpecBuffer -> (Int, SpecBuffer)+removeSpecBuffer (SpecBuffer n xs) = (last xs, SpecBuffer n (init xs))++------------------------------------------------------------------------++-- | The model is a map from buffer references to their values.+newtype Model r = Model [(Reference (Opaque Buffer) r, SpecBuffer)]+ deriving (Generic, Show)++deriving instance ToExpr (Model Concrete)++-- | Initially, there are no references to buffers.+initModel :: Model v+initModel = Model []++precondition :: Bugs -> Model Symbolic -> Action Symbolic -> Logic+precondition _ _ (New n) = n .> 0+precondition bugs (Model m) (Put _ buffer) | NoSizeCheck `P.elem` bugs =+ buffer `elem` map fst m+precondition _ (Model m) (Put _ buffer) = Boolean $ isJust $ do+ specBuffer <- lookup buffer m+ guard $ length (specContents specBuffer) < specSize specBuffer+precondition _ (Model m) (Get buffer) = Boolean $ isJust $ do+ specBuffer <- lookup buffer m+ guard $ not (null (specContents specBuffer))+precondition _ (Model m) (Len buffer) = buffer `elem` map fst m++transition :: Eq1 r => Model r -> Action r -> Response r -> Model r+transition (Model m) (New n) (NewR ref) =+ Model ((ref, emptySpecBuffer n) : m)+transition (Model m) (Put x buffer) _ =+ case lookup buffer m of+ Just old -> Model (update buffer (insertSpecBuffer x old) m)+ Nothing -> error "transition: put"+transition (Model m) (Get buffer) _ =+ case lookup buffer m of+ Just old ->+ let (_, new) = removeSpecBuffer old in+ Model (update buffer new m)+ Nothing -> error "transition: get"+transition m _ _ = m++update :: Eq a => a -> b -> [(a, b)] -> [(a, b)]+update ref i m = (ref, i) : filter ((/= ref) . fst) m++postcondition :: Model Concrete -> Action Concrete -> Response Concrete -> Logic+postcondition _ (New _) _ = Top+postcondition _ (Put _ _) _ = Top+postcondition (Model m) (Get buffer) (GetR y) = case lookup buffer m of+ Nothing -> Bot+ Just specBuffer ->+ let (y', _) = removeSpecBuffer specBuffer+ in y .== y'+postcondition (Model m) (Len buffer) (LenR k) = case lookup buffer m of+ Nothing -> Bot+ Just specBuffer -> k .== length (specContents specBuffer)+postcondition _ _ _ = error "postcondition"++------------------------------------------------------------------------++genNew :: Gen (Action Symbolic)+genNew = do+ Positive n <- arbitrary+ return (New n)++generator :: Version -> Model Symbolic -> Gen (Action Symbolic)+generator _ (Model m) | null m = genNew+generator version (Model m) = frequency $+ [ (1, genNew)+ , (4, Put <$> arbitrary <*> (fst <$> elements m))+ , (4, Get <$> (fst <$> elements m))+ ] +++ [ (4, Len <$> (fst <$> elements m)) | version == YesLen ]++shrinker :: Action Symbolic -> [Action Symbolic]+shrinker (New n) = [ New n' | n' <- shrink n ]+shrinker (Put x buffer) = [ Put x' buffer | x' <- shrink x ]+shrinker _ = []++------------------------------------------------------------------------++semantics :: Bugs -> Action Concrete -> IO (Response Concrete)+semantics bugs (New n) = NewR . reference . Opaque <$> newBuffer bugs n+semantics _ (Put x buffer) = PutR <$ putBuffer x (opaque buffer)+semantics _ (Get buffer) = GetR <$> getBuffer (opaque buffer)+semantics bugs (Len buffer) = LenR <$> lenBuffer bugs (opaque buffer)++mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)+mock _ (New _) = NewR <$> genSym+mock _ (Put _ _) = pure PutR+mock (Model m) (Get buffer) = case lookup buffer m of+ Nothing -> error "mock: get"+ Just spec -> case specContents spec of+ [] -> error "mock: get 2"+ (i : _) -> pure (GetR i)+mock (Model m) (Len buffer) = case lookup buffer m of+ Nothing -> error "mock: len"+ Just spec -> pure (LenR (specSize spec))++------------------------------------------------------------------------++sm :: Version -> Bugs -> StateMachine Model Action IO Response+sm version bugs = StateMachine+ initModel transition (precondition bugs) postcondition+ Nothing Nothing (generator version) Nothing+ shrinker (semantics bugs) P.id mock++-- | Property parameterized by spec version and bugs.+prepropcircularBuffer :: Version -> Bugs -> Property+prepropcircularBuffer version bugs =+ forAllCommands sm' Nothing $ \cmds -> monadicIO $ do+ (hist, _, res) <- runCommands sm' cmds+ prettyCommands sm' hist $+ checkCommandNames cmds (res === Ok)+ where+ sm' = sm version bugs++-- Adapted from John Hughes'+-- /Experiences with QuickCheck: Testing the hard stuff and staying sane/,++-- | The first bug. 'NoSizeCheck'+--+-- Putting more elements than the capacity of the buffer (set when it is+-- constructed using 'New') causes a buffer overflow: new elements overwrite+-- older ones that haven't been removed yet.+-- A minimal counterexample that reveals the bug is simply:+--+-- > buffer <- newBuffer 1+-- > putBuffer 0 buffer+-- > putBuffer 1 buffer+-- > getBuffer buffer+-- >+-- > -- Expected: 0+-- > -- Actual: 1+--+-- The mistake is in the specification: it models an unbounded buffer.+-- For a bounded buffer, that sequence of calls makes no sense.+-- The fix is to add a precondition to forbid 'Put' when the buffer is full.++unpropNoSizeCheck :: Property+unpropNoSizeCheck = prepropcircularBuffer NoLen [NoSizeCheck ..]++-- | The second bug. 'FullIsEmpty'+--+-- The top and bottom pointers wrap around when they reach the end of the+-- array. We have that @top == bottom@ whenever the buffer is either empty or+-- full.+-- In other words, a full buffer is undistinguishable from an empty one.+-- A minimal counterexample:+--+-- > buffer <- newBuffer 1+-- > putBuffer 0 buffer+-- > lenBuffer buffer+-- >+-- > -- Expected: 1+-- > -- Actual: 0+--+-- In this implementation, the length of a buffer is given by the remainder of+-- a division by its capacity. When the capacity is one, that remainder is+-- always 0.+-- The fix is to allocate one more cell when we allocate a 'New' buffer.+--+-- In a way, the bug is still there. But to observe it, one has to+-- 'Put' one more element than the buffer capacity. Since this violates the+-- specification, it's the user's fault!++unpropFullIsEmpty :: Property+unpropFullIsEmpty = prepropcircularBuffer YesLen [FullIsEmpty ..]++-- | The third bug. 'BadRem'+--+-- The length of a buffer uses 'rem', which is the remainder of a+-- division truncated towards zero (the standard division in many languages,+-- such as C, but not Haskell). When the dividend @(top - bottom)@ is negative,+-- the remainder is non-positive.+-- A minimal counterexample:+--+-- > buffer <- newBuffer 1+-- > putBuffer 0 buffer+-- > getBuffer buffer+-- > putBuffer 0 buffer+-- > lenBuffer buffer+-- >+-- > -- Expected: 1+-- > -- Actual: -1+--+-- The fix is to ensure the remainder is non-negative...++unpropBadRem :: Property+unpropBadRem = prepropcircularBuffer YesLen [BadRem ..]++-- | The fourth bug. 'StillBadRem'+--+-- ... One way to obtain a non-negative remainder is to make the dividend+-- non-negative. /Clearly/ we should divide by the absolute value instead.+-- QuickCheck provides a minimal counterexample to that "obvious" fix:+--+-- > buffer <- newBuffer 2+-- > putBuffer 0 buffer+-- > getBuffer buffer+-- > putBuffer 0 buffer+-- > putBuffer 0 buffer+-- > lenBuffer len+-- >+-- > -- Expected: 2+-- > -- Actual: 1+--+-- As an aside, for the first time, the buffer /needs/ to be of capacity two.+-- That non-fix fixed buffers of capacity one!+--+-- The actual fix is to use 'mod',+-- which performs division rounding towards -∞.++unpropStillBadRem :: Property+unpropStillBadRem = prepropcircularBuffer YesLen [StillBadRem]++-- | And now tests pass.++prop_circularBuffer :: Property+prop_circularBuffer = prepropcircularBuffer YesLen []
+ test/CrudWebserverDb.hs view
@@ -0,0 +1,521 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++-- NOTE: Make sure NOT to use DeriveAnyClass, or persistent-template+-- will do the wrong thing.++------------------------------------------------------------------------+-- |+-- Module : CrudWebserverDb+-- Copyright : (C) 2016, James M.C. Haver II, Sönke Hahn;+-- (C) 2017-2018, Stevan Andjelkovic+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains the implementation and specification of a simple+-- CRUD webserver that uses a postgresql database to store data.+--+-- The implementation is based on Servant's+-- <https://github.com/haskell-servant/example-servant-persistent example-servant-persistent>+-- repository.+--+-- Readers who are not familiar with the+-- <http://haskell-servant.readthedocs.io/en/stable/ Servant> library+-- and/or the <http://www.yesodweb.com/book/persistent Persistent>+-- library might want consult the respective library's documentation in+-- case any part of the implementation of the webserver is unclear.+--+------------------------------------------------------------------------++module CrudWebserverDb+ ( prop_crudWebserverDb+ , prop_crudWebserverDbParallel+ , Bug(..)+ , setup+ , cleanup+ , connectionString+ , demoNoBug+ , demoLogicBug+ , demoNoRace+ , demoRace+ , UserId -- Only to silence unused warning.+ )+ where++import Control.Concurrent+ (newEmptyMVar, putMVar, takeMVar, threadDelay)+import Control.Concurrent.Async.Lifted+ (Async, async, cancel, waitEither)+import Control.Exception+ (IOException, bracket)+import Control.Exception+ (catch)+import Control.Monad.IO.Class+ (liftIO)+import Control.Monad.Logger+ (NoLoggingT, runNoLoggingT)+import Control.Monad.Reader+ (ReaderT, ask, runReaderT)+import Control.Monad.Trans.Control+ (MonadBaseControl, liftBaseWith)+import Control.Monad.Trans.Resource+ (ResourceT)+import qualified Data.ByteString.Char8 as BS+import Data.Char+ (isPrint)+import Data.Functor.Classes+ (Eq1)+import Data.List+ (dropWhileEnd)+import Data.Monoid+ ((<>))+import Data.Proxy+ (Proxy(Proxy))+import Data.String.Conversions+ (cs)+import Data.Text+ (Text)+import qualified Data.Text as T+import Data.TreeDiff+ (Expr(App), ToExpr, toExpr)+import Database.Persist.Postgresql+ (ConnectionPool, ConnectionString, Key, SqlBackend,+ delete, get, getJust, insert, liftSqlPersistMPool,+ replace, runMigration, runSqlPool, update,+ withPostgresqlPool, (+=.))+import Database.Persist.TH+ (mkMigrate, mkPersist, persistLowerCase, share,+ sqlSettings)+import GHC.Generics+ (Generic, Generic1)+import Network+ (PortID(PortNumber), connectTo)+import Network.HTTP.Client+ (Manager, defaultManagerSettings, newManager)+import qualified Network.Wai.Handler.Warp as Warp+import Prelude hiding+ (elem)+import qualified Prelude+import Servant+ ((:<|>)(..), (:>), Application, Capture, Delete,+ Get, JSON, Post, Put, ReqBody, Server, serve)+import Servant.Client+ (BaseUrl(..), ClientEnv(..), ClientM, Scheme(Http),+ client, mkClientEnv, runClientM)+import Servant.Server+ (Handler)+import System.IO+ (Handle, hClose)+import System.Process+ (callProcess, readProcess)+import Test.QuickCheck+ (Arbitrary, Gen, Property, arbitrary, elements,+ expectFailure, frequency, ioProperty, listOf,+ quickCheck, shrink, suchThat, verboseCheck, (===))+import Test.QuickCheck.Instances+ ()+import Test.QuickCheck.Monadic+ (monadic)++import Test.StateMachine+import qualified Test.StateMachine.Types.Rank2 as Rank2++------------------------------------------------------------------------+-- * User datatype+++++share [mkPersist sqlSettings, mkMigrate "migrateAll"] [persistLowerCase|+User json+ name Text+ age Int+ deriving Eq Read Show Generic+|]++-- data User = User+-- { name :: Text+-- , age :: Int+-- }++instance ToExpr User where++------------------------------------------------------------------------+-- * API+++++type Api =+ "user" :> "add" :> ReqBody '[JSON] User :> Post '[JSON] (Key User)+ :<|> "user" :> "get" :> Capture "key" (Key User) :> Get '[JSON] (Maybe User)+ :<|> "user" :> "inc" :> Capture "key" (Key User) :> Put '[JSON] ()+ :<|> "user" :> "del" :> Capture "key" (Key User) :> Delete '[JSON] ()++ :<|> "health" :> Get '[JSON] ()++++++++------------------------------------------------------------------------+-- * Server implementation++data Bug = None | Logic | Race++server :: Bug -> ConnectionPool -> Server Api+server bug pool =+ userAdd :<|> userGet :<|> userBirthday :<|> userDelete :<|> health+ where+ userAdd :: User -> Handler (Key User)+ userAdd newUser = sql (insert newUser)++ userGet :: Key User -> Handler (Maybe User)+ userGet key = sql (get key)++ userBirthday :: Key User -> Handler ()+ userBirthday key = sql $ case bug of+ None -> update key [UserAge +=. 1]+ Logic -> update key [UserAge +=. 2]+ Race -> do+ User name age <- getJust key+ replace key (User name (age + 1))++ userDelete :: Key User -> Handler ()+ userDelete key = sql $ do+ muser <- get key -- Make sure that the record exists.+ case muser of+ Just _ -> delete key+ Nothing -> error "userDelete: user doesn't exist."++ health :: Handler ()+ health = return ()++ sql :: ReaderT SqlBackend (NoLoggingT (ResourceT IO)) a -> Handler a+ sql q = liftSqlPersistMPool q pool++------------------------------------------------------------------------+-- * Client bindings+++postUserC :: User -> ClientM (Key User)+getUserC :: Key User -> ClientM (Maybe User)+incAgeUserC :: Key User -> ClientM ()+deleteUserC :: Key User -> ClientM ()+healthC :: ClientM ()++postUserC :<|> getUserC :<|> incAgeUserC :<|> deleteUserC :<|> healthC+ = client api++++++++------------------------------------------------------------------------+-- * Implementation done, modelling starts++++data Action (r :: * -> *)+ = PostUser User+ | GetUser (Reference (Key User) r)+ | IncAgeUser (Reference (Key User) r)+ | DeleteUser (Reference (Key User) r)+ deriving (Show, Generic1)++instance Rank2.Functor Action where+instance Rank2.Foldable Action where+instance Rank2.Traversable Action where++data Response (r :: * -> *)+ = PostedUser (Reference (Key User) r)+ | GotUser (Maybe User)+ | IncedAgeUser+ | DeletedUser+ deriving (Show, Generic1)++instance Rank2.Foldable Response where++------------------------------------------------------------------------+-- * State machine model+++newtype Model r = Model [(Reference (Key User) r, User)]+ deriving (Generic, Show)++instance ToExpr (Model Concrete) where++instance ToExpr (Key User) where+ toExpr key = App (show key) []++initModel :: Model v+initModel = Model []++transitions :: Eq1 r => Model r -> Action r -> Response r -> Model r+transitions (Model m) (PostUser user) (PostedUser key) =+ Model (m ++ [(key, user)])+transitions m (GetUser _) (GotUser _) =+ m+transitions (Model m) (IncAgeUser key) IncedAgeUser =+ case lookup key m of+ Nothing -> Model m+ Just (User user age) ->+ Model (updateModel key (User user (age + 1)) m)+transitions (Model m) (DeleteUser key) DeletedUser =+ Model (filter ((/= key) . fst) m)+transitions _ _ _ =+ error "transitions"+++------------------------------------------------------------------------+-- * Pre-requisites and invariants++preconditions :: Model Symbolic -> Action Symbolic -> Logic+preconditions _ (PostUser _) = Top+preconditions (Model m) (GetUser key) = key `elem` map fst m+preconditions (Model m) (IncAgeUser key) = key `elem` map fst m+preconditions (Model m) (DeleteUser key) = key `elem` map fst m++++postconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic+postconditions _ (PostUser _) _ = Top+postconditions (Model m) (GetUser key) (GotUser musr) = lookup key m .== musr+postconditions _ (IncAgeUser _) _ = Top+postconditions _ (DeleteUser _) _ = Top+postconditions _ _ _ = error "postconditions"++++------------------------------------------------------------------------+-- * How to generate and shrink programs.++generator :: Model Symbolic -> Gen (Action Symbolic)+generator (Model m) = frequency+ [ (1, PostUser <$> arbitrary)+ , (3, GetUser <$> elements (map fst m))+ , (4, IncAgeUser <$> elements (map fst m))+ , (2, DeleteUser <$> elements (map fst m))+ ]++shrinker :: Action Symbolic -> [Action Symbolic]+shrinker (PostUser (User user age)) =+ [ PostUser (User user' age') | (user', age') <- shrink (user, age) ]+shrinker _ = []++------------------------------------------------------------------------+-- * The semantics.+++semantics :: Action Concrete -> ReaderT ClientEnv IO (Response Concrete)+semantics act = do+ env <- ask+ res <- liftIO $ flip runClientM env $ case act of+ PostUser user -> PostedUser . reference <$> postUserC user+ GetUser key -> GotUser <$> getUserC (concrete key)+ IncAgeUser key -> IncedAgeUser <$ incAgeUserC (concrete key)+ DeleteUser key -> DeletedUser <$ deleteUserC (concrete key)+ case res of+ Left err -> error (show err)+ Right resp -> return resp++mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)+mock (Model m) act = case act of+ PostUser _ -> PostedUser <$> genSym+ GetUser key -> GotUser <$> pure (lookup key m)+ IncAgeUser _key -> pure IncedAgeUser+ DeleteUser _key -> pure DeletedUser++------------------------------------------------------------------------++sm :: Warp.Port -> StateMachine Model Action (ReaderT ClientEnv IO) Response+sm port = StateMachine initModel transitions preconditions postconditions+ Nothing Nothing generator Nothing+ shrinker semantics (runner port) mock++------------------------------------------------------------------------+-- * Sequential property++prop_crudWebserverDb :: Int -> Property+prop_crudWebserverDb port =+ forAllCommands sm' Nothing $ \cmds -> monadic (ioProperty . runner port) $ do+ (hist, _, res) <- runCommands sm' cmds+ prettyCommands sm' hist (res === Ok)+ where+ sm' = sm port++withCrudWebserverDb :: Bug -> Int -> IO () -> IO ()+withCrudWebserverDb bug port run =+ bracket+ (setup bug connectionString port)+ cleanup+ (const run)++demoNoBug', demoLogicBug', demoNoRace' :: Int -> IO ()+demoNoBug' port = withCrudWebserverDb None port+ (verboseCheck (prop_crudWebserverDb port))+demoLogicBug' port = withCrudWebserverDb Logic port+ (verboseCheck (expectFailure (prop_crudWebserverDb port)))+demoNoRace' port = withCrudWebserverDb Race port+ (quickCheck (prop_crudWebserverDb port))++demoNoBug, demoLogicBug, demoNoRace :: IO ()+demoNoBug = demoNoBug' crudWebserverDbPort+demoLogicBug = demoLogicBug' crudWebserverDbPort+demoNoRace = demoNoRace' crudWebserverDbPort++-----------------------------------------------------------------------+-- * Parallel property++prop_crudWebserverDbParallel :: Int -> Property+prop_crudWebserverDbParallel port =+ forAllParallelCommands sm' $ \cmds -> monadic (ioProperty . runner port) $ do+ prettyParallelCommands cmds =<< runParallelCommandsNTimes 30 sm' cmds+ where+ sm' = sm port++demoRace' :: Int -> IO ()+demoRace' port = withCrudWebserverDb Race port+ (quickCheck (expectFailure (prop_crudWebserverDbParallel port)))++demoRace :: IO ()+demoRace = demoRace' crudWebserverDbParallelPort++------------------------------------------------------------------------++app :: Bug -> ConnectionPool -> Application+app bug pool = serve (Proxy :: Proxy Api) (server bug pool)++mkApp :: Bug -> ConnectionString -> IO Application+mkApp bug conn = runNoLoggingT $+ withPostgresqlPool (cs conn) 10 $ \pool -> do+ runSqlPool (runMigration migrateAll) pool+ return (app bug pool)++runServer :: Bug -> ConnectionString -> Warp.Port -> IO () -> IO ()+runServer bug conn port ready = do+ app' <- mkApp bug conn+ Warp.runSettings settings app'+ where+ settings+ = Warp.setPort port+ . Warp.setBeforeMainLoop ready+ $ Warp.defaultSettings++------------------------------------------------------------------------++connectionString :: String -> ConnectionString+connectionString ip = "host=" <> BS.pack ip+ <> " dbname=postgres user=postgres password=mysecretpassword port=5432"++updateModel :: Eq a => a -> b -> [(a, b)] -> [(a, b)]+updateModel x y xys = (x, y) : filter ((/= x) . fst) xys++api :: Proxy Api+api = Proxy++crudWebserverDbPort :: Int+crudWebserverDbPort = 8083++crudWebserverDbParallelPort :: Int+crudWebserverDbParallelPort = 8084++instance Arbitrary User where+ arbitrary = User <$> (T.pack <$> listOf (arbitrary `suchThat` isPrint))+ <*> arbitrary++runner :: Warp.Port -> ReaderT ClientEnv IO Property -> IO Property+runner port p = do+ mgr <- newManager defaultManagerSettings+ runReaderT p (mkClientEnv mgr (burl port))++burl :: Warp.Port -> BaseUrl+burl port = BaseUrl Http "localhost" port ""++setup+ :: MonadBaseControl IO m+ => Bug -> (String -> ConnectionString) -> Warp.Port -> m (String, Async ())+setup bug conn port = liftBaseWith $ \_ -> do+ (pid, dbIp) <- setupDb+ signal <- newEmptyMVar+ aServer <- async (runServer bug (conn dbIp) port (putMVar signal ()))+ aConfirm <- async (takeMVar signal)+ ok <- waitEither aServer aConfirm+ case ok of+ Right () -> do+ mgr <- newManager defaultManagerSettings+ healthy mgr 10+ return (pid, aServer)+ Left () -> error "Server should not return"+ where+ healthy :: Manager -> Int -> IO ()+ healthy _ 0 = error "healthy: server isn't healthy"+ healthy mgr tries = do+ res <- liftIO $ runClientM healthC (mkClientEnv mgr (burl port))+ case res of+ Left _ -> do+ threadDelay 1000000+ healthy mgr (tries - 1)+ Right () -> return ()++setupDb :: IO (String, String)+setupDb = do+ pid <- trim <$> readProcess "docker"+ [ "run"+ , "-d"+ , "-e", "POSTGRES_PASSWORD=mysecretpassword"+ , "postgres:10.2"+ ] ""+ ip <- trim <$> readProcess "docker"+ [ "inspect"+ , pid+ , "--format"+ , "'{{range .NetworkSettings.Networks}}{{.IPAddress}}{{end}}'"+ ] ""+ healthyDb ip+ return (pid, ip)+ where+ trim :: String -> String+ trim = dropWhileEnd isGarbage . dropWhile isGarbage+ where+ isGarbage = flip Prelude.elem ['\'', '\n']++ healthyDb :: String -> IO ()+ healthyDb ip = do+ handle <- go 10+ hClose handle+ where+ go :: Int -> IO Handle+ go 0 = error "healtyDb: db isn't healthy"+ go n = do+ connectTo ip (PortNumber 5432)+ `catch` (\(_ :: IOException) -> do+ threadDelay 1000000+ go (n - 1))+++cleanup :: (String, Async ()) -> IO ()+cleanup (pid, aServer) = do+ callProcess "docker" [ "rm", "-f", pid ]+ cancel aServer
+ test/DieHard.hs view
@@ -0,0 +1,215 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}++-----------------------------------------------------------------------------+-- |+-- Module : DieHard+-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains a solution to the water jug puzzle featured in+-- /Die Hard 3/.+--+-----------------------------------------------------------------------------++module DieHard+ ( Command(..)+ , Model(..)+ , initModel+ , transitions+ , prop_dieHard+ ) where++import Data.TreeDiff+ (ToExpr)+import GHC.Generics+ (Generic, Generic1)+import Prelude+import Test.QuickCheck+ (Gen, Property, oneof, (===))+import Test.QuickCheck.Monadic+ (monadicIO)++import Test.StateMachine+import qualified Test.StateMachine.Types.Rank2 as Rank2++------------------------------------------------------------------------++-- The problem is to measure exactly 4 liters of water given a 3- and+-- 5-liter jug.++-- We start of defining the different actions that are allowed:++data Command (r :: * -> *)+ = FillBig -- Fill the 5-liter jug.+ | FillSmall -- Fill the 3-liter jug.+ | EmptyBig -- Empty the 5-liter jug.+ | EmptySmall+ | SmallIntoBig -- Pour the contents of the 3-liter jug+ -- into 5-liter jug.+ | BigIntoSmall+ deriving (Eq, Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)++data Response (r :: * -> *) = Done+ deriving (Show, Generic1, Rank2.Foldable)++------------------------------------------------------------------------++-- The model (or state) keeps track of what amount of water is in the+-- two jugs.++data Model (r :: * -> *) = Model+ { bigJug :: Int+ , smallJug :: Int+ } deriving (Show, Eq, Generic)++deriving instance ToExpr (Model Concrete)++initModel :: Model r+initModel = Model 0 0++------------------------------------------------------------------------++-- There are no pre-conditions for our actions. That simply means that+-- any action can happen at any state.++preconditions :: Model Symbolic -> Command Symbolic -> Logic+preconditions _ _ = Top++-- The transitions describe how the actions change the state.++transitions :: Model r -> Command r -> Response r -> Model r+transitions m FillBig _ = m { bigJug = 5 }+transitions m FillSmall _ = m { smallJug = 3 }+transitions m EmptyBig _ = m { bigJug = 0 }+transitions m EmptySmall _ = m { smallJug = 0 }+transitions (Model big small) SmallIntoBig _ =+ let big' = min 5 (big + small) in+ Model { bigJug = big'+ , smallJug = small - (big' - big) }+transitions (Model big small) BigIntoSmall _ =+ let small' = min 3 (big + small) in+ Model { bigJug = big - (small' - small)+ , smallJug = small'+ }++-- The post-condition is used in a bit of a funny way. Recall that we+-- want to find a series of actions that leads to the big jug containing+-- 4 liters. So the idea is to state an invariant saying that the big+-- jug is NOT equal to 4 after we performed any action. If we happen to+-- find a series of actions where this is not true, i.e. the big jug+-- actually does contain 4 liters, then a minimal counter example will+-- be presented -- this will be our solution.++postconditions :: Model r -> Command r -> Response r -> Logic+postconditions s c r = bigJug (transitions s c r) ./= 4++------------------------------------------------------------------------++-- The generator of actions is simple, with equal distribution pick an+-- action.++generator :: Model Symbolic -> Gen (Command Symbolic)+generator _ = oneof+ [ return FillBig+ , return FillSmall+ , return EmptyBig+ , return EmptySmall+ , return SmallIntoBig+ , return BigIntoSmall+ ]++-- There's nothing to shrink.++shrinker :: Command r -> [Command r]+shrinker _ = []++------------------------------------------------------------------------++-- We are not modelling an actual program here, so there's no semantics+-- for our actions. We are merely doing model checking.++semantics :: Command Concrete -> IO (Response Concrete)+semantics _ = return Done++mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)+mock _ _ = return Done++------------------------------------------------------------------------++-- Finally we have all the pieces needed to get the sequential property!++-- To make the code fit on a line, we first group all things related to+-- generation and execution of programs respectively.++sm :: StateMachine Model Command IO Response+sm = StateMachine initModel transitions preconditions postconditions+ (Just postconditions) Nothing+ generator Nothing shrinker semantics id mock++prop_dieHard :: Property+prop_dieHard = forAllCommands sm Nothing $ \cmds -> monadicIO $ do+ (hist, _model, res) <- runCommands sm cmds+ prettyCommands sm hist (checkCommandNames cmds (res === Ok))++-- If we run @quickCheck prop_dieHard@ we get:+--+-- @+-- *** Failed! Falsifiable (after 43 tests and 4 shrinks):+-- Commands+-- { unCommands =+-- [ Command FillBig (fromList [])+-- , Command BigIntoSmall (fromList [])+-- , Command EmptySmall (fromList [])+-- , Command BigIntoSmall (fromList [])+-- , Command FillBig (fromList [])+-- , Command BigIntoSmall (fromList [])+-- ]+-- }+--+-- Model {bigJug = 0,smallJug = 0}+--+-- == FillBig ==> Done [ 0 ]+--+-- Model {bigJug = -0 +5+-- ,smallJug = 0}+--+-- == BigIntoSmall ==> Done [ 0 ]+--+-- Model {bigJug = -5 +2+-- ,smallJug = -0 +3}+--+-- == EmptySmall ==> Done [ 0 ]+--+-- Model {bigJug = 2+-- ,smallJug = -3 +0}+--+-- == BigIntoSmall ==> Done [ 0 ]+--+-- Model {bigJug = -2 +0+-- ,smallJug = -0 +2}+--+-- == FillBig ==> Done [ 0 ]+--+-- Model {bigJug = -0 +5+-- ,smallJug = 2}+--+-- == BigIntoSmall ==> Done [ 0 ]+--+-- Model {bigJug = -5 +4+-- ,smallJug = -2 +3}+--+-- PostconditionFailed "PredicateC (4 :== 4)" /= Ok+-- @+--+-- The counterexample is our solution.
+ test/MemoryReference.hs view
@@ -0,0 +1,168 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MonoLocalBinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}++module MemoryReference+ ( prop_sequential+ , prop_parallel+ , Bug(..)+ )+ where++import Control.Concurrent+ (threadDelay)+import Data.Functor.Classes+ (Eq1)+import Data.IORef+ (IORef, atomicModifyIORef', newIORef, readIORef,+ writeIORef)+import Data.TreeDiff+ (ToExpr)+import GHC.Generics+ (Generic, Generic1)+import Prelude hiding+ (elem)+import qualified Prelude+import System.Random+ (randomRIO)+import Test.QuickCheck+ (Gen, Property, arbitrary, elements, frequency,+ shrink, (===))+import Test.QuickCheck.Monadic+ (monadicIO)++import Test.StateMachine+import qualified Test.StateMachine.Types.Rank2 as Rank2+import Test.StateMachine.Z++------------------------------------------------------------------------++data Command r+ = Create+ | Read (Reference (Opaque (IORef Int)) r)+ | Write (Reference (Opaque (IORef Int)) r) Int+ | Increment (Reference (Opaque (IORef Int)) r)+ deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)++deriving instance Show (Command Symbolic)+deriving instance Show (Command Concrete)++data Response r+ = Created (Reference (Opaque (IORef Int)) r)+ | ReadValue Int+ | Written+ | Incremented+ deriving (Generic1, Rank2.Foldable)++deriving instance Show (Response Symbolic)+deriving instance Show (Response Concrete)++newtype Model r = Model [(Reference (Opaque (IORef Int)) r, Int)]+ deriving (Generic, Show)++instance ToExpr (Model Symbolic)+instance ToExpr (Model Concrete)++initModel :: Model r+initModel = Model empty++transition :: Eq1 r => Model r -> Command r -> Response r -> Model r+transition m@(Model model) cmd resp = case (cmd, resp) of+ (Create, Created ref) -> Model ((ref, 0) : model)+ (Read _, ReadValue _) -> m+ (Write ref x, Written) -> Model (update ref x model)+ (Increment ref, Incremented) -> case lookup ref model of+ Just i -> Model (update ref (succ i) model)+ Nothing -> error "transition: increment"+ _ -> error "transition: impossible."++update :: Eq a => a -> b -> [(a, b)] -> [(a, b)]+update ref i m = (ref, i) : filter ((/= ref) . fst) m++precondition :: Model Symbolic -> Command Symbolic -> Logic+precondition (Model m) cmd = case cmd of+ Create -> Top+ Read ref -> ref `elem` domain m+ Write ref _ -> ref `elem` domain m+ Increment ref -> ref `elem` domain m++postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic+postcondition (Model m) cmd resp = case (cmd, resp) of+ (Create, Created ref) -> m' ! ref .== 0 .// "Create"+ where+ Model m' = transition (Model m) cmd resp+ (Read ref, ReadValue v) -> v .== m ! ref .// "Read"+ (Write _ref _x, Written) -> Top+ (Increment _ref, Incremented) -> Top+ _ -> Bot++data Bug+ = None+ | Logic+ | Race+ deriving Eq++semantics :: Bug -> Command Concrete -> IO (Response Concrete)+semantics bug cmd = case cmd of+ Create -> Created <$> (reference . Opaque <$> newIORef 0)+ Read ref -> ReadValue <$> readIORef (opaque ref)+ Write ref i -> Written <$ writeIORef (opaque ref) i'+ where+ -- One of the problems is a bug that writes a wrong value to the+ -- reference.+ i' | i `Prelude.elem` [5..10] = if bug == Logic then i + 1 else i+ | otherwise = i+ Increment ref -> do+ -- The other problem is that we introduce a possible race condition+ -- when incrementing.+ if bug == Race+ then do+ i <- readIORef (opaque ref)+ threadDelay =<< randomRIO (0, 5000)+ writeIORef (opaque ref) (i + 1)+ else+ atomicModifyIORef' (opaque ref) (\i -> (i + 1, ()))+ return Incremented++mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)+mock (Model m) cmd = case cmd of+ Create -> Created <$> genSym+ Read ref -> ReadValue <$> pure (m ! ref)+ Write _ _ -> pure Written+ Increment _ -> pure Incremented++generator :: Model Symbolic -> Gen (Command Symbolic)+generator (Model model) = frequency+ [ (1, pure Create)+ , (4, Read <$> elements (domain model))+ , (4, Write <$> elements (domain model) <*> arbitrary)+ , (4, Increment <$> elements (domain model))+ ]++shrinker :: Command Symbolic -> [Command Symbolic]+shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]+shrinker _ = []++sm :: Bug -> StateMachine Model Command IO Response+sm bug = StateMachine initModel transition precondition postcondition+ Nothing Nothing generator Nothing shrinker (semantics bug) id mock++prop_sequential :: Bug -> Property+prop_sequential bug = forAllCommands sm' Nothing $ \cmds -> monadicIO $ do+ (hist, _model, res) <- runCommands sm' cmds+ prettyCommands sm' hist (checkCommandNames cmds (res === Ok))+ where+ sm' = sm bug++prop_parallel :: Bug -> Property+prop_parallel bug = forAllParallelCommands sm' $ \cmds -> monadicIO $ do+ prettyParallelCommands cmds =<< runParallelCommands sm' cmds+ where+ sm' = sm bug
test/Spec.hs view
@@ -1,4 +1,63 @@-module Main where+module Main (main) where +import Prelude+import Test.Tasty+import Test.Tasty.QuickCheck++import CircularBuffer+import qualified CrudWebserverDb as WS+import DieHard+import MemoryReference+import TicketDispenser++------------------------------------------------------------------------++tests :: TestTree+tests = testGroup "Tests"+ [ testProperty "Die Hard"+ (expectFailure (withMaxSuccess 1000 prop_dieHard))+ , testGroup "Memory reference"+ [ testProperty "No bug" (prop_sequential None)+ , testProperty "Logic bug" (expectFailure (prop_sequential Logic))+ , testProperty "Race bug sequential" (prop_sequential Race)+ , testProperty "Race bug parallel" (expectFailure (prop_parallel Race))+ ]+ , testGroup "Crud webserver"+ [ webServer WS.None 8800 "No bug" WS.prop_crudWebserverDb+ , webServer WS.Logic 8801 "Logic bug" (expectFailure . WS.prop_crudWebserverDb)+ , webServer WS.Race 8802 "No race bug" WS.prop_crudWebserverDb+ , webServer WS.Race 8803 "Race bug" (expectFailure . WS.prop_crudWebserverDbParallel)+ ]+ , testGroup "Ticket dispenser"+ [ ticketDispenser "sequential" prop_ticketDispenser+ , ticketDispenser "parallel with exclusive lock" (withMaxSuccess 30 .+ prop_ticketDispenserParallelOK)+ , ticketDispenser "parallel with shared lock" (expectFailure .+ prop_ticketDispenserParallelBad)+ ]+ , testGroup "Circular buffer"+ [ testProperty "`unpropNoSizeCheck`: the first bug is found"+ (expectFailure unpropNoSizeCheck)+ , testProperty "`unpropFullIsEmpty`: the second bug is found"+ (expectFailure unpropFullIsEmpty)+ , testProperty "`unpropBadRem`: the third bug is found"+ (expectFailure unpropBadRem)+ , testProperty "`unpropStillBadRem`: the fourth bug is found"+ (expectFailure unpropStillBadRem)+ , testProperty "`prop_circularBuffer`: the fixed version is correct"+ prop_circularBuffer+ ]+ ]+ where+ webServer bug port test prop =+ withResource (WS.setup bug WS.connectionString port) WS.cleanup+ (const (testProperty test (prop port)))++ ticketDispenser test prop =+ withResource setupLock cleanupLock+ (\ioLock -> testProperty test (ioProperty (prop <$> ioLock)))++------------------------------------------------------------------------+ main :: IO ()-main = return ()+main = defaultMain tests
+ test/TicketDispenser.hs view
@@ -0,0 +1,222 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}++-----------------------------------------------------------------------------+-- |+-- Module : TicketDispenser+-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module contains a specification of a simple ticket dispenser.+--+-----------------------------------------------------------------------------++module TicketDispenser+ ( prop_ticketDispenser+ , prop_ticketDispenserParallel+ , prop_ticketDispenserParallelOK+ , prop_ticketDispenserParallelBad+ , withDbLock+ , setupLock+ , cleanupLock+ )+ where++import Control.Exception+ (IOException, catch)+import Data.TreeDiff+ (ToExpr)+import GHC.Generics+ (Generic, Generic1)+import Prelude hiding+ (readFile)+import System.Directory+ (createDirectoryIfMissing, getTemporaryDirectory,+ removeFile)+import System.FileLock+ (SharedExclusive(..), lockFile, unlockFile)+import System.FilePath+ ((</>))+import System.IO+ (hClose, openTempFile)+import System.IO.Strict+ (readFile)+import Test.QuickCheck+ (Gen, Property, frequency, (===))+import Test.QuickCheck.Monadic+ (monadicIO)++import Test.StateMachine+import qualified Test.StateMachine.Types.Rank2 as Rank2++------------------------------------------------------------------------++-- The actions of the ticket dispenser are:++data Action (r :: * -> *)+ = TakeTicket+ | Reset+ deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)++data Response (r :: * -> *)+ = GotTicket Int+ | ResetOk+ deriving (Show, Generic1, Rank2.Foldable)++-- Which correspond to taking a ticket and getting the next number, and+-- resetting the number counter of the dispenser.++------------------------------------------------------------------------++-- The dispenser has to be reset before use, hence the maybe integer.++newtype Model (r :: * -> *) = Model (Maybe Int)+ deriving (Eq, Show, Generic)++deriving instance ToExpr (Model Concrete)++initModel :: Model r+initModel = Model Nothing++preconditions :: Model Symbolic -> Action Symbolic -> Logic+preconditions (Model Nothing) TakeTicket = Bot+preconditions (Model (Just _)) TakeTicket = Top+preconditions _ Reset = Top++transitions :: Model r -> Action r -> Response r -> Model r+transitions (Model m) cmd _ = case cmd of+ TakeTicket -> Model (succ <$> m)+ Reset -> Model (Just 0)++postconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic+postconditions (Model m) TakeTicket (GotTicket n) = Just n .== (succ <$> m)+postconditions _ Reset ResetOk = Top+postconditions _ _ _ = error "postconditions"++------------------------------------------------------------------------++-- With stateful generation we ensure that the dispenser is reset before+-- use.++generator :: Model Symbolic -> Gen (Action Symbolic)+generator _ = frequency+ [ (1, pure Reset)+ , (4, pure TakeTicket)+ ]++shrinker :: Action Symbolic -> [Action Symbolic]+shrinker _ = []++------------------------------------------------------------------------++-- We will implement the dispenser using a simple database file which+-- stores the next number. A file lock is used to allow concurrent use.++semantics+ :: SharedExclusive -- ^ Indicates if the file+ -- lock should be shared+ -- between threads or if it+ -- should be exclusive.+ -- Sharing it could cause+ -- race conditions.++ -> (FilePath, FilePath) -- ^ File paths to the+ -- database storing the+ -- ticket counter and the+ -- file lock used for+ -- synchronisation.++ -> Action Concrete++ -> IO (Response Concrete)++semantics se (tdb, tlock) cmd = case cmd of+ TakeTicket -> do+ lock <- lockFile tlock se+ i <- read <$> readFile tdb+ `catch` (\(_ :: IOException) -> return "-1")+ writeFile tdb (show (i + 1))+ `catch` (\(_ :: IOException) -> return ())+ unlockFile lock+ return (GotTicket (i + 1))+ Reset -> do+ lock <- lockFile tlock se+ writeFile tdb (show (0 :: Integer))+ `catch` (\(_ :: IOException) -> return ())+ unlockFile lock+ return ResetOk++mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)+mock (Model Nothing) TakeTicket = error "mock: TakeTicket"+mock (Model (Just n)) TakeTicket = GotTicket <$> pure n+mock _ Reset = pure ResetOk++------------------------------------------------------------------------++type DbLock = (FilePath, FilePath)++setupLock :: IO DbLock+setupLock = do+ tmp <- getTemporaryDirectory+ let tmpTD = tmp </> "ticket-dispenser"+ createDirectoryIfMissing True tmpTD+ (tdb, dbh) <- openTempFile tmpTD "ticket-dispenser.db"+ hClose dbh+ (tlock, lockh) <- openTempFile tmpTD "ticket-dispenser.lock"+ hClose lockh+ return (tdb, tlock)++cleanupLock :: DbLock -> IO ()+cleanupLock (tdb, tlock) = do+ removeFile tdb+ removeFile tlock++withDbLock :: (DbLock -> IO ()) -> IO ()+withDbLock run = do+ lock <- setupLock+ run lock+ cleanupLock lock++sm :: SharedExclusive -> DbLock -> StateMachine Model Action IO Response+sm se files = StateMachine+ initModel transitions preconditions postconditions+ Nothing Nothing generator Nothing+ shrinker (semantics se files) id mock++-- Sequentially the model is consistent (even though the lock is+-- shared).++prop_ticketDispenser :: DbLock -> Property+prop_ticketDispenser files = forAllCommands sm' Nothing $ \cmds -> monadicIO $ do+ (hist, _, res) <- runCommands sm' cmds+ prettyCommands sm' hist $+ checkCommandNames cmds (res === Ok)+ where+ sm' = sm Shared files++prop_ticketDispenserParallel :: SharedExclusive -> DbLock -> Property+prop_ticketDispenserParallel se files =+ forAllParallelCommands sm' $ \cmds -> monadicIO $+ prettyParallelCommands cmds =<< runParallelCommandsNTimes 100 sm' cmds+ where+ sm' = sm se files++-- So long as the file locks are exclusive, i.e. not shared, the+-- parallel property passes.+prop_ticketDispenserParallelOK :: DbLock -> Property+prop_ticketDispenserParallelOK = prop_ticketDispenserParallel Exclusive++prop_ticketDispenserParallelBad :: DbLock -> Property+prop_ticketDispenserParallelBad = prop_ticketDispenserParallel Shared