quickcheck-state-machine 0.4.2 → 0.4.3
raw patch · 10 files changed
+249/−155 lines, 10 filesdep ~basedep ~bytestringdep ~directoryPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: base, bytestring, 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, stm, strict, string-conversions, tasty, tasty-hunit, tasty-quickcheck, text, tree-diff, wai, warp
API changes (from Hackage documentation)
+ Test.StateMachine.Types.History: Crash :: cmd Concrete -> String -> Pid -> Operation cmd resp
+ Test.StateMachine.Types.History: Exception :: !String -> HistoryEvent cmd resp
+ Test.StateMachine.Types.History: instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.Operation cmd resp)
+ Test.StateMachine.Utils: oldCover :: Testable prop => Bool -> Int -> String -> prop -> Property
+ Test.StateMachine.Z: infixr 1 :/->
- Test.StateMachine: ExceptionThrown :: String -> Reason
+ Test.StateMachine: ExceptionThrown :: Reason
- Test.StateMachine: StateMachine :: forall r. model r -> forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r -> model Symbolic -> cmd Symbolic -> Logic -> model Concrete -> cmd Concrete -> resp Concrete -> Logic -> Maybe (model Concrete -> Logic) -> model Symbolic -> Gen (cmd Symbolic) -> Maybe (Matrix Int) -> cmd Symbolic -> [cmd Symbolic] -> cmd Concrete -> m (resp Concrete) -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) -> StateMachine model cmd m resp
+ Test.StateMachine: StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Gen (cmd Symbolic)) -> Maybe (Matrix Int) -> (cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> StateMachine model cmd m resp
- Test.StateMachine: prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> [(History cmd resp, Bool)] -> PropertyM m ()
+ Test.StateMachine: prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> [(History cmd resp, Logic)] -> PropertyM m ()
- Test.StateMachine: runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
+ Test.StateMachine: runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)]
- Test.StateMachine: runParallelCommandsNTimes :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
+ Test.StateMachine: runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)]
- Test.StateMachine.Parallel: linearise :: forall model cmd m resp. StateMachine model cmd m resp -> History cmd resp -> Bool
+ Test.StateMachine.Parallel: linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic
- Test.StateMachine.Parallel: prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> [(History cmd resp, Bool)] -> PropertyM m ()
+ Test.StateMachine.Parallel: prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> [(History cmd resp, Logic)] -> PropertyM m ()
- Test.StateMachine.Parallel: runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
+ Test.StateMachine.Parallel: runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)]
- Test.StateMachine.Parallel: runParallelCommandsNTimes :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
+ Test.StateMachine.Parallel: runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)]
- Test.StateMachine.Parallel: shrinkParallelCommands :: forall cmd model m resp. Foldable cmd => Foldable resp => StateMachine model cmd m resp -> (ParallelCommands cmd -> [ParallelCommands cmd])
+ Test.StateMachine.Parallel: shrinkParallelCommands :: forall cmd model m resp. Foldable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd -> [ParallelCommands cmd]
- Test.StateMachine.Sequential: liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic]) -> (Command cmd -> [Command cmd])
+ Test.StateMachine.Sequential: liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic]) -> Command cmd -> [Command cmd]
- Test.StateMachine.Types: Command :: !(cmd Symbolic) -> !(Set Var) -> Command cmd
+ Test.StateMachine.Types: Command :: !cmd Symbolic -> !Set Var -> Command cmd
- Test.StateMachine.Types: ExceptionThrown :: String -> Reason
+ Test.StateMachine.Types: ExceptionThrown :: Reason
- Test.StateMachine.Types: ParallelCommands :: !(Commands cmd) -> [t (Commands cmd)] -> ParallelCommandsF t cmd
+ Test.StateMachine.Types: ParallelCommands :: !Commands cmd -> [t (Commands cmd)] -> ParallelCommandsF t cmd
- Test.StateMachine.Types: StateMachine :: forall r. model r -> forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r -> model Symbolic -> cmd Symbolic -> Logic -> model Concrete -> cmd Concrete -> resp Concrete -> Logic -> Maybe (model Concrete -> Logic) -> model Symbolic -> Gen (cmd Symbolic) -> Maybe (Matrix Int) -> cmd Symbolic -> [cmd Symbolic] -> cmd Concrete -> m (resp Concrete) -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) -> StateMachine model cmd m resp
+ Test.StateMachine.Types: StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Gen (cmd Symbolic)) -> Maybe (Matrix Int) -> (cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> StateMachine model cmd m resp
- Test.StateMachine.Types: [prefix] :: ParallelCommandsF t cmd -> !(Commands cmd)
+ Test.StateMachine.Types: [prefix] :: ParallelCommandsF t cmd -> !Commands cmd
- Test.StateMachine.Types.Environment: reifyEnvironment :: Environment -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))
+ Test.StateMachine.Types.Environment: reifyEnvironment :: Environment -> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
- Test.StateMachine.Types.History: Invocation :: !(cmd Concrete) -> !(Set Var) -> HistoryEvent cmd resp
+ Test.StateMachine.Types.History: Invocation :: !cmd Concrete -> !Set Var -> HistoryEvent cmd resp
- Test.StateMachine.Types.History: Operation :: (cmd Concrete) -> (resp Concrete) -> Pid -> Operation cmd resp
+ Test.StateMachine.Types.History: Operation :: cmd Concrete -> resp Concrete -> Pid -> Operation cmd resp
- Test.StateMachine.Types.History: Response :: !(resp Concrete) -> HistoryEvent cmd resp
+ Test.StateMachine.Types.History: Response :: !resp Concrete -> HistoryEvent cmd resp
- Test.StateMachine.Types.Rank2: class Foldable (f :: (k -> *) -> *)
+ Test.StateMachine.Types.Rank2: class Foldable (f :: (k -> Type) -> Type)
- Test.StateMachine.Types.Rank2: class Functor (f :: (k -> *) -> *)
+ Test.StateMachine.Types.Rank2: class Functor (f :: (k -> Type) -> Type)
- Test.StateMachine.Types.Rank2: class (Functor t, Foldable t) => Traversable (t :: (k -> *) -> *)
+ Test.StateMachine.Types.Rank2: class (Functor t, Foldable t) => Traversable (t :: (k -> Type) -> Type)
- Test.StateMachine.Types.References: Reference :: (r a) -> Reference a r
+ Test.StateMachine.Types.References: Reference :: r a -> Reference a r
- Test.StateMachine.Utils: shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)])
+ Test.StateMachine.Utils: shrinkPair :: (a -> [a]) -> (a, a) -> [(a, a)]
- Test.StateMachine.Utils: shrinkPair' :: (a -> [a]) -> (b -> [b]) -> ((a, b) -> [(a, b)])
+ Test.StateMachine.Utils: shrinkPair' :: (a -> [a]) -> (b -> [b]) -> (a, b) -> [(a, b)]
Files
- CHANGELOG.md +9/−0
- README.md +20/−10
- quickcheck-state-machine.cabal +113/−104
- src/Test/StateMachine/Parallel.hs +42/−22
- src/Test/StateMachine/Sequential.hs +25/−8
- src/Test/StateMachine/Types.hs +1/−1
- src/Test/StateMachine/Types/History.hs +13/−3
- src/Test/StateMachine/Types/Rank2.hs +5/−3
- src/Test/StateMachine/Utils.hs +12/−1
- test/Spec.hs +9/−3
CHANGELOG.md view
@@ -1,3 +1,12 @@+#### 0.4.3 (2018-12-7)++ * Support QuickCheck-2.12.*;+ * Use new compact diffing of records from tree-diff library when displaying+ counterexamples;+ * Explain mock better in the README;+ * Handle exceptions more gracefully;+ * Show, possibly multiple, counterexample when parallel property fails.+ #### 0.4.2 (2018-9-3) * Fix bug that made tests fail on systems without docker;
README.md view
@@ -140,8 +140,7 @@ (Increment _ref, Incremented) -> Top ``` -Finally, we have to explain how to generate, mock responses given a model, and-shrink actions.+Next we have to explain how to generate and shrink actions. ```haskell generator :: Model Symbolic -> Gen (Command Symbolic)@@ -152,18 +151,27 @@ , (4, Increment <$> elements (domain model)) ] +shrinker :: Command Symbolic -> [Command Symbolic]+shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]+shrinker _ = []+```++Finally, we show how to mock responses given a model.++```haskell mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic) mock (Model m) cmd = case cmd of Create -> Created <$> genSym Read ref -> ReadValue <$> pure (m ! ref) Write _ _ -> pure Written Increment _ -> pure Incremented--shrinker :: Command Symbolic -> [Command Symbolic]-shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]-shrinker _ = [] ``` +(`mock` is a hack to make it possible for responses to have multiple reference,+and an experiment which maybe one day will let us create mocked APIs. See issue+[#236](https://github.com/advancedtelematic/quickcheck-state-machine/issues/236)+for further details.)+ To be able to fit the code on a line we pack up all of them above into a record. @@ -280,6 +288,8 @@ │ [] ← Read (Reference (Concrete Opaque)) │ │ │ → ReadValue 1 │ │ └──────────────────────────────────────────────┘ │++AnnotateC "Read" (PredicateC (1 :/= 2)) ``` As we can see above, a mutable reference is first created, and then in@@ -437,10 +447,10 @@ [video](https://vimeo.com/6638041)] -- this is the first paper to describe how Erlang's QuickCheck works (including the parallel testing); - * *Linearizability: a correctness condition for concurrent- objects* [[PDF](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)], this- is a classic paper that describes the main technique of the parallel- property;+ * *Linearizability: a correctness condition for concurrent objects*+ [[PDF](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf), TLA++ [formalisation](https://github.com/lorin/tla-linearizability)], this is a classic+ paper that describes the main technique of the parallel property; * Aphyr's blogposts about [Jepsen](https://github.com/jepsen-io/jepsen), which also uses the linearisability technique, and has found bugs in many
quickcheck-state-machine.cabal view
@@ -1,119 +1,128 @@-cabal-version: >=1.10-name: quickcheck-state-machine-version: 0.4.2-license: BSD3-license-file: LICENSE-copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;- 2018, HERE Europe B.V.-maintainer: Stevan Andjelkovic <stevan.andjelkovic@here.com>-author: Stevan Andjelkovic-tested-with: ghc ==8.2.2 ghc ==8.4.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+name: quickcheck-state-machine+version: 0.4.3+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, 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 library- 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:+ 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: ansi-wl-pprint >=0.6.7.3,- base >=4.7 && <5,+ 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 >=1.7,+ pretty-show, QuickCheck >=2.9.2, split >=0.2.3.3, stm >=2.4.4.1,- tree-diff >=0.0.1,+ tree-diff >=0.0.2, vector >=0.12.0.1+ default-language: Haskell2010 test-suite quickcheck-state-machine-test- type: exitcode-stdio-1.0- main-is: Spec.hs- hs-source-dirs: test- other-modules:- CircularBuffer- CrudWebserverDb- DieHard- Echo- MemoryReference- TicketDispenser- default-language: Haskell2010- 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- build-depends:- base >=4.11.1.0,- bytestring >=0.10.8.2,- directory >=1.3.1.5,- doctest >=0.16.0,- filelock >=0.1.1.2,- filepath >=1.4.2,- http-client >=0.5.13.1,- lifted-async >=0.9.3,- matrix >=0.3.5.0,- monad-control >=1.0.2.2,- monad-logger >=0.3.28.5,- mtl >=2.2.2,- network >=2.6.3.6,- persistent >=2.8.2,- persistent-postgresql >=2.8.2.0,- persistent-template >=2.5.4,- process >=1.6.3.0,- QuickCheck >=2.9.2,- quickcheck-instances >=0.3.18,- quickcheck-state-machine -any,- random >=1.1,- resourcet >=1.2.1,- servant >=0.14.1,- servant-client >=0.14,- servant-server >=0.14.1,- stm >=2.4.5.0,- strict >=0.3.2,- string-conversions >=0.4.0.1,- tasty >=1.1.0.2,- tasty-hunit >=0.10.0.1,- tasty-quickcheck >=0.10,- text >=1.2.3.0,- tree-diff >=0.0.1,- vector >=0.12.0.1,- wai >=3.2.1.2,- warp >=3.2.23+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends: base,+ bytestring,+ 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,+ persistent,+ persistent-postgresql,+ persistent-template,+ process,+ QuickCheck >=2.9.2,+ quickcheck-instances,+ quickcheck-state-machine,+ random,+ resourcet,+ servant,+ servant-client,+ servant-server,+ stm,+ strict,+ string-conversions,+ tasty,+ tasty-hunit,+ tasty-quickcheck,+ text,+ tree-diff,+ vector >=0.12.0.1,+ wai,+ warp++ other-modules: CircularBuffer,+ CrudWebserverDb,+ DieHard,+ Echo,+ 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
src/Test/StateMachine/Parallel.hs view
@@ -56,7 +56,7 @@ ((<>)) import Data.Set (Set)-import qualified Data.Set as S+import qualified Data.Set as S import Data.Tree (Tree(Node)) import GHC.Generics@@ -75,10 +75,9 @@ import Test.StateMachine.BoxDrawer import Test.StateMachine.ConstructorName import Test.StateMachine.Logic- (boolean) import Test.StateMachine.Sequential import Test.StateMachine.Types-import qualified Test.StateMachine.Types.Rank2 as Rank2+import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils ------------------------------------------------------------------------@@ -257,19 +256,21 @@ ------------------------------------------------------------------------ -runParallelCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)+runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))+ => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd- -> PropertyM m [(History cmd resp, Bool)]+ -> PropertyM m [(History cmd resp, Logic)] runParallelCommands sm = runParallelCommandsNTimes 10 sm -runParallelCommandsNTimes :: (Rank2.Traversable cmd, Rank2.Foldable resp)+runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete))+ => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -- ^ How many times to execute the parallel program. -> StateMachine model cmd m resp -> ParallelCommands cmd- -> PropertyM m [(History cmd resp, Bool)]+ -> PropertyM m [(History cmd resp, Logic)] runParallelCommandsNTimes n sm cmds = replicateM n $ do (hist, _reason) <- run (executeParallelCommands sm cmds)@@ -319,22 +320,24 @@ -- | Try to linearise a history of a parallel program execution using a -- sequential model. See the *Linearizability: a correctness condition for -- concurrent objects* paper linked to from the README for more info.-linearise :: forall model cmd m resp. StateMachine model cmd m resp- -> History cmd resp -> Bool+linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete))+ => StateMachine model cmd m resp -> History cmd resp -> Logic linearise StateMachine { transition, postcondition, initModel } = go . unHistory where- go :: [(Pid, HistoryEvent cmd resp)] -> Bool- go [] = True- go es = any (step initModel) (interleavings es)+ go :: [(Pid, HistoryEvent cmd resp)] -> Logic+ go [] = Top+ go es = exists (interleavings es) (step initModel) - step :: model Concrete -> Tree (Operation cmd resp) -> Bool- step model (Node (Operation cmd resp _) roses) =- boolean (postcondition model cmd resp) &&- any' (step (transition model cmd resp)) roses+ step :: model Concrete -> Tree (Operation cmd resp) -> Logic+ step _model (Node (Crash _cmd _err _pid) _roses) =+ error "Not implemented yet, see issue #162 for more details."+ step model (Node (Operation cmd resp _) roses) =+ postcondition model cmd resp .&&+ exists' roses (step (transition model cmd resp)) -any' :: (a -> Bool) -> [a] -> Bool-any' _ [] = True-any' p xs = any p xs+exists' :: Show a => [a] -> (a -> Logic) -> Logic+exists' [] _ = Top+exists' xs p = exists xs p ------------------------------------------------------------------------ @@ -343,11 +346,26 @@ prettyParallelCommands :: (MonadIO m, Rank2.Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd- -> [(History cmd resp, Bool)] -- ^ Output of 'runParallelCommands'.+ -> [(History cmd resp, Logic)] -- ^ Output of 'runParallelCommands'. -> PropertyM m () prettyParallelCommands cmds =- mapM_ (\(hist, bool) -> print (toBoxDrawings cmds hist) `whenFailM` property bool)+ mapM_ (\(hist, l) -> printCounterexample hist (logic l) `whenFailM` property (boolean l))+ where+ printCounterexample hist (VFalse ce) = do+ print (toBoxDrawings cmds hist)+ putStrLn ""+ print (simplify ce)+ putStrLn ""+ printCounterexample _hist _+ = error "prettyParallelCommands: impossible, because `boolean l` was False." + simplify :: Counterexample -> Counterexample+ simplify (ExistsC _ [Fst ce]) = ce+ simplify (ExistsC x (Fst ce : ces)) = ce `EitherC` simplify (ExistsC x ces)+ simplify (ExistsC _ (Snd ce : _)) = simplify ce+ simplify _ = error "simplify: impossible,\+ \ because of the structure of linearise."+ -- | Draw an ASCII diagram of the history of a parallel program. Useful for -- seeing how a race condition might have occured. toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd@@ -369,6 +387,7 @@ | vars `S.isSubsetOf` knownVars = show (S.toList vars) ++ " ← " ++ show cmd | otherwise = show cmd out (Response resp) = show resp+ out (Exception err) = err toEventType :: History' cmd resp -> [(EventType, Pid)] toEventType = map go@@ -376,9 +395,10 @@ go e = case e of (pid, Invocation _ _) -> (Open, pid) (pid, Response _) -> (Close, pid)+ (pid, Exception _) -> (Close, pid) evT :: [(EventType, Pid)]- evT = toEventType (filter (\e -> fst e `elem` map Pid [1, 2]) h)+ 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
src/Test/StateMachine/Sequential.hs view
@@ -78,14 +78,14 @@ (Set) import qualified Data.Set as S import Data.TreeDiff- (ToExpr, ansiWlBgEditExpr, ediff)+ (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, cover,- generate, resize, shrinkList, sized, suchThat)+ (Gen, Property, Testable, choose, collect, generate,+ resize, shrinkList, sized, suchThat) import Test.QuickCheck.Monadic (PropertyM, run) import Text.PrettyPrint.ANSI.Leijen@@ -283,11 +283,13 @@ liftBaseWith (const (atomically (writeTChan hchan (pid, Invocation ccmd vars)))) !ecresp <- lift (fmap Right (semantics ccmd)) `catch` (\(err :: IOException) ->- return (Left (ExceptionThrown (displayException err))))+ return (Left (displayException err))) `catch` (\(err :: ErrorCall) ->- return (Left (ExceptionThrown (displayException err))))+ return (Left (displayException err))) case ecresp of- Left err -> return err+ 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@@ -310,7 +312,7 @@ getUsedConcrete = Rank2.foldMap (\(Concrete x) -> [toDyn x]) modelDiff :: ToExpr (model r) => model r -> Maybe (model r) -> Doc-modelDiff model = ansiWlBgEditExpr . flip ediff model . fromMaybe model+modelDiff model = ansiWlBgEditExprCompact . flip ediff model . fromMaybe model prettyPrintHistory :: forall model cmd m resp. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete))@@ -326,6 +328,20 @@ go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc go current previous [] = PP.line <> modelDiff current previous <> PP.line <> PP.line+ go current previous [Crash cmd err pid] =+ mconcat+ [ PP.line+ , modelDiff current previous+ , PP.line, PP.line+ , PP.string " == "+ , PP.string (show cmd)+ , PP.string " ==> "+ , PP.string err+ , PP.string " [ "+ , PP.int (unPid pid)+ , PP.string " ]"+ , PP.line+ ] go current previous (Operation cmd resp pid : ops) = mconcat [ PP.line@@ -341,6 +357,7 @@ , PP.line , go (transition current cmd resp) (Just current) ops ]+ go _ _ _ = error "prettyPrintHistory: impossible." prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete))@@ -359,7 +376,7 @@ => Commands cmd -> Property -> Property checkCommandNames cmds = collect names- . cover (length names == numOfConstructors) 1 "coverage"+ . oldCover (length names == numOfConstructors) 1 "coverage" where names = commandNames cmds numOfConstructors = length (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic)))
src/Test/StateMachine/Types.hs view
@@ -88,7 +88,7 @@ | PreconditionFailed | PostconditionFailed String | InvariantBroken String- | ExceptionThrown String+ | ExceptionThrown deriving (Eq, Show) data ParallelCommandsF t cmd = ParallelCommands
src/Test/StateMachine/Types/History.hs view
@@ -53,6 +53,7 @@ data HistoryEvent cmd resp = Invocation !(cmd Concrete) !(Set Var) | Response !(resp Concrete)+ | Exception !String deriving instance (Eq (cmd Concrete), Eq (resp Concrete)) => Eq (HistoryEvent cmd resp)@@ -65,7 +66,8 @@ takeInvocations :: History' cmd resp -> [(Pid, cmd Concrete)] takeInvocations [] = [] takeInvocations ((pid, Invocation cmd _) : hist) = (pid, cmd) : takeInvocations hist-takeInvocations ((_, Response _) : _) = []+takeInvocations ((_, Response _) : _) = []+takeInvocations ((_, Exception _) : _) = [] findResponse :: Pid -> History' cmd resp -> [(resp Concrete, History' cmd resp)] findResponse _ [] = []@@ -77,13 +79,21 @@ -- | An operation packs up an invocation event with its corresponding -- response event.-data Operation cmd resp = Operation (cmd Concrete) (resp Concrete) Pid+data Operation cmd resp+ = Operation (cmd Concrete) (resp Concrete) Pid+ | Crash (cmd Concrete) String Pid +deriving instance (Show (cmd Concrete), Show (resp Concrete)) =>+ Show (Operation cmd resp)+ makeOperations :: History' cmd resp -> [Operation cmd resp] makeOperations [] = []+makeOperations [(pid1, Invocation cmd _), (pid2, Exception err)]+ | pid1 == pid2 = [Crash cmd err pid1]+ | otherwise = error "makeOperations: impossible, pid mismatch." makeOperations ((pid1, Invocation cmd _) : (pid2, Response resp) : hist) | pid1 == pid2 = Operation cmd resp pid1 : makeOperations hist- | otherwise = error "makeOperations: pid mismatch."+ | otherwise = error "makeOperations: impossible, pid mismatch." makeOperations _ = error "makeOperations: impossible." -- | Given a history, return all possible interleavings of invocations
src/Test/StateMachine/Types/Rank2.hs view
@@ -21,6 +21,8 @@ import qualified Control.Applicative as Rank1 import qualified Control.Monad as Rank1 import qualified Data.Foldable as Rank1+import Data.Kind+ (Type) import qualified Data.Traversable as Rank1 import GHC.Generics ((:*:)((:*:)), (:+:)(L1, R1), Generic1, K1(K1),@@ -31,7 +33,7 @@ ------------------------------------------------------------------------ -class Functor (f :: (k -> *) -> *) where+class Functor (f :: (k -> Type) -> Type) where fmap :: (forall x. p x -> q x) -> f p -> f q default fmap :: (Generic1 f, Functor (Rep1 f)) => (forall x. p x -> q x) -> f p -> f q@@ -68,7 +70,7 @@ ------------------------------------------------------------------------ -class Foldable (f :: (k -> *) -> *) where+class Foldable (f :: (k -> Type) -> Type) where foldMap :: Monoid m => (forall x. p x -> m) -> f p -> m default foldMap :: (Generic1 f, Foldable (Rep1 f), Monoid m) => (forall a. p a -> m) -> f p -> m@@ -102,7 +104,7 @@ ------------------------------------------------------------------------ -class (Functor t, Foldable t) => Traversable (t :: (k -> *) -> *) where+class (Functor t, Foldable t) => Traversable (t :: (k -> Type) -> Type) where traverse :: Rank1.Applicative f => (forall a. p a -> f (q a)) -> t p -> f (t q) default traverse :: (Generic1 t, Traversable (Rep1 t), Rank1.Applicative f) => (forall a. p a -> f (q a)) -> t p -> f (t q)
src/Test/StateMachine/Utils.hs view
@@ -25,6 +25,7 @@ , shrinkPair , shrinkPair' , suchThatOneOf+ , oldCover ) where @@ -37,7 +38,7 @@ (PropertyM(MkPropertyM)) import Test.QuickCheck.Property (Property(MkProperty), property, unProperty, (.&&.),- (.||.))+ (.||.), cover) #if !MIN_VERSION_QuickCheck(2,10,0) import Test.QuickCheck.Property (succeeded)@@ -110,3 +111,13 @@ case mx of Just x -> return (Just x) Nothing -> go (gens' ++ gens'') (n - 1)++-- QuickCheck-2.12.0 introduced a breaking change in the cover combinator, see+-- issue #248 for details.+oldCover :: Testable prop => Bool -> Int -> String -> prop -> Property+oldCover x n s p =+#if !MIN_VERSION_QuickCheck(2,12,0)+ cover x n s p+#else+ cover (fromIntegral n) x s p+#endif
test/Spec.hs view
@@ -8,7 +8,8 @@ import System.Exit (ExitCode(..)) import System.Process- (rawSystem)+ (StdStream(CreatePipe), proc, std_out,+ waitForProcess, withCreateProcess) import Test.DocTest (doctest) import Test.Tasty@@ -32,7 +33,7 @@ tests docker0 = testGroup "Tests" [ testCase "Doctest Z module" (doctest ["src/Test/StateMachine/Z.hs"]) , testProperty "Die Hard"- (expectFailure (withMaxSuccess 1000 prop_dieHard))+ (expectFailure (withMaxSuccess 2000 prop_dieHard)) , testGroup "Memory reference" [ testProperty "No bug" (prop_sequential None) , testProperty "Logic bug" (expectFailure (prop_sequential Logic))@@ -86,9 +87,14 @@ main :: IO () main = do -- Check if docker is avaiable.- ec <- rawSystem "docker" ["version"]+ ec <- rawSystemNoStdout "docker" ["version"] `catch` (\(_ :: IOError) -> return (ExitFailure 127)) let docker = case ec of ExitSuccess -> True ExitFailure _ -> False defaultMain (tests docker)+ where+ rawSystemNoStdout cmd args =+ withCreateProcess+ (proc cmd args) { std_out = CreatePipe }+ (\_ _ _ -> waitForProcess)