quickcheck-state-machine 0.7.2 → 0.7.3
raw patch · 15 files changed
+158/−79 lines, 15 files
Files
- CHANGELOG.md +9/−0
- README.md +41/−13
- quickcheck-state-machine.cabal +3/−2
- src/Test/StateMachine/BoxDrawer.hs +2/−1
- src/Test/StateMachine/DotDrawing.hs +6/−6
- src/Test/StateMachine/Lockstep/Auxiliary.hs +4/−5
- src/Test/StateMachine/Lockstep/NAry.hs +3/−4
- src/Test/StateMachine/Lockstep/Simple.hs +2/−3
- src/Test/StateMachine/Markov.hs +7/−11
- src/Test/StateMachine/Parallel.hs +59/−18
- src/Test/StateMachine/Types.hs +0/−2
- src/Test/StateMachine/Types/References.hs +4/−0
- src/Test/StateMachine/Utils.hs +8/−9
- src/Test/StateMachine/Z.hs +3/−1
- test/Spec.hs +7/−4
CHANGELOG.md view
@@ -1,3 +1,12 @@+#### 0.7.3 (2023-6-1)++ * Fix compatibility with GHC 9.6 (PR #20, thanks @erikd);++ * Fix printing of boxed diagrams of parallel properties (PR #21);++ * Parallel properties will now show a message indicating what looks like it+ could be the cause of the property failing (PR #21).+ #### 0.7.2 (2023-4-20) * Fix compatibility with GHC 9.0 and 9.2 (PR #7, thanks @edsko);
README.md view
@@ -309,6 +309,8 @@ └──────────────────────────────────────────────┘ │ AnnotateC "Read" (PredicateC (1 :/= 2))++However, some repetitions of this sequence of commands passed. Maybe there is a race condition? ``` As we can see above, a mutable reference is first created, and then in@@ -434,6 +436,32 @@ varies between runs. One can further increase entropy by introducing random `threadDelay`s in the semantic function. +#### Why is a parallel property failing?++Unless in presence of more severe bugs, parallel properties can fail because of+mainly two reasons: a race condition is happening or a logic bug is present in+the code. Taking advantage of the fact that we are repeating multiple times each+sequence of commands, we can have some insight on which one of those cases seems+to be the cause.++The parallel counterexample will show one of the following messages:++- `However, some repetitions of this sequence of commands passed. Maybe there is+ a race condition?`: In this case as some parallel executions of a given+ sequence of commands have passed, it seems that the test outcome is being+ affected by a race condition or a non-deterministic error. This message is+ accurate in the sense that a logic bug will not result in some repetitions+ succeeding.+- `And all repetitions of this sequence of commands failed. Maybe there is a+ logic bug? Try with more repetitions to be sure that it happens consistently`:+ In this case, one of two things can happen. Either there is a logic bug that+ is triggered always (which is what the message suggest) or we were just super+ unlucky (or super lucky, as we found an error) in this run and a race+ condition manifested in all runs. In order to rule out this last case, one can+ run the tests with more repetitions, which if the problem is that there is+ indeed a race condition, should result in the other message being printed+ instead.+ #### SUT initialization Some tests might require an environment that is used by the SUT to perform its@@ -446,7 +474,7 @@ ``` haskell -semantics :: Env -> Command Concrete -> m Response Concrete+semantics :: Env -> Command Concrete -> m (Response Concrete) semantics = ... sm :: m (StateMachine Model Command m Response)@@ -526,7 +554,7 @@ has no meaningful semantics, we merely model-check. It might be helpful to compare the solution to the Hedgehog- [solution](http://clrnd.com.ar/posts/2017-04-21-the-water-jug-problem-in-hedgehog.html) and+ [solution](https://clrnd.com.ar/posts/2017-04-21-the-water-jug-problem-in-hedgehog.html) and the TLA+ [solution](https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla);@@ -548,7 +576,7 @@ -- another example that shows how the sequential property can find help find different kind of bugs. This example is borrowed from the paper *Testing the Hard Stuff and Staying Sane*- [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),+ [[PDF](https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf), [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)]. For a more direct translation from the paper, see the following [variant](https://github.com/polux/qsm-ffi-demo) which uses the C FFI;@@ -558,7 +586,7 @@ -- an imperative implementation of the union-find algorithm. It could be useful to compare the solution to the one that appears in the paper *Testing Monadic Code with QuickCheck*- [[PS](http://www.cse.chalmers.se/~rjmh/Papers/QuickCheckST.ps)], which the+ [[PS](https://www.cse.chalmers.se/~rjmh/Papers/QuickCheckST.ps)], which the [`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html) module is based on; @@ -571,7 +599,7 @@ *Testing a Database for Race Conditions with QuickCheck* and *Testing the Hard Stuff and Staying Sane*- [[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),+ [[PDF](https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf), [video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)] papers; * CRUD webserver where create returns unique@@ -603,7 +631,7 @@ [video](https://www.youtube.com/watch?v=w2fin2V83e8)] papers. All properties from the examples can be found in the-[`Spec`](https://github.com/stevana/quickcheck-state-machine/tree/master/test/Spec.hs)+[`Spec`](https://github.com/stevana/quickcheck-state-machine/blob/master/test/Spec.hs) module located in the [`test`](https://github.com/stevana/quickcheck-state-machine/tree/master/test) directory.@@ -620,7 +648,7 @@ * IOHK are using a state machine models in several [places](https://github.com/search?l=Haskell&q=org%3Ainput-output-hk+Test.StateMachine&type=Code). For example- [here](https://github.com/input-output-hk/ouroboros-network/blob/master/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/FS/StateMachine.hs)+ [here](https://github.com/input-output-hk/fs-sim/blob/main/fs-sim/test/Test/System/FS/StateMachine.hs) is a test of a mock file system that they in turn use to simulate file system errors when testing a blockchain database. The following blog [post](http://www.well-typed.com/blog/2019/01/qsm-in-depth/) describes their@@ -650,14 +678,14 @@ QuickCheck started; * John Hughes' Midlands Graduate School 2019- [course](http://www.cse.chalmers.se/~rjmh/MGS2019/) on property-based+ [course](https://www.cse.chalmers.se/~rjmh/MGS2019/) on property-based testing, which covers the basics of state machine modelling and testing. It also contains a minimal implementation of a state machine testing library built on top of Haskell's QuickCheck; * *Finding Race Conditions in Erlang with QuickCheck and PULSE*- [[PDF](http://www.cse.chalmers.se/~nicsma/papers/finding-race-conditions.pdf),+ [[PDF](https://www.cse.chalmers.se/~nicsma/papers/finding-race-conditions.pdf), [video](https://vimeo.com/6638041)] -- this is the first paper to describe how Erlang's QuickCheck works (including the parallel testing); @@ -713,7 +741,7 @@ status report of the hypervisor that Microsoft Research are developing using Event-B. - - [Abstract State Machines](http://www.di.unipi.it/~boerger/AsmBook/): A+ - [Abstract State Machines](http://groups.di.unipi.it/~boerger/AsmBook/): A Method for High-Level System Design and Analysis. The books contain general advice how to model systems using state machines,@@ -735,7 +763,7 @@ property based testing library to have support for state machines (closed source); - - The Erlang library [PropEr](https://github.com/manopapad/proper) is+ - The Erlang library [PropEr](https://github.com/proper-testing/proper) is *eqc*-inspired, open source, and has support for state machine [testing](http://propertesting.com/); @@ -743,10 +771,10 @@ library [Hedgehog](https://github.com/hedgehogqa/haskell-hedgehog), also has support for state machine based testing; - - [ScalaCheck](http://www.scalacheck.org/), likewise has support for state+ - [ScalaCheck](https://scalacheck.org/), likewise has support for state machine based- [testing](https://github.com/rickynils/scalacheck/blob/master/doc/UserGuide.md#stateful-testing) (no+ [testing](https://github.com/typelevel/scalacheck/blob/master/doc/UserGuide.md) (no parallel property); - The Python
quickcheck-state-machine.cabal view
@@ -1,5 +1,5 @@ name: quickcheck-state-machine-version: 0.7.2+version: 0.7.3 synopsis: Test monadic programs using state machine based models description: See README at <https://github.com/stevana/quickcheck-state-machine#readme> homepage: https://github.com/stevana/quickcheck-state-machine#readme@@ -16,7 +16,7 @@ , CHANGELOG.md , CONTRIBUTING.md cabal-version: >=1.10-tested-with: GHC == 8.4.3, GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.7+tested-with: GHC == 8.4.3, GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.7, GHC == 9.6.1 library hs-source-dirs: src@@ -32,6 +32,7 @@ -Wno-monomorphism-restriction -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode+ -Wno-missing-kind-signatures exposed-modules: Test.StateMachine , Test.StateMachine.BoxDrawer , Test.StateMachine.ConstructorName
src/Test/StateMachine/BoxDrawer.hs view
@@ -102,5 +102,6 @@ exec :: [(EventType, Pid)] -> Fork [String] -> Doc exec evT (Fork lops pops rops) = vsep $ map text (preBoxes ++ parBoxes) where- preBoxes = map (adjust $ maximum $ 0:map ((2+) . length) (take 1 parBoxes)) $ compilePrefix pops+ preBoxes = let pref = compilePrefix pops+ in map (adjust $ maximum $ map ((2+) . size) pref ++ map ((2+) . length) (take 1 parBoxes)) pref parBoxes = next . compile $ toEvent evT (lops, rops)
src/Test/StateMachine/DotDrawing.hs view
@@ -71,17 +71,17 @@ in (p, n, e) nodes = concatMap (\(_,n,_) -> n) nodesAndEdges edges = concatMap (\(_,_,e) -> e) nodesAndEdges- firstOfEachPid = (\(p, n, _) -> (p, fmap fst $ uncons n)) <$> nodesAndEdges+ firstOfEachPid = (\(p, n, _) -> (p, fst <$> uncons n)) <$> nodesAndEdges -- create barrier edges - edgesFromBarrier = concat $ (\(p, mn) -> case mn of+ edgesFromBarrier = concatMap (\(p, mn) -> case mn of Nothing -> [] Just n -> [DotEdge { fromNode = nodeID barrierNode , toNode = nodeID n , edgeAttributes = [TailPort (LabelledPort (PN {portName = pack $ show p}) Nothing)]- }]) <$> firstOfEachPid+ }]) firstOfEachPid prefixToBarrier = case prefixNodes of [] -> [] _ -> [DotEdge {@@ -118,11 +118,11 @@ toDotNode :: String -> (Int, (String,String)) -> DotNode String toDotNode nodeIdGroup (n, (invocation, resp)) = DotNode {- nodeID = (nodeIdGroup ++ "-" ++ show n)+ nodeID = nodeIdGroup ++ "-" ++ show n , nodeAttributes = [Label $ StrLabel $ pack $- (newLinesAfter "\\l" 60 invocation)+ newLinesAfter "\\l" 60 invocation ++ "\\n"- ++ (newLinesAfter "\\r" 60 resp)]+ ++ newLinesAfter "\\r" 60 resp] } byTwoUnsafe :: String -> [a] -> [(a,a)]
src/Test/StateMachine/Lockstep/Auxiliary.hs view
@@ -3,7 +3,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -61,7 +60,7 @@ ntraverse :: (NTraversable f, Applicative m, SListI xs) => (forall a. Elem xs a -> g a -> m (h a)) -> f g xs -> m (f h xs)-ntraverse f = nctraverse (Proxy @Top) f+ntraverse = nctraverse (Proxy @Top) ncfmap :: (NTraversable f, All c xs) => proxy c@@ -72,7 +71,7 @@ nfmap :: (NTraversable f, SListI xs) => (forall a. Elem xs a -> g a -> h a) -> f g xs -> f h xs-nfmap f xs = ncfmap (Proxy @Top) f xs+nfmap = ncfmap (Proxy @Top) ncfoldMap :: forall proxy f g m c xs. (NTraversable f, Monoid m, All c xs)@@ -82,7 +81,7 @@ ncfoldMap p f = \xs -> execState (aux xs) mempty where aux :: f g xs -> State m (f g xs)- aux xs = nctraverse p aux' xs+ aux = nctraverse p aux' aux' :: c a => Elem xs a -> g a -> State m (g a) aux' ix ga = modify (f ix ga `mappend`) >> return ga@@ -90,4 +89,4 @@ nfoldMap :: (NTraversable f, Monoid m, SListI xs) => (forall a. Elem xs a -> g a -> m) -> f g xs -> m-nfoldMap f xs = ncfoldMap (Proxy @Top) f xs+nfoldMap = ncfoldMap (Proxy @Top)
src/Test/StateMachine/Lockstep/NAry.hs view
@@ -7,7 +7,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -161,7 +160,7 @@ . unRefss where toExprOne :: (ToExpr a, ToExpr (MockHandle t a))- => Refs t Concrete a -> K (TD.Expr) a+ => Refs t Concrete a -> K TD.Expr a toExprOne = K . toExpr instance SListI (RealHandles t) => Semigroup (Refss t r) where@@ -272,7 +271,7 @@ -> Cmd t :@ Concrete -> m (Resp t :@ Concrete) semantics StateMachineTest{..} (At c) =- (At . ncfmap (Proxy @Typeable) (const wrapConcrete)) <$>+ At . ncfmap (Proxy @Typeable) (const wrapConcrete) <$> runReal (nfmap (const unwrapConcrete) c) unwrapConcrete :: FlipRef Concrete a -> I a@@ -368,7 +367,7 @@ Boolean (M.getAll $ nfoldMap check c) .// "No undefined handles" where check :: Elem (RealHandles t) a -> FlipRef Symbolic a -> M.All- check ix (FlipRef a) = M.All $ any (sameRef a) $ map fst (unRefs (hs `npAt` ix))+ check ix (FlipRef a) = M.All $ any (sameRef a . fst) (unRefs (hs `npAt` ix)) -- TODO: Patch QSM sameRef :: Reference a Symbolic -> Reference a Symbolic -> Bool
src/Test/StateMachine/Lockstep/Simple.hs view
@@ -4,7 +4,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -142,7 +141,7 @@ cmdAtFromSimple = NAry.At . SimpleCmd . fmap NAry.FlipRef . unAt cmdAtToSimple :: Functor (Cmd t) => NAry.Cmd (Simple t) NAry.:@ r -> Cmd t :@ r-cmdAtToSimple = At . fmap (NAry.unFlipRef) . unSimpleCmd . NAry.unAt+cmdAtToSimple = At . fmap NAry.unFlipRef . unSimpleCmd . NAry.unAt cmdMockToSimple :: Functor (Cmd t) => NAry.Cmd (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t]@@ -275,7 +274,7 @@ fromSimple :: StateMachineTest t -> NAry.StateMachineTest (Simple t) IO fromSimple StateMachineTest{..} = NAry.StateMachineTest { runMock = \cmd st -> first respMockFromSimple (runMock (cmdMockToSimple cmd) st)- , runReal = \cmd -> respRealFromSimple <$> (runReal (cmdRealToSimple cmd))+ , runReal = \cmd -> respRealFromSimple <$> runReal (cmdRealToSimple cmd) , initMock = initMock , newHandles = \r -> Comp (newHandles (unSimpleResp r)) :* Nil , generator = \m -> fmap cmdAtFromSimple <$> generator (modelToSimple m)
src/Test/StateMachine/Markov.hs view
@@ -142,7 +142,7 @@ go (Right ((command, probability), to)) = Transition {..} (ls, rs) = partitionEithers es- uniform = (100 - sum (map snd (map fst rs))) / genericLength ls+ uniform = (100 - sum (map (snd . fst) rs)) / genericLength ls -- ^ Note: If `length ls == 0` then `uniform` is not used, so division by -- zero doesn't happen. @@ -194,9 +194,8 @@ => Markov state cmd_ Double -> prop -> Property coverMarkov markov prop = foldr go (property prop) (Map.toList (unMarkov markov)) where- go (from, ts) ih =- coverTable (show from)- (map (\Transition{..} -> (toTransitionString command to, probability)) ts) ih+ go (from, ts) = coverTable (show from)+ (map (\Transition{..} -> (toTransitionString command to, probability)) ts) toTransitionString :: (Show state, Show cmd_) => cmd_ -> state -> String toTransitionString cmd to = "-< " ++ show cmd ++ " >- " ++ show to@@ -218,8 +217,7 @@ -> Property tabulateTransitions ts prop = foldr go (property prop) ts where- go (from, Transition {..}) ih =- tabulate (show from) [ toTransitionString command to ] ih+ go (from, Transition {..}) = tabulate (show from) [ toTransitionString command to ] commandsToTransitions :: StateMachine model cmd m resp -> Commands cmd resp@@ -438,7 +436,7 @@ let mprior' = case (mprior, mnew) of (Just (sprior, fprior), Just new) ->- Just (bimap sumElem sumElem (bimap (sprior :) (fprior :) (unzip new)))+ Just (bimap (sumElem . (sprior :)) (sumElem . (fprior :)) (unzip new)) (Nothing, Just new) -> Just (bimap sumElem sumElem (unzip new)) (Just prior, Nothing) -> Just prior (Nothing, Nothing) -> Nothing@@ -452,10 +450,8 @@ return mprior' where- parseMany :: String -> Maybe ([(Matrix Double, Matrix Double)])- parseMany = sequence- . map parse- . lines+ parseMany :: String -> Maybe [(Matrix Double, Matrix Double)]+ parseMany = mapM parse . lines parse :: String -> Maybe (Matrix Double, Matrix Double) parse = fmap (bimap fromLists fromLists) . readMaybe
src/Test/StateMachine/Parallel.hs view
@@ -87,7 +87,7 @@ import Data.Foldable (toList) import Data.List- (find, partition, permutations)+ (find, partition, permutations, foldl') import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe, mapMaybe)@@ -120,6 +120,7 @@ import Test.StateMachine.Types import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils+import qualified Text.PrettyPrint.ANSI.Leijen as PP ------------------------------------------------------------------------ @@ -241,13 +242,13 @@ return (ParallelCommands prefix (makeSuffixes (advanceModel sm initModel prefix) rest)) where- makeSuffixes :: model Symbolic -> Commands cmd resp -> [[(Commands cmd resp)]]+ makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]] makeSuffixes model0 = go model0 [] . unCommands where go :: model Symbolic- -> [[(Commands cmd resp)]]- -> [(Command cmd resp)]- -> [[(Commands cmd resp)]]+ -> [[Commands cmd resp]]+ -> [Command cmd resp]+ -> [[Commands cmd resp]] go _ acc [] = reverse acc go model acc cmds = go (advanceModel sm model (Commands safe)) (safes : acc)@@ -465,7 +466,7 @@ go' acc env shouldShrink (suffix : suffixes) = do (suffixWithShrinks, shrinkRest) <- shrinkOpts suffix (envFinal, suffix') <- snd $ foldl f (True, [(env,[])]) suffixWithShrinks- go' ((reverse suffix') : acc) envFinal shrinkRest suffixes+ go' (reverse suffix' : acc) envFinal shrinkRest suffixes where f :: (Bool, [(ValidateEnv model, [Commands cmd resp])])@@ -488,7 +489,7 @@ shrinks = if len == 0 then error "Invariant violation! A suffix should never be an empty list" else flip map [1..len] $ \n ->- (replicate (n - 1) DontShrink) ++ [MustShrink] ++ (replicate (len - n) DontShrink)+ replicate (n - 1) DontShrink ++ [MustShrink] ++ replicate (len - n) DontShrink in case shouldShrink of DontShrink -> [(zip dontShrink ls, DontShrink)] MustShrink -> fmap (\shrinkLs -> (zip shrinkLs ls, DontShrink)) shrinks@@ -815,11 +816,19 @@ mapM_ (\(h, _, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) histories where printCounterexample hist' (VFalse ce) = do- putStrLn ""- print (toBoxDrawings cmds hist')- putStrLn ""- print (simplify ce)- putStrLn ""+ PP.putDoc $+ mconcat+ [ PP.line+ , PP.string (show $ toBoxDrawings cmds hist')+ , PP.string (show $ simplify ce)+ , PP.line+ , PP.line+ , PP.string $+ if or [ boolean l | (_, _, l) <- histories]+ then "However, some repetitions of this sequence of commands passed. Maybe there is a race condition?"+ else "And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently"+ , PP.line+ ] case mGraphOptions of Nothing -> return () Just gOptions -> createAndPrintDot cmds gOptions hist'@@ -857,9 +866,18 @@ mapM_ (\(h, _, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l)) histories where printCounterexample hist' (VFalse ce) = do- putStrLn ""- print (simplify ce)- putStrLn ""+ PP.putDoc $+ mconcat+ [ PP.line+ , PP.string (show $ simplify ce)+ , PP.line+ , PP.line+ , PP.string $+ if or [ boolean l | (_, _, l) <- histories]+ then "However, some repetitions of this sequence of commands passed. Maybe there is a race condition?"+ else "And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently"+ , PP.line+ ] case mGraphOptions of Nothing -> return () Just gOptions -> createAndPrintDot cmds gOptions hist'@@ -885,9 +903,23 @@ foldMap (foldMap getAllUsedVars) suffixes toBoxDrawings'' :: Set Var -> History cmd resp -> Doc- toBoxDrawings'' knownVars (History h) = exec evT (fmap (out . snd) <$> Fork l p r)+ toBoxDrawings'' knownVars (History h) = mconcat+ ([ exec evT (fmap (out . snd) <$> Fork l p r)+ , PP.line+ , PP.line+ ]+ ++ map ppException exceptions+ ) where- (p, h') = partition (\e -> fst e == Pid 0) h+ (_, exceptions, h'') = foldl'+ (\(i, excs, evs) (pid, ev) ->+ case ev of+ Exception err -> (i + 1, excs ++ [(i, err)], evs ++ [(pid, Exception $ "Exception " <> show i)])+ _ -> (i, excs, evs ++ [(pid, ev)])+ )+ (0 :: Int, [], [])+ h+ (p, h') = partition (\e -> fst e == Pid 0) h'' (l, r) = partition (\e -> fst e == Pid 1) h' out :: HistoryEvent cmd resp -> String@@ -908,6 +940,15 @@ evT :: [(EventType, Pid)] evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h) + ppException :: (Int, String) -> Doc+ ppException (idx, err) = mconcat+ [ PP.string $ "Exception " <> show idx <> ":"+ , PP.line+ , PP.indent 2 $ PP.string err+ , PP.line+ , PP.line+ ]+ createAndPrintDot :: forall cmd resp t. Foldable t => Rank2.Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommandsF t cmd resp@@ -920,7 +961,7 @@ foldMap (foldMap getAllUsedVars) suffixes toDotGraph :: Set Var -> History cmd resp -> IO ()- toDotGraph knownVars (History h) = printDotGraph gOptions $ (fmap out) <$> (Rose (snd <$> prefixMessages) groupByPid)+ toDotGraph knownVars (History h) = printDotGraph gOptions $ fmap out <$> Rose (snd <$> prefixMessages) groupByPid where (prefixMessages, h') = partition (\e -> fst e == Pid 0) h alterF a Nothing = Just [a]
src/Test/StateMachine/Types.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleContexts #-}
src/Test/StateMachine/Types/References.hs view
@@ -91,8 +91,12 @@ where appPrec = 10 +deriving instance Eq a => Eq (Concrete a)+ instance Eq1 Concrete where liftEq eq (Concrete x) (Concrete y) = eq x y++deriving instance Ord a => Ord (Concrete a) instance Ord1 Concrete where liftCompare comp (Concrete x) (Concrete y) = comp x y
src/Test/StateMachine/Utils.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} ----------------------------------------------------------------------------- -- |@@ -40,8 +41,7 @@ import Prelude -import Control.Arrow- ((***))+import Data.Bifunctor (second) import Data.List (foldl') import Test.QuickCheck@@ -156,15 +156,15 @@ -- > == [ (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)+ map (second (,ys)) (pickOneReturnRest xs) +++ map (second (xs,)) (pickOneReturnRest ys) -- > 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)+pickOneReturnRest (x : xs) = (x, xs) : map (second (x :)) (pickOneReturnRest xs) -- > pickOneReturnRestL [[]] == [] -- > pickOneReturnRestL [[1]] == [(1,[[]])]@@ -174,13 +174,12 @@ -- > == [ (1,[[2],[3,4]]), (2,[[1],[3,4]]), (3,[[1,2],[4]]), (4,[[1,2],[3]]) ] pickOneReturnRestL :: [[a]] -> [(a, [[a]])] pickOneReturnRestL ls = concatMap- (\(prev, as, next) -> fmap (\(a, rest) -> (a, prev ++ [rest] ++ next)) $ pickOneReturnRest as)+ (\(prev, as, next) -> (\(a, rest) -> (a, prev ++ [rest] ++ next)) <$> pickOneReturnRest as) $ splitEach ls where splitEach :: [a] -> [([a], a, [a])] splitEach [] = []- splitEach (a : as) = fmap (\(prev, a', next) -> (prev, a', next)) $- go' [([], a, as)] ([], a, as)+ splitEach (a : as) = (\(prev, a', next) -> (prev, a', next)) <$> go' [([], a, as)] ([], a, as) where go' :: [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])] go' acc (_, _, []) = reverse acc@@ -196,4 +195,4 @@ where go m [] = m go m (Operation cmd resp _ : rest) = go (transition m cmd resp) rest- go m (Crash _ _ _ : rest) = go m rest+ go m (Crash {} : rest) = go m rest
src/Test/StateMachine/Z.hs view
@@ -63,6 +63,8 @@ ) where import qualified Data.List as L+import Data.Maybe+ (fromMaybe) import Prelude hiding (elem, notElem) import qualified Prelude as P@@ -272,7 +274,7 @@ -- | Application. (!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b-f ! x = maybe (error msg) Prelude.id (lookup x f)+f ! x = fromMaybe (error msg) (lookup x f) where msg = "!: failed to lookup `" ++ show x ++ "' in `" ++ show f ++ "'"
test/Spec.hs view
@@ -32,7 +32,6 @@ import Mock import Overflow import ProcessRegistry-import RQlite import qualified ShrinkingProps import SQLite import Test.StateMachine.Markov@@ -40,6 +39,9 @@ import TicketDispenser import qualified UnionFind +-- RQlite tests fail, see #14+import RQlite+ ------------------------------------------------------------------------ tests :: Bool -> TestTree@@ -218,9 +220,10 @@ (\io -> testProperty test (prop (snd <$> io))) | otherwise = testCase ("No docker, skipping: " ++ test) (return ()) - whenDocker docker test prop- | docker = prop- | otherwise = testCase ("No docker, skipping: " ++ test) (return ())+ -- Currently unused, see #14+ -- whenDocker docker test prop+ -- | docker = prop+ -- | otherwise = testCase ("No docker, skipping: " ++ test) (return ()) ------------------------------------------------------------------------