diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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); diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal --- a/quickcheck-state-machine.cabal +++ b/quickcheck-state-machine.cabal @@ -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 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 diff --git a/src/Test/StateMachine/BoxDrawer.hs b/src/Test/StateMachine/BoxDrawer.hs --- a/src/Test/StateMachine/BoxDrawer.hs +++ b/src/Test/StateMachine/BoxDrawer.hs @@ -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) diff --git a/src/Test/StateMachine/DotDrawing.hs b/src/Test/StateMachine/DotDrawing.hs --- a/src/Test/StateMachine/DotDrawing.hs +++ b/src/Test/StateMachine/DotDrawing.hs @@ -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)] diff --git a/src/Test/StateMachine/Lockstep/Auxiliary.hs b/src/Test/StateMachine/Lockstep/Auxiliary.hs --- a/src/Test/StateMachine/Lockstep/Auxiliary.hs +++ b/src/Test/StateMachine/Lockstep/Auxiliary.hs @@ -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) diff --git a/src/Test/StateMachine/Lockstep/NAry.hs b/src/Test/StateMachine/Lockstep/NAry.hs --- a/src/Test/StateMachine/Lockstep/NAry.hs +++ b/src/Test/StateMachine/Lockstep/NAry.hs @@ -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 diff --git a/src/Test/StateMachine/Lockstep/Simple.hs b/src/Test/StateMachine/Lockstep/Simple.hs --- a/src/Test/StateMachine/Lockstep/Simple.hs +++ b/src/Test/StateMachine/Lockstep/Simple.hs @@ -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) diff --git a/src/Test/StateMachine/Markov.hs b/src/Test/StateMachine/Markov.hs --- a/src/Test/StateMachine/Markov.hs +++ b/src/Test/StateMachine/Markov.hs @@ -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 diff --git a/src/Test/StateMachine/Parallel.hs b/src/Test/StateMachine/Parallel.hs --- a/src/Test/StateMachine/Parallel.hs +++ b/src/Test/StateMachine/Parallel.hs @@ -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] diff --git a/src/Test/StateMachine/Types.hs b/src/Test/StateMachine/Types.hs --- a/src/Test/StateMachine/Types.hs +++ b/src/Test/StateMachine/Types.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleContexts #-} diff --git a/src/Test/StateMachine/Types/References.hs b/src/Test/StateMachine/Types/References.hs --- a/src/Test/StateMachine/Types/References.hs +++ b/src/Test/StateMachine/Types/References.hs @@ -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 diff --git a/src/Test/StateMachine/Utils.hs b/src/Test/StateMachine/Utils.hs --- a/src/Test/StateMachine/Utils.hs +++ b/src/Test/StateMachine/Utils.hs @@ -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 diff --git a/src/Test/StateMachine/Z.hs b/src/Test/StateMachine/Z.hs --- a/src/Test/StateMachine/Z.hs +++ b/src/Test/StateMachine/Z.hs @@ -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 ++ "'" diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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 ()) ------------------------------------------------------------------------