diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,14 @@ +#### 0.5.0 (2019-1-4) + + The first and third item in the below list might break things, have a look at + the diffs of the PRs on how to fix your code (feel free to open an issue if it + isn't clear). + + * Allow the user to explicitly stop the generation of commands (PR #256); + * Fix shrinking bug (PR #255); + * Replace MonadBaseControl IO with MonadUnliftIO (PR #252); + * Check if the pre-condition holds before executing an action (PR #251). + #### 0.4.3 (2018-12-7) * Support QuickCheck-2.12.*; diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,5 +1,5 @@ -Copyright (c) 2017-2018 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley, - Xia Li-yao, Robert Danitz +Copyright (c) 2017-2019 Stevan Andjelkovic, Daniel Gustafsson, Jacob Stanley, + Xia Li-yao, Robert Danitz, Thomas Winant, Edsko de Vries All rights reserved. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -143,8 +143,8 @@ Next we have to explain how to generate and shrink actions. ```haskell -generator :: Model Symbolic -> Gen (Command Symbolic) -generator (Model model) = frequency +generator :: Model Symbolic -> Maybe (Gen (Command Symbolic)) +generator (Model model) = Just $ frequency [ (1, pure Create) , (4, Read <$> elements (domain model)) , (4, Write <$> elements (domain model) <*> arbitrary) @@ -156,6 +156,9 @@ shrinker _ = [] ``` +To stop the generation of new commands, e.g., when the model has reached a +terminal or error state, let `generator` return `Nothing`. + Finally, we show how to mock responses given a model. ```haskell @@ -427,6 +430,15 @@ e.g. `:l test/CrudWebserverDb.hs`, and run the different properties interactively. +### Real world examples + +More examples from the "real world": + + * Adjoint's implementation of the Raft consensus algorithm, contains state + machine + [tests](https://github.com/adjoint-io/raft/blob/master/test/QuickCheckStateMachine.hs) + combined with fault injection (node and network failures). + ### How to contribute The `quickcheck-state-machine` library is still very experimental. @@ -436,9 +448,9 @@ ### See also - * The QuickCheck - bugtrack [issue](https://github.com/nick8325/quickcheck/issues/139) -- where - the initial discussion about how how to add state machine based testing to + * The QuickCheck bugtrack + [issue](https://github.com/nick8325/quickcheck/issues/139) -- where the + initial discussion about how to add state machine based testing to QuickCheck started; * *Finding Race Conditions in Erlang with QuickCheck and diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal --- a/quickcheck-state-machine.cabal +++ b/quickcheck-state-machine.cabal @@ -1,5 +1,5 @@ name: quickcheck-state-machine -version: 0.4.3 +version: 0.5.0 synopsis: Test monadic programs using state machine based models description: See README at homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme @@ -8,7 +8,7 @@ author: Stevan Andjelkovic maintainer: Stevan Andjelkovic copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH; - 2018, HERE Europe B.V. + 2018-2019, HERE Europe B.V. category: Testing build-type: Simple extra-source-files: README.md @@ -50,16 +50,14 @@ base >=4.9 && <5, containers >=0.5.7.1, exceptions >=0.8.3, - lifted-async >=0.9.3, matrix >=0.3.5.0, - monad-control >=1.0.2.2, mtl >=2.2.1, pretty-show, QuickCheck >=2.9.2, split >=0.2.3.3, - stm >=2.4.4.1, tree-diff >=0.0.2, - vector >=0.12.0.1 + vector >=0.12.0.1, + unliftio >=0.2.7.0 default-language: Haskell2010 test-suite quickcheck-state-machine-test @@ -68,14 +66,13 @@ main-is: Spec.hs build-depends: base, bytestring, + containers, directory, doctest, filelock, filepath, http-client, - lifted-async >=0.9.3, matrix >=0.3.5.0, - monad-control >=1.0.2.2, monad-logger, mtl, network, @@ -91,7 +88,6 @@ servant, servant-client, servant-server, - stm, strict, string-conversions, tasty, @@ -101,12 +97,14 @@ tree-diff, vector >=0.12.0.1, wai, - warp + warp, + unliftio other-modules: CircularBuffer, CrudWebserverDb, DieHard, Echo, + ErrorEncountered, MemoryReference, TicketDispenser diff --git a/src/Test/StateMachine/Parallel.hs b/src/Test/StateMachine/Parallel.hs --- a/src/Test/StateMachine/Parallel.hs +++ b/src/Test/StateMachine/Parallel.hs @@ -34,24 +34,21 @@ import Control.Arrow ((***)) -import Control.Concurrent.Async.Lifted - (concurrently) -import Control.Concurrent.STM.TChan - (newTChanIO) import Control.Monad (foldM, replicateM) import Control.Monad.Catch (MonadCatch) import Control.Monad.State - (MonadIO, State, evalState, put, runStateT) -import Control.Monad.Trans.Control - (MonadBaseControl, liftBaseWith) + (State, evalState, put, runStateT) import Data.Bifunctor (bimap) import Data.List (partition, permutations) import Data.List.Split (splitPlacesBlanks) +import Data.Map + (Map) +import qualified Data.Map as M import Data.Monoid ((<>)) import Data.Set @@ -71,6 +68,8 @@ (Doc) import Text.Show.Pretty (ppShow) +import UnliftIO + (MonadIO, MonadUnliftIO, concurrently, newTChanIO) import Test.StateMachine.BoxDrawer import Test.StateMachine.ConstructorName @@ -85,7 +84,7 @@ forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) - => (Rank2.Foldable cmd, Rank2.Foldable resp) + => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> (ParallelCommands cmd -> prop) -- ^ Predicate. -> Property @@ -165,13 +164,13 @@ -- | Shrink a parallel program in a pre-condition and scope respecting -- way. shrinkParallelCommands - :: forall cmd model m resp. Rank2.Foldable cmd + :: forall cmd model m resp. Rank2.Traversable cmd => Rank2.Foldable resp => StateMachine model cmd m resp -> (ParallelCommands cmd -> [ParallelCommands cmd]) shrinkParallelCommands sm@StateMachine { shrinker, initModel } (ParallelCommands prefix suffixes) - = filterMaybe (flip evalState (initModel, S.empty, newCounter) . validParallelCommands sm) + = filterMaybe (flip evalState (initModel, M.empty, newCounter) . validParallelCommands sm) [ ParallelCommands prefix' (map toPair suffixes') | (prefix', suffixes') <- shrinkPair' shrinkCommands' shrinkSuffixes (prefix, map fromPair suffixes) @@ -207,9 +206,9 @@ map (id *** flip (,) ys) (pickOneReturnRest xs) ++ map (id *** (,) xs) (pickOneReturnRest ys) -validParallelCommands :: forall model cmd m resp. (Rank2.Foldable cmd, Rank2.Foldable resp) +validParallelCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd - -> State (model Symbolic, Set Var, Counter) (Maybe (ParallelCommands cmd)) + -> State (model Symbolic, Map Var Var, Counter) (Maybe (ParallelCommands cmd)) validParallelCommands sm@StateMachine { initModel } (ParallelCommands prefix suffixes) = do let prefixLength = lengthCommands prefix leftSuffixes = map (\(Pair l _r) -> l) suffixes @@ -219,7 +218,7 @@ leftSuffix = mconcat leftSuffixes rightSuffix = mconcat rightSuffixes mleft <- validCommands sm (prefix <> leftSuffix) - put (initModel, S.empty, newCounter) + put (initModel, M.empty, newCounter) mright <- validCommands sm (prefix <> rightSuffix) case (mleft, mright) of (Nothing, Nothing) -> return Nothing @@ -258,7 +257,7 @@ runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadCatch m, MonadBaseControl IO m) + => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)] @@ -266,7 +265,7 @@ runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadCatch m, MonadBaseControl IO m) + => (MonadCatch m, MonadUnliftIO m) => Int -- ^ How many times to execute the parallel program. -> StateMachine model cmd m resp -> ParallelCommands cmd @@ -277,36 +276,36 @@ return (hist, linearise sm hist) executeParallelCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadCatch m, MonadBaseControl IO m) + => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> m (History cmd resp, Reason) executeParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) = do - hchan <- liftBaseWith (const newTChanIO) + hchan <- newTChanIO - (reason0, (env0, _cmodel)) <- runStateT + (reason0, (env0, _smodel, _counter, _cmodel)) <- runStateT (executeCommands sm hchan (Pid 0) True prefix) - (emptyEnvironment, initModel) + (emptyEnvironment, initModel, newCounter, initModel) if reason0 /= Ok then do - hist <- liftBaseWith (const (getChanContents hchan)) + hist <- getChanContents hchan return (History hist, reason0) else do (reason, _) <- foldM (go hchan) (reason0, env0) suffixes - hist <- liftBaseWith (const (getChanContents hchan)) + hist <- getChanContents hchan return (History hist, reason) where go hchan (_, env) (Pair cmds1 cmds2) = do - ((reason1, (env1, _)), (reason2, (env2, _))) <- concurrently + ((reason1, (env1, _, _, _)), (reason2, (env2, _, _, _))) <- concurrently -- XXX: Post-conditions not checked, so we can pass in initModel here... -- It would be better if we made executeCommands take a Maybe model -- instead of the boolean... - (runStateT (executeCommands sm hchan (Pid 1) False cmds1) (env, initModel)) - (runStateT (executeCommands sm hchan (Pid 2) False cmds2) (env, initModel)) + (runStateT (executeCommands sm hchan (Pid 1) False cmds1) (env, initModel, newCounter, initModel)) + (runStateT (executeCommands sm hchan (Pid 2) False cmds2) (env, initModel, newCounter, initModel)) return ( reason1 `combineReason` reason2 , env1 <> env2 ) @@ -401,4 +400,4 @@ evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h) getAllUsedVars :: Rank2.Foldable cmd => Commands cmd -> Set Var -getAllUsedVars = foldMap (\(Command cmd _) -> getUsedVars cmd) . unCommands +getAllUsedVars = S.fromList . foldMap (\(Command cmd _) -> getUsedVars cmd) . unCommands diff --git a/src/Test/StateMachine/Sequential.hs b/src/Test/StateMachine/Sequential.hs --- a/src/Test/StateMachine/Sequential.hs +++ b/src/Test/StateMachine/Sequential.hs @@ -4,6 +4,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} ----------------------------------------------------------------------------- @@ -44,19 +45,13 @@ ) where -import Control.Concurrent.STM - (atomically) -import Control.Concurrent.STM.TChan - (TChan, newTChanIO, tryReadTChan, writeTChan) import Control.Exception (ErrorCall, IOException, displayException) import Control.Monad.Catch (MonadCatch, catch) import Control.Monad.State - (MonadIO, State, StateT, evalState, evalStateT, get, - lift, put, runStateT) -import Control.Monad.Trans.Control - (MonadBaseControl, liftBaseWith) + (State, StateT, evalState, evalStateT, get, lift, put, + runStateT) import Data.Dynamic (Dynamic, toDyn) import Data.Either @@ -74,8 +69,6 @@ ((<>)) import Data.Proxy (Proxy(..)) -import Data.Set - (Set) import qualified Data.Set as S import Data.TreeDiff (ToExpr, ansiWlBgEditExprCompact, ediff) @@ -93,6 +86,9 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP import Text.Show.Pretty (ppShow) +import UnliftIO + (MonadIO, TChan, newTChanIO, tryReadTChan, writeTChan, + atomically) import Test.StateMachine.ConstructorName import Test.StateMachine.Logic @@ -105,7 +101,7 @@ forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) - => (Rank2.Foldable cmd, Rank2.Foldable resp) + => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Maybe Int -- ^ Minimum number of commands. -> (Commands cmd -> prop) -- ^ Predicate. @@ -138,19 +134,22 @@ go 0 _ cmds = return (reverse cmds) go size counter cmds = do (model, mprevious) <- get - mnext <- lift $ commandFrequency (generator model) distribution mprevious - `suchThatOneOf` (boolean . precondition model) - case mnext of - Nothing -> error $ concat - [ "A deadlock occured while generating commands.\n" - , "No pre-condition holds in the following model:\n" - , ppShow model - -- XXX: show trace of commands generated so far? - ] - Just next -> do - let (resp, counter') = runGenSym (mock model next) counter - put (transition model next resp, Just next) - go (size - 1) counter' (Command next (getUsedVars resp) : cmds) + case generator model of + Nothing -> return (reverse cmds) + Just cmd -> do + mnext <- lift $ commandFrequency cmd distribution mprevious + `suchThatOneOf` (boolean . precondition model) + case mnext of + Nothing -> error $ concat + [ "A deadlock occured while generating commands.\n" + , "No pre-condition holds in the following model:\n" + , ppShow model + -- XXX: show trace of commands generated so far? + ] + Just next -> do + let (resp, counter') = runGenSym (mock model next) counter + put (transition model next resp, Just next) + go (size - 1) counter' (Command next (getUsedVars resp) : cmds) commandFrequency :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Gen (cmd Symbolic) -> Maybe (Matrix Int) -> Maybe (cmd Symbolic) @@ -193,15 +192,15 @@ = go (M.insertWith (\_ old -> old + 1) (gconName cmd1, Just (gconName cmd2)) 1 m) cmds -getUsedVars :: Rank2.Foldable f => f Symbolic -> Set Var -getUsedVars = Rank2.foldMap (\(Symbolic v) -> S.singleton v) +getUsedVars :: Rank2.Foldable f => f Symbolic -> [Var] +getUsedVars = Rank2.foldMap (\(Symbolic v) -> [v]) -- | Shrink commands in a pre-condition and scope respecting way. -shrinkCommands :: (Rank2.Foldable cmd, Rank2.Foldable resp) +shrinkCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Commands cmd -> [Commands cmd] shrinkCommands sm@StateMachine { initModel, shrinker } - = filterMaybe ( flip evalState (initModel, S.empty, newCounter) + = filterMaybe ( flip evalState (initModel, M.empty, newCounter) . validCommands sm . Commands) . shrinkList (liftShrinkCommand shrinker) @@ -218,45 +217,60 @@ Nothing -> filterMaybe f xs Just y -> y : filterMaybe f xs -validCommands :: forall model cmd m resp. (Rank2.Foldable cmd, Rank2.Foldable resp) +validCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Commands cmd - -> State (model Symbolic, Set Var, Counter) (Maybe (Commands cmd)) + -> State (model Symbolic, Map Var Var, Counter) (Maybe (Commands cmd)) validCommands StateMachine { precondition, transition, mock } = fmap (fmap Commands) . go . unCommands where - go :: [Command cmd] -> State (model Symbolic, Set Var, Counter) (Maybe [Command cmd]) - go [] = return (Just []) - go (Command cmd _vars : cmds) = do + -- As we validate we keep track of the variables that are in scope, in terms + -- of a mapping from old variables to new variables. For example, if a + -- command previously returned variables @[x',y']@, and in the new model + -- returns @[x,y]@, we extend our scope mapping with @[(x',x),(y',y)]@. + -- Later commands will then be translated accordingly, replacing references + -- to @x'@ by references to @y'@; references for which we have no updated + -- variable in scope are considered invalid: this may happen if those later + -- commands refer to a command which shrinking deleted altogether, /or/ it + -- may happen when the command was not deleted but in the new model returned + -- fewer references. + go :: [Command cmd] -> State (model Symbolic, Map Var Var, Counter) (Maybe [Command cmd]) + go [] = return (Just []) + go (Command cmd' vars' : cmds) = do (model, scope, counter) <- get - if boolean (precondition model cmd) && getUsedVars cmd `S.isSubsetOf` scope - then do - let (resp, counter') = runGenSym (mock model cmd) counter - vars = getUsedVars resp - put ( transition model cmd resp - , vars `S.union` scope - , counter') - mih <- go cmds - case mih of - Nothing -> return Nothing - Just ih -> return (Just (Command cmd vars : ih)) - else - return Nothing + case Rank2.traverse (remapVars scope) cmd' of + Just cmd | boolean (precondition model cmd) -> do + let (resp, counter') = runGenSym (mock model cmd) counter + vars = getUsedVars resp + put ( transition model cmd resp + , M.fromList (zip vars' vars) `M.union` scope + , counter') + mih <- go cmds + case mih of + Nothing -> return Nothing + Just ih -> return (Just (Command cmd vars : ih)) + _otherwise -> + return Nothing + + remapVars :: Map Var Var -> Symbolic a -> Maybe (Symbolic a) + remapVars scope (Symbolic v) = Symbolic <$> M.lookup v scope + runCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadCatch m, MonadBaseControl IO m) + => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd -> PropertyM m (History cmd resp, model Concrete, Reason) runCommands sm@StateMachine { initModel } = run . go where go cmds = do - hchan <- liftBaseWith (const newTChanIO) - (reason, (_, model)) <- runStateT (executeCommands sm hchan (Pid 0) True cmds) - (emptyEnvironment, initModel) - hist <- liftBaseWith (const (getChanContents hchan)) + hchan <- newTChanIO + (reason, (_, _, _, model)) <- runStateT + (executeCommands sm hchan (Pid 0) True cmds) + (emptyEnvironment, initModel, newCounter, initModel) + hist <- getChanContents hchan return (History hist, model, reason) -getChanContents :: TChan a -> IO [a] +getChanContents :: MonadIO m => TChan a -> m [a] getChanContents chan = reverse <$> atomically (go' []) where go' acc = do @@ -266,47 +280,47 @@ Nothing -> return acc executeCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp) - => (MonadCatch m, MonadBaseControl IO m) + => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Bool -- ^ Check invariant and post-condition? -> Commands cmd - -> StateT (Environment, model Concrete) m Reason -executeCommands StateMachine { transition, postcondition, invariant, semantics } hchan pid check = + -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason +executeCommands StateMachine {..} hchan pid check = go . unCommands where go [] = return Ok go (Command scmd vars : cmds) = do - (env, model) <- get - let ccmd = fromRight (error "executeCommands: impossible") (reify env scmd) - liftBaseWith (const (atomically (writeTChan hchan (pid, Invocation ccmd vars)))) - !ecresp <- lift (fmap Right (semantics ccmd)) - `catch` (\(err :: IOException) -> - return (Left (displayException err))) - `catch` (\(err :: ErrorCall) -> - return (Left (displayException err))) - case ecresp of - Left err -> do - liftBaseWith (const (atomically (writeTChan hchan (pid, Exception err)))) - return ExceptionThrown - Right cresp -> do - liftBaseWith (const (atomically (writeTChan hchan (pid, Response cresp)))) - if check - then case logic (postcondition model ccmd cresp) of - VFalse ce -> return (PostconditionFailed (show ce)) - VTrue -> case logic (fromMaybe (const Top) invariant model) of - VFalse ce' -> return (InvariantBroken (show ce')) - VTrue -> do - put ( insertConcretes (S.toList vars) (getUsedConcrete cresp) env - , transition model ccmd cresp - ) - go cmds - else do - put ( insertConcretes (S.toList vars) (getUsedConcrete cresp) env - , transition model ccmd cresp - ) - go cmds + (env, smodel, counter, cmodel) <- get + case (check, logic (precondition smodel scmd)) of + (True, VFalse ce) -> return (PreconditionFailed (show ce)) + _ -> do + let ccmd = fromRight (error "executeCommands: impossible") (reify env scmd) + atomically (writeTChan hchan (pid, Invocation ccmd (S.fromList vars))) + !ecresp <- lift (fmap Right (semantics ccmd)) + `catch` (\(err :: IOException) -> + return (Left (displayException err))) + `catch` (\(err :: ErrorCall) -> + return (Left (displayException err))) + case ecresp of + Left err -> do + atomically (writeTChan hchan (pid, Exception err)) + return ExceptionThrown + Right cresp -> do + atomically (writeTChan hchan (pid, Response cresp)) + let (sresp, counter') = runGenSym (mock smodel scmd) counter + case (check, logic (postcondition cmodel ccmd cresp)) of + (True, VFalse ce) -> return (PostconditionFailed (show ce)) + _ -> case (check, logic (fromMaybe (const Top) invariant cmodel)) of + (True, VFalse ce') -> return (InvariantBroken (show ce')) + _ -> do + put ( insertConcretes vars (getUsedConcrete cresp) env + , transition smodel scmd sresp + , counter' + , transition cmodel ccmd cresp + ) + go cmds getUsedConcrete :: Rank2.Foldable f => f Concrete -> [Dynamic] getUsedConcrete = Rank2.foldMap (\(Concrete x) -> [toDyn x]) 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 @@ -43,8 +43,6 @@ (Matrix) import Data.Semigroup (Semigroup) -import Data.Set - (Set) import Prelude import Test.QuickCheck (Gen) @@ -63,14 +61,14 @@ , precondition :: model Symbolic -> cmd Symbolic -> Logic , postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic , invariant :: Maybe (model Concrete -> Logic) - , generator :: model Symbolic -> Gen (cmd Symbolic) + , generator :: model Symbolic -> Maybe (Gen (cmd Symbolic)) , distribution :: Maybe (Matrix Int) , shrinker :: cmd Symbolic -> [cmd Symbolic] , semantics :: cmd Concrete -> m (resp Concrete) , mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) } -data Command cmd = Command !(cmd Symbolic) !(Set Var) +data Command cmd = Command !(cmd Symbolic) ![Var] deriving instance Show (cmd Symbolic) => Show (Command cmd) @@ -85,7 +83,7 @@ data Reason = Ok - | PreconditionFailed + | PreconditionFailed String | PostconditionFailed String | InvariantBroken String | ExceptionThrown diff --git a/test/CircularBuffer.hs b/test/CircularBuffer.hs --- a/test/CircularBuffer.hs +++ b/test/CircularBuffer.hs @@ -242,9 +242,9 @@ Positive n <- arbitrary return (New n) -generator :: Version -> Model Symbolic -> Gen (Action Symbolic) -generator _ (Model m) | null m = genNew -generator version (Model m) = frequency $ +generator :: Version -> Model Symbolic -> Maybe (Gen (Action Symbolic)) +generator _ (Model m) | null m = Just $ genNew +generator version (Model m) = Just $ frequency $ [ (1, genNew) , (4, Put <$> arbitrary <*> (fst <$> elements m)) , (4, Get <$> (fst <$> elements m)) diff --git a/test/CrudWebserverDb.hs b/test/CrudWebserverDb.hs --- a/test/CrudWebserverDb.hs +++ b/test/CrudWebserverDb.hs @@ -61,20 +61,14 @@ import Control.Concurrent (newEmptyMVar, putMVar, takeMVar, threadDelay) -import Control.Concurrent.Async.Lifted - (Async, async, cancel, waitEither) import Control.Exception (IOException, bracket) import Control.Exception (catch) -import Control.Monad.IO.Class - (liftIO) import Control.Monad.Logger (NoLoggingT, runNoLoggingT) import Control.Monad.Reader (ReaderT, ask, runReaderT) -import Control.Monad.Trans.Control - (MonadBaseControl, liftBaseWith) import Control.Monad.Trans.Resource (ResourceT) import qualified Data.ByteString.Char8 as BS @@ -133,6 +127,8 @@ () import Test.QuickCheck.Monadic (monadic) +import UnliftIO + (MonadIO, Async, liftIO, async, cancel, waitEither) import Test.StateMachine import qualified Test.StateMachine.Types.Rank2 as Rank2 @@ -311,8 +307,8 @@ ------------------------------------------------------------------------ -- * How to generate and shrink programs. -generator :: Model Symbolic -> Gen (Action Symbolic) -generator (Model m) = frequency +generator :: Model Symbolic -> Maybe (Gen (Action Symbolic)) +generator (Model m) = Just $ frequency [ (1, PostUser <$> arbitrary) , (3, GetUser <$> elements (map fst m)) , (4, IncAgeUser <$> elements (map fst m)) @@ -449,9 +445,9 @@ burl port = BaseUrl Http "localhost" port "" setup - :: MonadBaseControl IO m + :: MonadIO m => Bug -> (String -> ConnectionString) -> Warp.Port -> m (String, Async ()) -setup bug conn port = liftBaseWith $ \_ -> do +setup bug conn port = liftIO $ do (pid, dbIp) <- setupDb signal <- newEmptyMVar aServer <- async (runServer bug (conn dbIp) port (putMVar signal ())) diff --git a/test/DieHard.hs b/test/DieHard.hs --- a/test/DieHard.hs +++ b/test/DieHard.hs @@ -119,8 +119,8 @@ -- The generator of actions is simple, with equal distribution pick an -- action. -generator :: Model Symbolic -> Gen (Command Symbolic) -generator _ = oneof +generator :: Model Symbolic -> Maybe (Gen (Command Symbolic)) +generator _ = Just $ oneof [ return FillBig , return FillSmall , return EmptyBig diff --git a/test/Echo.hs b/test/Echo.hs --- a/test/Echo.hs +++ b/test/Echo.hs @@ -24,10 +24,6 @@ ) where -import Control.Concurrent.STM - (atomically) -import Control.Concurrent.STM.TVar - (TVar, newTVarIO, readTVar, writeTVar) import Data.TreeDiff (ToExpr) import GHC.Generics @@ -37,6 +33,8 @@ (Gen, Property, arbitrary, oneof, (===)) import Test.QuickCheck.Monadic (monadicIO) +import UnliftIO + (TVar, newTVarIO, readTVar, writeTVar, atomically) import Test.StateMachine import Test.StateMachine.Types @@ -124,8 +122,8 @@ mPostconditions (Buf _) Echo _ = Bot -- | Generator for symbolic actions. - mGenerator :: Model Symbolic -> Gen (Action Symbolic) - mGenerator _ = oneof + mGenerator :: Model Symbolic -> Maybe (Gen (Action Symbolic)) + mGenerator _ = Just $ oneof [ In <$> arbitrary , return Echo ] diff --git a/test/ErrorEncountered.hs b/test/ErrorEncountered.hs new file mode 100644 --- /dev/null +++ b/test/ErrorEncountered.hs @@ -0,0 +1,153 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} + +module ErrorEncountered + ( prop_error_sequential + , prop_error_parallel + ) + where + +import Data.Functor.Classes + (Eq1) +import Data.IORef + (IORef, newIORef, readIORef, + writeIORef) +import Data.TreeDiff + (ToExpr) +import GHC.Generics + (Generic, Generic1) +import Prelude hiding + (elem) +import Test.QuickCheck + (Gen, Property, arbitrary, elements, frequency, + shrink, (===)) +import Test.QuickCheck.Monadic + (monadicIO) + +import Test.StateMachine +import Test.StateMachine.Types + (Reference(..), Symbolic(..)) +import qualified Test.StateMachine.Types.Rank2 as Rank2 +import Test.StateMachine.Z + +----------------------------------------------------------------------------- + +-- Similar to MemoryReference, but with the possibilty of a 'Write' failing, +-- in which case the test should stop. +-- +-- Writing a negative value will result in the 'WriteFailed' response. This +-- will transition the model into the 'ErrorEncountered' state, resulting in +-- the termination of the test. This is achieved by letting the 'generator' +-- return 'Nothing' when the model is in the 'ErrorEncountered' state. + +----------------------------------------------------------------------------- + +data Command r + = Create + | Read (Reference (Opaque (IORef Int)) r) + | Write (Reference (Opaque (IORef Int)) r) Int + deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable) + +deriving instance Show (Command Symbolic) +deriving instance Show (Command Concrete) + +data Response r + = Created (Reference (Opaque (IORef Int)) r) + | ReadValue Int + | Written + | WriteFailed + deriving (Generic1, Rank2.Foldable) + +deriving instance Show (Response Symbolic) +deriving instance Show (Response Concrete) + +data Model r + = Model [(Reference (Opaque (IORef Int)) r, Int)] + | ErrorEncountered + deriving (Generic, Show) + +instance ToExpr (Model Symbolic) +instance ToExpr (Model Concrete) + +initModel :: Model r +initModel = Model empty + +transition :: Eq1 r => Model r -> Command r -> Response r -> Model r +transition ErrorEncountered _ _ = ErrorEncountered +transition m@(Model model) cmd resp = case (cmd, resp) of + (Create, Created ref) -> Model ((ref, 0) : model) + (Read _, ReadValue _) -> m + (Write ref x, Written) -> Model (update ref x model) + (Write _ _, WriteFailed) -> ErrorEncountered + _ -> error "transition: impossible." + +update :: Eq a => a -> b -> [(a, b)] -> [(a, b)] +update ref i m = (ref, i) : filter ((/= ref) . fst) m + +precondition :: Model Symbolic -> Command Symbolic -> Logic +precondition ErrorEncountered _ = Bot +precondition (Model m) cmd = case cmd of + Create -> Top + Read ref -> ref `elem` domain m + Write ref _ -> ref `elem` domain m + +postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic +postcondition (Model m) cmd resp = case (cmd, resp) of + (Create, Created ref) -> m' ! ref .== 0 .// "Create" + where + m' = case transition (Model m) cmd resp of + Model m1 -> m1 + ErrorEncountered -> error "postcondition ErrorEncountered" + -- A Create cannot lead to ErrorEncountered + (Read ref, ReadValue v) -> v .== m ! ref .// "Read" + (Write _ref _x, Written) -> Top + (Write _ref x, WriteFailed) + | x < 0 -> Top + _ -> Bot +postcondition ErrorEncountered _ _ = Bot + +semantics :: Command Concrete -> IO (Response Concrete) +semantics cmd = case cmd of + Create -> Created <$> (reference . Opaque <$> newIORef 0) + Read ref -> ReadValue <$> readIORef (opaque ref) + Write ref i + | i >= 0 -> Written <$ writeIORef (opaque ref) i + | otherwise -> pure $ WriteFailed + + +mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic) +mock ErrorEncountered _ = error "mock ErrorEncountered" +mock (Model m) cmd = case cmd of + Create -> Created <$> genSym + Read ref -> ReadValue <$> pure (m ! ref) + Write _ i + | i >= 0 -> pure Written + | otherwise -> pure WriteFailed + +generator :: Model Symbolic -> Maybe (Gen (Command Symbolic)) +generator (Model model) = Just $ frequency + [ (1, pure Create) + , (4, Read <$> elements (domain model)) + , (4, Write <$> elements (domain model) <*> arbitrary) + ] +generator ErrorEncountered = Nothing + +shrinker :: Command Symbolic -> [Command Symbolic] +shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ] +shrinker _ = [] + +sm :: StateMachine Model Command IO Response +sm = StateMachine initModel transition precondition postcondition + Nothing generator Nothing shrinker semantics mock + +prop_error_sequential :: Property +prop_error_sequential = forAllCommands sm Nothing $ \cmds -> monadicIO $ do + (hist, _model, res) <- runCommands sm cmds + prettyCommands sm hist (checkCommandNames cmds (res === Ok)) + +prop_error_parallel :: Property +prop_error_parallel = forAllParallelCommands sm $ \cmds -> monadicIO $ do + prettyParallelCommands cmds =<< runParallelCommands sm cmds diff --git a/test/MemoryReference.hs b/test/MemoryReference.hs --- a/test/MemoryReference.hs +++ b/test/MemoryReference.hs @@ -12,6 +12,7 @@ module MemoryReference ( prop_sequential , prop_parallel + , prop_precondition , Bug(..) ) where @@ -34,11 +35,14 @@ (randomRIO) import Test.QuickCheck (Gen, Property, arbitrary, elements, frequency, - shrink, (===)) + once, shrink, (===)) import Test.QuickCheck.Monadic (monadicIO) import Test.StateMachine +import Test.StateMachine.Types + (Commands(..), Reference(..), Symbolic(..), Var(..)) +import qualified Test.StateMachine.Types as Types import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Z @@ -138,8 +142,8 @@ Write _ _ -> pure Written Increment _ -> pure Incremented -generator :: Model Symbolic -> Gen (Command Symbolic) -generator (Model model) = frequency +generator :: Model Symbolic -> Maybe (Gen (Command Symbolic)) +generator (Model model) = Just $ frequency [ (1, pure Create) , (4, Read <$> elements (domain model)) , (4, Write <$> elements (domain model) <*> arbitrary) @@ -166,3 +170,13 @@ prettyParallelCommands cmds =<< runParallelCommands sm' cmds where sm' = sm bug + +prop_precondition :: Property +prop_precondition = once $ monadicIO $ do + (hist, _model, res) <- runCommands sm' cmds + prettyCommands sm' hist + (res === PreconditionFailed "PredicateC (NotElem (Reference (Symbolic (Var 0))) [])") + where + sm' = sm None + cmds = Commands + [ Types.Command (Read (Reference (Symbolic (Var 0)))) [] ] diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -24,6 +24,7 @@ import qualified CrudWebserverDb as WS import DieHard import Echo +import ErrorEncountered import MemoryReference import TicketDispenser @@ -39,6 +40,11 @@ , testProperty "Logic bug" (expectFailure (prop_sequential Logic)) , testProperty "Race bug sequential" (prop_sequential Race) , testProperty "Race bug parallel" (expectFailure (prop_parallel Race)) + , testProperty "Precondition failed" prop_precondition + ] + , testGroup "ErrorEncountered" + [ testProperty "sequential" prop_error_sequential + , testProperty "parallel" prop_error_parallel ] , testGroup "Crud webserver" [ webServer docker0 WS.None 8800 "No bug" WS.prop_crudWebserverDb diff --git a/test/TicketDispenser.hs b/test/TicketDispenser.hs --- a/test/TicketDispenser.hs +++ b/test/TicketDispenser.hs @@ -110,8 +110,8 @@ -- With stateful generation we ensure that the dispenser is reset before -- use. -generator :: Model Symbolic -> Gen (Action Symbolic) -generator _ = frequency +generator :: Model Symbolic -> Maybe (Gen (Action Symbolic)) +generator _ = Just $ frequency [ (1, pure Reset) , (4, pure TakeTicket) ]