diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 --- /dev/null +++ b/CONTRIBUTING.md @@ -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`. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal --- a/quickcheck-state-machine.cabal +++ b/quickcheck-state-machine.cabal @@ -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 -homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme -synopsis: Test monadic programs using state machine based models -description: - See README at -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 +homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme +license: BSD3 +license-file: LICENSE +author: Stevan Andjelkovic +maintainer: Stevan Andjelkovic +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 diff --git a/src/Test/StateMachine.hs b/src/Test/StateMachine.hs --- a/src/Test/StateMachine.hs +++ b/src/Test/StateMachine.hs @@ -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) -> diff --git a/src/Test/StateMachine/Internal/AlphaEquality.hs b/src/Test/StateMachine/Internal/AlphaEquality.hs deleted file mode 100644 --- a/src/Test/StateMachine/Internal/AlphaEquality.hs +++ /dev/null @@ -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 --- 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 --- . --- ------------------------------------------------------------------------------ - -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 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,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) "" 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) "" 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 diff --git a/src/Test/StateMachine/Internal/ScopeCheck.hs b/src/Test/StateMachine/Internal/ScopeCheck.hs deleted file mode 100644 --- a/src/Test/StateMachine/Internal/ScopeCheck.hs +++ /dev/null @@ -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 --- 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 --- . --- ------------------------------------------------------------------------------ - -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) 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 @@ -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) "" (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 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 @@ -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) ------------------------------------------------------------------------ diff --git a/src/Test/StateMachine/Internal/Types/Environment.hs b/src/Test/StateMachine/Internal/Types/Environment.hs --- a/src/Test/StateMachine/Internal/Types/Environment.hs +++ b/src/Test/StateMachine/Internal/Types/Environment.hs @@ -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 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 @@ -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 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 @@ -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 diff --git a/src/Test/StateMachine/Logic.hs b/src/Test/StateMachine/Logic.hs new file mode 100644 --- /dev/null +++ b/src/Test/StateMachine/Logic.hs @@ -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 +-- 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)) 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,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) diff --git a/src/Test/StateMachine/Types/Generics/TH.hs b/src/Test/StateMachine/Types/Generics/TH.hs --- a/src/Test/StateMachine/Types/Generics/TH.hs +++ b/src/Test/StateMachine/Types/Generics/TH.hs @@ -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. diff --git a/src/Test/StateMachine/Types/History.hs b/src/Test/StateMachine/Types/History.hs --- a/src/Test/StateMachine/Types/History.hs +++ b/src/Test/StateMachine/Types/History.hs @@ -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) "" 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 diff --git a/src/Test/StateMachine/Utils.hs b/src/Test/StateMachine/Utils.hs --- a/src/Test/StateMachine/Utils.hs +++ b/src/Test/StateMachine/Utils.hs @@ -18,10 +18,9 @@ , liftProperty , whenFailM , alwaysP - , shrinkPropertyHelperC - , shrinkPropertyHelperC' , shrinkPair , shrinkPair' + , forAllShrinkShowC ) where import Test.StateMachine.Internal.Utils diff --git a/src/Test/StateMachine/Z.hs b/src/Test/StateMachine/Z.hs --- a/src/Test/StateMachine/Z.hs +++ b/src/Test/StateMachine/Z.hs @@ -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)