quickcheck-state-machine 0.2.0 → 0.3.0
raw patch · 19 files changed
+843/−504 lines, 19 filesdep ~QuickCheckdep ~basedep ~template-haskell
Dependency ranges changed: QuickCheck, base, template-haskell
Files
- CHANGELOG.md +13/−0
- CONTRIBUTING.md +13/−0
- README.md +30/−24
- quickcheck-state-machine.cabal +50/−55
- src/Test/StateMachine.hs +59/−59
- src/Test/StateMachine/Internal/AlphaEquality.hs +0/−71
- src/Test/StateMachine/Internal/Parallel.hs +213/−105
- src/Test/StateMachine/Internal/ScopeCheck.hs +0/−52
- src/Test/StateMachine/Internal/Sequential.hs +92/−59
- src/Test/StateMachine/Internal/Types.hs +34/−12
- src/Test/StateMachine/Internal/Types/Environment.hs +3/−2
- src/Test/StateMachine/Internal/Utils.hs +44/−17
- src/Test/StateMachine/Internal/Utils/BoxDrawer.hs +7/−1
- src/Test/StateMachine/Logic.hs +126/−0
- src/Test/StateMachine/Types.hs +59/−20
- src/Test/StateMachine/Types/Generics/TH.hs +53/−10
- src/Test/StateMachine/Types/History.hs +36/−13
- src/Test/StateMachine/Utils.hs +1/−2
- src/Test/StateMachine/Z.hs +10/−2
CHANGELOG.md view
@@ -1,3 +1,16 @@+#### 0.3.0 (2017-12-15)++ * A propositional logic module was added to help provide better+ counterexamples when pre- and post-conditions don't hold;++ * Generation of parallel programs was improved (base on+ a [comment](https://github.com/Quviq/QuickCheckExamples/issues/2) by+ Hans Svensson about how Erlang QuickCheck does it);++ * Support for semantics that might fail was added;++ * Pretty printing of counterexamples was improved.+ #### 0.2.0 * Z-inspired definition of relations and associated operations were
+ CONTRIBUTING.md view
@@ -0,0 +1,13 @@+## Contributing++### Release checklist++ 1. Update CHANGELOG.md;+ 2. Bump version in .cabal file and fix bounds;+ 3. Make tarball with `stack sdist --pvp-bounds both`;+ 4. Upload tarball as a+ package+ [candidate](https://hackage.haskell.org/packages/candidates/upload), and if+ everything looks good then release it;+ 5. Git tag the version: `git tag -a v$VERSION -m "Tag v$VERISON" && git push+ origin v$VERSION`.
README.md view
@@ -119,11 +119,11 @@ result. ```haskell-postcondition :: Model Concrete -> Action Concrete resp -> resp -> Property-postcondition _ New _ = property True-postcondition (Model m) (Read ref) resp = lookup ref m === Just resp-postcondition _ (Write _ _) _ = property True-postcondition _ (Inc _) _ = property True+postcondition :: Model Concrete -> Action Concrete resp -> resp -> Bool+postcondition _ New _ = True+postcondition (Model m) (Read ref) resp = lookup ref m == Just resp+postcondition _ (Write _ _) _ = True+postcondition _ (Inc _) _ = True ``` Finally, we have to explain how to generate and shrink actions.@@ -149,7 +149,7 @@ ```haskell sm :: Problem -> StateMachine Model Action IO-sm prb = StateMachine+sm prb = stateMachine generator shrinker precondition transition postcondition initModel (semantics prb) id ```@@ -157,13 +157,13 @@ We can now define a sequential property as follows. ```haskell-prop_references :: Problem -> Property-prop_references prb = monadicSequential (sm prb) $ \prog -> do- (hist, model, prop) <- runProgram (sm prb) prog- prettyProgram prog hist model $- checkActionNames prog numberOfConstructors prop+prop_references :: Problem -> PropertyOf (Program Action)+prop_references prb = monadicSequentialC sm' $ \prog -> do+ (hist, _, res) <- runProgram sm' prog+ prettyProgram sm' hist $+ checkActionNames prog (res === Ok) where- numberOfConstructors = 4+ sm' = sm prb ``` If we run the sequential property without introducing any problems to the@@ -173,9 +173,23 @@ ``` > quickCheck (prop_references Bug)-*** Failed! Falsifiable (after 16 tests and 4 shrinks):-[New (Var 0),Write (Var 0) 5 (Var 2),Read (Var 0) (Var 3)]-Just 5 /= Just 6+*** Failed! Falsifiable (after 19 tests and 3 shrinks):++Model []++ New --> Opaque++Model [(Reference Concrete Opaque,0)]++ Write (Reference (Symbolic (Var 0))) 5 --> ()++Model [(Reference Concrete Opaque,5)]++ Read (Reference (Symbolic (Var 0))) --> 6++Model [(Reference Concrete Opaque,5)]++PostconditionFailed /= Ok ``` Recall that the bug problem causes the write of values ``i `elem` [5..10]`` to@@ -294,7 +308,7 @@ Here are some more examples to get you started: - * The water jug problem from *Die Hard 2* -- this is a+ * The water jug problem from *Die Hard 3* -- this is a simple [example](https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/DieHard.hs) of a specification where we use the sequential property to find a solution@@ -348,14 +362,6 @@ Sane* [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf), [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
quickcheck-state-machine.cabal view
@@ -1,47 +1,42 @@-name: quickcheck-state-machine-version: 0.2.0-cabal-version: >=1.10-build-type: Simple-license: BSD3-license-file: LICENSE-copyright: Copyright (C) 2017, ATS Advanced Telematic Systems GmbH-maintainer: Stevan Andjelkovic <stevan@advancedtelematic.com>-homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme-synopsis: Test monadic programs using state machine based models-description:- See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>-category: Testing-author: Stevan Andjelkovic-tested-with: GHC ==8.0.2-extra-source-files:- README.md- CHANGELOG.md--source-repository head- type: git- location: https://github.com/advancedtelematic/quickcheck-state-machine+name: quickcheck-state-machine+version: 0.3.0+synopsis: Test monadic programs using state machine based models+description: See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>+homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme+license: BSD3+license-file: LICENSE+author: Stevan Andjelkovic+maintainer: Stevan Andjelkovic <stevan@advancedtelematic.com>+copyright: Copyright (C) 2017, ATS Advanced Telematic Systems GmbH+category: Testing+build-type: Simple+extra-source-files: README.md+ , CHANGELOG.md+ , CONTRIBUTING.md+cabal-version: >=1.10+tested-with: GHC == 8.0.2, GHC == 8.2.2 library- exposed-modules:- Test.StateMachine- Test.StateMachine.Internal.AlphaEquality- Test.StateMachine.Internal.Parallel- Test.StateMachine.Internal.ScopeCheck- Test.StateMachine.Internal.Sequential- Test.StateMachine.Internal.Types- 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:+ hs-source-dirs: src+ exposed-modules: Test.StateMachine+ , Test.StateMachine.Internal.Parallel+ , Test.StateMachine.Internal.Sequential+ , Test.StateMachine.Internal.Types+ , Test.StateMachine.Internal.Types.Environment+ , Test.StateMachine.Internal.Utils+ , Test.StateMachine.Internal.Utils.BoxDrawer+ , Test.StateMachine.Logic+ , Test.StateMachine.TH+ , Test.StateMachine.Types+ , Test.StateMachine.Types.Generics+ , Test.StateMachine.Types.Generics.TH+ , Test.StateMachine.Types.HFunctor+ , Test.StateMachine.Types.HFunctor.TH+ , Test.StateMachine.Types.History+ , Test.StateMachine.Types.References+ , Test.StateMachine.Z+ other-modules: Test.StateMachine.Utils+ build-depends: ansi-wl-pprint >=0.6.7.3 && <0.7, async >=2.1.1.1 && <2.2, base >=4.7 && <5,@@ -50,22 +45,22 @@ lifted-base >=0.2.3.11 && <0.3, monad-control >=1.0.2.2 && <1.1, mtl >=2.2.1 && <2.3,- QuickCheck >=2.9.2 && <2.10,+ QuickCheck >=2.9.2 && <2.11, quickcheck-with-counterexamples >=1.0 && <2.0, random ==1.1.*, stm >=2.4.4.1 && <2.5,- template-haskell >=2.11.1.0 && <2.12,+ template-haskell >=2.11.1.0 && <2.13, th-abstraction >=0.2.6.0 && <0.3- default-language: Haskell2010- hs-source-dirs: src- other-modules:- Test.StateMachine.Utils+ default-language: Haskell2010 test-suite quickcheck-state-machine-test- type: exitcode-stdio-1.0- main-is: Spec.hs- build-depends:- base >=4.9.1.0 && <4.10- default-language: Haskell2010- hs-source-dirs: test- ghc-options: -threaded -rtsopts -with-rtsopts=-N+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends: base+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/advancedtelematic/quickcheck-state-machine
src/Test/StateMachine.hs view
@@ -1,3 +1,6 @@+{-# OPTIONS_GHC -Wno-orphans #-}++{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Rank2Types #-}@@ -34,7 +37,6 @@ -- * Parallel property combinators , ParallelProgram- , forAllParallelProgram , History , monadicParallel , runParallelProgram@@ -44,7 +46,6 @@ -- * With counterexamples , forAllProgramC , monadicSequentialC- , forAllParallelProgramC , monadicParallelC -- * Types@@ -60,23 +61,30 @@ (evalStateT, replicateM) import Control.Monad.Trans.Control (MonadBaseControl)+import Data.Functor.Classes+ (Show1) import Data.Map (Map) import qualified Data.Map as M+import Data.Typeable+ (Typeable) import Test.QuickCheck- (Property, collect, cover, ioProperty, property)+ (Property, Testable, collect, cover, ioProperty,+ property) import qualified Test.QuickCheck import Test.QuickCheck.Counterexamples- ((:&:)(..), PropertyOf, forAllShrink)+ ((:&:)(..), PropertyOf) import qualified Test.QuickCheck.Counterexamples as CE import Test.QuickCheck.Monadic (PropertyM, monadic, run)+import Test.QuickCheck.Property+ (succeeded) import Test.StateMachine.Internal.Parallel import Test.StateMachine.Internal.Sequential import Test.StateMachine.Internal.Types import Test.StateMachine.Internal.Utils- (whenFailM)+ (forAllShrinkShowC, whenFailM) import Test.StateMachine.Types import Test.StateMachine.Types.History @@ -84,12 +92,11 @@ -- | This function is like a 'forAllShrink' for sequential programs. forAllProgram- :: Show (Untyped act)- => HFoldable act+ :: HFoldable act => Generator model act -> Shrinker act -> Precondition model act- -> Transition model act+ -> Transition' model act err -> InitialModel model -> (Program act -> Property) -- ^ Predicate that should hold for all -- programs.@@ -102,28 +109,28 @@ -- | Variant of 'forAllProgram' which returns the generated and shrunk -- program if the property fails. forAllProgramC- :: Show (Untyped act)- => HFoldable act+ :: HFoldable act => Generator model act -> Shrinker act -> Precondition model act- -> Transition model act+ -> Transition' model act err -> InitialModel model -> (Program act -> PropertyOf a) -- ^ Predicate that should hold for all -- programs. -> PropertyOf (Program act :&: a) forAllProgramC generator shrinker precondition transition model =- forAllShrink+ forAllShrinkShowC (evalStateT (generateProgram generator precondition transition 0) model) (shrinkProgram shrinker precondition transition model)+ (const "") -- | Wrapper around 'forAllProgram' using the 'StateMachine' specification -- to generate and shrink sequential programs. monadicSequential :: Monad m- => Show (Untyped act) => HFoldable act- => StateMachine' model act err m+ => Testable a+ => StateMachine' model act m err -> (Program act -> PropertyM m a) -- ^ Predicate that should hold for all programs. -> Property@@ -132,9 +139,9 @@ -- | Variant of 'monadicSequential' with counterexamples. monadicSequentialC :: Monad m- => Show (Untyped act) => HFoldable act- => StateMachine' model act err m+ => Testable a+ => StateMachine' model act m err -> (Program act -> PropertyM m a) -- ^ Predicate that should hold for all programs. -> PropertyOf (Program act)@@ -145,29 +152,39 @@ . monadic (ioProperty . runner') . predicate +#if !MIN_VERSION_QuickCheck(2,10,0)+instance Testable () where+ property = property . liftUnit+ where+ liftUnit () = succeeded+#endif+ -- | Testable property of sequential programs derived from a -- 'StateMachine' specification. runProgram- :: forall m act err model- . Monad m- => Show (Untyped act)+ :: Monad m+ => Show1 (act Symbolic)+ => Show err+ => Typeable err => HTraversable act- => StateMachine' model act err m+ => StateMachine' model act m err -- ^ -> Program act- -> PropertyM m (History act err, model Concrete, Property)+ -> PropertyM m (History act err, model Concrete, Reason) runProgram sm = run . executeProgram sm -- | Takes the output of running a program and pretty prints a -- counterexample if the run failed. prettyProgram :: MonadIO m- => Program act+ => Show (model Concrete)+ => Show err+ => StateMachine' model act m err -> History act err- -> model Concrete -> Property -> PropertyM m ()-prettyProgram _ hist _ prop = putStrLn (ppHistory hist) `whenFailM` prop+prettyProgram StateMachine{..} hist prop =+ putStrLn (ppHistory model' transition' hist) `whenFailM` prop -- | Print distribution of actions and fail if some actions have not been -- executed.@@ -189,47 +206,32 @@ ------------------------------------------------------------------------ -- | This function is like a 'forAllShrink' for parallel programs.-forAllParallelProgram- :: Show (Untyped act)- => HFoldable act- => Generator model act- -> Shrinker act- -> Precondition model act- -> Transition model act- -> InitialModel model- -> (ParallelProgram act -> Property) -- ^ Predicate that should hold- -- 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)+ :: Show1 (act Symbolic)+ => Eq (Untyped act) => HFoldable act => Generator model act -> Shrinker act -> Precondition model act- -> Transition model act+ -> Transition' model act err -> InitialModel model -> (ParallelProgram act -> PropertyOf a) -- ^ Predicate that should hold -- for all parallel programs. -> PropertyOf (ParallelProgram act :&: a) forAllParallelProgramC generator shrinker precondition transition model =- forAllShrink+ forAllShrinkShowC (generateParallelProgram generator precondition transition model) (shrinkParallelProgram shrinker precondition transition model)+ (const "") --- | Wrapper around 'forAllParallelProgram' using the 'StateMachine'+-- | Wrapper around 'forAllParallelProgram using the 'StateMachine' -- specification to generate and shrink parallel programs. monadicParallel :: MonadBaseControl IO m- => Show (Untyped act)+ => Eq (Untyped act)+ => Show1 (act Symbolic) => HFoldable act- => StateMachine' model act err m+ => StateMachine' model act m err -> (ParallelProgram act -> PropertyM m ()) -- ^ Predicate that should hold for all parallel programs. -> Property@@ -238,9 +240,10 @@ -- | Variant of 'monadicParallel' with counterexamples. monadicParallelC :: MonadBaseControl IO m- => Show (Untyped act)+ => Eq (Untyped act)+ => Show1 (act Symbolic) => HFoldable act- => StateMachine' model act err m+ => StateMachine' model act m err -> (ParallelProgram act -> PropertyM m ()) -- ^ Predicate that should hold for all parallel programs. -> PropertyOf (ParallelProgram act)@@ -255,24 +258,20 @@ -- 'StateMachine' specification. runParallelProgram :: MonadBaseControl IO m- => Show (Untyped act)+ => Show1 (act Symbolic) => HTraversable act- => StateMachine' model act err m+ => StateMachine' model act m err -- ^ -> ParallelProgram act -> PropertyM m [(History act err, Property)] runParallelProgram = runParallelProgram' 10 --- | 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' :: MonadBaseControl IO m- => Show (Untyped act)+ => Show1 (act Symbolic) => HTraversable act => Int -- ^ How many times to execute the parallel program.- -> StateMachine' model act err m+ -> StateMachine' model act m err -- ^ -> ParallelProgram act -> PropertyM m [(History act err, Property)]@@ -286,8 +285,9 @@ prettyParallelProgram :: MonadIO m => HFoldable act+ => Show (Untyped act) => ParallelProgram act- -> [(History act err, Property)] -- ^ Output of 'runParallelProgram'.+ -> [(History act err, Property)] -- ^ Output of 'runParallelProgram. -> PropertyM m () prettyParallelProgram prog = mapM_ (\(hist, prop) ->
− src/Test/StateMachine/Internal/AlphaEquality.hs
@@ -1,71 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.AlphaEquality--- 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 provides \(\alpha\)-equality for internal actions. This--- functionality isn't used anywhere in the library, but can be useful--- for writing--- <https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs metaproperties>.-----------------------------------------------------------------------------------module Test.StateMachine.Internal.AlphaEquality- ( alphaEq- , alphaEqFork- ) where--import Control.Monad.State- (State, get, modify, evalState, runState)-import Data.Map- (Map)-import qualified Data.Map as M--import Test.StateMachine.Types-import Test.StateMachine.Internal.Types------------------------------------------------------------------------------ | Check if two lists of actions are equal modulo--- \(\alpha\)-conversion.-alphaEq- :: (HFunctor act, Eq (Program act))- => Program act -> Program act -- ^ The two input programs.- -> Bool-alphaEq acts1 acts2 = canonical acts1 == canonical acts2--canonical :: HFunctor act => Program act -> Program act-canonical = Program . fst . flip runState M.empty . canonical' . unProgram--canonical' :: HFunctor act => [Internal act] -> State (Map Var Var) [Internal act]-canonical' [] = return []-canonical' (Internal act (Symbolic var) : acts) = do- env <- get- let act' = hfmap (\(Symbolic v) -> Symbolic (env M.! v)) act- var' = Var (M.size env)- sym' = Symbolic var'- modify (M.insert var var')- ih <- canonical' acts- return (Internal act' sym' : ih)---- | Check if two forks of actions are equal modulo--- \(\alpha\)-conversion.-alphaEqFork- :: (HFunctor act, Eq (Program act))- => Fork (Program act) -> Fork (Program act) -- ^ The two input forks.- -> Bool-alphaEqFork f1 f2 = canonicalFork f1 == canonicalFork f2--canonicalFork :: HFunctor act => Fork (Program act) -> Fork (Program act)-canonicalFork (Fork l p r) = Fork (Program l') (Program p') (Program r')- where- (p', m) = runState (canonical' (unProgram p)) M.empty- l' = evalState (canonical' (unProgram l)) m- r' = evalState (canonical' (unProgram r)) m
src/Test/StateMachine/Internal/Parallel.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- |@@ -22,37 +22,47 @@ module Test.StateMachine.Internal.Parallel ( generateParallelProgram , shrinkParallelProgram+ , validParallelProgram , executeParallelProgram , linearise , toBoxDrawings ) where +import Control.Arrow+ ((***)) import Control.Concurrent.Async.Lifted (concurrently) import Control.Concurrent.Lifted (threadDelay) import Control.Concurrent.STM- (STM, atomically)+ (atomically) import Control.Concurrent.STM.TChan- (TChan, newTChanIO, tryReadTChan, writeTChan)+ (TChan, newTChanIO, writeTChan) import Control.Monad- (foldM)+ (foldM, forM_) import Control.Monad.State- (StateT, evalState, evalStateT, execStateT, get,- lift, modify, runState, runStateT)+ (StateT, evalStateT, execStateT, get,+ lift, modify) import Control.Monad.Trans.Control (MonadBaseControl, liftBaseWith)+import Data.Bifunctor+ (bimap) import Data.Dynamic (toDyn)+import Data.Functor.Classes+ (Show1, showsPrec1) import Data.List- (partition)+ (partition, permutations)+import Data.Monoid+ ((<>)) import Data.Set (Set) import qualified Data.Set as S import Data.Tree (Tree(Node)) import Test.QuickCheck- (Gen, Property, property, shrinkList, (.&&.))+ (Gen, Property, choose, property, shrinkList, sized,+ (.&&.)) import Text.PrettyPrint.ANSI.Leijen (Doc) @@ -72,49 +82,136 @@ generateParallelProgram :: Generator model act -> Precondition model act- -> Transition model act+ -> Transition' model act err -> model Symbolic -> Gen (ParallelProgram act) generateParallelProgram generator precondition transition model = do- let generate = generateProgram generator precondition transition- (prefix, model') <- runStateT (generate 0) model- let offset = length (unProgram prefix)- left <- evalStateT (generate offset) model'- let offset' = offset + length (unProgram left)- right <- evalStateT (generate offset') model'- return (ParallelProgram (Fork left prefix right))+ Program is <- generateProgram' generator precondition transition model+ prefixLength <- sized (\k -> choose (0, k `div` 3))+ let (prefix, rest) = bimap Program Program (splitAt prefixLength is)+ return (ParallelProgram prefix+ (splitProgram precondition transition (advanceModel transition model prefix) rest)) -- | Shrink a parallel program in a pre-condition and scope respecting -- way. shrinkParallelProgram- :: HFoldable act+ :: forall act model err+ . HFoldable act+ => Eq (Untyped act) => Shrinker act -> Precondition model act- -> Transition model act+ -> Transition' model act err -> model Symbolic -> (ParallelProgram act -> [ParallelProgram act])-shrinkParallelProgram shrinker precondition transition model- = fmap ParallelProgram- . go- . unParallelProgram+shrinkParallelProgram shrinker precondition transition model (ParallelProgram prefix suffixes)+ = filter (validParallelProgram precondition transition model)+ [ ParallelProgram prefix' suffixes'+ | (prefix', suffixes') <- shrinkPair' shrinkProgram' shrinkSuffixes (prefix, suffixes)+ ]+ +++ shrinkMoveSuffixToPrefix where- go (Fork l p r) = map forkFilterInvalid- [ Fork l' p' r'- | (p', (l', r')) <- shrinkPair' shrinker' (shrinkPair shrinker') (p, (l, r))- ]+ shrinkProgram' :: Program act -> [Program act]+ shrinkProgram'+ = map Program+ . shrinkList (liftShrinkInternal shrinker)+ . unProgram++ shrinkSuffixes :: [(Program act, Program act)] -> [[(Program act, Program act)]]+ shrinkSuffixes = shrinkList (shrinkPair shrinkProgram')++ shrinkMoveSuffixToPrefix :: [ParallelProgram act]+ shrinkMoveSuffixToPrefix = case suffixes of+ [] -> []+ (suffix : suffixes') ->+ [ ParallelProgram (prefix <> Program [prefix'])+ (bimap Program Program suffix' : suffixes')+ | (prefix', suffix') <- pickOneReturnRest2 (unProgram (fst suffix),+ unProgram (snd suffix))+ ]++ pickOneReturnRest :: [a] -> [(a, [a])]+ pickOneReturnRest [] = []+ pickOneReturnRest (x : xs) = (x, xs) : map (id *** (x :)) (pickOneReturnRest xs)++ pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a],[a]))]+ pickOneReturnRest2 (xs, ys) =+ map (id *** flip (,) ys) (pickOneReturnRest xs) +++ map (id *** (,) xs) (pickOneReturnRest ys)++validParallelProgram+ :: HFoldable act+ => Precondition model act+ -> Transition' model act err+ -> model Symbolic+ -> ParallelProgram act+ -> Bool+validParallelProgram precondition transition model (ParallelProgram prefix suffixes)+ = validProgram precondition transition model prefix+ && validSuffixes precondition transition prefixModel prefixScope (parallelProgramToList suffixes)+ where+ prefixModel = advanceModel transition model prefix+ prefixScope = boundVars prefix++boundVars :: Program act -> Set Var+boundVars+ = foldMap (\(Internal _ (Symbolic var)) -> S.singleton var)+ . unProgram++usedVars :: HFoldable act => Program act -> Set Var+usedVars+ = foldMap (\(Internal act _) -> hfoldMap (\(Symbolic var) -> S.singleton var) act)+ . unProgram++validSuffixes+ :: forall act model err+ . HFoldable act+ => Precondition model act+ -> Transition' model act err+ -> model Symbolic+ -> Set Var+ -> [Program act]+ -> Bool+validSuffixes precondition transition model0 scope0 = go model0 scope0+ where+ go :: model Symbolic -> Set Var -> [Program act] -> Bool+ go _ _ [] = True+ go model scope (prog : progs)+ = usedVars prog `S.isSubsetOf` scope' -- This assumes that variables+ -- are bound before used in a+ -- program.+ && parallelSafe precondition transition model prog+ && go (advanceModel transition model prog) scope' progs where- shrinker'- = map Program- . shrinkList (liftShrinkInternal shrinker)- . unProgram+ scope' = boundVars prog `S.union` scope - forkFilterInvalid (Fork l p r) =- let- filterProgram = filterInvalid precondition transition- (p', (model', scope)) = runState (filterProgram p) (model, S.empty)- l' = evalState (filterProgram l) (model', scope)- r' = evalState (filterProgram r) (model', scope)- in Fork l' p' r'+runMany+ :: MonadBaseControl IO m+ => HTraversable act+ => Show1 (act Symbolic)+ => Semantics' act m err+ -> TChan (HistoryEvent (UntypedConcrete act) err)+ -> Pid+ -> [Internal act]+ -> StateT Environment m ()+runMany semantics hchan pid = flip foldM () $ \_ (Internal act sym@(Symbolic var)) -> do+ env <- get+ case reify env act of+ Left _ -> return () -- The reference that the action uses failed to+ -- create.+ Right cact -> do+ liftBaseWith $ const $ atomically $ writeTChan hchan $+ InvocationEvent (UntypedConcrete cact) (showsPrec1 10 act "") var pid+ mresp <- lift (semantics cact)+ threadDelay 10+ case mresp of+ Fail err ->+ liftBaseWith $ const $+ atomically $ writeTChan hchan $ ResponseEvent (Fail err) "<fail>" pid+ Success resp -> do+ modify (insertConcrete sym (Concrete resp))+ liftBaseWith $ const $+ atomically $ writeTChan hchan $ ResponseEvent (Success (toDyn resp)) (show resp) pid -- | Run a parallel program, by first executing the prefix sequentially -- and then the suffixes in parallel, and return the history (or@@ -123,60 +220,22 @@ :: forall m act err . MonadBaseControl IO m => HTraversable act- => Show (Untyped act)- => Semantics act err m+ => Show1 (act Symbolic)+ => Semantics' act m err -> ParallelProgram act -> m (History act err)-executeParallelProgram semantics = liftSemFork . unParallelProgram- where- liftSemFork- :: HTraversable act- => Show (Untyped act)- => Fork (Program act)- -> m (History act err)- liftSemFork (Fork left prefix right) = do- hchan <- liftBaseWith (const newTChanIO)- env <- execStateT (runMany hchan (Pid 0) (unProgram prefix)) emptyEnvironment- _ <- 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 [])- where- go :: [a] -> STM [a]- go acc = do- mx <- tryReadTChan chan- case mx of- Just x -> go $ x : acc- Nothing -> return acc+executeParallelProgram semantics (ParallelProgram prefix suffixes) = do+ hchan <- liftBaseWith (const newTChanIO)+ env <- execStateT+ (runMany semantics hchan (Pid 0) (unProgram prefix))+ emptyEnvironment+ forM_ suffixes $ \(prog1, prog2) -> do+ _ <- concurrently+ (evalStateT (runMany semantics hchan (Pid 1) (unProgram prog1)) env)+ (evalStateT (runMany semantics hchan (Pid 2) (unProgram prog2)) env)+ return () - runMany- :: HTraversable act- => Show (Untyped act)- => TChan (HistoryEvent (UntypedConcrete act) err)- -> Pid- -> [Internal act]- -> StateT Environment m ()- runMany hchan pid = flip foldM () $ \_ (Internal act sym@(Symbolic var)) -> do- env <- get- case reify env act of- Left _ -> return () -- The reference that the action uses failed to- -- create.- Right cact -> do- liftBaseWith $ const $ atomically $ writeTChan hchan $- InvocationEvent (UntypedConcrete cact) (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+ History <$> liftBaseWith (const (getChanContents hchan)) ------------------------------------------------------------------------ @@ -185,8 +244,8 @@ -- concurrent objects* paper linked to from the README for more info. linearise :: forall model act err- . Transition model act- -> Postcondition model act+ . Transition' model act err+ -> Postcondition' model act err -> InitialModel model -> History act err -> Property@@ -197,11 +256,9 @@ go es = anyP (step model0) (linearTree es) 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+ step model (Node (Operation act _ resp _ _) roses) =+ postcondition model act resp .&&.+ anyP' (step (transition model act (fmap Concrete resp))) roses anyP' :: (a -> Property) -> [a] -> Property anyP' _ [] = property True@@ -212,14 +269,12 @@ -- | 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+toBoxDrawings (ParallelProgram prefix suffixes) = toBoxDrawings'' allVars where- allVars = S.unions [l0, p0, r0]- Fork l0 p0 r0 = fmap (S.unions . vars . unProgram) (unParallelProgram prog)- vars xs = [ getUsedVars x | Internal x _ <- xs]+ allVars = usedVars prefix `S.union` foldMap usedVars (parallelProgramToList suffixes) - toBoxDrawings' :: Set Var -> History act err -> Doc- toBoxDrawings' knownVars (History h) = exec evT (fmap out <$> Fork l p r)+ 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'@@ -239,3 +294,56 @@ evT :: [(EventType, Pid)] evT = toEventType (filter (\e -> getProcessIdEvent e `elem` map Pid [1,2]) h)++------------------------------------------------------------------------++splitProgram+ :: Precondition model act+ -> Transition' model act err+ -> model Symbolic+ -> Program act+ -> [(Program act, Program act)]+splitProgram precondition transition model0 = go model0 [] . unProgram+ where+ go _ acc [] = reverse acc+ go model acc iacts = go (advanceModel transition model (Program safe))+ ((Program safe1, Program safe2) : acc)+ rest+ where+ (safe, rest) = spanSafe model [] iacts+ (safe1, safe2) = splitAt (length safe `div` 2) safe++ spanSafe _ safe [] = (reverse safe, [])+ spanSafe model safe (iact@(Internal _ _) : iacts)+ | length safe <= 5 && parallelSafe precondition transition model (Program (iact : safe))+ = spanSafe model (iact : safe) iacts+ | otherwise+ = (reverse safe, iact : iacts)++parallelSafe+ :: Precondition model act+ -> Transition' model act err+ -> model Symbolic+ -> Program act+ -> Bool+parallelSafe precondition transition model0+ = and+ . map (preconditionsHold model0)+ . permutations+ . unProgram+ where+ preconditionsHold _ [] = True+ preconditionsHold model (Internal act sym : iacts)+ = precondition model act+ && preconditionsHold (transition model act (Success sym)) iacts++advanceModel+ :: Transition' model act err+ -> model Symbolic+ -> Program act+ -> model Symbolic+advanceModel transition model0 = go model0 . unProgram+ where+ go model [] = model+ go model (Internal act sym : iacts) =+ go (transition model act (Success sym)) iacts
− src/Test/StateMachine/Internal/ScopeCheck.hs
@@ -1,52 +0,0 @@-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ScopedTypeVariables #-}---------------------------------------------------------------------------------- |--- Module : Test.StateMachine.Internal.ScopeCheck--- 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 provides scope-checking for internal actions. This--- functionality isn't used anywhere in the library, but can be useful--- for writing--- <https://github.com/advancedtelematic/quickcheck-state-machine/blob/master/example/src/MutableReference/Prop.hs metaproperties>.-----------------------------------------------------------------------------------module Test.StateMachine.Internal.ScopeCheck- ( scopeCheck- , scopeCheckParallel- ) where--import Data.Monoid- ((<>))-import Data.Set- (Set)-import qualified Data.Set as S--import Test.StateMachine.Internal.Sequential- (getUsedVars)-import Test.StateMachine.Internal.Types-import Test.StateMachine.Types------------------------------------------------------------------------------ | Scope-check a program, i.e. make sure that no action uses a--- reference that doesn't exist.-scopeCheck :: forall act. HFoldable act => Program act -> Bool-scopeCheck = go S.empty . unProgram- where- go :: Set Var -> [Internal act] -> Bool- go _ [] = True- go known (Internal act (Symbolic var) : iacts) =- getUsedVars act `S.isSubsetOf` known && go (S.insert var known) iacts---- | Same as above, but for parallel programs.-scopeCheckParallel :: HFoldable act => ParallelProgram act -> Bool-scopeCheckParallel (ParallelProgram (Fork l p r)) =- scopeCheck (p <> l) && scopeCheck (p <> r)
src/Test/StateMachine/Internal/Sequential.hs view
@@ -20,28 +20,34 @@ module Test.StateMachine.Internal.Sequential ( generateProgram+ , generateProgram' , filterInvalid , getUsedVars , liftShrinkInternal+ , validProgram , shrinkProgram , executeProgram ) where import Control.Monad- (filterM, foldM, when)+ (filterM, when) import Control.Monad.State- (State, StateT, evalState, get, lift, put)+ (State, StateT, evalStateT, get, lift,+ put) import Data.Dynamic (toDyn)+import Data.Functor.Classes+ (Show1, showsPrec1) import Data.Monoid ((<>)) import Data.Set (Set) import qualified Data.Set as S+import Data.Typeable+ (Typeable) import Test.QuickCheck- (Gen, Property, choose, counterexample, property,- shrinkList, sized, suchThat, (.&&.))+ (Gen, choose, shrinkList, sized, suchThat) import Test.StateMachine.Internal.Types import Test.StateMachine.Internal.Types.Environment@@ -52,10 +58,10 @@ -- | Generate programs whose actions all respect their pre-conditions. generateProgram- :: forall model act+ :: forall model act err . Generator model act -> Precondition model act- -> Transition model act+ -> Transition' model act err -> Int -- ^ Name supply for symbolic variables. -> StateT (model Symbolic) Gen (Program act) generateProgram generator precondition transition index = do@@ -69,17 +75,25 @@ Untyped act <- lift (generator model `suchThat` \(Untyped act) -> precondition model act) let sym = Symbolic (Var ix)- put (transition model act sym)+ put (transition model act (Success sym)) acts <- go (sz - 1) (ix + 1) return (Internal act sym : acts) +generateProgram'+ :: Generator model act+ -> Precondition model act+ -> Transition' model act err+ -> model Symbolic+ -> Gen (Program act)+generateProgram' g p t = evalStateT (generateProgram g p t 0)+ -- | Filter out invalid actions from a program. An action is invalid if -- either its pre-condition doesn't hold, or it uses references that -- are not in scope. filterInvalid :: HFoldable act => Precondition model act- -> Transition model act+ -> Transition' model act err -> Program act -> State (model Symbolic, Set Var) (Program act) -- ^ Where @Set Var@ -- is the scope.@@ -91,7 +105,7 @@ go (Internal act sym@(Symbolic var)) = do (model, scope) <- get let valid = precondition model act && getUsedVars act `S.isSubsetOf` scope- when valid (put (transition model act sym, S.insert var scope))+ when valid (put (transition model act (Success sym), S.insert var scope)) return valid -- | Returns the set of references an action uses.@@ -104,81 +118,100 @@ liftShrinkInternal shrinker (Internal act sym) = [ Internal act' sym | act' <- shrinker act ] +validProgram+ :: forall act model err+ . HFoldable act+ => Precondition model act+ -> Transition' model act err+ -> model Symbolic+ -> Program act+ -> Bool+validProgram precondition transition model0 = go model0 S.empty . unProgram+ where+ go :: model Symbolic -> Set Var -> [Internal act] -> Bool+ go _ _ [] = True+ go model scope (Internal act sym@(Symbolic var) : is) =+ valid && go (transition model act (Success sym)) (S.insert var scope) is+ where+ valid = precondition model act && getUsedVars act `S.isSubsetOf` scope+ -- | Shrink a program in a pre-condition and scope respecting way. shrinkProgram :: HFoldable act => Shrinker act -> Precondition model act- -> Transition model act+ -> Transition' model act err -> model Symbolic -> Program act -- ^ Program to shrink. -> [Program act] shrinkProgram shrinker precondition transition model- = map ( flip evalState (model, S.empty)- . filterInvalid precondition transition- . Program- )+ = filter (validProgram precondition transition model)+ . map Program . shrinkList (liftShrinkInternal shrinker) . unProgram --- | Execute a program and return a history, the final model and a property--- which contains the information of whether the execution respects the state+-- | Execute a program and return a history, the final model and a result which+-- contains the information of whether the execution respects the state -- machine model or not. executeProgram- :: forall m act err model+ :: forall m act model err . Monad m- => Show (Untyped act)+ => Typeable err+ => Show1 (act Symbolic)+ => Show err => HTraversable act- => StateMachine' model act err m+ => StateMachine' model act m err -> 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)+ -> m (History act err, model Concrete, Reason)+executeProgram StateMachine{..}+ = fmap (\(hist, _, cmodel, _, reason) -> (hist, cmodel, reason))+ . go (mempty, model', model', emptyEnvironment) . unProgram where- go :: (History act err, model Symbolic, model Concrete, Environment, Property)- -> Internal act- -> m (History act err, model Symbolic, model Concrete, Environment, Property)- go (hist, smodel, cmodel, env, prop) (Internal act sym@(Symbolic var)) =+ go :: (History act err, model Symbolic, model Concrete, Environment)+ -> [Internal act]+ -> m (History act err, model Symbolic, model Concrete, Environment, Reason)+ go (hist, smodel, cmodel, env) [] =+ return (hist, smodel, cmodel, env, Ok)+ go (hist, smodel, cmodel, env) (Internal act sym@(Symbolic var) : acts) = if not (precondition' smodel act) then return ( hist , smodel , cmodel , env- , counterexample ("precondition failed for: " ++ show (Untyped act)) prop+ , PreconditionFailed )- else- case reify env act of+ else do+ let Right cact = reify env act+ resp <- semantics' cact+ let hist' = hist <> History+ [ InvocationEvent (UntypedConcrete cact) (showsPrec1 10 act "") var (Pid 0)+ , ResponseEvent (fmap toDyn resp) (ppResult resp) (Pid 0)+ ]+ if not (postcondition' cmodel cact resp)+ then+ return ( hist'+ , smodel+ , cmodel+ , env+ , PostconditionFailed+ )+ else+ case resp of - -- This means that the reference that the action uses- -- failed to be created, so we do nothing.- Left _ -> return (hist, smodel, cmodel, env, prop)+ Fail err ->+ go ( hist'+ , transition' smodel act (Fail err)+ , transition' cmodel cact (Fail err)+ , env+ )+ acts - 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- )+ Success resp' ->+ go ( hist'+ , transition' smodel act (Success sym)+ , transition' cmodel cact (fmap Concrete resp)+ , insertConcrete sym (Concrete resp') env+ )+ acts
src/Test/StateMachine/Internal/Types.hs view
@@ -23,11 +23,19 @@ ( Program(..) , programLength , ParallelProgram(..)+ , parallelProgramLength+ , parallelProgramToList+ , parallelProgramFromList+ , parallelProgramAsList+ , flattenParallelProgram , Pid(..)- , Fork(..) , Internal(..) ) where +import Data.Bifunctor+ (bimap)+import Data.Monoid+ ((<>)) import Data.Typeable (Typeable) import Text.Read@@ -63,21 +71,35 @@ ------------------------------------------------------------------------ --- | A parallel program is an abstract datatype that represents three--- sequences of actions; a sequential prefix and two parallel--- suffixes. Analogous to the sequential case, the user shows how to--- generate, shrink, execute and modelcheck individual actions, and--- then the below combinators lift those things to whole parallel--- programs.-newtype ParallelProgram act = ParallelProgram- { unParallelProgram :: Fork (Program act) }+data ParallelProgram act+ = ParallelProgram (Program act) [(Program act, Program act)] +deriving instance Eq (Untyped act) => Eq (ParallelProgram act) deriving instance Show (Untyped act) => Show (ParallelProgram act) deriving instance Read (Untyped act) => Read (ParallelProgram act) --- | Forks are used to represent parallel programs.-data Fork a = Fork a a a- deriving (Eq, Functor, Show, Ord, Read)+parallelProgramLength :: ParallelProgram act -> Int+parallelProgramLength (ParallelProgram prefix suffixes) =+ programLength prefix ++ programLength (mconcat (parallelProgramToList suffixes))++parallelProgramFromList :: [Program act] -> [(Program act, Program act)]+parallelProgramFromList+ = map (\prog -> bimap Program Program+ (splitAt (programLength prog `div` 2) (unProgram prog)))++parallelProgramToList :: [(Program act, Program act)] -> [Program act]+parallelProgramToList = map (\(prog1, prog2) -> prog1 <> prog2)++parallelProgramAsList+ :: ([Program act] -> [Program act])+ -> [(Program act, Program act)]+ -> [(Program act, Program act)]+parallelProgramAsList f = parallelProgramFromList . f . parallelProgramToList++flattenParallelProgram :: ParallelProgram act -> Program act+flattenParallelProgram (ParallelProgram prefix suffixes)+ = prefix <> mconcat (parallelProgramToList suffixes) ------------------------------------------------------------------------
src/Test/StateMachine/Internal/Types/Environment.hs view
@@ -28,11 +28,12 @@ ) where import Data.Dynamic- (Dynamic, Proxy(Proxy), TypeRep, Typeable,- dynTypeRep, fromDynamic, toDyn, typeRep)+ (Dynamic, Typeable, dynTypeRep, fromDynamic, toDyn) import Data.Map (Map) import qualified Data.Map as M+import Data.Typeable+ (Proxy(Proxy), TypeRep, typeRep) import Test.StateMachine.Types
src/Test/StateMachine/Internal/Utils.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE TypeOperators #-}+ ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Internal.Utils@@ -12,17 +14,24 @@ module Test.StateMachine.Internal.Utils where +import Control.Concurrent.STM+ (atomically)+import Control.Concurrent.STM.TChan+ (TChan, tryReadTChan) import Data.List (group, sort) import Test.QuickCheck- (Property, chatty, counterexample, property,+ (Gen, Property, Testable, again, chatty,+ counterexample, ioProperty, property, shrinking, stdArgs, whenFail) import Test.QuickCheck.Counterexamples- (PropertyOf)+ ((:&:)(..), Counterexample, PropertyOf) import qualified Test.QuickCheck.Counterexamples as CE import Test.QuickCheck.Monadic- (PropertyM(MkPropertyM), monadicIO, run)+ (PropertyM(MkPropertyM), run) import Test.QuickCheck.Property+ (Property(MkProperty), unProperty)+import Test.QuickCheck.Property ((.&&.), (.||.)) ------------------------------------------------------------------------@@ -47,20 +56,6 @@ | 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.-shrinkPropertyHelperC :: Show a => PropertyOf a -> (a -> Bool) -> Property-shrinkPropertyHelperC prop p = shrinkPropertyHelperC' prop (property . p)---- | Same as above, but using a property predicate.-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)]) shrinkPair' shrinkerA shrinkerB (x, y) =@@ -71,6 +66,27 @@ shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)]) shrinkPair shrinker = shrinkPair' shrinker shrinker +-- | A variant of 'Test.QuickCheck.Monadic.forAllShrink' with an explicit show+-- function.+forAllShrinkShow+ :: Testable prop+ => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property+forAllShrinkShow gen shrinker shower pf =+ again $+ MkProperty $+ gen >>= \x ->+ unProperty $+ shrinking shrinker x $ \x' ->+ counterexample (shower x') (pf x')++forAllShrinkShowC+ :: CE.Testable prop+ => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> PropertyOf (a :&: Counterexample prop)+forAllShrinkShowC arb shr shower prop =+ CE.MkProperty $ \f ->+ forAllShrinkShow arb shr shower $ \x ->+ CE.unProperty (CE.property (prop x)) (\y -> f (x :&: y))+ ------------------------------------------------------------------------ -- | Remove duplicate elements from a list.@@ -84,3 +100,14 @@ -- | Indexing starting from the back of a list. toLast :: Int -> [a] -> a toLast n = last . dropLast n++------------------------------------------------------------------------++getChanContents :: TChan a -> IO [a]+getChanContents chan = reverse <$> atomically (go [])+ where+ go acc = do+ mx <- tryReadTChan chan+ case mx of+ Just x -> go $ x : acc+ Nothing -> return acc
src/Test/StateMachine/Internal/Utils/BoxDrawer.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE DeriveFunctor #-}+ ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Internal.Parallel@@ -15,6 +17,7 @@ module Test.StateMachine.Internal.Utils.BoxDrawer ( EventType(..)+ , Fork(..) , exec ) where @@ -22,7 +25,7 @@ (Doc, text, vsep) import Test.StateMachine.Internal.Types- (Fork(Fork), Pid(..))+ (Pid(..)) ------------------------------------------------------------------------ @@ -89,6 +92,9 @@ compilePrefix [] = [] compilePrefix (cmd:res:prefix) = Top : Start cmd : Ret res : Bottom : compilePrefix prefix compilePrefix [cmd] = error $ "compilePrefix: doesn't have response for cmd: " ++ cmd++data Fork a = Fork a a a+ deriving Functor -- | Given a history, and output from processes generate Doc with boxes exec :: [(EventType, Pid)] -> Fork [String] -> Doc
+ src/Test/StateMachine/Logic.hs view
@@ -0,0 +1,126 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE StandaloneDeriving #-}++-----------------------------------------------------------------------------+-- |+-- Module : Test.StateMachine.Logic+-- 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 provides a propositional logic which gives counterexamples when+-- the proposition is false.+--+-----------------------------------------------------------------------------++module Test.StateMachine.Logic where++infixr 1 :=>+infixr 2 :||+infixr 3 :&&++data Logic+ = Bot+ | Top+ | Logic :&& Logic+ | Logic :|| Logic+ | Logic :=> Logic+ | Not Logic+ | Predicate Predicate+ | Annotate String Logic+ deriving Show++data Predicate+ = forall a. (Eq a, Show a) => a :== a+ | forall a. (Eq a, Show a) => a :/= a+ | forall a. (Ord a, Show a) => a :< a+ | forall a. (Ord a, Show a) => a :<= a+ | forall a. (Ord a, Show a) => a :> a+ | forall a. (Ord a, Show a) => a :>= a+ | forall a. (Eq a, Show a) => Elem a [a]+ | forall a. (Eq a, Show a) => NotElem a [a]++deriving instance Show Predicate++dual :: Predicate -> Predicate+dual p = case p of+ x :== y -> x :/= y+ x :/= y -> x :== y+ x :< y -> x :>= y+ x :<= y -> x :> y+ x :> y -> x :<= y+ x :>= y -> x :< y+ x `Elem` xs -> x `NotElem` xs+ x `NotElem` xs -> x `Elem` xs++-- See Yuri Gurevich's "Intuitionistic logic with strong negation" (1977).+strongNeg :: Logic -> Logic+strongNeg l = case l of+ Bot -> Top+ Top -> Bot+ l :&& r -> strongNeg l :|| strongNeg r+ l :|| r -> strongNeg l :&& strongNeg r+ l :=> r -> l :&& strongNeg r+ Not l -> l+ Predicate p -> Predicate (dual p)+ Annotate s l -> Annotate s (strongNeg l)++data Counterexample+ = BotC+ | Fst Counterexample+ | Snd Counterexample+ | EitherC Counterexample Counterexample+ | ImpliesC Counterexample+ | NotC Counterexample+ | PredicateC Predicate+ | AnnotateC String Counterexample+ deriving Show++data Value+ = VFalse Counterexample+ | VTrue+ deriving Show++logic :: Logic -> Value+logic Bot = VFalse BotC+logic Top = VTrue+logic (l :&& r) = case logic l of+ VFalse ce -> VFalse (Fst ce)+ VTrue -> case logic r of+ VFalse ce' -> VFalse (Snd ce')+ VTrue -> VTrue+logic (l :|| r) = case logic l of+ VTrue -> VTrue+ VFalse ce -> case logic r of+ VTrue -> VTrue+ VFalse ce' -> VFalse (EitherC ce ce')+logic (l :=> r) = case logic l of+ VFalse _ -> VTrue+ VTrue -> case logic r of+ VTrue -> VTrue+ VFalse ce -> VFalse (ImpliesC ce)+logic (Not l) = case logic (strongNeg l) of+ VTrue -> VTrue+ VFalse ce -> VFalse (NotC ce)+logic (Predicate p) = predicate p+logic (Annotate s l) = case logic l of+ VTrue -> VTrue+ VFalse ce -> VFalse (AnnotateC s ce)++predicate :: Predicate -> Value+predicate p = let b = boolean p in case p of+ x :== y -> b (x == y)+ x :/= y -> b (x /= y)+ x :< y -> b (x < y)+ x :<= y -> b (x <= y)+ x :> y -> b (x > y)+ x :>= y -> b (x >= y)+ x `Elem` xs -> b (x `elem` xs)+ x `NotElem` xs -> b (x `notElem` xs)+ where+ boolean :: Predicate -> Bool -> Value+ boolean p True = VTrue+ boolean p False = VFalse (PredicateC (dual p))
src/Test/StateMachine/Types.hs view
@@ -1,7 +1,9 @@-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- |@@ -26,16 +28,24 @@ -- * Type aliases , StateMachine , stateMachine+ , okTransition+ , okPostcondition+ , okSemantics , StateMachine'(..) , Generator , Shrinker , Precondition , Transition+ , Transition' , Postcondition+ , Postcondition' , InitialModel , Result(..)+ , ppResult , Semantics+ , Semantics' , Runner+ , Reason(..) -- * Data type generic operations , module Test.StateMachine.Types.Generics@@ -49,11 +59,11 @@ where import Data.Functor.Classes- (Ord1)+ (Ord1, Show1) import Data.Typeable (Typeable) import Data.Void- (Void)+ (Void, absurd) import Test.QuickCheck (Gen, Property) @@ -77,36 +87,49 @@ -- | 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+type StateMachine model act m = StateMachine' model act m Void -- | Same as above, but with possibly failing semantics.-data StateMachine' model act err m = StateMachine+data StateMachine' model act m err = StateMachine { generator' :: Generator model act , shrinker' :: Shrinker act , precondition' :: Precondition model act- , transition' :: Transition model act- , postcondition' :: Postcondition model act+ , transition' :: Transition' model act err+ , postcondition' :: Postcondition' model act err , model' :: InitialModel model- , semantics' :: Semantics act err m+ , semantics' :: Semantics' act m err , runner' :: Runner m } -- | Helper for lifting non-failing semantics to a possibly failing -- state machine record. stateMachine- :: Functor m+ :: forall m model act+ . 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)+ -> Semantics act m -> Runner m- -> StateMachine' model act Void m+ -> StateMachine' model act m Void stateMachine gen shr precond trans post model sem run =- StateMachine gen shr precond trans post model (fmap Ok . sem) run+ StateMachine gen shr precond (okTransition trans)+ (okPostcondition post) model (okSemantics sem) run +okTransition :: Transition model act -> Transition' model act Void+okTransition transition model act (Success resp) = transition model act resp+okTransition _ _ _ (Fail false) = absurd false++okPostcondition :: Postcondition model act -> Postcondition' model act Void+okPostcondition postcondition model act (Success resp) = postcondition model act resp+okPostcondition _ _ _ (Fail false) = absurd false++okSemantics :: Functor m => Semantics act m -> Semantics' act m Void+okSemantics sem = fmap Success . sem+ -- | When generating actions we have access to a model containing -- symbolic references. type Generator model act = model Symbolic -> Gen (Untyped act)@@ -122,24 +145,40 @@ -- | The transition function must be polymorphic in the type of -- variables used, as it is used both while generating and executing.-type Transition model act = forall resp v. Ord1 v =>+type Transition model act = forall resp v. (Ord1 v, Show1 v) => model v -> act v resp -> v resp -> model v +type Transition' model act err = forall resp v. (Ord1 v, Show1 v) =>+ model v -> act v resp -> Result err (v resp) -> model v+ -- | Post-conditions are checked after the actions have been executed -- and we got a response. type Postcondition model act = forall resp.- model Concrete -> act Concrete resp -> resp -> Property+ model Concrete -> act Concrete resp -> resp -> Bool +type Postcondition' model act err = forall resp.+ model Concrete -> act Concrete resp -> Result err resp -> Bool+ -- | The initial model is polymorphic in the type of references it uses, -- so that it can be used both in the pre- and the post-condition -- check. type InitialModel m = forall (v :: * -> *). m v +-- | When we execute our actions we have access to concrete references.+type Semantics act m = forall resp. act Concrete resp -> m resp+ -- | The result of executing an action.-data Result resp err = Ok resp | Fail err+data Result err resp = Success resp | Fail err+ deriving Functor --- | 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)+ppResult :: (Show err, Show resp) => Result err resp -> String+ppResult (Success resp) = show resp+ppResult (Fail err) = show err +type Semantics' act m err = forall resp. act Concrete resp -> m (Result err resp)+ -- | How to run the monad used by the semantics. type Runner m = m Property -> IO Property++data Reason = Ok | PreconditionFailed | PostconditionFailed+ deriving (Eq, Show)
src/Test/StateMachine/Types/Generics/TH.hs view
@@ -23,42 +23,54 @@ ) where import Control.Applicative- (liftA2)+ (liftA3) import Control.Monad (filterM, (>=>)) import Data.Foldable (asum, foldl') import Data.Functor.Classes- (Show1)+ (Show1, liftShowsPrec) import Data.Maybe (maybeToList) import Language.Haskell.TH+ (Body(NormalB), Clause(Clause), Cxt,+ Dec(FunD, InstanceD), Exp(AppE, ConE, LitE, VarE),+ ExpQ, Lit(IntegerL, StringL), Match, Name,+ Pat(RecP, VarP, WildP), PatQ, Q,+ Type(AppT, ConT, SigT, VarT), appE, caseE, conE,+ conP, lamE, listE, match, mkName, nameBase, newName,+ normalB, standaloneDerivD, tupE, tupP,+ tupleDataName, varE, varP, wildP) import Language.Haskell.TH.Datatype+ (ConstructorInfo, DatatypeInfo, constructorFields,+ constructorName, datatypeCons, datatypeName,+ datatypeVars, reifyDatatype, resolveTypeSynonyms) import Test.QuickCheck (shrink) import Test.StateMachine.Internal.Utils (dropLast, nub, toLast) import Test.StateMachine.Types- (Untyped)+ (Symbolic, Untyped) import Test.StateMachine.Types.Generics import Test.StateMachine.Types.References (Reference) -- * Show of actions --- | Given a name @''Action@,--- derive 'Show' for @(Action v a)@ and @('Untyped' Action)@.--- See 'deriveShow' and 'deriveShowUntyped'.+-- | Given a name @''Action@, derive 'Show' for @(Action v a)@ and @('Untyped'+-- Action)@, and 'Show1' @(Action Symbolic)@. See 'deriveShow',+-- 'deriveShowUntyped', and 'deriveShow1'. deriveShows :: Name -> Q [Dec]-deriveShows = (liftA2 . liftA2) (++) deriveShow deriveShowUntyped+deriveShows = (liftA3 . liftA3)+ (\xs ys zs -> xs ++ ys ++ zs) deriveShow deriveShowUntyped deriveShow1 -- | -- -- @ -- 'deriveShow' ''Action -- ===>--- deriving instance 'Show1' v => 'Show' (Action v a)@.+-- deriving instance 'Show1' v => 'Show' (Action v a). -- @ deriveShow :: Name -> Q [Dec] deriveShow = reifyDatatype >=> deriveShow'@@ -71,8 +83,11 @@ instanceHead_ = AppT (ConT ''Show) (foldl' AppT (ConT (datatypeName info)) (datatypeVars info))- return [StandaloneDerivD cxt_ instanceHead_]+ standaloneDerivD' cxt_ instanceHead_ +standaloneDerivD' :: Cxt -> Type -> Q [Dec]+standaloneDerivD' cxt ty = (:[]) <$> standaloneDerivD (return cxt) (return ty)+ -- | -- @ -- 'deriveShowUntyped' ''Action@@ -91,7 +106,35 @@ (AppT (ConT ''Untyped) (foldl' AppT (ConT (datatypeName info)) (dropLast 2 (datatypeVars info))))- return [StandaloneDerivD cxt_ instanceHead_]+ standaloneDerivD' cxt_ instanceHead_++-- |+-- @ 'derivingShow1' ''Action+-- ===>+-- instance Show1 (Action Symbolic) where+-- liftShowsPrec _ _ _ act _ = show act+-- @+deriveShow1 :: Name -> Q [Dec]+deriveShow1 = (fmap . fmap) deriveShow1' reifyDatatype++deriveShow1' :: DatatypeInfo -> [Dec]+deriveShow1' info0 = pure $+ InstanceD Nothing [] (instanceHead' info0)+ [ deriveLiftShows ]+ where+ instanceHead' :: DatatypeInfo -> Type+ instanceHead' info =+ ConT ''Show1 `AppT`+ (ConT (datatypeName info) `AppT` ConT ''Symbolic)++ deriveLiftShows :: Dec+ deriveLiftShows =+ let+ act = mkName "act"+ body = VarE 'show `AppE` VarE act+ in+ FunD 'liftShowsPrec+ [Clause [WildP, WildP, WildP, VarP act, WildP] (NormalB body) []] -- | Gather types of fields with parametric types to form @Show@ constraints -- for a derived instance.
src/Test/StateMachine/Types/History.hs view
@@ -2,6 +2,8 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- |@@ -38,8 +40,8 @@ (Typeable) import Test.StateMachine.Internal.Types-import Test.StateMachine.Types import Test.StateMachine.Internal.Types.Environment+import Test.StateMachine.Types ------------------------------------------------------------------------ @@ -54,7 +56,7 @@ -- | An event is either an invocation or a response. data HistoryEvent act err = InvocationEvent act String Var Pid- | ResponseEvent (Result Dynamic err) String Pid+ | ResponseEvent (Result err Dynamic) String Pid -- | Untyped concrete actions. data UntypedConcrete (act :: (* -> *) -> * -> *) where@@ -62,12 +64,24 @@ act Concrete resp -> UntypedConcrete act -- | Pretty print a history.-ppHistory :: History act err -> String-ppHistory = foldr go "" . unHistory+ppHistory+ :: forall model act err+ . Show (model Concrete)+ => Show err+ => model Concrete -> Transition' model act err -> History act err -> String+ppHistory model0 transition+ = showsPrec 10 model0+ . go model0+ . makeOperations+ . unHistory where- go :: HistoryEvent (UntypedConcrete act) err -> String -> String- go (InvocationEvent _ str _ _) ih = " " ++ str ++ " ==> " ++ ih- go (ResponseEvent _ str _) ih = str ++ "\n" ++ ih+ go :: model Concrete -> [Operation act err] -> String+ go _ [] = "\n"+ go model (Operation act astr resp rstr _ : ops) =+ let model1 = transition model act (fmap Concrete resp) in+ "\n\n " ++ astr ++ (case resp of+ Success _ -> " --> "+ Fail _ -> " -/-> ") ++ rstr ++ "\n\n" ++ show model1 ++ go model1 ops -- | Get the process id of an event. getProcessIdEvent :: HistoryEvent act err -> Pid@@ -79,7 +93,7 @@ InvocationEvent {} -> True _ -> False -findCorrespondingResp :: Pid -> History' act err -> [(Result Dynamic err, History' act err)]+findCorrespondingResp :: Pid -> History' act err -> [(Result err Dynamic, History' act err)] findCorrespondingResp _ [] = [] findCorrespondingResp pid (ResponseEvent resp _ pid' : es) | pid == pid' = [(resp, es)] findCorrespondingResp pid (e : es) =@@ -90,21 +104,30 @@ -- | 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+ Operation (act Concrete resp) String (Result err resp) String Pid +dynResp :: forall err resp. Typeable resp => Result err Dynamic -> Result err resp+dynResp (Success resp) = Success+ (either (error . show) (\(Concrete resp') -> resp') (reifyDynamic resp))+dynResp (Fail err) = Fail err++makeOperations :: History' act err -> [Operation act err]+makeOperations [] = []+makeOperations (InvocationEvent (UntypedConcrete act) astr _ pid :+ ResponseEvent resp rstr _ : hist) =+ Operation act astr (dynResp resp) rstr pid : makeOperations hist+makeOperations _ = error "makeOperations: impossible."+ -- | Given a history, return all possible interleavings of invocations -- and corresponding response events. linearTree :: History' act err -> [Tree (Operation act err)] linearTree [] = [] linearTree es =- [ Node (Operation act str (dynResp resp) pid) (linearTree es')+ [ Node (Operation act str (dynResp resp) "<resp>" pid) (linearTree es') | InvocationEvent (UntypedConcrete act) str _ pid <- takeInvocations es , (resp, es') <- findCorrespondingResp pid $ filter1 (not . matchInv pid) es ] 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
src/Test/StateMachine/Utils.hs view
@@ -18,10 +18,9 @@ , liftProperty , whenFailM , alwaysP- , shrinkPropertyHelperC- , shrinkPropertyHelperC' , shrinkPair , shrinkPair'+ , forAllShrinkShowC ) where import Test.StateMachine.Internal.Utils
src/Test/StateMachine/Z.hs view
@@ -176,8 +176,16 @@ 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+(!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b+f ! x = maybe (error msg) Prelude.id (lookup x f)+ where+ msg = "!: failed to lookup `" ++ show x ++ "' in `" ++ show f ++ "'"++(.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b+(f, x) .% g = f .! x .= g (f ! x)++------------------------------------------------------------------------+ (.!) :: Rel a b -> a -> (Rel a b, a) f .! x = (f, x)