Initial stab at parallel actions

Author: MaximilianAlgehed

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -27,6 +27,9 @@ source-repository head
   type:     git
   location: https://github.com/input-output-hk/quickcheck-dynamic
 
+flag dev
+  default: False
+
 common lang
   default-language:   Haskell2010
   default-extensions:
@@ -62,6 +65,7 @@ common lang
     -Wall -Wnoncanonical-monad-instances -Wunused-packages
     -Wincomplete-uni-patterns -Wincomplete-record-updates
     -Wredundant-constraints -Widentities -Wno-unused-do-bind
+    -Wno-name-shadowing -Wno-x-partial
 
 library
   import:          lang
@@ -76,6 +80,23 @@ library
     Test.QuickCheck.Extras
     Test.QuickCheck.StateModel
     Test.QuickCheck.StateModel.Variables
+    Test.QuickCheck.ParallelActions
+
+  if flag(dev)
+    hs-source-dirs: test
+    exposed-modules:
+      Spec.DynamicLogic.Counters
+      Spec.DynamicLogic.Registry
+      Spec.DynamicLogic.RegistryModel
+      Test.QuickCheck.DynamicLogic.QuantifySpec
+      Test.QuickCheck.StateModelSpec
+    build-depends:
+      , io-classes
+      , io-sim
+      , stm
+      , tasty
+      , tasty-hunit
+      , tasty-quickcheck
 
   build-depends:
     , base        >=4.7 && <5
@@ -100,6 +121,8 @@ test-suite quickcheck-dynamic-test
   build-depends:
     , base
     , containers
+    , io-classes
+    , io-sim
     , mtl
     , QuickCheck
     , quickcheck-dynamic

quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs

@@ -60,10 +60,10 @@ instance Monad (DL s) where
 instance MonadFail (DL s) where
   fail = errorDL
 
-action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
+action :: (Typeable a, Show a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
 action cmd = DL $ \_ k -> DL.after cmd k
 
-failingAction :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
+failingAction :: (Typeable a, Show a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
 failingAction cmd = DL $ \_ k -> DL.afterNegative cmd (k ())
 
 anyAction :: DL s ()
@@ -96,7 +96,7 @@ getModelStateDL = DL $ \s k -> k (underlyingState s) s
 getVarContextDL :: DL s VarContext
 getVarContextDL = DL $ \s k -> k (vars s) s
 
-forAllVar :: forall a s. Typeable a => DL s (Var a)
+forAllVar :: forall a s. (Typeable a, Show a) => DL s (Var a)
 forAllVar = do
   xs <- ctxAtType <$> getVarContextDL
   forAllQ $ elementsQ xs

quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs

@@ -33,7 +33,7 @@ data DynLogic s
     Stopping (DynLogic s)
   | -- | After a specific action the predicate should hold
     forall a.
-    (Eq (Action s a), Show (Action s a), Typeable a) =>
+    (Eq (Action s a), Show (Action s a), Typeable a, Show a) =>
     After (ActionWithPolarity s a) (Var a -> DynPred s)
   | Error String (DynPred s)
   | -- | Adjust the probability of picking a branch
@@ -66,7 +66,7 @@ afterAny :: (Annotated s -> DynFormula s) -> DynFormula s
 afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f s) n
 
 afterPolar
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => ActionWithPolarity s a
   -> (Var a -> Annotated s -> DynFormula s)
   -> DynFormula s
@@ -75,7 +75,7 @@ afterPolar act f = DynFormula $ \n -> After act $ \x s -> unDynFormula (f x s) n
 -- | Given `f` must be `True` after /some/ action.
 -- `f` is passed the state resulting from executing the `Action`.
 after
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => Action s a
   -> (Var a -> Annotated s -> DynFormula s)
   -> DynFormula s
@@ -85,7 +85,7 @@ after act f = afterPolar (ActionWithPolarity act PosPolarity) f
 -- `f` is passed the state resulting from executing the `Action`
 -- as a negative action.
 afterNegative
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Show a, Eq (Action s a), Show (Action s a))
   => Action s a
   -> (Annotated s -> DynFormula s)
   -> DynFormula s
@@ -592,9 +592,11 @@ keepTryingUntil n g p = do
 shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s]
 shrinkDLTest _ (Looping _) = []
 shrinkDLTest d tc =
-  [ test | as' <- shrinkScript d (getScript tc), let pruned = pruneDLTest d as'
-                                                     test = makeTestFromPruned d pruned,
-  -- Don't shrink a non-executable test case to an executable one.
+  [ test
+  | as' <- shrinkScript d (getScript tc)
+  , let pruned = pruneDLTest d as'
+        test = makeTestFromPruned d pruned
+  , -- Don't shrink a non-executable test case to an executable one.
   case (tc, test) of
     (DLScript _, _) -> True
     (_, DLScript _) -> False
@@ -619,10 +621,10 @@ shrinkScript = shrink' initialAnnotatedState
       [TestSeqStep (unsafeCoerceVar var := act') ss | Some act'@ActionWithPolarity{} <- computeShrinkAction s act]
         ++ [ TestSeqStep step ss'
            | ss' <-
-              shrink'
-                (nextStateStep step s)
-                (stepDLStep d s step)
-                ss
+               shrink'
+                 (nextStateStep step s)
+                 (stepDLStep d s step)
+                 ss
            ]
     nonstructural _ _ TestSeqStop = []
 

quickcheck-dynamic/src/Test/QuickCheck/Extras.hs

@@ -2,6 +2,7 @@ module Test.QuickCheck.Extras where
 
 import Control.Monad.Reader
 import Control.Monad.State
+import Test.QuickCheck
 import Test.QuickCheck.Monadic
 
 runPropertyStateT :: Monad m => PropertyM (StateT s m) a -> s -> PropertyM m (a, s)
@@ -13,3 +14,9 @@ runPropertyReaderT :: Monad m => PropertyM (ReaderT e m) a -> e -> PropertyM m a
 runPropertyReaderT p e = MkPropertyM $ \k -> do
   m <- unPropertyM p $ fmap lift . k
   return $ runReaderT m e
+
+sometimes :: Testable p => Int -> p -> Property
+sometimes i = disjoin . replicate i
+
+always :: Testable p => Int -> p -> Property
+always i = conjoin . replicate i