quickcheck-state-machine 0.4.3 → 0.5.0
raw patch · 15 files changed
+356/−157 lines, 15 filesdep +unliftiodep −lifted-asyncdep −monad-controldep −stmdep ~containers
Dependencies added: unliftio
Dependencies removed: lifted-async, monad-control, stm
Dependency ranges changed: containers
Files
- CHANGELOG.md +11/−0
- LICENSE +2/−2
- README.md +17/−5
- quickcheck-state-machine.cabal +8/−10
- src/Test/StateMachine/Parallel.hs +24/−25
- src/Test/StateMachine/Sequential.hs +98/−84
- src/Test/StateMachine/Types.hs +3/−5
- test/CircularBuffer.hs +3/−3
- test/CrudWebserverDb.hs +6/−10
- test/DieHard.hs +2/−2
- test/Echo.hs +4/−6
- test/ErrorEncountered.hs +153/−0
- test/MemoryReference.hs +17/−3
- test/Spec.hs +6/−0
- test/TicketDispenser.hs +2/−2
CHANGELOG.md view
@@ -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.*;
LICENSE view
@@ -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.
README.md view
@@ -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
quickcheck-state-machine.cabal view
@@ -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 <https://github.com/advancedtelematic/quickcheck-state-machine#readme> homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme@@ -8,7 +8,7 @@ author: Stevan Andjelkovic maintainer: Stevan Andjelkovic <stevan.andjelkovic@here.com> 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
src/Test/StateMachine/Parallel.hs view
@@ -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
src/Test/StateMachine/Sequential.hs view
@@ -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])
src/Test/StateMachine/Types.hs view
@@ -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
test/CircularBuffer.hs view
@@ -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))
test/CrudWebserverDb.hs view
@@ -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 ()))
test/DieHard.hs view
@@ -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
test/Echo.hs view
@@ -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 ]
+ test/ErrorEncountered.hs view
@@ -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
test/MemoryReference.hs view
@@ -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)))) [] ]
test/Spec.hs view
@@ -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
test/TicketDispenser.hs view
@@ -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) ]