From 3e68b61069b1789aee758272b47c84fc9d8ee232 Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Tue, 2 Apr 2024 14:03:37 +0200 Subject: [PATCH 1/4] First draft of parallel state machine testing Co-authored-by: Joris Dral --- quickcheck-dynamic/quickcheck-dynamic.cabal | 1 + .../src/Test/QuickCheck/StateModel.hs | 218 +++++++++++++++++- 2 files changed, 217 insertions(+), 2 deletions(-) diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal index eabc03f5..cf412888 100644 --- a/quickcheck-dynamic/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic/quickcheck-dynamic.cabal @@ -81,6 +81,7 @@ library , base >=4.7 && <5 , containers , mtl + , io-classes , QuickCheck , random diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs index a09e5adf..a836915b 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs @@ -1,5 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} -- | Model-Based Testing library for use with Haskell QuickCheck. @@ -38,9 +39,12 @@ module Test.QuickCheck.StateModel ( computePrecondition, computeArbitraryAction, computeShrinkAction, + runParallelActions, + ParActions (..), ) where import Control.Monad +import Control.Monad.Class.MonadAsync import Control.Monad.Identity import Control.Monad.Reader import Control.Monad.State @@ -193,12 +197,18 @@ newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property, instance MonadTrans PostconditionM where lift = PostconditionM . lift +-- | Evaluate a postcondition in @PropertyM m@ and make the property fail if +-- postcondition results in @False@ evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m () -evaluatePostCondition post = do +evaluatePostCondition post = assert =<< evaluatePostCondition' post + +-- | Evaluate a postcondition in @PropertyM m@ and return the boolean result +evaluatePostCondition' :: Monad m => PostconditionM m Bool -> PropertyM m Bool +evaluatePostCondition' post = do (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post monitor mon unless b $ monitor onFail - assert b + pure b -- | Apply the property transformation to the property after evaluating -- the postcondition. Useful for collecting statistics while avoiding @@ -223,6 +233,8 @@ class (forall a. Show (Action state a), Monad m) => RunModel state m where -- a` instances from previous steps. perform :: Typeable a => state -> Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a)) + perform' :: Typeable a => Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a)) + -- | Postcondition on the `a` value produced at some step. -- The result is `assert`ed and will make the property fail should it be `False`. This is useful -- to check the implementation produces expected values. @@ -310,6 +322,26 @@ infix 5 := instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where getAllVariables (var := act) = Set.insert (Some var) $ getAllVariables (polarAction act) +{- + do action $ Inc + action $ Inc + action $ Inc + action $ Inc + action $ Inc + action $ Reset + action $ Inc + action $ Inc + action $ Inc + action $ Inc + pure () + do action $ Inc + pure () + do action $ Inc + pure () + +as = ParActions (Actions_ [] (Smart 0 [mkVar 0 := ActionWithPolarity Inc PosPolarity, mkVar 1 := ActionWithPolarity Inc PosPolarity, mkVar 2 := ActionWithPolarity Inc PosPolarity, mkVar 3 := ActionWithPolarity Inc PosPolarity, mkVar 4 := ActionWithPolarity Inc PosPolarity, mkVar 5 := ActionWithPolarity Reset PosPolarity, mkVar 6 := ActionWithPolarity Inc PosPolarity, mkVar 7 := ActionWithPolarity Inc PosPolarity, mkVar 8 := ActionWithPolarity Inc PosPolarity, mkVar 9 := ActionWithPolarity Inc PosPolarity])) [Actions_ [] (Smart 0 [mkVar 10 := ActionWithPolarity Inc PosPolarity]), Actions_ [] (Smart 0 [mkVar 11 := ActionWithPolarity Inc PosPolarity])] +-} + funName :: Polarity -> String funName PosPolarity = "action" funName _ = "failingAction" @@ -356,6 +388,7 @@ instance StateModel state => Show (Actions state) where let as' = WithUsedVars (usedVariables (Actions as)) <$> as in intercalate "\n" $ zipWith (++) ("do " : repeat " ") (map show as' ++ ["pure ()"]) + usedVariables :: forall state. StateModel state => Actions state -> VarContext usedVariables (Actions as) = go initialAnnotatedState as where @@ -585,3 +618,184 @@ runSteps s env ((v := act) : as) = do stateTransition = (underlyingState s, underlyingState s') monitor $ monitoring @state @m stateTransition action (lookUpVar env') ret pure (s', env', stateTransition) + +{------------------------------------------------------------------------------- + Parallel State Machines +-------------------------------------------------------------------------------} + +-- | A sequential prefix and some number of parallel suffixes +data ParActions state = ParActions (Actions state) [Actions state] + +instance StateModel state => Show (ParActions state) where + show (ParActions as ass) = + unlines $ [ "Sequential prefix" + , unlines $ map ('\t':) $ lines $ show as + , "Parallel suffixes" + ] + ++ (concatMap (\(idx, acts) -> [ [idx] <> ":" + , unlines $ map ('\t':) $ lines $ show acts + ]) + (zip ['a'..] ass)) + +-- | Existential on @a@ +data Performed m state where + Performed + :: (Typeable a, Eq (Action state a), Show (Action state a)) + => Var a + -> ActionWithPolarity state a + -> Either (Error state) (Realized m a) + -> Performed m state + +runParallelActions + :: forall state m e + . ( StateModel state + , RunModel state m + , e ~ Error state + , forall a. IsPerformResult e a + , MonadAsync m + ) + => ParActions state + -> PropertyM m () +runParallelActions (ParActions (Actions_ _ (Smart _ seqPrefix)) suffixes) = do + (env, seqPerformed) <- run $ runParallelSteps [] [] seqPrefix + results <- run $ mapConcurrently (\(Actions_ _ (Smart _ actions)) -> runParallelSteps env [] actions) suffixes + let possibleLinearizations = interleavings (env, seqPerformed) results + + hasOneSucceded <- + if null possibleLinearizations + then pure True + else + fmap or + . mapM (\(anEnv, anInterleaving) -> + snd <$> foldM (foldModel anEnv) (initialAnnotatedState, True) anInterleaving) + $ possibleLinearizations + assert hasOneSucceded + where + foldModel :: Env m + -> (Annotated state, Bool) + -> Performed m state + -> PropertyM m (Annotated state, Bool) + foldModel _ (s, False) _ = pure (s, False) + foldModel env (s, _) (Performed var act ret) = + case (polar, ret) of + (PosPolarity, Left err) -> + (s,) <$> positiveActionFailed err + (PosPolarity, Right val) -> do + positiveActionSucceeded val + (NegPolarity, _) -> do + negativeActionResult + where + action = polarAction act + polar = polarity act + + positiveActionFailed err = do + monitor $ + monitoringFailure @state @m + (underlyingState s) + action + (lookUpVar env) + err + pure False + + positiveActionSucceeded val = do + (s', stateTransition) <- computeNewState + b <- evaluatePostCondition' $ + postcondition + stateTransition + action + (lookUpVar env) + val + pure (s', b) + + negativeActionResult = do + (s', stateTransition) <- computeNewState + b <- evaluatePostCondition' $ + postconditionOnFailure + stateTransition + action + (lookUpVar env) + ret + pure (s', b) + + computeNewState = do + let s' = computeNextState s act var + stateTransition = (underlyingState s, underlyingState s') + monitor $ monitoring @state @m stateTransition action (lookUpVar env) ret + pure (s', stateTransition) + +runParallelSteps + :: forall state m e + . ( StateModel state + , RunModel state m + , e ~ Error state + , forall a. IsPerformResult e a + ) + => Env m + -> [Performed m state] + -> [Step state] + -> m (Env m, [Performed m state]) +runParallelSteps env rets [] = return (reverse env, reverse rets) +runParallelSteps env rets ((v := act) : as) = do + let action = polarAction act + (ret, env') <- runStep action + runParallelSteps env' (Performed v act ret:rets) as + where + runStep :: + forall a. Typeable a + => Action state a + -> m (Either (Error state) (Realized m a), Env m) + runStep action = do + ret :: Either (Error state) (Realized m a) <- performResultToEither <$> perform' action (lookUpVar env) + let var :: Var a + var = unsafeCoerceVar v + env' + | Right (val :: Realized m a) <- ret = (var :== val) : env + | otherwise = env + pure (ret, env') + +instance forall state. StateModel state => Arbitrary (ParActions state) where + arbitrary = do + (Actions_ rej (Smart _ allActions)) <- arbitrary + foo rej allActions + where + foo rej allActions = do + seqLength <- chooseInt (0, length allActions - 1) + let (prefix, suffix) = splitAt seqLength allActions + (suff1, suff2) = splitAt (length suffix `div` 2) suffix + f :: (state, Bool) -> Step state -> (state, Bool) + f (st, False) _ = (st, False) + f (st, b) (v := act) = + ( nextState st (polarAction act) v + , b && precondition st (polarAction act) + ) + if and + $ map (\anInterleaving -> snd $ foldl' f (initialState, True) anInterleaving) (interleaves [suff1, suff2]) + then pure (ParActions (Actions_ rej (Smart 0 prefix)) + [(Actions_ rej (Smart 0 suff1)), (Actions_ rej (Smart 0 suff2))]) + else foo rej allActions + +-- | Generate all possible interleavings. +-- +-- Note that the environment should be able to handle duplicates so we just +-- concat all environments together. +interleavings :: + (Env m, [Performed m state]) + -> [(Env m, [Performed m state])] + -> [(Env m, [Performed m state])] +interleavings (_, seqPrefix) parallelSuffixes = + let env = concat [ e | (e, _) <- parallelSuffixes ] + in map ((env,) . (seqPrefix ++)) $ interleaves $ map snd parallelSuffixes + +-- | All interleavings of a list of lists (preserving the relative order) +interleaves :: [[a]] -> [[a]] +interleaves [] = [] +interleaves [as] = [as] +interleaves (a:as) = foldl' (\b x -> concatMap (interleave x) b) [a] as + +-- | All interleavings of two lists (preserving the relative order) +interleave :: [a] -> [a] -> [[a]] +interleave [] [] = [] +interleave as [] = [as] +interleave [] bs = [bs] +interleave a@(ah:as) b@(bh:bs) = [ ah:arest | arest <- interleave as b ] + ++ [ bh:brest | brest <- interleave a bs ] From feb05fa169833e6277f8530d9d2b02e682d78b8e Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Tue, 2 Apr 2024 14:04:10 +0200 Subject: [PATCH 2/4] Add parallel test for Counter --- .../test/Test/QuickCheck/StateModelSpec.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs index 12add896..b6c19083 100644 --- a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs +++ b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs @@ -12,6 +12,8 @@ import Test.QuickCheck.Extras (runPropertyReaderT) import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick) import Test.QuickCheck.StateModel ( Actions, + ParActions, + runParallelActions, lookUpVarMaybe, mkVar, runActions, @@ -29,6 +31,7 @@ tests = testGroup "Running actions" [ testProperty "simple counter" $ prop_counter + , testProperty "par simple counter" $ prop_counter' , testProperty "returns final state updated from actions" prop_returnsFinalState , testProperty "environment variables indices are 1-based " prop_variablesIndicesAre1Based , testCase "prints distribution of actions and polarity" $ do @@ -51,6 +54,12 @@ prop_counter as = monadicIO $ do runPropertyReaderT (runActions as) ref assert True +prop_counter' :: ParActions Counter -> Property +prop_counter' as = monadicIO $ do + ref <- lift $ newIORef (0 :: Int) + runPropertyReaderT (runParallelActions as) ref + assert True + prop_returnsFinalState :: Actions SimpleCounter -> Property prop_returnsFinalState actions@(Actions as) = monadicIO $ do From 8b1b15ca4170a28aef9e1305271af3900d618e36 Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Tue, 2 Apr 2024 14:08:28 +0200 Subject: [PATCH 3/4] Some tentative adaptation of the tests --- .../test/Spec/DynamicLogic/Counters.hs | 27 ++++++++++++++----- .../test/Spec/DynamicLogic/RegistryModel.hs | 18 +++++++++++++ 2 files changed, 39 insertions(+), 6 deletions(-) diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs index aa68c99b..8bc2cd99 100644 --- a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs +++ b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs @@ -34,6 +34,10 @@ instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where ref <- ask lift $ atomicModifyIORef' ref (\count -> (succ count, count)) + perform' IncSimple _ = do + ref <- ask + lift $ atomicModifyIORef' ref (\count -> (succ count, count)) + -- A very simple model with a single action whose postcondition fails in a -- predictable way. This model is useful for testing the runtime. newtype FailingCounter = FailingCounter {failingCount :: Int} @@ -59,6 +63,10 @@ instance RunModel FailingCounter (ReaderT (IORef Int) IO) where ref <- ask lift $ atomicModifyIORef' ref (\count -> (succ count, count)) + perform' Inc' _ = do + ref <- ask + lift $ atomicModifyIORef' ref (\count -> (succ count, count)) + postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4 -- A generic but simple counter model @@ -84,14 +92,21 @@ instance StateModel Counter where instance RunModel Counter (ReaderT (IORef Int) IO) where perform _ Inc _ = do - ref <- ask - lift $ modifyIORef ref succ + ref <- ask + lift $ modifyIORef ref succ perform _ Reset _ = do + ref <- ask + lift $ do + n <- readIORef ref + writeIORef ref 0 + pure n + + perform' Inc _ = do + ref <- ask + lift $ atomicModifyIORef' ref ((,()) . succ) + perform' Reset _ = do ref <- ask - lift $ do - n <- readIORef ref - writeIORef ref 0 - pure n + lift $ atomicModifyIORef' ref (\n -> (0, n)) postcondition (Counter n, _) Reset _ res = pure $ n == res postcondition _ _ _ _ = pure True diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs index ce5ff0f5..fdbceafa 100644 --- a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs +++ b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs @@ -128,6 +128,24 @@ instance RunModel RegState RegM where lift $ threadDelay 100 pure $ Right () + perform' Spawn _ = do + tid <- lift $ forkIO (threadDelay 10000000) + pure $ Right tid + perform' (Register name tid) env = do + reg <- ask + lift $ try $ register reg name (env tid) + perform' (Unregister name) _ = do + reg <- ask + lift $ try $ unregister reg name + perform' (WhereIs name) _ = do + reg <- ask + res <- lift $ whereis reg name + pure $ Right res + perform' (KillThread tid) env = do + lift $ killThread (env tid) + lift $ threadDelay 100 + pure $ Right () + postcondition (s, _) (WhereIs name) env mtid = do pure $ (env <$> Map.lookup name (regs s)) == mtid postcondition _ _ _ _ = pure True From cfc4773fa0346b8b12b3ebeb65d037ff39647be9 Mon Sep 17 00:00:00 2001 From: Javier Sagredo Date: Tue, 2 Apr 2024 15:05:03 +0200 Subject: [PATCH 4/4] Formatters --- quickcheck-dynamic/quickcheck-dynamic.cabal | 2 +- .../src/Test/QuickCheck/StateModel.hs | 203 ++++++++++-------- .../test/Spec/DynamicLogic/Counters.hs | 14 +- .../test/Test/QuickCheck/StateModelSpec.hs | 2 +- 4 files changed, 118 insertions(+), 103 deletions(-) diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal index cf412888..3a0a7385 100644 --- a/quickcheck-dynamic/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic/quickcheck-dynamic.cabal @@ -80,8 +80,8 @@ library build-depends: , base >=4.7 && <5 , containers - , mtl , io-classes + , mtl , QuickCheck , random diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs index a836915b..f626d5a4 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs @@ -388,7 +388,6 @@ instance StateModel state => Show (Actions state) where let as' = WithUsedVars (usedVariables (Actions as)) <$> as in intercalate "\n" $ zipWith (++) ("do " : repeat " ") (map show as' ++ ["pure ()"]) - usedVariables :: forall state. StateModel state => Actions state -> VarContext usedVariables (Actions as) = go initialAnnotatedState as where @@ -628,14 +627,19 @@ data ParActions state = ParActions (Actions state) [Actions state] instance StateModel state => Show (ParActions state) where show (ParActions as ass) = - unlines $ [ "Sequential prefix" - , unlines $ map ('\t':) $ lines $ show as - , "Parallel suffixes" - ] - ++ (concatMap (\(idx, acts) -> [ [idx] <> ":" - , unlines $ map ('\t':) $ lines $ show acts - ]) - (zip ['a'..] ass)) + unlines $ + [ "Sequential prefix" + , unlines $ map ('\t' :) $ lines $ show as + , "Parallel suffixes" + ] + ++ ( concatMap + ( \(idx, acts) -> + [ [idx] <> ":" + , unlines $ map ('\t' :) $ lines $ show acts + ] + ) + (zip ['a' ..] ass) + ) -- | Existential on @a@ data Performed m state where @@ -663,65 +667,70 @@ runParallelActions (ParActions (Actions_ _ (Smart _ seqPrefix)) suffixes) = do hasOneSucceded <- if null possibleLinearizations - then pure True - else - fmap or - . mapM (\(anEnv, anInterleaving) -> - snd <$> foldM (foldModel anEnv) (initialAnnotatedState, True) anInterleaving) - $ possibleLinearizations + then pure True + else + fmap or + . mapM + ( \(anEnv, anInterleaving) -> + snd <$> foldM (foldModel anEnv) (initialAnnotatedState, True) anInterleaving + ) + $ possibleLinearizations assert hasOneSucceded - where - foldModel :: Env m - -> (Annotated state, Bool) - -> Performed m state - -> PropertyM m (Annotated state, Bool) - foldModel _ (s, False) _ = pure (s, False) - foldModel env (s, _) (Performed var act ret) = - case (polar, ret) of - (PosPolarity, Left err) -> - (s,) <$> positiveActionFailed err - (PosPolarity, Right val) -> do - positiveActionSucceeded val - (NegPolarity, _) -> do - negativeActionResult - where - action = polarAction act - polar = polarity act - - positiveActionFailed err = do - monitor $ - monitoringFailure @state @m - (underlyingState s) - action - (lookUpVar env) - err - pure False - - positiveActionSucceeded val = do - (s', stateTransition) <- computeNewState - b <- evaluatePostCondition' $ - postcondition - stateTransition - action - (lookUpVar env) - val - pure (s', b) - - negativeActionResult = do - (s', stateTransition) <- computeNewState - b <- evaluatePostCondition' $ - postconditionOnFailure - stateTransition - action - (lookUpVar env) - ret - pure (s', b) - - computeNewState = do - let s' = computeNextState s act var - stateTransition = (underlyingState s, underlyingState s') - monitor $ monitoring @state @m stateTransition action (lookUpVar env) ret - pure (s', stateTransition) + where + foldModel + :: Env m + -> (Annotated state, Bool) + -> Performed m state + -> PropertyM m (Annotated state, Bool) + foldModel _ (s, False) _ = pure (s, False) + foldModel env (s, _) (Performed var act ret) = + case (polar, ret) of + (PosPolarity, Left err) -> + (s,) <$> positiveActionFailed err + (PosPolarity, Right val) -> do + positiveActionSucceeded val + (NegPolarity, _) -> do + negativeActionResult + where + action = polarAction act + polar = polarity act + + positiveActionFailed err = do + monitor $ + monitoringFailure @state @m + (underlyingState s) + action + (lookUpVar env) + err + pure False + + positiveActionSucceeded val = do + (s', stateTransition) <- computeNewState + b <- + evaluatePostCondition' $ + postcondition + stateTransition + action + (lookUpVar env) + val + pure (s', b) + + negativeActionResult = do + (s', stateTransition) <- computeNewState + b <- + evaluatePostCondition' $ + postconditionOnFailure + stateTransition + action + (lookUpVar env) + ret + pure (s', b) + + computeNewState = do + let s' = computeNextState s act var + stateTransition = (underlyingState s, underlyingState s') + monitor $ monitoring @state @m stateTransition action (lookUpVar env) ret + pure (s', stateTransition) runParallelSteps :: forall state m e @@ -738,20 +747,21 @@ runParallelSteps env rets [] = return (reverse env, reverse rets) runParallelSteps env rets ((v := act) : as) = do let action = polarAction act (ret, env') <- runStep action - runParallelSteps env' (Performed v act ret:rets) as + runParallelSteps env' (Performed v act ret : rets) as where - runStep :: - forall a. Typeable a + runStep + :: forall a + . Typeable a => Action state a -> m (Either (Error state) (Realized m a), Env m) runStep action = do - ret :: Either (Error state) (Realized m a) <- performResultToEither <$> perform' action (lookUpVar env) - let var :: Var a - var = unsafeCoerceVar v - env' - | Right (val :: Realized m a) <- ret = (var :== val) : env - | otherwise = env - pure (ret, env') + ret :: Either (Error state) (Realized m a) <- performResultToEither <$> perform' action (lookUpVar env) + let var :: Var a + var = unsafeCoerceVar v + env' + | Right (val :: Realized m a) <- ret = (var :== val) : env + | otherwise = env + pure (ret, env') instance forall state. StateModel state => Arbitrary (ParActions state) where arbitrary = do @@ -768,34 +778,39 @@ instance forall state. StateModel state => Arbitrary (ParActions state) where ( nextState st (polarAction act) v , b && precondition st (polarAction act) ) - if and - $ map (\anInterleaving -> snd $ foldl' f (initialState, True) anInterleaving) (interleaves [suff1, suff2]) - then pure (ParActions (Actions_ rej (Smart 0 prefix)) - [(Actions_ rej (Smart 0 suff1)), (Actions_ rej (Smart 0 suff2))]) - else foo rej allActions + if and $ + map (\anInterleaving -> snd $ foldl' f (initialState, True) anInterleaving) (interleaves [suff1, suff2]) + then + pure + ( ParActions + (Actions_ rej (Smart 0 prefix)) + [(Actions_ rej (Smart 0 suff1)), (Actions_ rej (Smart 0 suff2))] + ) + else foo rej allActions -- | Generate all possible interleavings. -- -- Note that the environment should be able to handle duplicates so we just -- concat all environments together. -interleavings :: - (Env m, [Performed m state]) +interleavings + :: (Env m, [Performed m state]) -> [(Env m, [Performed m state])] -> [(Env m, [Performed m state])] interleavings (_, seqPrefix) parallelSuffixes = - let env = concat [ e | (e, _) <- parallelSuffixes ] - in map ((env,) . (seqPrefix ++)) $ interleaves $ map snd parallelSuffixes + let env = concat [e | (e, _) <- parallelSuffixes] + in map ((env,) . (seqPrefix ++)) $ interleaves $ map snd parallelSuffixes -- | All interleavings of a list of lists (preserving the relative order) interleaves :: [[a]] -> [[a]] -interleaves [] = [] -interleaves [as] = [as] -interleaves (a:as) = foldl' (\b x -> concatMap (interleave x) b) [a] as +interleaves [] = [] +interleaves [as] = [as] +interleaves (a : as) = foldl' (\b x -> concatMap (interleave x) b) [a] as -- | All interleavings of two lists (preserving the relative order) interleave :: [a] -> [a] -> [[a]] -interleave [] [] = [] -interleave as [] = [as] -interleave [] bs = [bs] -interleave a@(ah:as) b@(bh:bs) = [ ah:arest | arest <- interleave as b ] - ++ [ bh:brest | brest <- interleave a bs ] +interleave [] [] = [] +interleave as [] = [as] +interleave [] bs = [bs] +interleave a@(ah : as) b@(bh : bs) = + [ah : arest | arest <- interleave as b] + ++ [bh : brest | brest <- interleave a bs] diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs index 8bc2cd99..f72f3bac 100644 --- a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs +++ b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs @@ -92,14 +92,14 @@ instance StateModel Counter where instance RunModel Counter (ReaderT (IORef Int) IO) where perform _ Inc _ = do - ref <- ask - lift $ modifyIORef ref succ + ref <- ask + lift $ modifyIORef ref succ perform _ Reset _ = do - ref <- ask - lift $ do - n <- readIORef ref - writeIORef ref 0 - pure n + ref <- ask + lift $ do + n <- readIORef ref + writeIORef ref 0 + pure n perform' Inc _ = do ref <- ask diff --git a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs index b6c19083..701cce89 100644 --- a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs +++ b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs @@ -13,10 +13,10 @@ import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick) import Test.QuickCheck.StateModel ( Actions, ParActions, - runParallelActions, lookUpVarMaybe, mkVar, runActions, + runParallelActions, underlyingState, viewAtType, pattern Actions,