quickcheck-state-machine 0.5.0 → 0.6.0
raw patch · 18 files changed
+1286/−468 lines, 18 filesdep −splitdep ~basedep ~bytestringdep ~containers
Dependencies removed: split
Dependency ranges changed: base, bytestring, containers, directory, doctest, filelock, filepath, http-client, monad-logger, mtl, network, persistent, persistent-postgresql, persistent-template, pretty-show, process, quickcheck-instances, random, resourcet, servant, servant-client, servant-server, strict, string-conversions, tasty, tasty-hunit, tasty-quickcheck, text, tree-diff, unliftio, wai, warp
Files
- CHANGELOG.md +16/−0
- README.md +3/−3
- quickcheck-state-machine.cabal +105/−113
- src/Test/StateMachine.hs +2/−0
- src/Test/StateMachine/ConstructorName.hs +53/−49
- src/Test/StateMachine/Parallel.hs +166/−118
- src/Test/StateMachine/Sequential.hs +156/−99
- src/Test/StateMachine/Types.hs +15/−12
- src/Test/StateMachine/Utils.hs +75/−5
- test/CircularBuffer.hs +11/−7
- test/CrudWebserverDb.hs +29/−19
- test/DieHard.hs +9/−6
- test/Echo.hs +10/−7
- test/ErrorEncountered.hs +18/−19
- test/MemoryReference.hs +5/−5
- test/ShrinkingProps.hs +602/−0
- test/Spec.hs +2/−0
- test/TicketDispenser.hs +9/−6
CHANGELOG.md view
@@ -1,3 +1,19 @@+#### 0.6.0 (2019-1-15)++ This is a breaking release. See mentioned PRs for how to upgrade your code,+ and feel free to open an issue if anything isn't clear.++ * Generalise shrinking so that it might depend on the model (PR #263);++ * Drop support for GHC 8.0.* or older, by requiring base >= 4.10 (PR #267). If+ you need support for older GHC versions, open a ticket;++ * Use Stack resolver lts-13 as default (PR #261);++ * Generalise the `GConName` type class to make it possible to use it for+ commands that cannot have `Generic1` instances. Also rename the type class+ to `CommandNames` (PR #259).+ #### 0.5.0 (2019-1-4) The first and third item in the below list might break things, have a look at
README.md view
@@ -151,9 +151,9 @@ , (4, Increment <$> elements (domain model)) ] -shrinker :: Command Symbolic -> [Command Symbolic]-shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]-shrinker _ = []+shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]+shrinker _ (Write ref i) = [ Write ref i' | i' <- shrink i ]+shrinker _ _ = [] ``` To stop the generation of new commands, e.g., when the model has reached a
quickcheck-state-machine.cabal view
@@ -1,126 +1,118 @@-name: quickcheck-state-machine-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-license: BSD3-license-file: LICENSE-author: Stevan Andjelkovic-maintainer: Stevan Andjelkovic <stevan.andjelkovic@here.com>-copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;- 2018-2019, HERE Europe B.V.-category: Testing-build-type: Simple-extra-source-files: README.md- , CHANGELOG.md- , CONTRIBUTING.md-cabal-version: >=1.10-tested-with: GHC == 8.2.2, GHC == 8.4.3+cabal-version: >=1.10+name: quickcheck-state-machine+version: 0.6.0+license: BSD3+license-file: LICENSE+copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;+ 2018-2019, HERE Europe B.V.+maintainer: Stevan Andjelkovic <stevan.andjelkovic@here.com>+author: Stevan Andjelkovic+tested-with: ghc ==8.2.2 ghc ==8.4.3 ghc ==8.6.3+homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme+synopsis: Test monadic programs using state machine based models+description:+ See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>+category: Testing+build-type: Simple+extra-source-files:+ README.md+ CHANGELOG.md+ CONTRIBUTING.md +source-repository head+ type: git+ location: https://github.com/advancedtelematic/quickcheck-state-machine+ library- hs-source-dirs: src- ghc-options:- -Weverything- -Wno-missing-exported-signatures- -Wno-missing-import-lists- -Wno-missed-specialisations- -Wno-all-missed-specialisations- -Wno-unsafe- -Wno-safe- -Wno-missing-local-signatures- -Wno-monomorphism-restriction- exposed-modules: Test.StateMachine- , Test.StateMachine.BoxDrawer- , Test.StateMachine.ConstructorName- , Test.StateMachine.Logic- , Test.StateMachine.Parallel- , Test.StateMachine.Sequential- , Test.StateMachine.Types- , Test.StateMachine.Types.Environment- , Test.StateMachine.Types.GenSym- , Test.StateMachine.Types.History- , Test.StateMachine.Types.Rank2- , Test.StateMachine.Types.References- , Test.StateMachine.Utils- , Test.StateMachine.Z- other-modules:- Paths_quickcheck_state_machine- build-depends:+ exposed-modules:+ Test.StateMachine+ Test.StateMachine.BoxDrawer+ Test.StateMachine.ConstructorName+ Test.StateMachine.Logic+ Test.StateMachine.Parallel+ Test.StateMachine.Sequential+ Test.StateMachine.Types+ Test.StateMachine.Types.Environment+ Test.StateMachine.Types.GenSym+ Test.StateMachine.Types.History+ Test.StateMachine.Types.Rank2+ Test.StateMachine.Types.References+ Test.StateMachine.Utils+ Test.StateMachine.Z+ hs-source-dirs: src+ other-modules:+ Paths_quickcheck_state_machine+ default-language: Haskell2010+ ghc-options: -Weverything -Wno-missing-exported-signatures+ -Wno-missing-import-lists -Wno-missed-specialisations+ -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe+ -Wno-missing-local-signatures -Wno-monomorphism-restriction+ build-depends: ansi-wl-pprint >=0.6.7.3,- base >=4.9 && <5,+ base >=4.10 && <5, containers >=0.5.7.1, exceptions >=0.8.3, matrix >=0.3.5.0, mtl >=2.2.1,- pretty-show,+ pretty-show >=1.9.5, QuickCheck >=2.9.2,- split >=0.2.3.3, tree-diff >=0.0.2, vector >=0.12.0.1, unliftio >=0.2.7.0- default-language: Haskell2010 test-suite quickcheck-state-machine-test- type: exitcode-stdio-1.0- hs-source-dirs: test- main-is: Spec.hs- build-depends: base,- bytestring,- containers,- directory,- doctest,- filelock,- filepath,- http-client,- matrix >=0.3.5.0,- monad-logger,- mtl,- network,- persistent,- persistent-postgresql,- persistent-template,- process,- QuickCheck >=2.9.2,- quickcheck-instances,- quickcheck-state-machine,- random,- resourcet,- servant,- servant-client,- servant-server,- strict,- string-conversions,- tasty,- tasty-hunit,- tasty-quickcheck,- text,- tree-diff,- vector >=0.12.0.1,- wai,- warp,- unliftio-- other-modules: CircularBuffer,- CrudWebserverDb,- DieHard,- Echo,- ErrorEncountered,- MemoryReference,- TicketDispenser-- ghc-options:- -threaded -rtsopts -with-rtsopts=-N- -Weverything- -Wno-missing-exported-signatures- -Wno-missing-import-lists- -Wno-missed-specialisations- -Wno-all-missed-specialisations- -Wno-unsafe- -Wno-safe- -Wno-missing-local-signatures- -Wno-monomorphism-restriction- default-language: Haskell2010--source-repository head- type: git- location: https://github.com/advancedtelematic/quickcheck-state-machine+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ hs-source-dirs: test+ other-modules:+ CircularBuffer+ CrudWebserverDb+ DieHard+ Echo+ ErrorEncountered+ MemoryReference+ TicketDispenser+ ShrinkingProps+ default-language: Haskell2010+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ -fno-ignore-asserts -Weverything -Wno-missing-exported-signatures+ -Wno-missing-import-lists -Wno-missed-specialisations+ -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe+ -Wno-missing-local-signatures -Wno-monomorphism-restriction+ build-depends:+ base >=4.12.0.0,+ bytestring >=0.10.8.2,+ containers >=0.6.0.1,+ directory >=1.3.3.0,+ doctest >=0.16.0.1,+ filelock >=0.1.1.2,+ filepath >=1.4.2.1,+ http-client >=0.5.14,+ matrix >=0.3.5.0,+ monad-logger >=0.3.30,+ mtl >=2.2.2,+ network >=2.8.0.0,+ persistent >=2.9.0,+ persistent-postgresql >=2.9.0,+ persistent-template >=2.5.4,+ pretty-show >=1.9.5,+ process >=1.6.3.0,+ QuickCheck >=2.9.2,+ quickcheck-instances >=0.3.19,+ quickcheck-state-machine -any,+ random >=1.1,+ resourcet >=1.2.2,+ servant >=0.15,+ servant-client >=0.15,+ servant-server >=0.15,+ strict >=0.3.2,+ string-conversions >=0.4.0.1,+ tasty >=1.2,+ tasty-hunit >=0.10.0.1,+ tasty-quickcheck >=0.10,+ text >=1.2.3.1,+ tree-diff >=0.0.2,+ vector >=0.12.0.1,+ wai >=3.2.1.2,+ warp >=3.2.25,+ unliftio >=0.2.10
src/Test/StateMachine.hs view
@@ -42,6 +42,7 @@ , Reason(..) , GenSym , genSym+ , CommandNames(..) , module Test.StateMachine.Logic @@ -49,6 +50,7 @@ import Prelude ()+import Test.StateMachine.ConstructorName import Test.StateMachine.Logic import Test.StateMachine.Parallel import Test.StateMachine.Sequential
src/Test/StateMachine/ConstructorName.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PolyKinds #-}@@ -7,15 +9,13 @@ {-# LANGUAGE UndecidableInstances #-} module Test.StateMachine.ConstructorName- ( GConName- , gconName- , gconNames- , GConName1- , gconName1- , gconNames1+ ( CommandNames(..)+ , commandName ) where +import Data.Kind+ (Type) import Data.Proxy (Proxy(Proxy)) import GHC.Generics@@ -25,64 +25,68 @@ import Prelude import Test.StateMachine.Types- (Command(..), Reference, Symbolic)+ (Command(..)) ------------------------------------------------------------------------ -class GConName a where- gconName :: a -> String- gconNames :: Proxy a -> [String]+-- | The names of all possible commands+--+-- This is used for things like tagging, coverage checking, etc.+class CommandNames (cmd :: k -> Type) where+ -- | Name of this particular command+ cmdName :: cmd r -> String -class GConName1 f where- gconName1 :: f a -> String- gconNames1 :: Proxy (f a) -> [String]+ -- | Name of all possible commands+ cmdNames :: Proxy (cmd r) -> [String] -instance GConName1 U1 where- gconName1 _ = ""- gconNames1 _ = []+ default cmdName :: (Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String+ cmdName = cmdName . from1 -instance GConName1 (K1 i c) where- gconName1 _ = ""- gconNames1 _ = []+ default cmdNames :: forall r. CommandNames (Rep1 cmd) => Proxy (cmd r) -> [String]+ cmdNames _ = cmdNames (Proxy @(Rep1 cmd r)) -instance Constructor c => GConName1 (M1 C c f) where- gconName1 = conName- gconNames1 (_ :: Proxy (M1 C c f p)) = [ conName @c undefined ] -- Can we do+instance CommandNames U1 where+ cmdName _ = ""+ cmdNames _ = []++instance CommandNames (K1 i c) where+ cmdName _ = ""+ cmdNames _ = []++instance Constructor c => CommandNames (M1 C c f) where+ cmdName = conName+ cmdNames (_ :: Proxy (M1 C c f p)) = [ conName @c undefined ] -- Can we do -- better -- here? -instance GConName1 f => GConName1 (M1 D c f) where- gconName1 = gconName1 . unM1- gconNames1 (_ :: Proxy (M1 D c f p)) = gconNames1 (Proxy :: Proxy (f p))+instance CommandNames f => CommandNames (M1 D c f) where+ cmdName = cmdName . unM1+ cmdNames (_ :: Proxy (M1 D c f p)) = cmdNames (Proxy :: Proxy (f p)) -instance GConName1 f => GConName1 (M1 S c f) where- gconName1 = gconName1 . unM1- gconNames1 (_ :: Proxy (M1 S c f p)) = gconNames1 (Proxy :: Proxy (f p))+instance CommandNames f => CommandNames (M1 S c f) where+ cmdName = cmdName . unM1+ cmdNames (_ :: Proxy (M1 S c f p)) = cmdNames (Proxy :: Proxy (f p)) -instance (GConName1 f, GConName1 g) => GConName1 (f :+: g) where- gconName1 (L1 x) = gconName1 x- gconName1 (R1 y) = gconName1 y+instance (CommandNames f, CommandNames g) => CommandNames (f :+: g) where+ cmdName (L1 x) = cmdName x+ cmdName (R1 y) = cmdName y - gconNames1 (_ :: Proxy ((f :+: g) a)) =- gconNames1 (Proxy :: Proxy (f a)) ++- gconNames1 (Proxy :: Proxy (g a))+ cmdNames (_ :: Proxy ((f :+: g) a)) =+ cmdNames (Proxy :: Proxy (f a)) +++ cmdNames (Proxy :: Proxy (g a)) -instance (GConName1 f, GConName1 g) => GConName1 (f :*: g) where- gconName1 (x :*: y) = gconName1 x ++ gconName1 y- gconNames1 (_ :: Proxy ((f :*: g) a)) =- gconNames1 (Proxy :: Proxy (f a)) ++- gconNames1 (Proxy :: Proxy (g a))+instance (CommandNames f, CommandNames g) => CommandNames (f :*: g) where+ cmdName (x :*: y) = cmdName x ++ cmdName y+ cmdNames (_ :: Proxy ((f :*: g) a)) =+ cmdNames (Proxy :: Proxy (f a)) +++ cmdNames (Proxy :: Proxy (g a)) -instance GConName1 f => GConName1 (Rec1 f) where- gconName1 = gconName1 . unRec1- gconNames1 (_ :: Proxy (Rec1 f p)) = gconNames1 (Proxy :: Proxy (f p))+instance CommandNames f => CommandNames (Rec1 f) where+ cmdName = cmdName . unRec1+ cmdNames (_ :: Proxy (Rec1 f p)) = cmdNames (Proxy :: Proxy (f p)) ------------------------------------------------------------------------ -instance GConName1 (Reference a) where- gconName1 _ = ""- gconNames1 _ = []--instance (Generic1 cmd, GConName1 (Rep1 cmd)) => GConName (Command cmd) where- gconName (Command cmd _) = gconName1 (from1 cmd)- gconNames _ = gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))+-- | Convenience wrapper for 'Command'+commandName :: CommandNames cmd => Command cmd resp -> String+commandName (Command cmd _ _) = cmdName cmd
src/Test/StateMachine/Parallel.hs view
@@ -22,14 +22,14 @@ ( forAllParallelCommands , generateParallelCommands , shrinkParallelCommands- , validParallelCommands- , prop_splitCombine+ , shrinkAndValidateParallel , runParallelCommands , runParallelCommandsNTimes , executeParallelCommands , linearise , toBoxDrawings , prettyParallelCommands+ , advanceModel ) where import Control.Arrow@@ -39,16 +39,12 @@ import Control.Monad.Catch (MonadCatch) import Control.Monad.State- (State, evalState, put, runStateT)+ (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 qualified Data.Map.Strict as Map import Data.Monoid ((<>)) import Data.Set@@ -56,12 +52,9 @@ import qualified Data.Set as S import Data.Tree (Tree(Node))-import GHC.Generics- (Generic1, Rep1) import Prelude import Test.QuickCheck- (Gen, Property, Testable, choose, property,- shrinkList, sized)+ (Gen, Property, Testable, choose, property, sized) import Test.QuickCheck.Monadic (PropertyM, run) import Text.PrettyPrint.ANSI.Leijen@@ -82,82 +75,120 @@ ------------------------------------------------------------------------ forAllParallelCommands :: Testable prop- => (Show (cmd Symbolic), Show (model Symbolic))- => (Generic1 cmd, GConName1 (Rep1 cmd))+ => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))+ => CommandNames cmd => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp- -> (ParallelCommands cmd -> prop) -- ^ Predicate.+ -> (ParallelCommands cmd resp -> prop) -- ^ Predicate. -> Property forAllParallelCommands sm = forAllShrinkShow (generateParallelCommands sm) (shrinkParallelCommands sm) ppShow +-- | Generate parallel commands.+--+-- Parallel commands are generated as follows. We begin by generating+-- sequential commands and then splitting this list in two at some index. The+-- first half will be used as the prefix.+--+-- The second half will be used to build suffixes. For example, starting from+-- the following sequential commands:+--+-- > [A, B, C, D, E, F, G, H, I]+--+-- We split it in two, giving us the prefix and the rest:+--+-- > prefix: [A, B]+-- > rest: [C, D, E, F, G, H, I]+--+-- We advance the model with the prefix.+--+-- __Make a suffix__: we take commands from @rest@ as long as these are+-- parallel safe (see 'parallelSafe'). This means that the pre-conditions+-- (using the \'advanced\' model) of each of those commands will hold no+-- matter in which order they are executed.+--+-- Say this is true for @[C, D, E]@, but not anymore for @F@, maybe because+-- @F@ depends on one of @[C, D, E]@. Then we divide this \'chunk\' in two by+-- splitting it in the middle, obtaining @[C]@ and @[D, E]@. These two halves+-- of the chunk (stored as a 'Pair') will later be executed in parallel.+-- Together they form one suffix.+--+-- Then the model is advanced using the whole chunk @[C, D, E]@. Think of it+-- as a barrier after executing the two halves of the chunk in parallel. Then+-- this process of building a chunk/suffix repeats itself, starting from+-- __Make a suffix__ using the \'advanced\' model.+--+-- In the end we might end up with something like this:+--+-- > ┌─ [C] ──┐ ┌ [F, G] ┐+-- > [A, B] ─┤ ├──┤ │+-- > └ [D, E] ┘ └ [H, I] ┘+-- generateParallelCommands :: forall model cmd m resp . (Rank2.Foldable resp, Show (model Symbolic))- => (Generic1 cmd, GConName1 (Rep1 cmd))+ => CommandNames cmd => StateMachine model cmd m resp- -> Gen (ParallelCommands cmd)+ -> Gen (ParallelCommands cmd resp) generateParallelCommands sm@StateMachine { initModel } = do Commands cmds <- generateCommands sm Nothing prefixLength <- sized (\k -> choose (0, k `div` 3)) let (prefix, rest) = bimap Commands Commands (splitAt prefixLength cmds) return (ParallelCommands prefix- (makeSuffixes (advanceModel sm initModel newCounter prefix) rest))+ (makeSuffixes (advanceModel sm initModel prefix) rest)) where- makeSuffixes :: (model Symbolic, Counter) -> Commands cmd -> [Pair (Commands cmd)]- makeSuffixes (model0, counter0) = go (model0, counter0) [] . unCommands+ makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]+ makeSuffixes model0 = go model0 [] . unCommands where- go _ acc [] = reverse acc- go (model, counter) acc cmds = go (advanceModel sm model counter (Commands safe))- (Pair (Commands safe1) (Commands safe2) : acc)- rest+ go _ acc [] = reverse acc+ go model acc cmds = go (advanceModel sm model (Commands safe))+ (Pair (Commands safe1) (Commands safe2) : acc)+ rest where- (safe, rest) = spanSafe model counter [] cmds+ (safe, rest) = spanSafe model [] cmds (safe1, safe2) = splitAt (length safe `div` 2) safe suffixLength = 5 - spanSafe :: model Symbolic -> Counter -> [Command cmd] -> [Command cmd]- -> ([Command cmd], [Command cmd])- spanSafe _ _ safe [] = (reverse safe, [])- spanSafe model counter safe (cmd@(Command _ _) : cmds)- | length safe <= suffixLength &&- parallelSafe sm model counter (Commands (cmd : safe)) =- spanSafe model counter (cmd : safe) cmds- | otherwise = (reverse safe, cmd : cmds)+ -- Split the list of commands in two such that the first half is a+ -- list of commands for which the preconditions of all commands hold+ -- for permutation of the list, i.e. it is parallel safe. The other+ -- half is the remainder of the input list.+ spanSafe :: model Symbolic -> [Command cmd resp] -> [Command cmd resp]+ -> ([Command cmd resp], [Command cmd resp])+ spanSafe _ safe [] = (reverse safe, [])+ spanSafe model safe (cmd : cmds)+ | length safe <= suffixLength+ , parallelSafe sm model (Commands (cmd : safe))+ = spanSafe model (cmd : safe) cmds+ | otherwise+ = (reverse safe, cmd : cmds) -- | A list of commands is parallel safe if the pre-conditions for all commands -- hold in all permutations of the list. parallelSafe :: StateMachine model cmd m resp -> model Symbolic- -> Counter -> Commands cmd -> Bool-parallelSafe StateMachine { precondition, transition, mock } model0 counter0+ -> Commands cmd resp -> Bool+parallelSafe StateMachine { precondition, transition } model0 = and- . map (preconditionsHold model0 counter0)+ . map (preconditionsHold model0) . permutations . unCommands where- preconditionsHold _ _ [] = True- preconditionsHold model counter (Command cmd _vars : cmds) =- let- (resp, counter') = runGenSym (mock model cmd) counter- in+ preconditionsHold _ [] = True+ preconditionsHold model (Command cmd resp _vars : cmds) = boolean (precondition model cmd) &&- preconditionsHold (transition model cmd resp) counter' cmds+ preconditionsHold (transition model cmd resp) cmds -- | Apply the transition of some commands to a model. advanceModel :: StateMachine model cmd m resp- -> model Symbolic -- ^ The model.- -> Counter- -> Commands cmd -- ^ The commands.- -> (model Symbolic, Counter)-advanceModel StateMachine { transition, mock } model0 counter0 =- go model0 counter0 . unCommands+ -> model Symbolic -- ^ The model.+ -> Commands cmd resp -- ^ The commands.+ -> model Symbolic+advanceModel StateMachine { transition } model0 =+ go model0 . unCommands where- go model counter [] = (model, counter)- go model counter (Command cmd _vars : cmds) =- let- (resp, counter') = runGenSym (mock model cmd) counter- in- go (transition model cmd resp) counter' cmds+ go model [] = model+ go model (Command cmd resp _vars : cmds) =+ go (transition model cmd resp) cmds ------------------------------------------------------------------------ @@ -167,27 +198,33 @@ :: 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 cmd resp -> [ParallelCommands cmd resp])+shrinkParallelCommands sm@StateMachine { initModel } (ParallelCommands prefix suffixes)- = filterMaybe (flip evalState (initModel, M.empty, newCounter) . validParallelCommands sm)- [ ParallelCommands prefix' (map toPair suffixes')- | (prefix', suffixes') <- shrinkPair' shrinkCommands' shrinkSuffixes- (prefix, map fromPair suffixes)+ = concatMap go+ [ Shrunk s (ParallelCommands prefix' (map toPair suffixes'))+ | Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' shrinkSuffixes+ (prefix, map fromPair suffixes) ] ++ shrinkMoveSuffixToPrefix where- shrinkCommands' :: Commands cmd -> [Commands cmd]- shrinkCommands'- = map Commands- . shrinkList (liftShrinkCommand shrinker)- . unCommands+ go :: Shrunk (ParallelCommands cmd resp) -> [ParallelCommands cmd resp]+ go (Shrunk shrunk cmds) =+ shrinkAndValidateParallel sm+ (if shrunk then DontShrink else MustShrink)+ (initValidateEnv initModel)+ cmds - shrinkSuffixes :: [(Commands cmd, Commands cmd)] -> [[(Commands cmd, Commands cmd)]]- shrinkSuffixes = shrinkList (shrinkPair shrinkCommands')+ shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)]+ shrinkCommands' = map (fmap Commands) . shrinkListS' . unCommands - shrinkMoveSuffixToPrefix :: [ParallelCommands cmd]+ shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)]+ -> [Shrunk [(Commands cmd resp, Commands cmd resp)]]+ shrinkSuffixes = shrinkListS (shrinkPairS' shrinkCommands')++ -- Moving a command from a suffix to the prefix preserves validity+ shrinkMoveSuffixToPrefix :: [ParallelCommands cmd resp] shrinkMoveSuffixToPrefix = case suffixes of [] -> [] (suffix : suffixes') ->@@ -197,61 +234,72 @@ unCommands (proj2 suffix)) ] + -- > pickOneReturnRest [] == []+ -- > pickOneReturnRest [1] == [ (1,[]) ]+ -- > pickOneReturnRest [1..3] == [ (1,[2,3]), (2,[1,3]), (3,[1,2]) ] pickOneReturnRest :: [a] -> [(a, [a])] pickOneReturnRest [] = [] pickOneReturnRest (x : xs) = (x, xs) : map (id *** (x :)) (pickOneReturnRest xs) + -- > pickOneReturnRest2 ([], []) == []+ -- > pickOneReturnRest2 ([1,2], [3,4])+ -- > == [ (1,([2],[3,4])), (2,([1],[3,4])), (3,([1,2],[4])), (4,([1,2],[3])) ] pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a],[a]))] pickOneReturnRest2 (xs, ys) = map (id *** flip (,) ys) (pickOneReturnRest xs) ++ map (id *** (,) xs) (pickOneReturnRest ys) -validParallelCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)- => StateMachine model cmd m resp -> 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- rightSuffixes = map (\(Pair _l r) -> r) suffixes- leftSuffixLengths = map lengthCommands leftSuffixes- rightSuffixLengths = map lengthCommands rightSuffixes- leftSuffix = mconcat leftSuffixes- rightSuffix = mconcat rightSuffixes- mleft <- validCommands sm (prefix <> leftSuffix)- put (initModel, M.empty, newCounter)- mright <- validCommands sm (prefix <> rightSuffix)- case (mleft, mright) of- (Nothing, Nothing) -> return Nothing- (Just _, Nothing) -> return Nothing- (Nothing, Just _) -> return Nothing- (Just left, Just right) ->- case (splitPlacesBlanks (prefixLength : leftSuffixLengths) (unCommands left),- splitPlacesBlanks (prefixLength : rightSuffixLengths) (unCommands right)) of- ([] , []) -> error "validParallelCommands: impossible"- ([] , _ : _) -> error "validParallelCommands: impossible"- (_ : _ , []) -> error "validParallelCommands: impossible"- (prefix' : leftSuffixes', _ : rightSuffixes') -> do- let suffixes' = zipWith Pair (map Commands leftSuffixes')- (map Commands rightSuffixes')- (model', counter') = advanceModel sm initModel newCounter (Commands prefix')-- if parallelSafeMany sm model' counter' suffixes'- then return (Just (ParallelCommands (Commands prefix') suffixes'))- else return Nothing--parallelSafeMany :: StateMachine model cmd m resp -> model Symbolic- -> Counter -> [Pair (Commands cmd)] -> Bool-parallelSafeMany sm = go+shrinkAndValidateParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp+ -> ShouldShrink+ -> ValidateEnv model+ -> ParallelCommands cmd resp+ -> [ParallelCommands cmd resp]+shrinkAndValidateParallel sm = \shouldShrink env (ParallelCommands prefix suffixes) ->+ let go' shouldShrink' (env', prefix') = go prefix' env' shouldShrink' suffixes in+ case shouldShrink of+ DontShrink -> concatMap (go' DontShrink) (shrinkAndValidate sm DontShrink env prefix)+ MustShrink -> concatMap (go' DontShrink) (shrinkAndValidate sm MustShrink env prefix)+ ++ concatMap (go' MustShrink) (shrinkAndValidate sm DontShrink env prefix) where- go _ _ [] = True- go model counter (Pair cmds1 cmds2 : cmdss) = parallelSafe sm model counter cmds- && go model' counter' cmdss+ withCounterFrom :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model+ e `withCounterFrom` e' = e { veCounter = veCounter e' }++ go :: Commands cmd resp -- validated prefix+ -> ValidateEnv model -- environment after the prefix+ -> ShouldShrink -- should we /still/ shrink something?+ -> [Pair (Commands cmd resp)] -- suffixes to validate+ -> [ParallelCommands cmd resp]+ go prefix' envAfterPrefix = go' [] envAfterPrefix where- cmds = cmds1 <> cmds2- (model', counter') = advanceModel sm model counter cmds+ go' :: [Pair (Commands cmd resp)] -- accumulated validated suffixes (in reverse order)+ -> ValidateEnv model -- environment after the validated suffixes+ -> ShouldShrink -- should we /still/ shrink something?+ -> [Pair (Commands cmd resp)] -- suffixes to validate+ -> [ParallelCommands cmd resp]+ go' _ _ MustShrink [] = [] -- Failed to shrink something+ go' acc _ DontShrink [] = [ParallelCommands prefix' (reverse acc)]+ go' acc env shouldShrink (Pair l r : suffixes) =+ flip concatMap shrinkOpts $ \((shrinkL, shrinkR), shrinkRest) -> concat+ [ go' (Pair l' r' : acc) (combineEnv envL envR) shrinkRest suffixes+ | (envL, l') <- shrinkAndValidate sm shrinkL env l+ , (envR, r') <- shrinkAndValidate sm shrinkR (env `withCounterFrom` envL) r+ ]+ where+ combineEnv :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model+ combineEnv envL envR = ValidateEnv {+ veModel = advanceModel sm (veModel envL) r+ , veScope = Map.union (veScope envL) (veScope envR)+ , veCounter = veCounter envR+ } -prop_splitCombine :: [[Int]] -> Bool-prop_splitCombine xs = splitPlacesBlanks (map length xs) (concat xs) == xs+ shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)]+ shrinkOpts =+ case shouldShrink of+ DontShrink -> [ ((DontShrink, DontShrink), DontShrink) ]+ MustShrink -> [ ((MustShrink, DontShrink), DontShrink)+ , ((DontShrink, MustShrink), DontShrink)+ , ((DontShrink, DontShrink), MustShrink) ] ------------------------------------------------------------------------ @@ -259,7 +307,7 @@ => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp- -> ParallelCommands cmd+ -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runParallelCommands sm = runParallelCommandsNTimes 10 sm @@ -268,7 +316,7 @@ => (MonadCatch m, MonadUnliftIO m) => Int -- ^ How many times to execute the parallel program. -> StateMachine model cmd m resp- -> ParallelCommands cmd+ -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)] runParallelCommandsNTimes n sm cmds = replicateM n $ do@@ -278,7 +326,7 @@ executeParallelCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp- -> ParallelCommands cmd+ -> ParallelCommands cmd resp -> m (History cmd resp, Reason) executeParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) = do @@ -344,7 +392,7 @@ -- counterexample if any of the runs fail. prettyParallelCommands :: (MonadIO m, Rank2.Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete))- => ParallelCommands cmd+ => ParallelCommands cmd resp -> [(History cmd resp, Logic)] -- ^ Output of 'runParallelCommands'. -> PropertyM m () prettyParallelCommands cmds =@@ -369,7 +417,7 @@ -- seeing how a race condition might have occured. toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd => (Show (cmd Concrete), Show (resp Concrete))- => ParallelCommands cmd -> History cmd resp -> Doc+ => ParallelCommands cmd resp -> History cmd resp -> Doc toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars where allVars = getAllUsedVars prefix `S.union`@@ -399,5 +447,5 @@ evT :: [(EventType, Pid)] evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h) -getAllUsedVars :: Rank2.Foldable cmd => Commands cmd -> Set Var-getAllUsedVars = S.fromList . foldMap (\(Command cmd _) -> getUsedVars cmd) . unCommands+getAllUsedVars :: Rank2.Foldable cmd => Commands cmd resp -> Set Var+getAllUsedVars = S.fromList . foldMap (\(Command cmd _ _) -> getUsedVars cmd) . unCommands
src/Test/StateMachine/Sequential.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} ----------------------------------------------------------------------------- -- |@@ -30,9 +31,10 @@ , calculateFrequency , getUsedVars , shrinkCommands- , liftShrinkCommand- , validCommands- , filterMaybe+ , shrinkAndValidate+ , ValidateEnv(..)+ , ShouldShrink(..)+ , initValidateEnv , runCommands , getChanContents , executeCommands@@ -50,8 +52,9 @@ import Control.Monad.Catch (MonadCatch, catch) import Control.Monad.State- (State, StateT, evalState, evalStateT, get, lift, put,- runStateT)+ (StateT, evalStateT, get, lift, put, runStateT)+import Data.Bifunctor+ (second) import Data.Dynamic (Dynamic, toDyn) import Data.Either@@ -73,12 +76,10 @@ import Data.TreeDiff (ToExpr, ansiWlBgEditExprCompact, ediff) import qualified Data.Vector as V-import GHC.Generics- (Generic1, Rep1, from1) import Prelude import Test.QuickCheck (Gen, Property, Testable, choose, collect, generate,- resize, shrinkList, sized, suchThat)+ resize, sized, suchThat) import Test.QuickCheck.Monadic (PropertyM, run) import Text.PrettyPrint.ANSI.Leijen@@ -87,8 +88,8 @@ import Text.Show.Pretty (ppShow) import UnliftIO- (MonadIO, TChan, newTChanIO, tryReadTChan, writeTChan,- atomically)+ (MonadIO, TChan, atomically, newTChanIO,+ tryReadTChan, writeTChan) import Test.StateMachine.ConstructorName import Test.StateMachine.Logic@@ -99,38 +100,38 @@ ------------------------------------------------------------------------ forAllCommands :: Testable prop- => (Show (cmd Symbolic), Show (model Symbolic))- => (Generic1 cmd, GConName1 (Rep1 cmd))+ => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))+ => CommandNames cmd => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Maybe Int -- ^ Minimum number of commands.- -> (Commands cmd -> prop) -- ^ Predicate.+ -> (Commands cmd resp -> prop) -- ^ Predicate. -> Property forAllCommands sm mnum = forAllShrinkShow (generateCommands sm mnum) (shrinkCommands sm) ppShow generateCommands :: (Rank2.Foldable resp, Show (model Symbolic))- => (Generic1 cmd, GConName1 (Rep1 cmd))+ => CommandNames cmd => StateMachine model cmd m resp -> Maybe Int -- ^ Minimum number of commands.- -> Gen (Commands cmd)+ -> Gen (Commands cmd resp) generateCommands sm@StateMachine { initModel } mnum = evalStateT (generateCommandsState sm newCounter mnum) (initModel, Nothing) generateCommandsState :: forall model cmd m resp. Rank2.Foldable resp => Show (model Symbolic)- => (Generic1 cmd, GConName1 (Rep1 cmd))+ => CommandNames cmd => StateMachine model cmd m resp -> Counter -> Maybe Int -- ^ Minimum number of commands.- -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd)+ -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd resp) generateCommandsState StateMachine { precondition, generator, transition , mock, distribution } counter0 mnum = do size0 <- lift (sized (\k -> choose (fromMaybe 0 mnum, k))) Commands <$> go size0 counter0 [] where- go :: Int -> Counter -> [Command cmd]- -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen [Command cmd]+ go :: Int -> Counter -> [Command cmd resp]+ -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen [Command cmd resp] go 0 _ cmds = return (reverse cmds) go size counter cmds = do (model, mprevious) <- get@@ -149,30 +150,29 @@ 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)+ go (size - 1) counter' (Command next resp (getUsedVars resp) : cmds) -commandFrequency :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))+commandFrequency :: forall cmd. CommandNames cmd => Gen (cmd Symbolic) -> Maybe (Matrix Int) -> Maybe (cmd Symbolic) -> [(Int, Gen (cmd Symbolic))] commandFrequency gen Nothing _ = [ (1, gen) ] commandFrequency gen (Just distribution) mprevious =- [ (freq, gen `suchThat` ((== con) . gconName1 . from1)) | (freq, con) <- weights ]+ [ (freq, gen `suchThat` ((== con) . cmdName)) | (freq, con) <- weights ] where idx = case mprevious of Nothing -> 1 Just previous -> let- rep = from1 previous- con = gconName1 rep+ con = cmdName previous err = "genetateCommandState: no command: " <> con in fromMaybe (error err) ((+ 2) <$>- elemIndex con (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))))+ elemIndex con (cmdNames (Proxy :: Proxy (cmd Symbolic)))) row = V.toList (getRow idx distribution)- weights = zip row (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic)))+ weights = zip row (cmdNames (Proxy :: Proxy (cmd Symbolic))) measureFrequency :: (Rank2.Foldable resp, Show (model Symbolic))- => (Generic1 cmd, GConName1 (Rep1 cmd))+ => CommandNames cmd => StateMachine model cmd m resp -> Maybe Int -- ^ Minimum number of commands. -> Int -- ^ Maximum number of commands.@@ -181,76 +181,133 @@ cmds <- generate (sequence [ resize n (generateCommands sm min0) | n <- [0, 2..size] ]) return (M.unions (map calculateFrequency cmds)) -calculateFrequency :: (Generic1 cmd, GConName1 (Rep1 cmd))- => Commands cmd -> Map (String, Maybe String) Int+calculateFrequency :: CommandNames cmd+ => Commands cmd resp -> Map (String, Maybe String) Int calculateFrequency = go M.empty . unCommands where go m [] = m go m [cmd]- = M.insertWith (\_ old -> old + 1) (gconName cmd, Nothing) 1 m+ = M.insertWith (\_ old -> old + 1) (commandName cmd, Nothing) 1 m go m (cmd1 : cmd2 : cmds)- = go (M.insertWith (\_ old -> old + 1) (gconName cmd1,- Just (gconName cmd2)) 1 m) cmds+ = go (M.insertWith (\_ old -> old + 1) (commandName cmd1,+ Just (commandName cmd2)) 1 m) cmds 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.Traversable cmd, Rank2.Foldable resp)- => StateMachine model cmd m resp -> Commands cmd- -> [Commands cmd]-shrinkCommands sm@StateMachine { initModel, shrinker }- = filterMaybe ( flip evalState (initModel, M.empty, newCounter)- . validCommands sm- . Commands)- . shrinkList (liftShrinkCommand shrinker)- . unCommands+shrinkCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp -> Commands cmd resp+ -> [Commands cmd resp]+shrinkCommands sm@StateMachine { initModel } =+ concatMap go . shrinkListS' . unCommands+ where+ go :: Shrunk [Command cmd resp] -> [Commands cmd resp]+ go (Shrunk shrunk cmds) = map snd $+ shrinkAndValidate sm+ (if shrunk then DontShrink else MustShrink)+ (initValidateEnv initModel)+ (Commands cmds) -liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic])- -> (Command cmd -> [Command cmd])-liftShrinkCommand shrinker (Command cmd resp) =- [ Command cmd' resp | cmd' <- shrinker cmd ]+-- | Environment required during 'shrinkAndValidate'+data ValidateEnv model = ValidateEnv {+ -- | The model we're starting validation from+ veModel :: model Symbolic -filterMaybe :: (a -> Maybe b) -> [a] -> [b]-filterMaybe _ [] = []-filterMaybe f (x : xs) = case f x of- Nothing -> filterMaybe f xs- Just y -> y : filterMaybe f xs+ -- | Reference renumbering+ --+ -- When a command+ --+ -- > Command .. [Var i, ..]+ --+ -- is changed during validation to+ --+ -- > Command .. [Var j, ..]+ --+ -- then any subsequent uses of @Var i@ should be replaced by @Var j@. This+ -- is recorded in 'veScope'. When we /remove/ the first command+ -- altogether (during shrinking), then @Var i@ won't appear in the+ -- 'veScope' and shrank candidates that contain commands referring to @Var+ -- i@ should be considered as invalid.+ , veScope :: Map Var Var -validCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)- => StateMachine model cmd m resp -> Commands cmd- -> State (model Symbolic, Map Var Var, Counter) (Maybe (Commands cmd))-validCommands StateMachine { precondition, transition, mock } =- fmap (fmap Commands) . go . unCommands+ -- | Counter (for generating new references)+ , veCounter :: Counter+ }++initValidateEnv :: model Symbolic -> ValidateEnv model+initValidateEnv initModel = ValidateEnv {+ veModel = initModel+ , veScope = M.empty+ , veCounter = newCounter+ }++data ShouldShrink = MustShrink | DontShrink++-- | Validate list of commands, optionally shrinking one of the commands+--+-- The input to this function is a list of commands ('Commands'), for example+--+-- > [A, B, C, D, E, F, G, H]+--+-- The /result/ is a /list/ of 'Commands', i.e. a list of lists. The+-- outermost list is used for all the shrinking possibilities. For example,+-- let's assume we haven't shrunk something yet, and therefore need to shrink+-- one of the commands. Let's further assume that only commands B and E can be+-- shrunk, to B1, B2 and E1, E2, E3 respectively. Then the result will look+-- something like+--+-- > [ -- outermost list recording all the shrink possibilities+-- > [A', B1', C', D', E' , F', G', H'] -- B shrunk to B1+-- > , [A', B1', C', D', E' , F', G', H'] -- B shrunk to B2+-- > , [A', B' , C', D', E1', F', G', H'] -- E shrunk to E1+-- > , [A', B' , C', D', E2', F', G', H'] -- E shrunk to E2+-- > , [A', B' , C', D', E3', F', G', H'] -- E shrunk to E3+-- > ]+--+-- where one of the commands has been shrunk and all commands have been+-- validated and renumbered (references updated). So, in this example, the+-- result will contain at most 5 lists; it may contain fewer, since some of+-- these lists may not be valid.+--+-- If we _did_ already shrink something, then no commands will be shrunk, and+-- the resulting list will either be empty (if the list of commands was invalid)+-- or contain a /single/ element with the validated and renumbered commands.+shrinkAndValidate :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)+ => StateMachine model cmd m resp+ -> ShouldShrink+ -> ValidateEnv model+ -> Commands cmd resp+ -> [(ValidateEnv model, Commands cmd resp)]+shrinkAndValidate StateMachine { precondition, transition, mock, shrinker } =+ \env shouldShrink cmds -> map (second Commands) $ go env shouldShrink (unCommands cmds) where- -- 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+ go :: ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])]+ go MustShrink _ [] = [] -- we failed to shrink anything+ go DontShrink env [] = [(env, [])] -- successful termination+ go shouldShrink (ValidateEnv model scope counter) (Command cmd' _resp vars' : cmds) = 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+ Just remapped ->+ -- shrink at most one command+ let candidates :: [(ShouldShrink, cmd Symbolic)]+ candidates =+ case shouldShrink of+ DontShrink -> [(DontShrink, remapped)]+ MustShrink -> map (DontShrink,) (shrinker model remapped)+ ++ [(MustShrink, remapped)]+ in flip concatMap candidates $ \(shouldShrink', cmd) ->+ if boolean (precondition model cmd)+ then let (resp, counter') = runGenSym (mock model cmd) counter+ vars = getUsedVars resp+ env' = ValidateEnv {+ veModel = transition model cmd resp+ , veScope = M.fromList (zip vars' vars) `M.union` scope+ , veCounter = counter'+ }+ in map (second (Command cmd resp vars:)) $ go shouldShrink' env' cmds+ else []+ Nothing ->+ [] remapVars :: Map Var Var -> Symbolic a -> Maybe (Symbolic a) remapVars scope (Symbolic v) = Symbolic <$> M.lookup v scope@@ -258,7 +315,7 @@ runCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp- -> Commands cmd+ -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) runCommands sm@StateMachine { initModel } = run . go where@@ -285,13 +342,13 @@ -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Bool -- ^ Check invariant and post-condition?- -> Commands cmd+ -> Commands cmd resp -> 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+ go [] = return Ok+ go (Command scmd _ vars : cmds) = do (env, smodel, counter, cmodel) <- get case (check, logic (precondition smodel scmd)) of (True, VFalse ce) -> return (PreconditionFailed (show ce))@@ -386,35 +443,35 @@ -- | Print distribution of commands and fail if some commands have not -- been executed.-checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))- => Commands cmd -> Property -> Property+checkCommandNames :: forall cmd resp. CommandNames cmd+ => Commands cmd resp -> Property -> Property checkCommandNames cmds = collect names . oldCover (length names == numOfConstructors) 1 "coverage" where names = commandNames cmds- numOfConstructors = length (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic)))+ numOfConstructors = length (cmdNames (Proxy :: Proxy (cmd Symbolic))) -commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))- => Commands cmd -> [(String, Int)]+commandNames :: forall cmd resp. CommandNames cmd+ => Commands cmd resp -> [(String, Int)] commandNames = M.toList . foldl go M.empty . unCommands where- go :: Map String Int -> Command cmd -> Map String Int- go ih cmd = M.insertWith (+) (gconName cmd) 1 ih+ go :: Map String Int -> Command cmd resp -> Map String Int+ go ih cmd = M.insertWith (+) (commandName cmd) 1 ih -commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))- => Commands cmd -> [String]+commandNamesInOrder :: forall cmd resp. CommandNames cmd+ => Commands cmd resp -> [String] commandNamesInOrder = reverse . foldl go [] . unCommands where- go :: [String] -> Command cmd -> [String]- go ih cmd = gconName cmd : ih+ go :: [String] -> Command cmd resp -> [String]+ go ih cmd = commandName cmd : ih -transitionMatrix :: forall cmd. GConName1 (Rep1 cmd)+transitionMatrix :: forall cmd. CommandNames cmd => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int transitionMatrix _ f =- let cons = gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))+ let cons = cmdNames (Proxy :: Proxy (cmd Symbolic)) n = length cons m = succ n in matrix m n $ \case
src/Test/StateMachine/Types.hs view
@@ -63,22 +63,25 @@ , invariant :: Maybe (model Concrete -> Logic) , generator :: model Symbolic -> Maybe (Gen (cmd Symbolic)) , distribution :: Maybe (Matrix Int)- , shrinker :: cmd Symbolic -> [cmd Symbolic]+ , shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic] , semantics :: cmd Concrete -> m (resp Concrete) , mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) } -data Command cmd = Command !(cmd Symbolic) ![Var]+-- | Previously symbolically executed command+--+-- Invariant: the variables must be the variables in the response.+data Command cmd resp = Command !(cmd Symbolic) !(resp Symbolic) ![Var] -deriving instance Show (cmd Symbolic) => Show (Command cmd)+deriving instance (Show (cmd Symbolic), Show (resp Symbolic)) => Show (Command cmd resp) -newtype Commands cmd = Commands- { unCommands :: [Command cmd] }+newtype Commands cmd resp = Commands+ { unCommands :: [Command cmd resp] } deriving (Semigroup, Monoid) -deriving instance Show (cmd Symbolic) => Show (Commands cmd)+deriving instance (Show (cmd Symbolic), Show (resp Symbolic)) => Show (Commands cmd resp) -lengthCommands :: Commands cmd -> Int+lengthCommands :: Commands cmd resp -> Int lengthCommands = length . unCommands data Reason@@ -89,13 +92,13 @@ | ExceptionThrown deriving (Eq, Show) -data ParallelCommandsF t cmd = ParallelCommands- { prefix :: !(Commands cmd)- , suffixes :: [t (Commands cmd)]+data ParallelCommandsF t cmd resp = ParallelCommands+ { prefix :: !(Commands cmd resp)+ , suffixes :: [t (Commands cmd resp)] } -deriving instance (Show (cmd Symbolic), Show (t (Commands cmd))) =>- Show (ParallelCommandsF t cmd)+deriving instance (Show (cmd Symbolic), Show (resp Symbolic), Show (t (Commands cmd resp))) =>+ Show (ParallelCommandsF t cmd resp) data Pair a = Pair { proj1 :: !a
src/Test/StateMachine/Utils.hs view
@@ -1,6 +1,8 @@ {-# OPTIONS_GHC -Wno-orphans #-} -{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- |@@ -26,19 +28,27 @@ , shrinkPair' , suchThatOneOf , oldCover+ , Shrunk(..)+ , shrinkS+ , shrinkListS+ , shrinkListS'+ , shrinkPairS+ , shrinkPairS' ) where import Prelude+ import Test.QuickCheck- (Gen, Property, Testable, again, counterexample,- frequency, resize, shrinking, sized, suchThatMaybe,+ (Arbitrary, Gen, Property, Testable, again,+ counterexample, frequency, resize, shrink,+ shrinkList, shrinking, sized, suchThatMaybe, whenFail) import Test.QuickCheck.Monadic (PropertyM(MkPropertyM)) import Test.QuickCheck.Property- (Property(MkProperty), property, unProperty, (.&&.),- (.||.), cover)+ (Property(MkProperty), cover, property, unProperty,+ (.&&.), (.||.)) #if !MIN_VERSION_QuickCheck(2,10,0) import Test.QuickCheck.Property (succeeded)@@ -121,3 +131,63 @@ #else cover (fromIntegral n) x s p #endif++-----------------------------------------------------------------------------++-- | More permissive notion of shrinking where a value can shrink to itself+--+-- For example+--+-- > shrink 3 == [0, 2] -- standard QuickCheck shrink+-- > shrinkS 3 == [Shrunk True 0, Shrunk True 2, Shrunk False 3]+--+-- This is primarily useful when shrinking composite structures: the combinators+-- here keep track of whether something was shrunk /somewhere/ in the structure.+-- For example, we have+--+-- > shrinkListS (shrinkPairS shrinkS shrinkS) [(1,3),(2,4)]+-- > == [ Shrunk True [] -- removed all elements of the list+-- > , Shrunk True [(2,4)] -- removed the first+-- > , Shrunk True [(1,3)] -- removed the second+-- > , Shrunk True [(0,3),(2,4)] -- shrinking the '1'+-- > , Shrunk True [(1,0),(2,4)] -- shrinking the '3'+-- > , Shrunk True [(1,2),(2,4)] -- ..+-- > , Shrunk True [(1,3),(0,4)] -- shrinking the '2'+-- > , Shrunk True [(1,3),(1,4)] -- ..+-- > , Shrunk True [(1,3),(2,0)] -- shrinking the '4'+-- > , Shrunk True [(1,3),(2,2)] -- ..+-- > , Shrunk True [(1,3),(2,3)] -- ..+-- > , Shrunk False [(1,3),(2,4)] -- the original unchanged list+-- > ]+data Shrunk a = Shrunk { wasShrunk :: Bool, shrunk :: a }+ deriving (Show, Functor)++shrinkS :: Arbitrary a => a -> [Shrunk a]+shrinkS a = map (Shrunk True) (shrink a) ++ [Shrunk False a]++shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]+shrinkListS f = \xs -> concat [+ map (Shrunk True) (shrinkList (const []) xs)+ , shrinkOne xs+ , [Shrunk False xs]+ ]+ where+ shrinkOne :: [a] -> [Shrunk [a]]+ shrinkOne [] = []+ shrinkOne (x:xs) = [Shrunk True (x' : xs) | Shrunk True x' <- f x]+ ++ [Shrunk True (x : xs') | Shrunk True xs' <- shrinkOne xs]++-- | Shrink list without shrinking elements+shrinkListS' :: [a] -> [Shrunk [a]]+shrinkListS' = shrinkListS (\a -> [Shrunk False a])++shrinkPairS :: (a -> [Shrunk a])+ -> (b -> [Shrunk b])+ -> (a, b) -> [Shrunk (a, b)]+shrinkPairS f g (a, b) =+ [Shrunk True (a', b) | Shrunk True a' <- f a ]+ ++ [Shrunk True (a, b') | Shrunk True b' <- g b ]+ ++ [Shrunk False (a, b)]++shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]+shrinkPairS' f = shrinkPairS f f
test/CircularBuffer.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-}@@ -44,6 +45,9 @@ import Data.Functor.Classes (Eq1) import Data.IORef+ (IORef, newIORef, readIORef, writeIORef)+import Data.Kind+ (Type) import Data.Maybe (isJust) import Data.TreeDiff@@ -138,7 +142,7 @@ ------------------------------------------------------------------------ -- | Buffer actions.-data Action (r :: * -> *)+data Action (r :: Type -> Type) -- | Create a new buffer of bounded capacity. = New Int @@ -150,9 +154,9 @@ -- | Get the number of elements in the buffer. | Len (Reference (Opaque Buffer) r)- deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)+ deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames) -data Response (r :: * -> *)+data Response (r :: Type -> Type) = NewR (Reference (Opaque Buffer) r) | PutR | GetR Int@@ -251,10 +255,10 @@ ] ++ [ (4, Len <$> (fst <$> elements m)) | version == YesLen ] -shrinker :: Action Symbolic -> [Action Symbolic]-shrinker (New n) = [ New n' | n' <- shrink n ]-shrinker (Put x buffer) = [ Put x' buffer | x' <- shrink x ]-shrinker _ = []+shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]+shrinker _ (New n) = [ New n' | n' <- shrink n ]+shrinker _ (Put x buffer) = [ Put x' buffer | x' <- shrink x ]+shrinker _ _ = [] ------------------------------------------------------------------------
test/CrudWebserverDb.hs view
@@ -71,11 +71,13 @@ (ReaderT, ask, runReaderT) import Control.Monad.Trans.Resource (ResourceT)-import qualified Data.ByteString.Char8 as BS+import qualified Data.ByteString.Char8 as BS import Data.Char (isPrint) import Data.Functor.Classes (Eq1)+import Data.Kind+ (Type) import Data.List (dropWhileEnd) import Data.Monoid@@ -86,7 +88,7 @@ (cs) import Data.Text (Text)-import qualified Data.Text as T+import qualified Data.Text as T import Data.TreeDiff (Expr(App), ToExpr, toExpr) import Database.Persist.Postgresql@@ -99,12 +101,15 @@ sqlSettings) import GHC.Generics (Generic, Generic1)-import Network- (PortID(PortNumber), connectTo) import Network.HTTP.Client (Manager, defaultManagerSettings, newManager)-import qualified Network.Wai.Handler.Warp as Warp-import Prelude hiding+import Network.Socket+ (AddrInfoFlag(AI_NUMERICSERV, AI_NUMERICHOST),+ Socket, SocketType(Stream), addrAddress, addrFamily,+ addrFlags, addrProtocol, addrSocketType, close,+ connect, defaultHints, getAddrInfo, socket)+import qualified Network.Wai.Handler.Warp as Warp+import Prelude hiding (elem) import qualified Prelude import Servant@@ -115,8 +120,6 @@ client, mkClientEnv, runClientM) import Servant.Server (Handler)-import System.IO- (Handle, hClose) import System.Process (callProcess, readProcess) import Test.QuickCheck@@ -128,10 +131,10 @@ import Test.QuickCheck.Monadic (monadic) import UnliftIO- (MonadIO, Async, liftIO, async, cancel, waitEither)+ (Async, MonadIO, async, cancel, liftIO, waitEither) import Test.StateMachine-import qualified Test.StateMachine.Types.Rank2 as Rank2+import qualified Test.StateMachine.Types.Rank2 as Rank2 ------------------------------------------------------------------------ -- * User datatype@@ -233,7 +236,7 @@ -data Action (r :: * -> *)+data Action (r :: Type -> Type) = PostUser User | GetUser (Reference (Key User) r) | IncAgeUser (Reference (Key User) r)@@ -243,8 +246,9 @@ instance Rank2.Functor Action where instance Rank2.Foldable Action where instance Rank2.Traversable Action where+instance CommandNames Action where -data Response (r :: * -> *)+data Response (r :: Type -> Type) = PostedUser (Reference (Key User) r) | GotUser (Maybe User) | IncedAgeUser@@ -315,10 +319,10 @@ , (2, DeleteUser <$> elements (map fst m)) ] -shrinker :: Action Symbolic -> [Action Symbolic]-shrinker (PostUser (User user age)) =+shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]+shrinker _ (PostUser (User user age)) = [ PostUser (User user' age') | (user', age') <- shrink (user, age) ]-shrinker _ = []+shrinker _ _ = [] ------------------------------------------------------------------------ -- * The semantics.@@ -494,13 +498,19 @@ healthyDb :: String -> IO () healthyDb ip = do- handle <- go 10- hClose handle+ sock <- go 10+ close sock where- go :: Int -> IO Handle+ go :: Int -> IO Socket go 0 = error "healtyDb: db isn't healthy" go n = do- connectTo ip (PortNumber 5432)+ let hints = defaultHints+ { addrFlags = [AI_NUMERICHOST , AI_NUMERICSERV]+ , addrSocketType = Stream+ }+ addr : _ <- getAddrInfo (Just hints) (Just ip) (Just "5432")+ sock <- socket (addrFamily addr) (addrSocketType addr) (addrProtocol addr)+ (connect sock (addrAddress addr) >> return sock) `catch` (\(_ :: IOException) -> do threadDelay 1000000 go (n - 1))
test/DieHard.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-}@@ -30,6 +31,8 @@ , prop_dieHard ) where +import Data.Kind+ (Type) import Data.TreeDiff (ToExpr) import GHC.Generics@@ -50,7 +53,7 @@ -- We start of defining the different actions that are allowed: -data Command (r :: * -> *)+data Command (r :: Type -> Type) = FillBig -- Fill the 5-liter jug. | FillSmall -- Fill the 3-liter jug. | EmptyBig -- Empty the 5-liter jug.@@ -58,9 +61,9 @@ | SmallIntoBig -- Pour the contents of the 3-liter jug -- into 5-liter jug. | BigIntoSmall- deriving (Eq, Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)+ deriving (Eq, Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames) -data Response (r :: * -> *) = Done+data Response (r :: Type -> Type) = Done deriving (Show, Generic1, Rank2.Foldable) ------------------------------------------------------------------------@@ -68,7 +71,7 @@ -- The model (or state) keeps track of what amount of water is in the -- two jugs. -data Model (r :: * -> *) = Model+data Model (r :: Type -> Type) = Model { bigJug :: Int , smallJug :: Int } deriving (Show, Eq, Generic)@@ -131,8 +134,8 @@ -- There's nothing to shrink. -shrinker :: Command r -> [Command r]-shrinker _ = []+shrinker :: Model r -> Command r -> [Command r]+shrinker _ _ = [] ------------------------------------------------------------------------
test/Echo.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-}@@ -24,6 +25,8 @@ ) where +import Data.Kind+ (Type) import Data.TreeDiff (ToExpr) import GHC.Generics@@ -34,7 +37,7 @@ import Test.QuickCheck.Monadic (monadicIO) import UnliftIO- (TVar, newTVarIO, readTVar, writeTVar, atomically)+ (TVar, atomically, newTVarIO, readTVar, writeTVar) import Test.StateMachine import Test.StateMachine.Types@@ -129,8 +132,8 @@ ] -- | Trivial shrinker.- mShrinker :: Action Symbolic -> [Action Symbolic]- mShrinker _ = []+ mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]+ mShrinker _ _ = [] -- | Here we'd do the dispatch to the actual SUT. mSemantics :: Action Concrete -> IO (Response Concrete)@@ -152,7 +155,7 @@ -- | The model contains the last string that was communicated in an input -- action.-data Model (r :: * -> *)+data Model (r :: Type -> Type) = -- | The model hasn't been initialized. Empty | -- | Last input string (a buffer with size one).@@ -160,16 +163,16 @@ deriving (Eq, Show, Generic) -- | Actions supported by the system.-data Action (r :: * -> *)+data Action (r :: Type -> Type) = -- | Input a string, which should be echoed later. In String -- | Request a string output. | Echo- deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor)+ deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor, CommandNames) -- | The system gives a single type of output response, containing a string -- with the input previously received.-data Response (r :: * -> *)+data Response (r :: Type -> Type) = -- | Input acknowledgment. InAck -- | The previous action wasn't an input, so there is no input to echo.
test/ErrorEncountered.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneDeriving #-} module ErrorEncountered ( prop_error_sequential@@ -13,8 +13,7 @@ import Data.Functor.Classes (Eq1) import Data.IORef- (IORef, newIORef, readIORef,- writeIORef)+ (IORef, newIORef, readIORef, writeIORef) import Data.TreeDiff (ToExpr) import GHC.Generics@@ -49,7 +48,7 @@ = Create | Read (Reference (Opaque (IORef Int)) r) | Write (Reference (Opaque (IORef Int)) r) Int- deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)+ deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames) deriving instance Show (Command Symbolic) deriving instance Show (Command Concrete)@@ -78,11 +77,11 @@ 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."+ (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@@ -90,9 +89,9 @@ 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+ 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@@ -135,9 +134,9 @@ ] generator ErrorEncountered = Nothing -shrinker :: Command Symbolic -> [Command Symbolic]-shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]-shrinker _ = []+shrinker :: Model Symbolic -> 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
test/MemoryReference.hs view
@@ -53,7 +53,7 @@ | Read (Reference (Opaque (IORef Int)) r) | Write (Reference (Opaque (IORef Int)) r) Int | Increment (Reference (Opaque (IORef Int)) r)- deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)+ deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames) deriving instance Show (Command Symbolic) deriving instance Show (Command Concrete)@@ -150,9 +150,9 @@ , (4, Increment <$> elements (domain model)) ] -shrinker :: Command Symbolic -> [Command Symbolic]-shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]-shrinker _ = []+shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]+shrinker _ (Write ref i) = [ Write ref i' | i' <- shrink i ]+shrinker _ _ = [] sm :: Bug -> StateMachine Model Command IO Response sm bug = StateMachine initModel transition precondition postcondition@@ -179,4 +179,4 @@ where sm' = sm None cmds = Commands- [ Types.Command (Read (Reference (Symbolic (Var 0)))) [] ]+ [ Types.Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) [] ]
+ test/ShrinkingProps.hs view
@@ -0,0 +1,602 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module ShrinkingProps (+ tests+ -- Just to avoid compiler warnings+ , ShrinkSeqFailure(..)+ , ShrinkParFailure(..)+ ) where++import Prelude hiding+ (elem)++import Control.Monad+ (replicateM)+import Control.Monad.Except+ (Except, runExcept, throwError)+import Control.Monad.State+ (State, gets, modify, runState, state)+import Data.Bifunctor+ (first)+import Data.Foldable+ (toList)+import Data.Functor.Classes+ (Eq1, Show1)+import Data.Map.Strict+ (Map)+import qualified Data.Map.Strict as Map+import Data.Monoid+ ((<>))+import Data.Proxy+import Data.Set+ (Set)+import qualified Data.Set as Set+import Data.TreeDiff+ (ToExpr(..), defaultExprViaShow)+import Data.Typeable+ (Typeable)+import GHC.Generics+ (Generic, Generic1)+import GHC.Stack+import Text.Show.Pretty+ (ppShow)+import UnliftIO.STM++import Test.QuickCheck.Monadic+ (monadicIO)+import Test.Tasty+import Test.Tasty.QuickCheck+ (Arbitrary(..), Gen, Property, conjoin,+ counterexample, elements, getNonNegative, getSmall,+ oneof, property, testProperty, (===))++import Test.StateMachine+import qualified Test.StateMachine.Parallel as QSM+import qualified Test.StateMachine.Sequential as QSM+import qualified Test.StateMachine.Types as QSM+import qualified Test.StateMachine.Types.Rank2 as Rank2+import Test.StateMachine.Utils+ (forAllShrinkShow)++tests :: TestTree+tests = testGroup "Shrinking properties" [+ testProperty "Sanity check: standard sequential test" prop_sequential+ , testProperty "Sanity check: standard parallel test" prop_parallel+ , testProperty "Correct references after sequential shrinking" prop_sequential_subprog+ , testProperty "Correct references after parallel shrinking" prop_parallel_subprog+ , testProperty "Correct references after parallel shrinking (buggyShrinkCmds)" (prop_parallel_subprog' buggyShrinkCmds)+ , testProperty "Sequential shrinker provides correct model" prop_sequential_model+ , testProperty "Parallel shrinker provides correct model" prop_parallel_model+ ]++{-------------------------------------------------------------------------------+ Example set up++ This language is contrived, but designed to have lots of references, including+ commands that /use/ a variable number of references and commands that /create/+ a variable number of references.+-------------------------------------------------------------------------------}++-- | Unique command identifier+--+-- This is used when testing whether shrinking messes up references (see below)+newtype CmdID = CmdID Int+ deriving (Show, Eq, Ord, Generic)++-- | Commands+--+-- Commands have two somewhat unusual features that are just here for the+-- specific purpose of testing shrinking:+--+-- * The 'CmdID' fields are there so that we can build the reference graph+-- (see 'RefGraph') below to check that shrinking does not mess up references.+-- * The 'Maybe Model' field is there to check that the shrinker gets presented+-- with the right model.+data Cmd var =+ -- | Create @n@ new mutable variables+ CreateRef CmdID (Maybe (Model Symbolic)) Int++ -- | Increment the value of the specified variables+ | Incr CmdID (Maybe (Model Symbolic)) [var]++ -- | Get the value of the specified variables+ | Read CmdID (Maybe (Model Symbolic)) [var]+ deriving (Show, Eq, Functor, Foldable, Traversable, Generic1, CommandNames)++data Resp var =+ Refs [var]+ | Unit ()+ | Vals [Int]+ deriving (Show, Eq, Functor, Foldable, Traversable)++cmdID :: Cmd var -> CmdID+cmdID (CreateRef cid _ _) = cid+cmdID (Incr cid _ _) = cid+cmdID (Read cid _ _) = cid++cmdModel :: Cmd var -> Maybe (Model Symbolic)+cmdModel (CreateRef _ m _) = m+cmdModel (Incr _ m _) = m+cmdModel (Read _ m _) = m++{-------------------------------------------------------------------------------+ Mock implementation+-------------------------------------------------------------------------------}++-- | Mock variable+newtype MockVar = MockVar Int+ deriving (Show, Eq, Ord, Generic)++-- | Mock system state+newtype MockState = MockState (Map MockVar Int)+ deriving (Show, Eq, Ord, Generic)++newVar :: State MockState MockVar+newVar = state $ \(MockState m) ->+ let x = MockVar (Map.size m)+ in (x, MockState (Map.insert x 0 m))++incrVar :: MockVar -> State MockState ()+incrVar x = modify $ \(MockState m) ->+ let incr Nothing = error "incrVar: undefined variable"+ incr (Just v) = Just (v + 1)+ in MockState $ Map.alter incr x m++readVar :: MockVar -> State MockState Int+readVar x = gets $ \(MockState m) ->+ case Map.lookup x m of+ Just n -> n+ Nothing -> error $ "readVar: variable " ++ show x ++ " not found"++runMock :: Cmd MockVar -> MockState -> (Resp MockVar, MockState)+runMock (CreateRef _ _ n) = first Refs . runState (replicateM n newVar)+runMock (Incr _ _ xs) = first Unit . runState (mapM_ incrVar xs)+runMock (Read _ _ xs) = first Vals . runState (mapM readVar xs)++{-------------------------------------------------------------------------------+ I/O implementation++ We use STM variables here so guarantee atomicity of 'Incr' command+ (we are testing the shrinker, not looking for atomicity bugs! :)+-------------------------------------------------------------------------------}++data IOVar = IOVar String (TVar Int)+ deriving (Eq)++instance Show IOVar where+ show (IOVar l _) = "<" ++ l ++ ">"++newIOVar :: CmdID -> Int -> STM IOVar+newIOVar cid n = IOVar (show (cid, n)) <$> newTVar 0++incrIOVar :: IOVar -> STM ()+incrIOVar (IOVar _ x) = modifyTVar x (+1)++readIOVar :: IOVar -> STM Int+readIOVar (IOVar _ x) = readTVar x++runIO :: Cmd IOVar -> IO (Resp IOVar)+runIO (CreateRef cid _ n) = atomically $ Refs <$> mapM (newIOVar cid) [0 .. n - 1]+runIO (Incr _ _ xs) = atomically $ Unit <$> mapM_ incrIOVar xs+runIO (Read _ _ xs) = atomically $ Vals <$> mapM readIOVar xs++{-------------------------------------------------------------------------------+ Instantiate to references+-------------------------------------------------------------------------------}++newtype At f r = At (f (Reference IOVar r))+ deriving (Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)++type (:@) f r = At f r++{-------------------------------------------------------------------------------+ Model+-------------------------------------------------------------------------------}++type KnownRefs r = [(Reference IOVar r, MockVar)]++resolveRef :: (Eq1 r, Show1 r, HasCallStack)+ => KnownRefs r -> Reference IOVar r -> MockVar+resolveRef refs r =+ case lookup r refs of+ Just x -> x+ Nothing -> error $ "resolveRef: reference " ++ show r+ ++ "not found in environment " ++ show refs++-- | Model relating the mock state with the IO state+--+-- We include the CmdID so that we can reference it in the generator+data Model r = Model MockState (KnownRefs r) CmdID+ deriving (Generic, Eq)++initModel :: Model r+initModel = Model (MockState Map.empty) [] (CmdID 0)++toMock :: (Eq1 r, Show1 r, Functor f, HasCallStack)+ => Model r -> f :@ r -> f MockVar+toMock (Model _ knownRefs _) (At fr) = fmap (resolveRef knownRefs) fr++step :: (Eq1 r, Show1 r, HasCallStack) => Model r -> Cmd :@ r -> (Resp MockVar, MockState)+step model@(Model mockState _ _) cmd =+ let cs = callStack+ in let ?callStack = pushCallStack ("<stepping " ++ show cmd ++ ">", here) cs+ in runMock (toMock model cmd) mockState+ where+ here = SrcLoc "quickcheck-state-machine" "ShrinkingProps" "ShrinkingProps.hs" 0 0 0 0++{-------------------------------------------------------------------------------+ Events+-------------------------------------------------------------------------------}++data Event r = Event {+ eventBefore :: Model r+ , eventCmd :: Cmd :@ r+ , eventAfter :: Model r+ , eventMockResp :: Resp MockVar+ }++event :: forall r. (Eq1 r, Show1 r, HasCallStack)+ => Model r+ -> Cmd :@ r+ -> (Resp MockVar -> KnownRefs r)+ -> Event r+event model@(Model _ knownRefs (CmdID n)) cmd newRefs = Event {+ eventBefore = model+ , eventCmd = cmd+ , eventAfter = Model mock' (newRefs resp' ++ knownRefs) (CmdID (n + 1))+ , eventMockResp = resp'+ }+ where+ (resp', mock') = step model cmd++lockstep :: (Eq1 r, Show1 r, HasCallStack)+ => Model r -> Cmd :@ r -> Resp :@ r -> Event r+lockstep model cmd (At resp) = event model cmd $ \resp' ->+ zip (toList resp) (toList resp')++{-------------------------------------------------------------------------------+ Generator+-------------------------------------------------------------------------------}++generator :: Model Symbolic -> Maybe (Gen (Cmd :@ Symbolic))+generator (Model _ knownRefs cid) = Just $ oneof [+ At . CreateRef cid Nothing <$> small+ , small >>= \n -> At . Incr cid Nothing <$> replicateM n pickRef+ , small >>= \n -> At . Read cid Nothing <$> replicateM n pickRef+ ]+ where+ pickRef :: Gen (Reference IOVar Symbolic)+ pickRef = elements (map fst knownRefs)++ small :: Gen Int+ small = getSmall . getNonNegative <$> arbitrary++-- | Shrinker+--+-- The only thing the shrinker does is record the model we are given as part+-- of the shrunk command, so that we can check later we got the right model.+shrinker :: Model Symbolic -> Cmd :@ Symbolic -> [Cmd :@ Symbolic]+shrinker m (At cmd) =+ case cmd of+ CreateRef cid Nothing n -> [At $ CreateRef cid (Just m) n ]+ Incr cid Nothing xs -> [At $ Incr cid (Just m) xs]+ Read cid Nothing xs -> [At $ Read cid (Just m) xs]+ _otherwise -> []++{-------------------------------------------------------------------------------+ The state machine+-------------------------------------------------------------------------------}++transition :: (Eq1 r, Show1 r) => Model r -> Cmd :@ r -> Resp :@ r -> Model r+transition model cmd = eventAfter . lockstep model cmd++precondition :: Model Symbolic -> Cmd :@ Symbolic -> Logic+precondition (Model _ knownRefs _) (At cmd) =+ forall (toList cmd) (`elem` map fst knownRefs)++postcondition :: HasCallStack+ => Model Concrete -> Cmd :@ Concrete -> Resp :@ Concrete -> Logic+postcondition model cmd resp = toMock (eventAfter ev) resp .== eventMockResp ev+ where+ ev = lockstep model cmd resp++mock :: Model Symbolic -> Cmd :@ Symbolic -> GenSym (Resp :@ Symbolic)+mock model cmd = At <$> traverse (const QSM.genSym) resp+ where+ (resp, _mock') = step model cmd++semantics :: Cmd :@ Concrete -> IO (Resp :@ Concrete)+semantics (At cmd) = (At . fmap QSM.reference) <$> runIO (QSM.concrete <$> cmd)++sm :: StateMachine Model (At Cmd) IO (At Resp)+sm = QSM.StateMachine {+ initModel = initModel+ , transition = transition+ , precondition = precondition+ , postcondition = postcondition+ , generator = generator+ , shrinker = shrinker+ , semantics = semantics+ , mock = mock+ , invariant = Nothing+ , distribution = Nothing+ }++{-------------------------------------------------------------------------------+ The type class instances required by QSM+-------------------------------------------------------------------------------}++deriving instance Show1 r => Show (Cmd :@ r)+deriving instance Show1 r => Show (Resp :@ r)+deriving instance Show1 r => Show (Model r)++instance CommandNames (At Cmd) where+ cmdName (At cmd) = cmdName cmd+ cmdNames _ = cmdNames (Proxy @(Cmd ()))++deriving instance ToExpr (Model Concrete)+deriving instance ToExpr MockState+deriving instance ToExpr MockVar+deriving instance ToExpr CmdID++instance ToExpr IOVar where+ toExpr = defaultExprViaShow++{-------------------------------------------------------------------------------+ The standard QSM tests (as a sanity check)+-------------------------------------------------------------------------------}++prop_sequential :: Property+prop_sequential = forAllCommands sm Nothing $ \cmds -> monadicIO $ do+ (hist, _model, res) <- runCommands sm cmds+ prettyCommands sm hist (checkCommandNames cmds (res === Ok))++prop_parallel :: Property+prop_parallel = forAllParallelCommands sm $ \cmds -> monadicIO $+ prettyParallelCommands cmds =<< runParallelCommands sm cmds++{-------------------------------------------------------------------------------+ Test that shrinking does not mess up references++ We do this by translating the program to use references of an alternative+ shape: they explicitly say "the nth reference returned by command with ID id".+ Since command IDs do not change during shrinking, the translated program+ after shrinking should be a strict sublist of the translated original program.+-------------------------------------------------------------------------------}++data ExplicitRef = ExplicitRef CmdID Int+ deriving (Show, Eq, Ord)++type RefGraph = Map CmdID (Set ExplicitRef)++isSubGraphOf :: RefGraph -> RefGraph -> Bool+g `isSubGraphOf` g' = Map.isSubmapOfBy Set.isSubsetOf g g'++refGraph :: HasCallStack => QSM.Commands (At Cmd) (At Resp) -> RefGraph+refGraph (QSM.Commands cmds) = go Map.empty Map.empty cmds+ where+ go :: Map QSM.Var ExplicitRef+ -> RefGraph+ -> [QSM.Command (At Cmd) (At Resp)]+ -> RefGraph+ go _ !acc [] = acc+ go refs !acc (QSM.Command (At cmd) _resp vars : cs) =+ go (refs `union` newRefs)+ (Map.insert (cmdID cmd) (Set.fromList $ map deref (toList cmd)) acc)+ cs+ where+ deref :: Reference r Symbolic -> ExplicitRef+ deref (QSM.Reference (QSM.Symbolic x)) =+ case Map.lookup x refs of+ Just r -> r+ Nothing -> error $ "deref: reference " ++ show x ++ " not found "+ ++ "in environment " ++ show refs+ ++ " with commands " ++ show cmds++ newRefs :: Map QSM.Var ExplicitRef+ newRefs = Map.fromList $ zipWith mkRef vars [0..]++ -- When adding new 'QSM.Var's, check that they are not already present+ -- in the map, as the same 'QSM.Var' may never be created by two+ -- different commands.+ union :: Map QSM.Var ExplicitRef -- ^ Known references+ -> Map QSM.Var ExplicitRef -- ^ New references+ -> Map QSM.Var ExplicitRef+ union known new = foldr insertUnlessKnown known (Map.toList new)+ where+ insertUnlessKnown (var, newRef) =+ Map.insertWith (\_ oldRef -> error $ mkMsg var oldRef newRef)+ var newRef+ mkMsg var oldRef newRef = show var +++ " created by " ++ show oldRef +++ " already created by " ++ show newRef +++ " with commands\n" ++ ppShow cmds+++ mkRef :: QSM.Var -> Int -> (QSM.Var, ExplicitRef)+ mkRef x i = (x, ExplicitRef (cmdID cmd) i)++data ShrinkSeqFailure = SSF {+ ssfOrig :: QSM.Commands (At Cmd) (At Resp)+ , ssfShrunk :: QSM.Commands (At Cmd) (At Resp)+ , ssfGrOrig :: RefGraph+ , ssfGrShrunk :: RefGraph+ }+ deriving (Show)++-- | Test that sequential shrinking results in a program whose reference+-- graph is a subgraph of the reference graph of the original program+--+-- We don't use 'forAllCommands' directly as that would be circular (if the+-- shrinker is broken, we don't want to use it to test the shrinker!).+prop_sequential_subprog :: Property+prop_sequential_subprog =+ forAllShrinkShow (QSM.generateCommands sm Nothing) (const []) ppShow $ \cmds ->+ let cmds' = refGraph cmds in+ conjoin [ let shrunk' = refGraph shrunk in+ counterexample (ppShow (SSF cmds shrunk cmds' shrunk')) $+ shrunk' `isSubGraphOf` cmds'+ | shrunk <- QSM.shrinkCommands sm cmds+ ]++{-------------------------------------------------------------------------------+ For parallel shrinking we do pretty much the same thing, we just need to+ walk over all commands in 'ParallelCommands'+-------------------------------------------------------------------------------}++data ShrinkParFailure = SPF {+ spfOrig :: QSM.ParallelCommands (At Cmd) (At Resp)+ , spfShrunk :: QSM.ParallelCommands (At Cmd) (At Resp)+ , spfTrOrig :: RefGraph+ , spfTrShrunk :: RefGraph+ }+ deriving (Show)++-- | Compute reference graph for a parallel program+--+-- We do this by constructing the refernce graph of the sequential program+-- where we execute the left and right part of all suffices in interleaved+-- fashion.+refGraph' :: HasCallStack => QSM.ParallelCommands (At Cmd) (At Resp) -> RefGraph+refGraph' (QSM.ParallelCommands prefix suffixes) =+ refGraph (prefix <> mconcat (map (\(QSM.Pair l r) -> l `mappend` r) suffixes))++prop_parallel_subprog :: Property+prop_parallel_subprog =+ forAllShrinkShow (QSM.generateParallelCommands sm) (const []) ppShow $+ prop_parallel_subprog'+ where+ -- TODO add as a test (?)+ -- genCmds = return buggyShrinkCmds++prop_parallel_subprog' :: QSM.ParallelCommands (At Cmd) (At Resp) -> Property+prop_parallel_subprog' cmds =+ conjoin [ let shrunk' = refGraph' shrunk in+ counterexample (ppShow (SPF cmds shrunk cmds' shrunk')) $+ shrunk' `isSubGraphOf` cmds'+ | shrunk <- QSM.shrinkParallelCommands sm cmds+ ]+ where+ cmds' = refGraph' cmds++-- A set of valid commands to resulted in an invalid shrink+buggyShrinkCmds :: QSM.ParallelCommands (At Cmd) (At Resp)+buggyShrinkCmds = QSM.ParallelCommands (QSM.Commands [])+ [ QSM.Pair (QSM.Commands [mkCreateRef 0 [0]])+ (QSM.Commands [mkCreateRef 1 [1]])+ -- This Var 1 was shrunk to Var 0+ , QSM.Pair (QSM.Commands [mkRead 2 [0]])+ (QSM.Commands [mkRead 3 [1]])+ ]+ where+ mkCreateRef, mkRead :: Int -> [Int] -> QSM.Command (At Cmd) (At Resp)+ mkCreateRef cid vars =+ QSM.Command (At (CreateRef (CmdID cid) Nothing (length vars)))+ (At (Refs (map mkRef vars)))+ (map QSM.Var vars)+ mkRead cid vars =+ QSM.Command (At (Read (CmdID cid) Nothing (map mkRef vars)))+ (At (Vals (map (const 0) vars)))+ []++ mkRef :: Typeable a => Int -> Reference a Symbolic+ mkRef = QSM.Reference . QSM.Symbolic . QSM.Var+++{-------------------------------------------------------------------------------+ Check that the shrinker gets presented with the right model+-------------------------------------------------------------------------------}++execCmd :: Model Symbolic -> QSM.Command (At Cmd) (At Resp) -> Event Symbolic+execCmd model (QSM.Command cmd resp _) = lockstep model cmd resp++checkCorrectModel :: QSM.Commands (At Cmd) (At Resp) -> Property+checkCorrectModel cmds =+ case runExcept (checkCorrectModel' initModel cmds) of+ Left err -> counterexample err $ property False+ Right _ -> property True++-- | Verify that all commands have been paired with the right model+-- (if they have been paired)+--+-- Returns the final model if successful.+checkCorrectModel' :: Model Symbolic+ -> QSM.Commands (At Cmd) (At Resp)+ -> Except String (Model Symbolic)+checkCorrectModel' = \model (QSM.Commands cmds) -> go model cmds+ where+ go :: Model Symbolic+ -> [QSM.Command (At Cmd) (At Resp)]+ -> Except String (Model Symbolic)+ go m [] = return m+ go m (c : cs) = do verifyModel m (cmdModel' c)+ go (eventAfter (execCmd m c)) cs++ verifyModel :: Model Symbolic -> Maybe (Model Symbolic) -> Except String ()+ verifyModel _ Nothing = return ()+ verifyModel m (Just m')+ | m == m' = return ()+ | otherwise = throwError (show m ++ " /= " ++ show m')+++ cmdModel' :: QSM.Command (At Cmd) (At Resp) -> Maybe (Model Symbolic)+ cmdModel' (QSM.Command (At cmd) _ _) = cmdModel cmd+++prop_sequential_model :: Property+prop_sequential_model =+ forAllShrinkShow (QSM.generateCommands sm Nothing) (const []) ppShow $ \cmds ->+ conjoin [ checkCorrectModel shrunk+ | shrunk <- QSM.shrinkCommands sm cmds+ ]++{-------------------------------------------------------------------------------+ For the parallel case we do the same, but traversing the left and right+ suffix separately+-------------------------------------------------------------------------------}++checkCorrectModelParallel :: QSM.ParallelCommands (At Cmd) (At Resp) -> Property+checkCorrectModelParallel = \(QSM.ParallelCommands prefix suffixes) ->+ case runExcept (go prefix suffixes) of+ Left err -> counterexample err $ property False+ Right () -> property True+ where+ go :: QSM.Commands (At Cmd) (At Resp)+ -> [QSM.Pair (QSM.Commands (At Cmd) (At Resp))]+ -> Except String ()+ go prefix suffixes = do+ modelAfterPrefix <- checkCorrectModel' initModel prefix+ go' modelAfterPrefix suffixes++ go' :: Model Symbolic+ -> [QSM.Pair (QSM.Commands (At Cmd) (At Resp))]+ -> Except String ()+ go' _ [] = return ()+ go' m (QSM.Pair l r : suffixes) = do+ modelAfterLeft <- checkCorrectModel' m l+ -- The starting model for the right part is the /initial/ model:+ -- it should not be affected by the left part+ _ <- checkCorrectModel' m r+ -- But when we check the /next/ suffix, /both/ parts have been executed+ go' (QSM.advanceModel sm modelAfterLeft r) suffixes++prop_parallel_model :: Property+prop_parallel_model =+ forAllShrinkShow (QSM.generateParallelCommands sm) (const []) ppShow $ \cmds ->+ conjoin [ checkCorrectModelParallel shrunk+ | shrunk <- QSM.shrinkParallelCommands sm cmds+ ]
test/Spec.hs view
@@ -26,6 +26,7 @@ import Echo import ErrorEncountered import MemoryReference+import qualified ShrinkingProps import TicketDispenser ------------------------------------------------------------------------@@ -33,6 +34,7 @@ tests :: Bool -> TestTree tests docker0 = testGroup "Tests" [ testCase "Doctest Z module" (doctest ["src/Test/StateMachine/Z.hs"])+ , ShrinkingProps.tests , testProperty "Die Hard" (expectFailure (withMaxSuccess 2000 prop_dieHard)) , testGroup "Memory reference"
test/TicketDispenser.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-}@@ -36,6 +37,8 @@ import Control.Exception (IOException, catch)+import Data.Kind+ (Type) import Data.TreeDiff (ToExpr) import GHC.Generics@@ -65,12 +68,12 @@ -- The actions of the ticket dispenser are: -data Action (r :: * -> *)+data Action (r :: Type -> Type) = TakeTicket | Reset- deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)+ deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames) -data Response (r :: * -> *)+data Response (r :: Type -> Type) = GotTicket Int | ResetOk deriving (Show, Generic1, Rank2.Foldable)@@ -82,7 +85,7 @@ -- The dispenser has to be reset before use, hence the maybe integer. -newtype Model (r :: * -> *) = Model (Maybe Int)+newtype Model (r :: Type -> Type) = Model (Maybe Int) deriving (Eq, Show, Generic) deriving instance ToExpr (Model Concrete)@@ -116,8 +119,8 @@ , (4, pure TakeTicket) ] -shrinker :: Action Symbolic -> [Action Symbolic]-shrinker _ = []+shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]+shrinker _ _ = [] ------------------------------------------------------------------------