packages feed

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 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)