diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal --- a/quickcheck-state-machine.cabal +++ b/quickcheck-state-machine.cabal @@ -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 diff --git a/src/Test/StateMachine.hs b/src/Test/StateMachine.hs --- a/src/Test/StateMachine.hs +++ b/src/Test/StateMachine.hs @@ -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) diff --git a/src/Test/StateMachine/Internal/Parallel.hs b/src/Test/StateMachine/Internal/Parallel.hs --- a/src/Test/StateMachine/Internal/Parallel.hs +++ b/src/Test/StateMachine/Internal/Parallel.hs @@ -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) "" 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) diff --git a/src/Test/StateMachine/Internal/Sequential.hs b/src/Test/StateMachine/Internal/Sequential.hs --- a/src/Test/StateMachine/Internal/Sequential.hs +++ b/src/Test/StateMachine/Internal/Sequential.hs @@ -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) "" (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 + ) diff --git a/src/Test/StateMachine/Internal/Types.hs b/src/Test/StateMachine/Internal/Types.hs --- a/src/Test/StateMachine/Internal/Types.hs +++ b/src/Test/StateMachine/Internal/Types.hs @@ -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 ------------------------------------------------------------------------ diff --git a/src/Test/StateMachine/Internal/Utils.hs b/src/Test/StateMachine/Internal/Utils.hs --- a/src/Test/StateMachine/Internal/Utils.hs +++ b/src/Test/StateMachine/Internal/Utils.hs @@ -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 diff --git a/src/Test/StateMachine/Internal/Utils/BoxDrawer.hs b/src/Test/StateMachine/Internal/Utils/BoxDrawer.hs --- a/src/Test/StateMachine/Internal/Utils/BoxDrawer.hs +++ b/src/Test/StateMachine/Internal/Utils/BoxDrawer.hs @@ -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] diff --git a/src/Test/StateMachine/TH.hs b/src/Test/StateMachine/TH.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/TH.hs @@ -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 +-- 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 + ] diff --git a/src/Test/StateMachine/Types.hs b/src/Test/StateMachine/Types.hs --- a/src/Test/StateMachine/Types.hs +++ b/src/Test/StateMachine/Types.hs @@ -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 diff --git a/src/Test/StateMachine/Types/Generics.hs b/src/Test/StateMachine/Types/Generics.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Types/Generics.hs @@ -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 +-- 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 diff --git a/src/Test/StateMachine/Types/Generics/TH.hs b/src/Test/StateMachine/Types/Generics/TH.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Types/Generics/TH.hs @@ -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 +-- 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))) []] diff --git a/src/Test/StateMachine/Types/HFunctor/TH.hs b/src/Test/StateMachine/Types/HFunctor/TH.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Types/HFunctor/TH.hs @@ -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 +-- 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 diff --git a/src/Test/StateMachine/Types/History.hs b/src/Test/StateMachine/Types/History.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Types/History.hs @@ -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 +-- 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 diff --git a/src/Test/StateMachine/Types/References.hs b/src/Test/StateMachine/Types/References.hs --- a/src/Test/StateMachine/Types/References.hs +++ b/src/Test/StateMachine/Types/References.hs @@ -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 diff --git a/src/Test/StateMachine/Utils.hs b/src/Test/StateMachine/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Utils.hs @@ -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 +-- 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 diff --git a/src/Test/StateMachine/Z.hs b/src/Test/StateMachine/Z.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Z.hs @@ -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 +-- 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