Introduce a QuickCheck-style MoreActions type modifier to make it easier to increase the number of actions on average in tests (#84)

MaximilianAlgehed · UlfNorell · web-flow · commit 071092c90c36 · 2024-10-24T10:48:29.000+02:00
* Initial stab at `getMoreActions` as a way to get bigger tests

* Add a test to make sure MoreActions actually introduces a reasonable
number of long sequences

* Exports and documentation

* simplify the design

* Fix some warnings

* Better name for property

* refactor arbActions to make sure it's tail recursive

* More tracking of action sequences + work on profiling to figure out
what's slow

* Correct log computation for bucketing

* React to comments from Arnaud and Ulf

* Nicer bucketing for action sequence lengths

* Work-around for tabulate performance issue in quickcheck

* Note in changelog

* fourmoulu

---------

Co-authored-by: Ulf Norell &lt;ulf.norell@gmail.com&gt;
diff --git a/quickcheck-dynamic/CHANGELOG.md b/quickcheck-dynamic/CHANGELOG.md
@@ -20,6 +20,7 @@ changes.
     ```
 * **BREAKING**: Moved `Error state` from `StateModel` to `RunModel` and indexed it on both the `state` and the monad `m`
 * **BREAKING**: Changed `PerformResult` from `PerformResult (Error state) a` to `PerformResult state m a`
+* Added a `moreActions` property modifier to allow controlling the length of action sequences.
 
 ## 3.4.1 - 2024-03-22
 
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
@@ -1,5 +1,7 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | Model-Based Testing library for use with Haskell QuickCheck.
@@ -25,6 +27,7 @@ module Test.QuickCheck.StateModel (
   Env,
   Generic,
   IsPerformResult,
+  Options (..),
   monitorPost,
   counterexamplePost,
   stateAfter,
@@ -37,6 +40,10 @@ module Test.QuickCheck.StateModel (
   computePrecondition,
   computeArbitraryAction,
   computeShrinkAction,
+  generateActionsWithOptions,
+  shrinkActionsWithOptions,
+  defaultOptions,
+  moreActions,
 ) where
 
 import Control.Monad
@@ -358,56 +365,100 @@ usedVariables (Actions as) = go initialAnnotatedState as
         <> go (computeNextState aState act var) steps
 
 instance forall state. StateModel state => Arbitrary (Actions state) where
-  arbitrary = do
-    (as, rejected) <- arbActions initialAnnotatedState 1
-    return $ Actions_ rejected (Smart 0 as)
-    where
-      arbActions :: Annotated state -> Int -> Gen ([Step state], [String])
-      arbActions s step = sized $ \n ->
-        let w = n `div` 2 + 1
-         in frequency
-              [ (1, return ([], []))
-              ,
-                ( w
-                , do
-                    (mact, rej) <- satisfyPrecondition
-                    case mact of
-                      Just (Some act@ActionWithPolarity{}) -> do
-                        let var = mkVar step
-                        (as, rejected) <- arbActions (computeNextState s act var) (step + 1)
-                        return ((var := act) : as, rej ++ rejected)
-                      Nothing ->
-                        return ([], [])
-                )
-              ]
-        where
-          satisfyPrecondition = sized $ \n -> go n (2 * n) [] -- idea copied from suchThatMaybe
-          go m n rej
-            | m > n = return (Nothing, rej)
-            | otherwise = do
-                a <- resize m $ computeArbitraryAction s
-                case a of
-                  Some act ->
-                    if computePrecondition s act
-                      then return (Just (Some act), rej)
-                      else go (m + 1) n (actionName (polarAction act) : rej)
-
-  shrink (Actions_ rs as) =
-    map (Actions_ rs) (shrinkSmart (map (prune . map fst) . concatMap customActionsShrinker . shrinkList shrinker . withStates) as)
-    where
-      shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]
-      shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act'@ActionWithPolarity{} <- computeShrinkAction s act]
-
-      customActionsShrinker :: [(Step state, Annotated state)] -> [[(Step state, Annotated state)]]
-      customActionsShrinker acts =
-        let usedVars = mconcat [getAllVariables a <> getAllVariables (underlyingState s) | (_ := a, s) <- acts]
-            binding (v := _, _) = Some v `Set.member` usedVars
-            -- Remove at most one non-binding action
-            go [] = [[]]
-            go (p : ps)
-              | binding p = map (p :) (go ps)
-              | otherwise = ps : map (p :) (go ps)
-         in go acts
+  arbitrary = generateActionsWithOptions defaultOptions
+  shrink = shrinkActionsWithOptions defaultOptions
+
+data QCDProperty state = QCDProperty
+  { runQCDProperty :: Actions state -> Property
+  , qcdPropertyOptions :: Options state
+  }
+
+instance StateModel state => Testable (QCDProperty state) where
+  property QCDProperty{..} =
+    forAllShrink
+      (generateActionsWithOptions qcdPropertyOptions)
+      (shrinkActionsWithOptions qcdPropertyOptions)
+      runQCDProperty
+
+class QCDProp state p | p -> state where
+  qcdProperty :: p -> QCDProperty state
+
+instance QCDProp state (QCDProperty state) where
+  qcdProperty = id
+
+instance Testable p => QCDProp state (Actions state -> p) where
+  qcdProperty p = QCDProperty (property . p) defaultOptions
+
+modifyOptions :: QCDProperty state -> (Options state -> Options state) -> QCDProperty state
+modifyOptions p f =
+  let opts = qcdPropertyOptions p
+   in p{qcdPropertyOptions = f opts}
+
+moreActions :: QCDProp state p => Rational -> p -> QCDProperty state
+moreActions r p =
+  modifyOptions (qcdProperty p) $ \opts -> opts{actionLengthMultiplier = actionLengthMultiplier opts * r}
+
+-- NOTE: indexed on state for forwards compatibility, e.g. when we
+-- want to give an explicit initial state
+data Options state = Options {actionLengthMultiplier :: Rational}
+
+defaultOptions :: Options state
+defaultOptions = Options{actionLengthMultiplier = 1}
+
+-- | Generate arbitrary actions with the `GenActionsOptions`. More flexible than using the type-based
+-- modifiers.
+generateActionsWithOptions :: forall state. StateModel state => Options state -> Gen (Actions state)
+generateActionsWithOptions Options{..} = do
+  (as, rejected) <- arbActions [] [] initialAnnotatedState 1
+  return $ Actions_ rejected (Smart 0 as)
+  where
+    arbActions :: [Step state] -> [String] -> Annotated state -> Int -> Gen ([Step state], [String])
+    arbActions steps rejected s step = sized $ \n -> do
+      let w = round (actionLengthMultiplier * fromIntegral n) `div` 2 + 1
+      continue <- frequency [(1, pure False), (w, pure True)]
+      if continue
+        then do
+          (mact, rej) <- satisfyPrecondition
+          case mact of
+            Just (Some act@ActionWithPolarity{}) -> do
+              let var = mkVar step
+              arbActions
+                ((var := act) : steps)
+                (rej ++ rejected)
+                (computeNextState s act var)
+                (step + 1)
+            Nothing ->
+              return (reverse steps, rejected)
+        else return (reverse steps, rejected)
+      where
+        satisfyPrecondition = sized $ \n -> go n (2 * n) [] -- idea copied from suchThatMaybe
+        go m n rej
+          | m > n = return (Nothing, rej)
+          | otherwise = do
+              a <- resize m $ computeArbitraryAction s
+              case a of
+                Some act ->
+                  if computePrecondition s act
+                    then return (Just (Some act), rej)
+                    else go (m + 1) n (actionName (polarAction act) : rej)
+
+shrinkActionsWithOptions :: forall state. StateModel state => Options state -> Actions state -> [Actions state]
+shrinkActionsWithOptions _ (Actions_ rs as) =
+  map (Actions_ rs) (shrinkSmart (map (prune . map fst) . concatMap customActionsShrinker . shrinkList shrinker . withStates) as)
+  where
+    shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]
+    shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act'@ActionWithPolarity{} <- computeShrinkAction s act]
+
+    customActionsShrinker :: [(Step state, Annotated state)] -> [[(Step state, Annotated state)]]
+    customActionsShrinker acts =
+      let usedVars = mconcat [getAllVariables a <> getAllVariables (underlyingState s) | (_ := a, s) <- acts]
+          binding (v := _, _) = Some v `Set.member` usedVars
+          -- Remove at most one non-binding action
+          go [] = [[]]
+          go (p : ps)
+            | binding p = map (p :) (go ps)
+            | otherwise = ps : map (p :) (go ps)
+       in go acts
 
 -- Running state models
 
@@ -498,14 +549,25 @@ runActions
   => Actions state
   -> PropertyM m (Annotated state, Env)
 runActions (Actions_ rejected (Smart _ actions)) = do
-  (finalState, env) <- runSteps initialAnnotatedState [] actions
+  let bucket = \n -> let (a, b) = go n in show a ++ " - " ++ show b
+        where
+          go n
+            | n < 100 = (d * 10, d * 10 + 9)
+            | otherwise = let (a, b) = go d in (a * 10, b * 10 + 9)
+            where
+              d = div n 10
+  monitor $ tabulate "# of actions" [show $ bucket $ length actions]
+  (finalState, env, names, polars) <- runSteps initialAnnotatedState [] actions
+  monitor $ tabulate "Actions" names
+  monitor $ tabulate "Action polarity" $ map show polars
   unless (null rejected) $
     monitor $
       tabulate "Actions rejected by precondition" rejected
   return (finalState, env)
 
--- | Core function to execute a sequence of `Step` given some initial `Env`ironment
--- and `Annotated` state.
+-- | Core function to execute a sequence of `Step` given some initial `Env`ironment and `Annotated`
+-- state. Return the list of action names and polarities to work around
+-- https://github.com/nick8325/quickcheck/issues/416 causing repeated calls to tabulate being slow.
 runSteps
   :: forall state m e
    . ( StateModel state
@@ -516,23 +578,23 @@ runSteps
   => Annotated state
   -> Env
   -> [Step state]
-  -> PropertyM m (Annotated state, Env)
-runSteps s env [] = return (s, reverse env)
+  -> PropertyM m (Annotated state, Env, [String], [Polarity])
+runSteps s env [] = return (s, reverse env, [], [])
 runSteps s env ((v := act) : as) = do
   pre $ computePrecondition s act
   ret <- run $ performResultToEither <$> perform (underlyingState s) action (lookUpVar env)
   let name = show polar ++ actionName action
-  monitor $ tabulate "Actions" [name]
-  monitor $ tabulate "Action polarity" [show polar]
   case (polar, ret) of
     (PosPolarity, Left err) ->
       positiveActionFailed err
     (PosPolarity, Right val) -> do
       (s', env') <- positiveActionSucceeded ret val
-      runSteps s' env' as
+      (s'', env'', names, polars) <- runSteps s' env' as
+      pure (s'', env'', name : names, polar : polars)
     (NegPolarity, _) -> do
       (s', env') <- negativeActionResult ret
-      runSteps s' env' as
+      (s'', env'', names, polars) <- runSteps s' env' as
+      pure (s'', env'', name : names, polar : polars)
   where
     polar = polarity act
 
diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
@@ -55,30 +55,31 @@ instance StateModel RegState where
   validFailingAction _ _ = True
 
   arbitraryAction ctx s =
-    frequency $
-      [
-        ( max 1 $ 10 - length (ctxAtType @ThreadId ctx)
-        , return $ Some Spawn
-        )
-      ,
-        ( 2 * Map.size (regs s)
-        , Some <$> (Unregister <$> probablyRegistered s)
-        )
-      ,
-        ( 10
-        , Some <$> (WhereIs <$> probablyRegistered s)
-        )
-      ]
-        ++ [ ( max 1 $ 3 - length (dead s)
-             , Some <$> (KillThread <$> arbitraryVar ctx)
-             )
-           | not . null $ ctxAtType @ThreadId ctx
-           ]
-        ++ [ ( max 1 $ 10 - Map.size (regs s)
-             , Some <$> (Register <$> probablyUnregistered s <*> arbitraryVar ctx)
-             )
-           | not . null $ ctxAtType @ThreadId ctx
-           ]
+    let threadIdCtx = ctxAtType @ThreadId ctx
+     in frequency $
+          [
+            ( max 1 $ 10 - length threadIdCtx
+            , return $ Some Spawn
+            )
+          ,
+            ( 2 * Map.size (regs s)
+            , Some <$> (Unregister <$> probablyRegistered s)
+            )
+          ,
+            ( 10
+            , Some <$> (WhereIs <$> probablyRegistered s)
+            )
+          ]
+            ++ [ ( max 1 $ 3 - length (dead s)
+                 , Some <$> (KillThread <$> arbitraryVar ctx)
+                 )
+               | not . null $ threadIdCtx
+               ]
+            ++ [ ( max 1 $ 10 - Map.size (regs s)
+                 , Some <$> (Register <$> probablyUnregistered s <*> arbitraryVar ctx)
+                 )
+               | not . null $ threadIdCtx
+               ]
 
   shrinkAction ctx _ (Register name tid) =
     [Some (Unregister name)]
@@ -267,6 +268,7 @@ tests =
   testGroup
     "registry model example"
     [ testProperty "prop_Registry" $ prop_Registry
+    , testProperty "moreActions 10 $ prop_Registry" $ moreActions 10 prop_Registry
     , testProperty "canRegister" $ propDL canRegister
     , testProperty "canRegisterNoUnregister" $ expectFailure $ propDL canRegisterNoUnregister
     ]
diff --git a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs
@@ -7,13 +7,14 @@ import Control.Monad.Reader (lift)
 import Data.IORef (newIORef)
 import Data.List (isInfixOf)
 import Spec.DynamicLogic.Counters (Counter (..), FailingCounter, SimpleCounter (..))
-import Test.QuickCheck (Property, Result (..), Testable, chatty, choose, counterexample, noShrinking, property, stdArgs)
+import Test.QuickCheck (Property, Result (..), Testable, chatty, checkCoverage, choose, counterexample, cover, noShrinking, property, stdArgs)
 import Test.QuickCheck.Extras (runPropertyReaderT)
 import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick)
 import Test.QuickCheck.StateModel (
   Actions,
   lookUpVarMaybe,
   mkVar,
+  moreActions,
   runActions,
   underlyingState,
   viewAtType,
@@ -29,6 +30,7 @@ tests =
   testGroup
     "Running actions"
     [ testProperty "simple counter" $ prop_counter
+    , testProperty "simple_counter_moreActions" $ moreActions 30 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
@@ -38,6 +40,9 @@ tests =
     , testCase "prints counterexample as sequence of steps when postcondition fails" $ do
         Failure{output} <- captureTerminal prop_failsOnPostcondition
         "do action $ Inc'" `isInfixOf` output @? "Output does not contain \"do action $ Inc'\": " <> output
+    , testProperty
+        "moreActions introduces long sequences of actions"
+        prop_longSequences
     ]
 
 captureTerminal :: Testable p => p -> IO Result
@@ -79,3 +84,7 @@ prop_failsOnPostcondition actions =
     ref <- lift $ newIORef (0 :: Int)
     runPropertyReaderT (runActions actions) ref
     assert True
+
+prop_longSequences :: Property
+prop_longSequences =
+  checkCoverage $ moreActions 10 $ \(Actions steps :: Actions SimpleCounter) -> cover 50 (100 < length steps) "Long sequences" True
