Define phases of execution

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -83,6 +83,7 @@ library
     , mtl
     , QuickCheck
     , random
+    , singletons
 
 test-suite quickcheck-dynamic-test
   import:         lang

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, Eq (Action s Symbolic a), Show (Action s Symbolic a)) => Action s Symbolic a -> DL s (Var Symbolic 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, Eq (Action s Symbolic a), Show (Action s Symbolic a)) => Action s Symbolic a -> DL s ()
 failingAction cmd = DL $ \_ k -> DL.afterNegative cmd (k ())
 
 anyAction :: DL s ()
@@ -90,13 +90,13 @@ weight w = DL $ \s k -> DL.weight w (k () s)
 getSize :: DL s Int
 getSize = DL $ \s k -> DL.withSize $ \n -> k n s
 
-getModelStateDL :: DL s s
+getModelStateDL :: DL s (s Symbolic)
 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 => DL s (Var Symbolic a)
 forAllVar = do
   xs <- ctxAtType <$> getVarContextDL
   forAllQ $ elementsQ xs
@@ -114,7 +114,7 @@ errorDL name = DL $ \_ _ -> DL.errorDL name
 assert :: String -> Bool -> DL s ()
 assert name b = if b then return () else errorDL name
 
-assertModel :: String -> (s -> Bool) -> DL s ()
+assertModel :: String -> (s Symbolic -> Bool) -> DL s ()
 assertModel name p = assert name . p =<< getModelStateDL
 
 monitorDL :: (Property -> Property) -> DL s ()

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

@@ -32,8 +32,8 @@ 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) =>
-    After (ActionWithPolarity s a) (Var a -> DynPred s)
+    (Eq (Action s Symbolic a), Show (Action s Symbolic a), Typeable a) =>
+    After (ActionWithPolarity s a) (Var Symbolic a -> DynPred s)
   | Error String (DynPred s)
   | -- | Adjust the probability of picking a branch
     Weight Double (DynLogic s)
@@ -65,27 +65,27 @@ 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, Eq (Action s Symbolic a), Show (Action s Symbolic a))
   => ActionWithPolarity s a
-  -> (Var a -> Annotated s -> DynFormula s)
+  -> (Var Symbolic a -> Annotated s -> DynFormula s)
   -> DynFormula s
 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))
-  => Action s a
-  -> (Var a -> Annotated s -> DynFormula s)
+  :: (Typeable a, Eq (Action s Symbolic a), Show (Action s Symbolic a))
+  => Action s Symbolic a
+  -> (Var Symbolic a -> Annotated s -> DynFormula s)
   -> DynFormula s
 after act f = afterPolar (ActionWithPolarity act PosPolarity) f
 
 -- | Given `f` must be `True` after /some/ negative action.
 -- `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))
-  => Action s a
+  :: (Typeable a, Eq (Action s Symbolic a), Show (Action s Symbolic a))
+  => Action s Symbolic a
   -> (Annotated s -> DynFormula s)
   -> DynFormula s
 afterNegative act f = afterPolar (ActionWithPolarity act NegPolarity) (const f)
@@ -127,7 +127,7 @@ withSize :: (Int -> DynFormula s) -> DynFormula s
 withSize f = DynFormula $ \n -> unDynFormula (f n) n
 
 -- | Prioritise doing this if we are
--- trying to stop generation.
+-- trying to stop Symbolic.
 toStop :: DynFormula s -> DynFormula s
 toStop (DynFormula f) = DynFormula $ Stopping . f
 
@@ -154,7 +154,7 @@ always p s = withSize $ \n -> toStop (p s) ||| p s ||| weight (fromIntegral n) (
 
 data FailingAction s
   = ErrorFail String
-  | forall a. (Typeable a, Eq (Action s a)) => ActionFail (ActionWithPolarity s a)
+  | forall a. (Typeable a, Eq (Action s Symbolic a)) => ActionFail (ActionWithPolarity s a)
 
 instance StateModel s => HasVariables (FailingAction s) where
   getAllVariables ErrorFail{} = mempty
@@ -329,7 +329,7 @@ usedVariables = go initialAnnotatedState
 -- properties at controlled times, so they are likely to fail if
 -- invoked at other times.
 class StateModel s => DynLogicModel s where
-  restricted :: Action s a -> Bool
+  restricted :: Action s Symbolic a -> Bool
   restricted _ = False
 
 restrictedPolar :: DynLogicModel s => ActionWithPolarity s a -> Bool
@@ -392,7 +392,7 @@ withDLScriptPrefix f k test =
 
 -- | Validate generated test case.
 --
--- Test case generation does not always produce a valid test case. In
+-- Test case Symbolic does not always produce a valid test case. In
 -- some cases, we did not find a suitable test case matching some
 -- `DynFormula` and we are `Stuck`, hence we want to discard the test
 -- case and start over ; in other cases we found a genuine issue with

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,7 @@ 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
+
+-- | Lifts a plain property into a monadic property.
+liftProperty :: Monad m => Property -> PropertyM m ()
+liftProperty prop = MkPropertyM (\k -> fmap (prop .&&.) <$> k ())