quickcheck-state-machine 0.1.0 → 0.2.0
raw patch · 19 files changed
+1516/−369 lines, 19 filesdep +asyncdep +lifted-asyncdep +lifted-basedep −parallel-io
Dependencies added: async, lifted-async, lifted-base, monad-control, quickcheck-with-counterexamples, template-haskell, th-abstraction
Dependencies removed: parallel-io
Files
- CHANGELOG.md +16/−2
- LICENSE +2/−1
- README.md +97/−51
- quickcheck-state-machine.cabal +17/−3
- src/Test/StateMachine.hs +199/−65
- src/Test/StateMachine/Internal/Parallel.hs +90/−139
- src/Test/StateMachine/Internal/Sequential.hs +73/−40
- src/Test/StateMachine/Internal/Types.hs +32/−17
- src/Test/StateMachine/Internal/Utils.hs +43/−22
- src/Test/StateMachine/Internal/Utils/BoxDrawer.hs +1/−1
- src/Test/StateMachine/TH.hs +51/−0
- src/Test/StateMachine/Types.hs +55/−5
- src/Test/StateMachine/Types/Generics.hs +33/−0
- src/Test/StateMachine/Types/Generics/TH.hs +233/−0
- src/Test/StateMachine/Types/HFunctor/TH.hs +209/−0
- src/Test/StateMachine/Types/History.hs +115/−0
- src/Test/StateMachine/Types/References.hs +29/−23
- src/Test/StateMachine/Utils.hs +27/−0
- src/Test/StateMachine/Z.hs +194/−0
CHANGELOG.md view
@@ -1,7 +1,21 @@+#### 0.2.0++ * Z-inspired definition of relations and associated operations were+ added to help defining concise and showable models;++ * Template Haskell derivation of `shrink` and type classes: `Show`,+ `Constructors`, `HFunctor`, `HFoldable`, `HTraversable`;++ * New and more flexible combinators for building sequential and+ parallel properties replaced the old clunky ones;++ * Circular buffer example was added;++ * Two examples of how to test CRUD web applications were added.+ #### 0.1.0 - * The API has been simplified, thanks to ideas stolen- from+ * The API was simplified, thanks to ideas stolen from [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog/commit/385c92f9dd0aa7e748fc677b2eeead5e3572685f). #### 0.0.0
LICENSE view
@@ -1,4 +1,5 @@-Copyright (c) 2017 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley+Copyright (c) 2017 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley,+ Xia Li-yao All rights reserved.
README.md view
@@ -22,7 +22,7 @@ As a first example, let's implement and test programs using mutable references. Our implementation will be using `IORef`s, but let's start with a-representation of what actions are possible with program using mutable+representation of what actions are possible with programs using mutable references. Our mutable references can be created, read from, written to and incremented: @@ -71,7 +71,7 @@ atomicModifyIORef' (opaque ref) (\i -> (i + 1, ())) ``` -Note that above `v` is instatiated to `Concrete`, which is essentially the+Note that above `v` 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@@ -86,7 +86,7 @@ ``` The pre-condition of an action specifies in what context the action is-well-defined. For example, we can always create a new mutuable reference, but+well-defined. For example, we can always create a new mutable reference, but we can only read from references that already have been created. The pre-conditions are used while generating programs (lists of actions). @@ -144,24 +144,26 @@ shrinker _ = [] ``` +To be able to fit the code on a line we pack up all of them above into a+record.++```haskell+sm :: Problem -> StateMachine Model Action IO+sm prb = StateMachine+ generator shrinker precondition transition+ postcondition initModel (semantics prb) id+```+ We can now define a sequential property as follows. ```haskell prop_references :: Problem -> Property-prop_references prb = forAllProgram- generator- shrinker- precondition- transition- initModel $ \prog ->- runAndCheckProgram- precondition- transition- postcondition- initModel- (semantics prb)- ioProperty- prog+prop_references prb = monadicSequential (sm prb) $ \prog -> do+ (hist, model, prop) <- runProgram (sm prb) prog+ prettyProgram prog hist model $+ checkActionNames prog numberOfConstructors prop+ where+ numberOfConstructors = 4 ``` If we run the sequential property without introducing any problems to the@@ -186,19 +188,8 @@ ```haskell prop_referencesParallel :: Problem -> Property-prop_referencesParallel prb = forAllParallelProgram- generator- shrinker- precondition- transition- initModel $ \parallel ->- runParallelProgram (semantics prb) parallel $ \hist ->- checkParallelProgram- transition- postcondition- initModel- parallel- hist+prop_referencesParallel prb = monadicParallel (sm prb) $ \prog ->+ prettyParallelProgram prog =<< runParallelProgram (sm prb) prog ``` And run it using the race condition problem, then we'll find the race@@ -212,19 +203,19 @@ ┌────────────────────────────────┐ │ Var 0 ← New │-│ ⟶ Opaque │+│ → Opaque │ └────────────────────────────────┘ ┌─────────────┐ │ │ Inc (Var 0) │ │ │ │ │ ┌──────────────┐ │ │ │ │ Inc (Var 0) │-│ ⟶ () │ │ │ │+│ → () │ │ │ │ └─────────────┘ │ │ │- │ │ ⟶ () │+ │ │ → () │ │ └──────────────┘ │ ┌──────────────┐ │ │ Read (Var 0) │- │ │ ⟶ 1 │+ │ │ → 1 │ │ └──────────────┘ Just 2 /= Just 1 ```@@ -235,7 +226,7 @@ Recall that incrementing is implemented by first reading the reference and then writing it, if two such actions are interleaved then one of the writes-might end up overwriting the other ones -- creating the race condition.+might end up overwriting the other one -- creating the race condition. We shall come back to this example below, but if your are impatient you can find the full source@@ -244,12 +235,12 @@ ### How it works -The rought idea is that the user of the library is asked to provide:+The rough idea is that the user of the library is asked to provide: * a datatype of actions; * a datatype model; * pre- and post-conditions of the actions on the model;- * a state transition function that given a model and a action advances the+ * a state transition function that given a model and an action advances the model to its next state; * a way to generate and shrink actions; * semantics for executing the actions.@@ -272,7 +263,7 @@ 4. advance the model using the transition function. 3. If something goes wrong, shrink the initial list of actions and present a- minimal counter example.+ minimal counterexample. #### Parallel property @@ -307,7 +298,7 @@ simple [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/DieHard.hs) of a specification where we use the sequential property to find a solution- (counter example) to a puzzle from an action movie. Note that this example+ (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 compare the solution to the Hedgehog@@ -324,34 +315,59 @@ 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 is- the+ 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) -- 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 counter examples are+ 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); + * Circular buffer+ [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/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*+ [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),+ [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)];+ * Ticket dispenser [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/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 teared down. This example also appears in the+ that needs to be setup and cleaned up. This example also appears in the *Testing a Database for Race Conditions with QuickCheck* and *Testing the Hard Stuff and Staying Sane* [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),- [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)] papers.+ [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)] papers; + * CRUD+ webserver+ [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/CrudWebserverFile.hs) --+ create, read, update and delete files on a webserver using an API written+ using [Servant](https://github.com/haskell-servant/servant). The+ specification uses two fixed file names for the tests, and the webserver is+ setup and torn down for every generated program;++ * 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+ 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.@@ -400,10 +416,41 @@ * The use of state machines to model and verify properties about programs is quite well-established, as witnessed by several books on the subject: - - [Specifying Systems](https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/):- The TLA+ Language and Tools for Hardware and Software Engineers;- - [Modeling in Event-B](http://www.event-b.org/abook.html): System and- Software Engineering;+ - [Specifying+ Systems](https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/):+ The TLA+ Language and Tools for Hardware and Software Engineers.+ Parts of this book are also presented by the author, Leslie+ Lamport, in the following video+ [course](https://lamport.azurewebsites.net/video/videos.html);++ - [Modeling in Event-B](http://www.event-b.org/abook.html): System+ and Software Engineering. Parts of this book are covered in the+ following (video) course given at Microsoft Research by the+ author, Jean-Raymond Abrial, himself:++ + [Lecture 1](https://www.youtube.com/watch?v=2GP1pJINVT4):+ introduction to modeling and Event-B (chapter 1 of the+ book) and start of "controlling cars on bridge" example+ (chapter 2);++ + [Lecture 2](https://www.youtube.com/watch?v=M8nvVaZ74wA):+ refining the "controlling cars on a bridge" example+ (sections 2.6 and 2.7);++ + [Lecture 3](https://www.youtube.com/watch?v=Y5OUtq8cdV8):+ design patterns and the "mechanical press controller"+ example (chapter 3);++ + [Lecture 4](https://www.youtube.com/watch?v=ku-lfjxM4WI):+ sorting algorithm example (chapter 15);++ + [Lecture 5](https://www.youtube.com/watch?v=C0tpgPOKAyg):+ designing sequential programs (chapter 15);++ + [Lecture 6](https://www.youtube.com/watch?v=i-GKHZAWWjU):+ status report of the hypervisor that Microsoft Research are+ developing using Event-B.+ - [Abstract State Machines](http://www.di.unipi.it/~boerger/AsmBook/): A Method for High-Level System Design and Analysis. @@ -432,8 +479,7 @@ - The Haskell library [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog), also- has support for state machine based testing (no parallel property yet- though);+ has support for state machine based testing; - [ScalaCheck](http://www.scalacheck.org/), likewise has support for state machine
quickcheck-state-machine.cabal view
@@ -1,5 +1,5 @@ name: quickcheck-state-machine-version: 0.1.0+version: 0.2.0 cabal-version: >=1.10 build-type: Simple license: BSD3@@ -32,20 +32,34 @@ Test.StateMachine.Internal.Types.Environment Test.StateMachine.Internal.Utils Test.StateMachine.Internal.Utils.BoxDrawer+ 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 build-depends: ansi-wl-pprint >=0.6.7.3 && <0.7,+ async >=2.1.1.1 && <2.2, base >=4.7 && <5, containers >=0.5.7.1 && <0.6,+ lifted-async >=0.9.3 && <0.10,+ lifted-base >=0.2.3.11 && <0.3,+ monad-control >=1.0.2.2 && <1.1, mtl >=2.2.1 && <2.3,- parallel-io >=0.3.3 && <0.4, QuickCheck >=2.9.2 && <2.10,+ quickcheck-with-counterexamples >=1.0 && <2.0, random ==1.1.*,- stm >=2.4.4.1 && <2.5+ stm >=2.4.4.1 && <2.5,+ template-haskell >=2.11.1.0 && <2.12,+ th-abstraction >=0.2.6.0 && <0.3 default-language: Haskell2010 hs-source-dirs: src+ other-modules:+ Test.StateMachine.Utils test-suite quickcheck-state-machine-test type: exitcode-stdio-1.0
src/Test/StateMachine.hs view
@@ -1,5 +1,9 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-} ----------------------------------------------------------------------------- -- |@@ -20,36 +24,61 @@ ( -- * Sequential property combinators Program+ , programLength , forAllProgram- , runAndCheckProgram- , runAndCheckProgram'+ , monadicSequential+ , runProgram+ , prettyProgram+ , actionNames+ , checkActionNames -- * Parallel property combinators , ParallelProgram , forAllParallelProgram , History+ , monadicParallel , runParallelProgram , runParallelProgram'- , checkParallelProgram+ , prettyParallelProgram + -- * With counterexamples+ , forAllProgramC+ , monadicSequentialC+ , forAllParallelProgramC+ , monadicParallelC+ -- * Types , module Test.StateMachine.Types++ -- * Reexport+ , Test.QuickCheck.quickCheck ) where +import Control.Monad.IO.Class+ (MonadIO) import Control.Monad.State- (evalStateT, replicateM_)+ (evalStateT, replicateM)+import Control.Monad.Trans.Control+ (MonadBaseControl)+import Data.Map+ (Map)+import qualified Data.Map as M+import Test.QuickCheck+ (Property, collect, cover, ioProperty, property)+import qualified Test.QuickCheck+import Test.QuickCheck.Counterexamples+ ((:&:)(..), PropertyOf, forAllShrink)+import qualified Test.QuickCheck.Counterexamples as CE import Test.QuickCheck.Monadic- (monadic, monadicIO, run)-import Test.QuickCheck.Property- (Property, forAllShrink, ioProperty)+ (PropertyM, monadic, run) import Test.StateMachine.Internal.Parallel import Test.StateMachine.Internal.Sequential import Test.StateMachine.Internal.Types-import Test.StateMachine.Internal.Types.Environment import Test.StateMachine.Internal.Utils- (liftProperty)+ (whenFailM) import Test.StateMachine.Types+import Test.StateMachine.Types.History ------------------------------------------------------------------------ @@ -66,52 +95,97 @@ -- 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+ :: Show (Untyped act)+ => HFoldable act+ => Generator model act+ -> Shrinker act+ -> Precondition model act+ -> Transition model act+ -> InitialModel model+ -> (Program act -> PropertyOf a) -- ^ Predicate that should hold for all+ -- programs.+ -> PropertyOf (Program act :&: a)+forAllProgramC generator shrinker precondition transition model = forAllShrink (evalStateT (generateProgram generator precondition transition 0) model) (shrinkProgram shrinker precondition transition model) --- | Run a sequential program and check if your model agrees with your--- semantics.-runAndCheckProgram+-- | Wrapper around 'forAllProgram' using the 'StateMachine' specification+-- to generate and shrink sequential programs.+monadicSequential :: Monad m- => HFunctor act- => Precondition model act- -> Transition model act- -> Postcondition model act- -> InitialModel model- -> Semantics act m- -> (m Property -> Property) -- ^ Runner- -> Program act+ => Show (Untyped act)+ => HFoldable act+ => StateMachine' model act err m+ -> (Program act -> PropertyM m a)+ -- ^ Predicate that should hold for all programs. -> Property-runAndCheckProgram precond trans postcond m sem runner =- runAndCheckProgram' precond trans postcond m sem (return ()) (const runner) (const (return ()))+monadicSequential sm = property . monadicSequentialC sm --- | Same as above, except with the possibility to setup some resource--- for the runner to use. The resource could be a database connection--- for example.-runAndCheckProgram'+-- | Variant of 'monadicSequential' with counterexamples.+monadicSequentialC :: Monad m- => HFunctor act- => Precondition model act- -> Transition model act- -> Postcondition model act- -> InitialModel model- -> Semantics act m- -> IO setup -- ^ Setup a resource.- -> (setup -> m Property -> Property)- -> (setup -> IO ()) -- ^ Tear down the resource.+ => Show (Untyped act)+ => HFoldable act+ => StateMachine' model act err m+ -> (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++-- | Testable property of sequential programs derived from a+-- 'StateMachine' specification.+runProgram+ :: forall m act err model+ . Monad m+ => Show (Untyped act)+ => HTraversable act+ => StateMachine' model act err m+ -- ^ -> Program act+ -> PropertyM m (History act err, model Concrete, Property)+runProgram sm = run . executeProgram sm++-- | Takes the output of running a program and pretty prints a+-- counterexample if the run failed.+prettyProgram+ :: MonadIO m+ => Program act+ -> History act err+ -> model Concrete -> Property-runAndCheckProgram' precond trans postcond m sem setup runner cleanup acts =- monadic (ioProperty . runnerWithSetup)- (checkProgram precond trans postcond m m sem acts)+ -> PropertyM m ()+prettyProgram _ hist _ prop = putStrLn (ppHistory 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- runnerWithSetup mp = do- s <- setup- let prop = runner s (evalStateT mp emptyEnvironment)- cleanup s- return prop+ 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.@@ -127,34 +201,94 @@ -- for all parallel programs. -> Property forAllParallelProgram generator shrinker precondition transition model =+ property+ . forAllParallelProgramC generator shrinker precondition transition model+ . \prop p -> CE.property (prop p)++-- | Variant of 'forAllParallelProgram' which returns the generated and shrunk+-- program if the property fails.+forAllParallelProgramC+ :: Show (Untyped act)+ => HFoldable act+ => Generator model act+ -> Shrinker act+ -> Precondition model act+ -> Transition model act+ -> InitialModel model+ -> (ParallelProgram act -> PropertyOf a) -- ^ Predicate that should hold+ -- for all parallel programs.+ -> PropertyOf (ParallelProgram act :&: a)+forAllParallelProgramC generator shrinker precondition transition model = forAllShrink (generateParallelProgram generator precondition transition model) (shrinkParallelProgram shrinker precondition transition model) --- | Run a parallel program and collect the history of the execution.+-- | Wrapper around 'forAllParallelProgram' using the 'StateMachine'+-- specification to generate and shrink parallel programs.+monadicParallel+ :: MonadBaseControl IO m+ => Show (Untyped act)+ => HFoldable act+ => StateMachine' model act err m+ -> (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+ => Show (Untyped act)+ => HFoldable act+ => StateMachine' model act err m+ -> (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- :: Show (Untyped act)+ :: MonadBaseControl IO m+ => Show (Untyped act) => HTraversable act- => Semantics act IO+ => StateMachine' model act err m+ -- ^ -> ParallelProgram act- -> (History act -> Property) -- ^ Predicate that should hold for the- -- execution history.- -> Property-runParallelProgram sem = runParallelProgram' (return ()) (const sem) (const (return ()))+ -> PropertyM m [(History act err, Property)]+runParallelProgram = runParallelProgram' 10 --- | Same as above, but with the possibility of setting up some resource.+-- | Same as above, but with the ability to choose how many times each+-- parallel program is executed. It can be important to tune this+-- value in order to reveal race conditions. The more runs, the more+-- likely we will find a bug, but it also takes longer. runParallelProgram'- :: Show (Untyped act)+ :: MonadBaseControl IO m+ => Show (Untyped act) => HTraversable act- => IO setup -- ^ Setup a resource.- -> (setup -> Semantics act IO)- -> (setup -> IO ()) -- ^ Tear down the resource.+ => Int -- ^ How many times to execute the parallel program.+ -> StateMachine' model act err m+ -- ^ -> ParallelProgram act- -> (History act -> Property)- -> Property-runParallelProgram' setup sem clean fork checkhistory = monadicIO $ do- res <- run setup- replicateM_ 10 $ do- hist <- run (executeParallelProgram (sem res) fork)- run (clean res)- liftProperty (checkhistory hist)+ -> 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+ => 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/Internal/Parallel.hs view
@@ -1,9 +1,8 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- |@@ -24,14 +23,14 @@ ( generateParallelProgram , shrinkParallelProgram , executeParallelProgram- , checkParallelProgram- , History(..)+ , linearise+ , toBoxDrawings ) where -import Control.Concurrent+import Control.Concurrent.Async.Lifted+ (concurrently)+import Control.Concurrent.Lifted (threadDelay)-import Control.Concurrent.ParallelIO.Local- (parallel_, withPool) import Control.Concurrent.STM (STM, atomically) import Control.Concurrent.STM.TChan@@ -39,10 +38,12 @@ import Control.Monad (foldM) import Control.Monad.State- (StateT, runStateT, evalState, evalStateT, execStateT, get,- lift, modify, runState)+ (StateT, evalState, evalStateT, execStateT, get,+ lift, modify, runState, runStateT)+import Control.Monad.Trans.Control+ (MonadBaseControl, liftBaseWith) import Data.Dynamic- (Dynamic, toDyn)+ (toDyn) import Data.List (partition) import Data.Set@@ -50,13 +51,8 @@ import qualified Data.Set as S import Data.Tree (Tree(Node))-import Data.Typeable- (Typeable)-import System.Random- (randomRIO) import Test.QuickCheck- (Gen, Property, counterexample, property,- shrinkList, (.&&.))+ (Gen, Property, property, shrinkList, (.&&.)) import Text.PrettyPrint.ANSI.Leijen (Doc) @@ -65,7 +61,9 @@ import Test.StateMachine.Internal.Types.Environment import Test.StateMachine.Internal.Utils import Test.StateMachine.Internal.Utils.BoxDrawer-import Test.StateMachine.Types+import Test.StateMachine.Types hiding+ (StateMachine'(..))+import Test.StateMachine.Types.History ------------------------------------------------------------------------ @@ -122,27 +120,27 @@ -- and then the suffixes in parallel, and return the history (or -- trace) of the execution. executeParallelProgram- :: forall act. HTraversable act+ :: forall m act err+ . MonadBaseControl IO m+ => HTraversable act => Show (Untyped act)- => Semantics act IO+ => Semantics act err m -> ParallelProgram act- -> IO (History act)+ -> m (History act err) executeParallelProgram semantics = liftSemFork . unParallelProgram where liftSemFork :: HTraversable act => Show (Untyped act) => Fork (Program act)- -> IO (History act)+ -> m (History act err) liftSemFork (Fork left prefix right) = do- hchan <- newTChanIO+ hchan <- liftBaseWith (const newTChanIO) env <- execStateT (runMany hchan (Pid 0) (unProgram prefix)) emptyEnvironment- withPool 2 $ \pool ->- parallel_ pool- [ evalStateT (runMany hchan (Pid 1) (unProgram left)) env- , evalStateT (runMany hchan (Pid 2) (unProgram right)) env- ]- History <$> getChanContents hchan+ _ <- concurrently+ (evalStateT (runMany hchan (Pid 1) (unProgram left)) env)+ (evalStateT (runMany hchan (Pid 2) (unProgram right)) env)+ History <$> liftBaseWith (const (getChanContents hchan)) where getChanContents :: forall a. TChan a -> IO [a] getChanContents chan = reverse <$> atomically (go [])@@ -157,134 +155,87 @@ runMany :: HTraversable act => Show (Untyped act)- => TChan (HistoryEvent (UntypedConcrete act))+ => TChan (HistoryEvent (UntypedConcrete act) err) -> Pid -> [Internal act]- -> StateT Environment IO ()+ -> StateT Environment m () runMany hchan pid = flip foldM () $ \_ (Internal act sym@(Symbolic var)) -> do env <- get- let cact = either (error . show) id (reify env act)- lift $ atomically $ writeTChan hchan $- InvocationEvent (UntypedConcrete cact) (show (Untyped act)) var pid- resp <- lift (semantics cact)- modify (insertConcrete sym (Concrete resp))- lift $ do- threadDelay =<< randomRIO (0, 20)- atomically $ writeTChan hchan $ ResponseEvent (toDyn resp) (show resp) pid---- | Check if a history from a parallel execution can be linearised.-checkParallelProgram- :: HFoldable act- => Transition model act- -> Postcondition model act- -> InitialModel model- -> ParallelProgram act- -> History act -- ^ History to be checked.- -> Property-checkParallelProgram transition postcondition model prog history- = counterexample ("Couldn't linearise:\n\n" ++ show (toBoxDrawings allVars history))- $ linearise transition postcondition model history- where- vars xs = [ getUsedVars x | Internal x _ <- xs]- Fork l p r = fmap (S.unions . vars . unProgram) $ unParallelProgram prog- allVars = S.unions [l, p, r]+ 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) (show (Untyped act)) var pid+ mresp <- lift (semantics cact)+ threadDelay 10+ case mresp of+ Fail err ->+ liftBaseWith $ const $+ atomically $ writeTChan hchan $ ResponseEvent (Fail err) "<fail>" pid+ Ok resp -> do+ modify (insertConcrete sym (Concrete resp))+ liftBaseWith $ const $+ atomically $ writeTChan hchan $ ResponseEvent (Ok (toDyn resp)) (show resp) pid ------------------------------------------------------------------------ --- The code below is used by checkParallelProgram.---- | A history is a trace of invocations and responses from running a--- parallel program.-newtype History act = History- { unHistory :: History' act }--type History' act = [HistoryEvent (UntypedConcrete act)]--data UntypedConcrete (act :: (* -> *) -> * -> *) where- UntypedConcrete :: (Show resp, Typeable resp) =>- act Concrete resp -> UntypedConcrete act--data HistoryEvent act- = InvocationEvent act String Var Pid- | ResponseEvent Dynamic String Pid--getProcessIdEvent :: HistoryEvent act -> Pid-getProcessIdEvent (InvocationEvent _ _ _ pid) = pid-getProcessIdEvent (ResponseEvent _ _ pid) = pid--data Operation act = forall resp. Typeable resp =>- Operation (act Concrete resp) String (Concrete resp) Pid--takeInvocations :: [HistoryEvent a] -> [HistoryEvent a]-takeInvocations = takeWhile $ \h -> case h of- InvocationEvent {} -> True- _ -> False--findCorrespondingResp :: Pid -> History' act -> [(Dynamic, History' act)]-findCorrespondingResp _ [] = []-findCorrespondingResp pid (ResponseEvent resp _ pid' : es) | pid == pid' = [(resp, es)]-findCorrespondingResp pid (e : es) =- [ (resp, e : es') | (resp, es') <- findCorrespondingResp pid es ]--linearTree :: History' act -> [Tree (Operation act)]-linearTree [] = []-linearTree es =- [ Node (Operation act str (dynResp resp) pid) (linearTree es')- | InvocationEvent (UntypedConcrete act) str _ pid <- takeInvocations es- , (resp, es') <- findCorrespondingResp pid $ filter1 (not . matchInv pid) es- ]- where- dynResp resp = either (error . show) id (reifyDynamic resp)-- filter1 :: (a -> Bool) -> [a] -> [a]- filter1 _ [] = []- filter1 p (x : xs) | p x = x : filter1 p xs- | otherwise = xs-- -- Hmm, is this enough?- matchInv pid (InvocationEvent _ _ _ pid') = pid == pid'- matchInv _ _ = False-+-- | 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+ :: forall model act err . Transition model act -> Postcondition model act -> InitialModel model- -> History act+ -> History act err -> Property linearise transition postcondition model0 = go . unHistory where- go :: History' act -> Property+ go :: History' act err -> Property go [] = property True go es = anyP (step model0) (linearTree es) - step :: model Concrete -> Tree (Operation act) -> Property- step model (Node (Operation act _ resp@(Concrete resp') _) roses) =+ step :: model Concrete -> Tree (Operation act err) -> Property+ step model (Node (Operation _ _ (Fail _) _) roses) =+ anyP' (step model) roses+ step model (Node (Operation act _ (Ok (resp@(Concrete resp'))) _) roses) = postcondition model act resp' .&&. anyP' (step (transition model act resp)) roses- where- anyP' :: (a -> Property) -> [a] -> Property- anyP' _ [] = property True- anyP' p xs = anyP p xs -toBoxDrawings :: Set Var -> History act -> Doc-toBoxDrawings knownVars (History h) = exec evT (fmap out <$> Fork l p r)+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 prog = toBoxDrawings' allVars where- (p, h') = partition (\e -> getProcessIdEvent e == Pid 0) h- (l, r) = partition (\e -> getProcessIdEvent e == Pid 1) h'+ allVars = S.unions [l0, p0, r0]+ Fork l0 p0 r0 = fmap (S.unions . vars . unProgram) (unParallelProgram prog)+ vars xs = [ getUsedVars x | Internal x _ <- xs] - out :: HistoryEvent act -> String- out (InvocationEvent _ str var _)- | var `S.member` knownVars = show var ++ " ← " ++ str- | otherwise = str- out (ResponseEvent _ str _) = str+ 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' - toEventType :: [HistoryEvent act] -> [(EventType, Pid)]- toEventType = map go- where- go e = case e of- InvocationEvent _ _ _ pid -> (Open, pid)- ResponseEvent _ _ pid -> (Close, pid)+ out :: HistoryEvent act err -> String+ out (InvocationEvent _ str var _)+ | var `S.member` knownVars = show var ++ " ← " ++ str+ | otherwise = str+ out (ResponseEvent _ str _) = str - evT :: [(EventType, Pid)]- evT = toEventType (filter (\e -> getProcessIdEvent e `elem` map Pid [1,2]) h)+ 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)
src/Test/StateMachine/Internal/Sequential.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} -----------------------------------------------------------------------------@@ -23,26 +24,29 @@ , getUsedVars , liftShrinkInternal , shrinkProgram- , checkProgram+ , executeProgram ) where import Control.Monad- (filterM, foldM_)+ (filterM, foldM, when) import Control.Monad.State- (State, StateT, get, lift, modify, put, evalState)+ (State, StateT, evalState, get, lift, put)+import Data.Dynamic+ (toDyn)+import Data.Monoid+ ((<>)) import Data.Set (Set) import qualified Data.Set as S import Test.QuickCheck- (Gen, shrinkList, sized, choose, suchThat)-import Test.QuickCheck.Monadic- (PropertyM, pre, run)+ (Gen, Property, choose, counterexample, property,+ shrinkList, sized, suchThat, (.&&.)) import Test.StateMachine.Internal.Types import Test.StateMachine.Internal.Types.Environment-import Test.StateMachine.Internal.Utils import Test.StateMachine.Types+import Test.StateMachine.Types.History ------------------------------------------------------------------------ @@ -86,8 +90,9 @@ where go (Internal act sym@(Symbolic var)) = do (model, scope) <- get- put (transition model act sym, S.insert var scope)- return (precondition model act && getUsedVars act `S.isSubsetOf` scope)+ let valid = precondition model act && getUsedVars act `S.isSubsetOf` scope+ when valid (put (transition model act sym, S.insert var scope))+ return valid -- | Returns the set of references an action uses. getUsedVars :: HFoldable act => act Symbolic a -> Set Var@@ -116,36 +121,64 @@ . shrinkList (liftShrinkInternal shrinker) . unProgram --- | For each action in a program, check that if the pre-condition holds--- for the action, then so does the post-condition.-checkProgram- :: Monad m- => HFunctor act- => Precondition model act- -> Transition model act- -> Postcondition model act- -> model Symbolic -- ^ The model with symbolic references is used to- -- check pre-conditions against.- -> model Concrete -- ^ While the one with concrete referenes is used- -- for checking post-conditions.- -> Semantics act m- -> Program act- -> PropertyM (StateT Environment m) ()-checkProgram precondition transition postcondition smodel0 cmodel0 semantics- = foldM_ go (smodel0, cmodel0)+-- | Execute a program and return a history, the final model and a property+-- which contains the information of whether the execution respects the state+-- machine model or not.+executeProgram+ :: forall m act err model+ . Monad m+ => Show (Untyped act)+ => HTraversable act+ => StateMachine' model act err m+ -> Program act+ -> m (History act err, model Concrete, Property)+executeProgram StateMachine {..}+ = fmap (\(hist, _, cmodel, _, prop) -> (hist, cmodel, prop))+ . foldM go (mempty, model', model', emptyEnvironment, property True) . unProgram where- go (smodel, cmodel) (Internal act sym) = do- pre (precondition smodel act)- env <- run get- let cact = hfmap (fromSymbolic env) act- resp <- run (lift (semantics cact))- liftProperty (postcondition cmodel cact resp)- let cresp = Concrete resp- run (modify (insertConcrete sym cresp))- return (transition smodel act sym, transition cmodel cact cresp)- where- fromSymbolic :: Environment -> Symbolic v -> Concrete v- fromSymbolic env sym' = case reifyEnvironment env sym' of- Left err -> error (show err)- Right con -> con+ go :: (History act err, model Symbolic, model Concrete, Environment, Property)+ -> Internal act+ -> m (History act err, model Symbolic, model Concrete, Environment, Property)+ go (hist, smodel, cmodel, env, prop) (Internal act sym@(Symbolic var)) =+ if not (precondition' smodel act)+ then+ return ( hist+ , smodel+ , cmodel+ , env+ , counterexample ("precondition failed for: " ++ show (Untyped act)) prop+ )+ else+ case reify env act of++ -- This means that the reference that the action uses+ -- failed to be created, so we do nothing.+ Left _ -> return (hist, smodel, cmodel, env, prop)++ Right cact -> do+ mresp <- semantics' cact+ case mresp of+ Fail err -> do+ let hist' = History+ [ InvocationEvent (UntypedConcrete cact) (show (Untyped act)) var (Pid 0)+ , ResponseEvent (Fail err) "<fail>" (Pid 0)+ ]+ return ( hist <> hist'+ , smodel+ , cmodel+ , env+ , prop+ )+ Ok resp -> do+ let cresp = Concrete resp+ hist' = History+ [ InvocationEvent (UntypedConcrete cact) (show (Untyped act)) var (Pid 0)+ , ResponseEvent (Ok (toDyn cresp)) (show resp) (Pid 0)+ ]+ return ( hist <> hist'+ , transition' smodel act sym+ , transition' cmodel cact cresp+ , insertConcrete sym cresp env+ , prop .&&. postcondition' cmodel cact resp+ )
src/Test/StateMachine/Internal/Types.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} -----------------------------------------------------------------------------@@ -20,22 +21,20 @@ module Test.StateMachine.Internal.Types ( Program(..)+ , programLength , ParallelProgram(..) , Pid(..) , Fork(..) , Internal(..) ) where -import Data.List- (intercalate) import Data.Typeable (Typeable) import Text.Read- (readListPrec, readListPrecDefault, readPrec)+ (Lexeme(Ident), lexP, parens, prec, readPrec, step) import Test.StateMachine.Types (Untyped(Untyped))-import Test.StateMachine.Types.HFunctor import Test.StateMachine.Types.References ------------------------------------------------------------------------@@ -55,18 +54,12 @@ mempty = Program [] Program acts1 `mappend` Program acts2 = Program (acts1 ++ acts2) -instance (Show (Untyped act), HFoldable act) => Show (Program act) where- show (Program iacts) = bracket . intercalate "," . map go $ iacts- where-- go (Internal act (Symbolic var)) =- show (Untyped act) ++ " " ++ show var-- bracket s = "[" ++ s ++ "]"+deriving instance Show (Untyped act) => Show (Program act)+deriving instance Read (Untyped act) => Read (Program act) -instance Read (Internal act) => Read (Program act) where- readPrec = Program <$> readPrec- readListPrec = readListPrecDefault+-- | Returns the number of actions in a program.+programLength :: Program act -> Int+programLength = length . unProgram ------------------------------------------------------------------------ @@ -79,8 +72,8 @@ newtype ParallelProgram act = ParallelProgram { unParallelProgram :: Fork (Program act) } -instance (Show (Untyped act), HFoldable act) => Show (ParallelProgram act) where- show = show . unParallelProgram+deriving instance Show (Untyped act) => Show (ParallelProgram act)+deriving instance Read (Untyped act) => Read (ParallelProgram act) -- | Forks are used to represent parallel programs. data Fork a = Fork a a a@@ -93,6 +86,28 @@ 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 ------------------------------------------------------------------------
src/Test/StateMachine/Internal/Utils.hs view
@@ -8,23 +8,18 @@ -- Stability : provisional -- Portability : non-portable (GHC extensions) ----- This module exports some QuickCheck utility functions. Some of these should--- perhaps be upstreamed.--- ----------------------------------------------------------------------------- -module Test.StateMachine.Internal.Utils- ( anyP- , liftProperty- , shrinkPropertyHelper- , shrinkPropertyHelper'- , shrinkPair- , shrinkPair'- ) where+module Test.StateMachine.Internal.Utils where +import Data.List+ (group, sort) import Test.QuickCheck- (Property, Result(Failure), chatty, counterexample,- output, property, quickCheckWithResult, stdArgs)+ (Property, chatty, counterexample, property,+ stdArgs, whenFail)+import Test.QuickCheck.Counterexamples+ (PropertyOf)+import qualified Test.QuickCheck.Counterexamples as CE import Test.QuickCheck.Monadic (PropertyM(MkPropertyM), monadicIO, run) import Test.QuickCheck.Property@@ -40,19 +35,31 @@ 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+ -- | Write a metaproperty on the output of QuickChecking a property using a -- boolean predicate on the output.-shrinkPropertyHelper :: Property -> (String -> Bool) -> Property-shrinkPropertyHelper prop p = shrinkPropertyHelper' prop (property . p)+shrinkPropertyHelperC :: Show a => PropertyOf a -> (a -> Bool) -> Property+shrinkPropertyHelperC prop p = shrinkPropertyHelperC' prop (property . p) -- | Same as above, but using a property predicate.-shrinkPropertyHelper' :: Property -> (String -> Property) -> Property-shrinkPropertyHelper' prop p = monadicIO $ do- result <- run $ quickCheckWithResult (stdArgs {chatty = False}) prop- case result of- Failure { output = outputLines } -> liftProperty $- counterexample ("failed: " ++ outputLines) $ p outputLines- _ -> return ()+shrinkPropertyHelperC' :: Show a => PropertyOf a -> (a -> Property) -> Property+shrinkPropertyHelperC' prop p = monadicIO $ do+ ce_ <- run $ CE.quickCheckWith (stdArgs {chatty = False}) prop+ case ce_ of+ Nothing -> return ()+ Just ce -> liftProperty $+ counterexample ("failed: " ++ show ce) $ p ce -- | Given shrinkers for the components of a pair we can shrink the pair. shrinkPair' :: (a -> [a]) -> (b -> [b]) -> ((a, b) -> [(a, b)])@@ -63,3 +70,17 @@ -- | Same above, but for homogeneous pairs. shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)]) shrinkPair shrinker = shrinkPair' shrinker shrinker++------------------------------------------------------------------------++-- | 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
src/Test/StateMachine/Internal/Utils/BoxDrawer.hs view
@@ -66,7 +66,7 @@ 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 (Ret l) = "│ " ++ replicate (n - 8 - length l) ' ' ++ "→ " ++ l ++ " │" adjust n Bottom = "└" ++ replicate (n - 4) '─' ++ "┘" next :: ([Cmd], [Cmd]) -> [String]
+ src/Test/StateMachine/TH.hs view
@@ -0,0 +1,51 @@+-----------------------------------------------------------------------------+-- |+-- 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,6 +1,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE Rank2Types #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |@@ -23,18 +24,26 @@ Untyped(..) -- * Type aliases+ , StateMachine+ , stateMachine+ , StateMachine'(..) , Generator , Shrinker , Precondition , Transition- , Semantics , Postcondition , InitialModel+ , Result(..)+ , Semantics+ , Runner + -- * Data type generic operations+ , module Test.StateMachine.Types.Generics+ -- * Higher-order functors, foldables and traversables , module Test.StateMachine.Types.HFunctor - -- * Referenses+ -- * References , module Test.StateMachine.Types.References ) where@@ -43,9 +52,12 @@ (Ord1) import Data.Typeable (Typeable)+import Data.Void+ (Void) import Test.QuickCheck (Gen, Property) +import Test.StateMachine.Types.Generics import Test.StateMachine.Types.HFunctor import Test.StateMachine.Types.References @@ -63,6 +75,38 @@ ------------------------------------------------------------------------ +-- | A (non-failing) state machine record bundles up all functionality+-- needed to perform our tests.+type StateMachine model act m = StateMachine' model act Void m++-- | Same as above, but with possibly failing semantics.+data StateMachine' model act err m = StateMachine+ { generator' :: Generator model act+ , shrinker' :: Shrinker act+ , precondition' :: Precondition model act+ , transition' :: Transition model act+ , postcondition' :: Postcondition model act+ , model' :: InitialModel model+ , semantics' :: Semantics act err m+ , runner' :: Runner m+ }++-- | Helper for lifting non-failing semantics to a possibly failing+-- state machine record.+stateMachine+ :: Functor m+ => Generator model act+ -> Shrinker act+ -> Precondition model act+ -> Transition model act+ -> Postcondition model act+ -> InitialModel model+ -> (forall resp. act Concrete resp -> m resp)+ -> Runner m+ -> StateMachine' model act Void m+stateMachine gen shr precond trans post model sem run =+ StateMachine gen shr precond trans post model (fmap Ok . sem) run+ -- | When generating actions we have access to a model containing -- symbolic references. type Generator model act = model Symbolic -> Gen (Untyped act)@@ -81,9 +125,6 @@ type Transition model act = forall resp v. Ord1 v => model v -> act v resp -> v resp -> model v --- | When we execute our actions we have access to concrete references.-type Semantics act m = forall resp. act Concrete resp -> m resp- -- | Post-conditions are checked after the actions have been executed -- and we got a response. type Postcondition model act = forall resp.@@ -93,3 +134,12 @@ -- so that it can be used both in the pre- and the post-condition -- check. type InitialModel m = forall (v :: * -> *). m v++-- | The result of executing an action.+data Result resp err = Ok resp | Fail err++-- | When we execute our actions we have access to concrete references.+type Semantics act err m = forall resp. act Concrete resp -> m (Result resp err)++-- | How to run the monad used by the semantics.+type Runner m = m Property -> IO Property
+ src/Test/StateMachine/Types/Generics.hs view
@@ -0,0 +1,33 @@+{-# 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 view
@@ -0,0 +1,233 @@+{-# 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+ (liftA2)+import Control.Monad+ (filterM, (>=>))+import Data.Foldable+ (asum, foldl')+import Data.Functor.Classes+ (Show1)+import Data.Maybe+ (maybeToList)+import Language.Haskell.TH+import Language.Haskell.TH.Datatype+import Test.QuickCheck+ (shrink)++import Test.StateMachine.Internal.Utils+ (dropLast, nub, toLast)+import Test.StateMachine.Types+ (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)@.+-- See 'deriveShow' and 'deriveShowUntyped'.+deriveShows :: Name -> Q [Dec]+deriveShows = (liftA2 . liftA2) (++) deriveShow deriveShowUntyped++-- |+--+-- @+-- '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))+ return [StandaloneDerivD cxt_ instanceHead_]++-- |+-- @+-- '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))))+ return [StandaloneDerivD cxt_ instanceHead_]++-- | 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/TH.hs view
@@ -0,0 +1,209 @@+{-# 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
@@ -0,0 +1,115 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}++-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Types.History+-- 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 the notion of a history of an execution of a+-- (parallel) program.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Types.History+ ( History(..)+ , History'+ , ppHistory+ , HistoryEvent(..)+ , getProcessIdEvent+ , UntypedConcrete(..)+ , Operation(..)+ , linearTree+ )+ where++import Data.Dynamic+ (Dynamic)+import Data.Tree+ (Tree(Node))+import Data.Typeable+ (Typeable)++import Test.StateMachine.Internal.Types+import Test.StateMachine.Types+import Test.StateMachine.Internal.Types.Environment++------------------------------------------------------------------------++-- | 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]++-- | An event is either an invocation or a response.+data HistoryEvent act err+ = InvocationEvent act String Var Pid+ | ResponseEvent (Result Dynamic err) String Pid++-- | Untyped concrete actions.+data UntypedConcrete (act :: (* -> *) -> * -> *) where+ UntypedConcrete :: (Show resp, Typeable resp) =>+ act Concrete resp -> UntypedConcrete act++-- | Pretty print a history.+ppHistory :: History act err -> String+ppHistory = foldr go "" . unHistory+ where+ go :: HistoryEvent (UntypedConcrete act) err -> String -> String+ go (InvocationEvent _ str _ _) ih = " " ++ str ++ " ==> " ++ ih+ go (ResponseEvent _ str _) ih = str ++ "\n" ++ ih++-- | 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++findCorrespondingResp :: Pid -> History' act err -> [(Result Dynamic err, 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 ]++------------------------------------------------------------------------++-- | 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 (Concrete resp) err) Pid++-- | 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) pid) (linearTree es')+ | InvocationEvent (UntypedConcrete act) str _ pid <- takeInvocations es+ , (resp, es') <- findCorrespondingResp pid $ filter1 (not . matchInv pid) es+ ]+ where+ dynResp (Ok resp) = Ok (either (error . show) id (reifyDynamic resp))+ dynResp (Fail err) = Fail err++ filter1 :: (a -> Bool) -> [a] -> [a]+ filter1 _ [] = []+ filter1 p (x : xs) | p x = x : filter1 p xs+ | otherwise = xs++ -- Hmm, is this enough?+ matchInv pid (InvocationEvent _ _ _ pid') = pid == pid'+ matchInv _ _ = False
src/Test/StateMachine/Types/References.hs view
@@ -35,8 +35,6 @@ showsPrec1) import Data.Typeable (Typeable)-import Text.Read- (readPrec) import Test.StateMachine.Types.HFunctor @@ -55,7 +53,7 @@ -- during test execution. They provide access to the actual runtime value of -- a variable. ---data Reference v a = Reference (v a)+newtype Reference v a = Reference (v a) -- | Take the value from a concrete variable. --@@ -73,11 +71,15 @@ instance (Ord1 v, Ord a) => Ord (Reference v a) where compare (Reference x) (Reference y) = compare1 x y -instance (Show a, Show1 v) => Show (Reference v a) where- showsPrec p (Reference x) =- showParen (p >= 11) $- showsPrec1 11 x+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) @@ -110,15 +112,9 @@ deriving instance Eq (Symbolic a) deriving instance Ord (Symbolic a)--instance Show (Symbolic a) where- showsPrec p (Symbolic x) = showsPrec p x--instance Show1 Symbolic where- liftShowsPrec _ _ p (Symbolic x) = showsPrec p x--instance Typeable a => Read (Symbolic a) where- readPrec = Symbolic <$> readPrec+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@@ -126,20 +122,30 @@ instance Ord1 Symbolic where liftCompare _ (Symbolic x) (Symbolic y) = compare x y +instance Show1 Symbolic where+ liftShowsPrec _ _ p (Symbolic x) =+ showParen (p > appPrec) $+ showString "Symbolic " .+ showsPrec (appPrec + 1) x+ where+ appPrec = 10+ -- | Concrete values. -- newtype Concrete a where Concrete :: a -> Concrete a- deriving (Eq, Ord, Functor, Foldable, Traversable)--instance Show a => Show (Concrete a) where- showsPrec = showsPrec1--instance Show1 Concrete where- liftShowsPrec sp _ p (Concrete x) = sp p x+ deriving (Eq, Ord, Show, Read, Functor, Foldable, Traversable) 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 Show1 Concrete where+ liftShowsPrec sp _ p (Concrete x) =+ showParen (p > appPrec) $+ showString "Concrete " .+ sp (appPrec + 1) x+ where+ appPrec = 10
+ src/Test/StateMachine/Utils.hs view
@@ -0,0 +1,27 @@+-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Utils+-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : non-portable (GHC extensions)+--+-- This module exports some QuickCheck utility functions. Some of these should+-- perhaps be upstreamed.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Utils+ ( anyP+ , liftProperty+ , whenFailM+ , alwaysP+ , shrinkPropertyHelperC+ , shrinkPropertyHelperC'+ , shrinkPair+ , shrinkPair'+ ) where++import Test.StateMachine.Internal.Utils
+ src/Test/StateMachine/Z.hs view
@@ -0,0 +1,194 @@+-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Z+-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>+-- Stability : provisional+-- Portability : portable+--+-- This module contains Z-inspried combinators for working with relations. The+-- idea is that they can be used to define concise and showable models. This+-- module is an experiment and will likely change or move to its own package.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Z where++import qualified Data.List as List++------------------------------------------------------------------------++union :: Eq a => [a] -> [a] -> [a]+union = List.union++intersect :: Eq a => [a] -> [a] -> [a]+intersect = List.intersect++isSubsetOf :: Eq a => [a] -> [a] -> Bool+r `isSubsetOf` s = r == r `intersect` s++(~=) :: Eq a => [a] -> [a] -> Bool+xs ~= ys = xs `isSubsetOf` ys && ys `isSubsetOf` xs++------------------------------------------------------------------------++-- | Relations.+type Rel a b = [(a, b)]++-- | (Partial) functions.+type Fun a b = Rel a b++------------------------------------------------------------------------++empty :: Rel a b+empty = []++identity :: [a] -> Rel a a+identity xs = [ (x, x) | x <- xs ]++singleton :: a -> b -> Rel a b+singleton x y = [(x, y)]++domain :: Rel a b -> [a]+domain xys = [ x | (x, _) <- xys ]++codomain :: Rel a b -> [b]+codomain xys = [ y | (_, y) <- xys ]++compose :: Eq b => Rel b c -> Rel a b -> Rel a c+compose yzs xys =+ [ (x, z)+ | (x, y) <- xys+ , (y', z) <- yzs+ , y == y'+ ]++fcompose :: Eq b => Rel a b -> Rel b c -> Rel a c+fcompose r s = compose s r++inverse :: Rel a b -> Rel b a+inverse xys = [ (y, x) | (x, y) <- xys ]++lookupDom :: Eq a => a -> Rel a b -> [b]+lookupDom x xys = xys >>= \(x', y) -> [ y | x == x' ]++lookupCod :: Eq b => b -> Rel a b -> [a]+lookupCod y xys = xys >>= \(x, y') -> [ x | y == y' ]++------------------------------------------------------------------------++-- | Domain restriction.+--+-- >>> ['a'] <| [ ('a', "apa"), ('b', "bepa") ]+-- [('a',"apa")]+--+(<|) :: Eq a => [a] -> Rel a b -> Rel a b+xs <| xys = [ (x, y) | (x, y) <- xys, x `elem` xs ]++-- | Codomain restriction.+--+-- >>> [ ('a', "apa"), ('b', "bepa") ] |> ["apa"]+-- [('a',"apa")]+--+(|>) :: Eq b => Rel a b -> [b] -> Rel a b+xys |> ys = [ (x, y) | (x, y) <- xys, y `elem` ys ]++-- | Domain substraction.+--+-- >>> ['a'] <-| [ ('a', "apa"), ('b', "bepa") ]+-- [('b',"bepa")]+--+(<-|) :: Eq a => [a] -> Rel a b -> Rel a b+xs <-| xys = [ (x, y) | (x, y) <- xys, x `notElem` xs ]++-- | Codomain substraction.+--+-- >>> [ ('a', "apa"), ('b', "bepa") ] |-> ["apa"]+-- [('b',"bepa")]+--+(|->) :: Eq b => Rel a b -> [b] -> Rel a b+xys |-> ys = [ (x, y) | (x, y) <- xys, y `notElem` ys ]++-- | The image of a relation.+image :: Eq a => Rel a b -> [a] -> [b]+image r xs = codomain (xs <| r)++-- | Overriding.+--+-- >>> [('a', "apa")] <+ [('a', "bepa")]+-- [('a',"bepa")]+--+-- >>> [('a', "apa")] <+ [('b', "bepa")]+-- [('a',"apa"),('b',"bepa")]+--+(<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b+r <+ s = domain s <-| r `union` s++-- | Direct product.+(<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c)+xys <**> xzs =+ [ (x, (y, z))+ | (x , y) <- xys+ , (x', z) <- xzs+ , x == x'+ ]++-- | Parallel product.+(<||>) :: Rel a c -> Rel b d -> Rel (a, b) (c, d)+acs <||> bds =+ [ ((a, b), (c, d))+ | (a, c) <- acs+ , (b, d) <- bds+ ]++------------------------------------------------------------------------++isTotalRel :: Eq a => Rel a b -> [a] -> Bool+isTotalRel r xs = domain r ~= xs++isSurjRel :: Eq b => Rel a b -> [b] -> Bool+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++isPartialFun :: (Eq a, Eq b) => Rel a b -> Bool+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++isPartialInj :: (Eq a, Eq b) => Rel a b -> Bool+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)++isPartialSurj :: (Eq a, Eq b) => Rel a b -> [b] -> Bool+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++isBijection :: (Eq a, Eq b) => Rel a b -> [a] -> [b] -> Bool+isBijection r xs ys = isTotalInj r xs && isTotalSurj r xs ys++-- | Application.+(!) :: Eq a => Rel a b -> a -> Maybe b+xys ! x = lookup x xys++(.!) :: Rel a b -> a -> (Rel a b, a)+f .! x = (f, x)++-- | Assignment.+--+-- >>> singleton 'a' "apa" .! 'a' .= "bepa"+-- [('a',"bepa")]+--+-- >>> singleton 'a' "apa" .! 'b' .= "bepa"+-- [('a',"apa"),('b',"bepa")]+--+(.=) :: (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b+(f, x) .= y = f <+ singleton x y