quickcheck-dynamic 2.0.0 → 3.0.0
raw patch · 11 files changed
+1233/−873 lines, 11 filesdep +containersdep +template-haskell
Dependencies added: containers, template-haskell
Files
- CHANGELOG.md +12/−0
- quickcheck-dynamic.cabal +14/−3
- src/Test/QuickCheck/DynamicLogic.hs +23/−40
- src/Test/QuickCheck/DynamicLogic/CanGenerate.hs +10/−10
- src/Test/QuickCheck/DynamicLogic/Core.hs +0/−668
- src/Test/QuickCheck/DynamicLogic/Internal.hs +815/−0
- src/Test/QuickCheck/DynamicLogic/Quantify.hs +32/−28
- src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs +6/−6
- src/Test/QuickCheck/Extras.hs +15/−0
- src/Test/QuickCheck/StateModel.hs +164/−118
- src/Test/QuickCheck/StateModel/Variables.hs +142/−0
CHANGELOG.md view
@@ -9,6 +9,18 @@ ## UNRELEASED +## 3.0.0 - 2023-02-14++* **BREAKING**: Add `HasVariables` class to keep track of symbolic variables and automatically insert precondition+ checks for well-scopedness of variables.+* **BREAKING**: Remove some unnecessary and unusead features in dynamic logic, including re-running tests from a+ counterexample directly.+* Improved printing of counterexamples in DL - they are now printed as code that can be copied more-or-less verbatim to+ create a runnable counterexample in code.+* Made the variable context explicit to avoid having to keep track of symbolic variables in the model+ * This introduces the `ctxAtType` and `arbitraryVar` functions to use in action generators (c.f. the+ `RegistryModel.hs` example).+ ## 2.0.0 - 2022-10-11 * **BREAKING**: Add `Realized` type family to distinguish between the model- and real type of an action
quickcheck-dynamic.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: quickcheck-dynamic-version: 2.0.0+version: 3.0.0 license: Apache-2.0 license-files: LICENSE@@ -31,7 +31,10 @@ common lang default-language: Haskell2010 default-extensions:+ ConstraintKinds DeriveFunctor+ DeriveFoldable+ DeriveTraversable DeriveDataTypeable StandaloneDeriving ImportQualifiedPost@@ -47,12 +50,16 @@ MultiParamTypeClasses RankNTypes ViewPatterns+ DefaultSignatures TypeOperators+ DerivingVia+ DeriveGeneric ghc-options: -Wall -Wnoncanonical-monad-instances -Wunused-packages -Wincomplete-uni-patterns -Wincomplete-record-updates -Wredundant-constraints -Widentities+ -Wno-unused-do-bind library import: lang@@ -60,13 +67,17 @@ exposed-modules: Test.QuickCheck.DynamicLogic Test.QuickCheck.DynamicLogic.CanGenerate- Test.QuickCheck.DynamicLogic.Core+ Test.QuickCheck.DynamicLogic.Internal Test.QuickCheck.DynamicLogic.Quantify Test.QuickCheck.DynamicLogic.SmartShrinking Test.QuickCheck.DynamicLogic.Utils+ Test.QuickCheck.Extras Test.QuickCheck.StateModel+ Test.QuickCheck.StateModel.Variables build-depends: QuickCheck -any, base >=4.7 && <5, random -any,- mtl -any+ mtl -any,+ containers -any,+ template-haskell >= 2.16
src/Test/QuickCheck/DynamicLogic.hs view
@@ -3,7 +3,7 @@ -- This interface offers a much nicer experience than manipulating the -- expressions it is implemented on top of, especially as it improves -- readability. It's still possible to express properties as pure--- expressions using the `Test.QuickCheck.DynamicLogic.Core` module+-- expressions using the `Test.QuickCheck.DynamicLogic.Internal` module -- and it might make sense depending on the context and the kind of -- properties one wants to express. module Test.QuickCheck.DynamicLogic (@@ -16,20 +16,16 @@ weight, getSize, getModelStateDL,+ getVarContextDL,+ forAllVar, assert, assertModel, monitorDL, forAllQ, forAllDL,- forAllDL_, forAllMappedDL,- forAllMappedDL_, forAllUniqueDL,- withDLTest,- DL.DynLogic, DL.DynLogicModel (..),- DL.DynLogicTest (..),- DL.TestStep (..), module Test.QuickCheck.DynamicLogic.Quantify, ) where @@ -37,14 +33,14 @@ import Control.Monad import Data.Typeable import Test.QuickCheck hiding (getSize)-import Test.QuickCheck.DynamicLogic.Core qualified as DL+import Test.QuickCheck.DynamicLogic.Internal qualified as DL import Test.QuickCheck.DynamicLogic.Quantify import Test.QuickCheck.StateModel -- | The `DL` monad provides a nicer interface to dynamic logic formulae than the plain API.--- It's a continuation monad producing a `DL.DynFormula` formula, with a state component threaded--- through.-newtype DL s a = DL {unDL :: s -> (a -> s -> DL.DynFormula s) -> DL.DynFormula s}+-- It's a continuation monad producing a `DL.DynFormula` formula, with a state component (with+-- variable context) threaded through.+newtype DL s a = DL {unDL :: Annotated s -> (a -> Annotated s -> DL.DynFormula s) -> DL.DynFormula s} deriving (Functor) instance Applicative (DL s) where@@ -62,8 +58,8 @@ instance MonadFail (DL s) where fail = errorDL -action :: (Typeable a, Eq (Action s a)) => Action s a -> DL s ()-action cmd = DL $ \_ k -> DL.after cmd $ k ()+action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)+action cmd = DL $ \_ k -> DL.after cmd k anyAction :: DL s () anyAction = DL $ \_ k -> DL.afterAny $ k ()@@ -90,8 +86,16 @@ getSize = DL $ \s k -> DL.withSize $ \n -> k n s getModelStateDL :: DL s s-getModelStateDL = DL $ \s k -> k s s+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 = do+ xs <- ctxAtType <$> getVarContextDL+ forAllQ $ elementsQ xs+ errorDL :: String -> DL s a errorDL name = DL $ \_ _ -> DL.errorDL name @@ -116,13 +120,13 @@ forAllQ :: Quantifiable q => q -> DL s (Quantifies q) forAllQ q = DL $ \s k -> DL.forAllQ q $ \x -> k x s -runDL :: s -> DL s () -> DL.DynFormula s+runDL :: Annotated s -> DL s () -> DL.DynFormula s runDL s dl = unDL dl s $ \_ _ -> DL.passTest forAllUniqueDL :: (DL.DynLogicModel s, Testable a) => Int ->- s ->+ Annotated s -> DL s () -> (Actions s -> a) -> Property@@ -133,17 +137,10 @@ DL s () -> (Actions s -> a) -> Property-forAllDL d = DL.forAllScripts (runDL initialState d)--forAllDL_ ::- (DL.DynLogicModel s, Testable a) =>- DL s () ->- (Actions s -> a) ->- Property-forAllDL_ d = DL.forAllScripts_ (runDL initialState d)+forAllDL d = DL.forAllScripts (runDL initialAnnotatedState d) forAllMappedDL ::- (DL.DynLogicModel s, Testable a, Show rep) =>+ (DL.DynLogicModel s, Testable a) => (rep -> DL.DynLogicTest s) -> (DL.DynLogicTest s -> rep) -> (Actions s -> srep) ->@@ -151,18 +148,4 @@ (srep -> a) -> Property forAllMappedDL to from fromScript d prop =- DL.forAllMappedScripts to from (runDL initialState d) (prop . fromScript)--forAllMappedDL_ ::- (DL.DynLogicModel s, Testable a, Show rep) =>- (rep -> DL.DynLogicTest s) ->- (DL.DynLogicTest s -> rep) ->- (Actions s -> srep) ->- DL s () ->- (srep -> a) ->- Property-forAllMappedDL_ to from fromScript d prop =- DL.forAllMappedScripts_ to from (runDL initialState d) (prop . fromScript)--withDLTest :: (DL.DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> DL.DynLogicTest s -> Property-withDLTest d = DL.withDLScriptPrefix (runDL initialState d)+ DL.forAllMappedScripts to from (runDL initialAnnotatedState d) (prop . fromScript)
src/Test/QuickCheck/DynamicLogic/CanGenerate.hs view
@@ -8,14 +8,14 @@ -- otherwise @True@ (and we know such an x can be generated). canGenerate :: Double -> Gen a -> (a -> Bool) -> Bool canGenerate prob g p = unsafePerformIO $ tryToGenerate 1- where- tryToGenerate luck- | luck < eps = return False- | otherwise = do- x <- generate g- if p x- then return True- else tryToGenerate (luck * (1 - prob))+ where+ tryToGenerate luck+ | luck < eps = return False+ | otherwise = do+ x <- generate g+ if p x+ then return True+ else tryToGenerate (luck * (1 - prob)) - -- Our confidence level is 1-eps- eps = 1.0e-9+ -- Our confidence level is 1-eps+ eps = 1.0e-9
− src/Test/QuickCheck/DynamicLogic/Core.hs
@@ -1,668 +0,0 @@-module Test.QuickCheck.DynamicLogic.Core (- module Test.QuickCheck.DynamicLogic.Quantify,- DynLogic,- DynPred,- DynFormula,- DynLogicModel (..),- DynLogicTest (..),- TestStep (..),- ignore,- passTest,- afterAny,- after,- (|||),- forAllQ,- weight,- withSize,- toStop,- done,- errorDL,- monitorDL,- always,- forAllScripts,- forAllScripts_,- withDLScript,- withDLScriptPrefix,- forAllMappedScripts,- forAllMappedScripts_,- forAllUniqueScripts,- propPruningGeneratedScriptIsNoop,-) where--import Control.Applicative-import Data.List-import Data.Typeable-import Test.QuickCheck hiding (generate)-import Test.QuickCheck.DynamicLogic.CanGenerate-import Test.QuickCheck.DynamicLogic.Quantify-import Test.QuickCheck.DynamicLogic.SmartShrinking-import Test.QuickCheck.DynamicLogic.Utils qualified as QC-import Test.QuickCheck.StateModel---- | A `DynFormula` may depend on the QuickCheck size parameter-newtype DynFormula s = DynFormula {unDynFormula :: Int -> DynLogic s}---- | Base Dynamic logic formulae language.--- Formulae are parameterised--- over the type of state `s` to which they apply. A `DynLogic` value--- cannot be constructed directly, one has to use the various "smart--- constructors" provided, see the /Building formulae/ section.-data DynLogic s- = -- | False- EmptySpec- | -- | True- Stop- | -- | After any action the predicate should hold- AfterAny (DynPred s)- | -- | Choice (angelic or demonic)- Alt ChoiceType (DynLogic s) (DynLogic s)- | -- | Prefer this branch if trying to stop.- Stopping (DynLogic s)- | -- | After a specific action the predicate should hold- After (Any (Action s)) (DynPred s)- | -- | Adjust the probability of picking a branch- Weight Double (DynLogic s)- | -- | Generating a random value- forall a.- (Eq a, Show a, Typeable a) =>- ForAll (Quantification a) (a -> DynLogic s)- | -- | Apply a QuickCheck property modifier (like `tabulate` or `collect`)- Monitor (Property -> Property) (DynLogic s)--data ChoiceType = Angelic | Demonic- deriving (Eq, Show)--type DynPred s = s -> DynLogic s---- * Building formulae---- | `False` for DL formulae.-ignore :: DynFormula s---- | `True` for DL formulae.-passTest :: DynFormula s---- | Given `f` must be `True` given /any/ state.-afterAny :: (s -> DynFormula s) -> DynFormula s---- | 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)) =>- Action s a ->- (s -> DynFormula s) ->- DynFormula s---- | Disjunction for DL formulae.--- Is `True` if either formula is `True`. The choice is /angelic/, ie. it is--- always made by the "caller". This is mostly important in case a test is--- `Stuck`.-(|||) :: DynFormula s -> DynFormula s -> DynFormula s---- | First-order quantification of variables.--- Formula @f@ is `True` iff. it is `True` /for all/ possible values of `q`. The--- underlying framework will generate values of `q` and check the formula holds--- for those values. `Quantifiable` values are thus values that can be generated--- and checked and the `Test.QuickCheck.DynamicLogic.Quantify` module defines--- basic combinators to build those from building blocks.-forAllQ ::- Quantifiable q =>- q ->- (Quantifies q -> DynFormula s) ->- DynFormula s---- | Adjust weight for selecting formula.--- This is mostly useful in relation with `(|||)` combinator, in order to tweak the--- priority for generating the next step(s) of the test that matches the formula.-weight :: Double -> DynFormula s -> DynFormula s--- ??-withSize :: (Int -> DynFormula s) -> DynFormula s--- ??-toStop :: DynFormula s -> DynFormula s---- | Successfully ends the test.-done :: s -> DynFormula s---- | Ends test with given error message.-errorDL :: String -> DynFormula s---- | Embed QuickCheck's monitoring functions (eg. `label`, `tabulate`) in--- a formula.--- This is useful to improve the reporting from test execution, esp. in the--- case of failures.-monitorDL :: (Property -> Property) -> DynFormula s -> DynFormula s---- | Formula should hold at any state.--- In effect this leads to exploring alternatives from a given state `s` and ensuring--- formula holds in all those states.-always :: (s -> DynFormula s) -> (s -> DynFormula s)--ignore = DynFormula . const $ EmptySpec-passTest = DynFormula . const $ Stop-afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f s) n-after act f = DynFormula $ \n -> After (Some act) $ \s -> unDynFormula (f s) n-DynFormula f ||| DynFormula g = DynFormula $ \n -> Alt Angelic (f n) (g n)---- In formulae, we use only angelic--- choice. But it becomes demonic after one--- step (that is, the choice has been made).-forAllQ q f- | isEmptyQ q' = ignore- | otherwise = DynFormula $ \n -> ForAll q' $ ($ n) . unDynFormula . f- where- q' = quantify q--weight w f = DynFormula $ Weight w . unDynFormula f--withSize f = DynFormula $ \n -> unDynFormula (f n) n--toStop (DynFormula f) = DynFormula $ Stopping . f--done _ = passTest--errorDL s = DynFormula . const $ After (Error s) (const EmptySpec)--monitorDL m (DynFormula f) = DynFormula $ Monitor m . f--always p s = withSize $ \n -> toStop (p s) ||| p s ||| weight (fromIntegral n) (afterAny (always p))--data DynLogicTest s- = BadPrecondition [TestStep s] [Any (Action s)] s- | Looping [TestStep s]- | Stuck [TestStep s] s- | DLScript [TestStep s]--data TestStep s- = Do (Step s)- | forall a. (Eq a, Show a, Typeable a) => Witness a--instance Eq (TestStep s) where- Do s == Do s' = s == s'- Witness (a :: a) == Witness (a' :: a') =- case eqT @a @a' of- Just Refl -> a == a'- Nothing -> False- _ == _ = False--instance StateModel s => Show (TestStep s) where- show (Do step) = "Do $ " ++ show step- show (Witness a) = "Witness (" ++ show a ++ " :: " ++ show (typeOf a) ++ ")"--instance StateModel s => Show (DynLogicTest s) where- show (BadPrecondition as bads s) =- unlines $- ["BadPrecondition"]- ++ bracket (map show as)- ++ [" " ++ show (nub bads)]- ++ [" " ++ showsPrec 11 s ""]- show (Looping as) =- unlines $ "Looping" : bracket (map show as)- show (Stuck as s) =- unlines $ ["Stuck"] ++ bracket (map show as) ++ [" " ++ showsPrec 11 s ""]- show (DLScript as) =- unlines $ "DLScript" : bracket (map show as)--bracket :: [String] -> [String]-bracket [] = [" []"]-bracket [s] = [" [" ++ s ++ "]"]-bracket (first : rest) =- [" [" ++ first ++ ", "]- ++ map ((" " ++) . (++ ", ")) (init rest)- ++ [" " ++ last rest ++ "]"]---- | Restricted calls are not generated by "AfterAny"; they are included--- in tests explicitly using "After" in order to check specific--- 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 _ = False---- * Generate Properties---- | Simplest "execution" function for `DynFormula`.--- Turns a given a `DynFormula` paired with an interpreter function to produce some result from an----- `Actions` sequence into a proper `Property` than can then be run by QuickCheck.-forAllScripts ::- (DynLogicModel s, Testable a) =>- DynFormula s ->- (Actions s -> a) ->- Property-forAllScripts = forAllMappedScripts id id---- | `Property` function suitable for formulae without choice.-forAllUniqueScripts ::- (DynLogicModel s, Testable a) =>- Int ->- s ->- DynFormula s ->- (Actions s -> a) ->- Property-forAllUniqueScripts n s f k =- QC.withSize $ \sz ->- let d = unDynFormula f sz- in case generate chooseUniqueNextStep d n s 500 [] of- Nothing -> counterexample "Generating Non-unique script in forAllUniqueScripts" False- Just test -> validDLTest d test .&&. (applyMonitoring d test . property $ k (scriptFromDL test))--forAllScripts_ ::- (DynLogicModel s, Testable a) =>- DynFormula s ->- (Actions s -> a) ->- Property-forAllScripts_ f k =- QC.withSize $ \n ->- let d = unDynFormula f n- in forAll (sized $ generateDLTest d) $- withDLScript d k---- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose.--- ??-forAllMappedScripts ::- (DynLogicModel s, Testable a, Show rep) =>- (rep -> DynLogicTest s) ->- (DynLogicTest s -> rep) ->- DynFormula s ->- (Actions s -> a) ->- Property-forAllMappedScripts to from f k =- QC.withSize $ \n ->- let d = unDynFormula f n- in forAllShrink- (Smart 0 <$> sized ((from <$>) . generateDLTest d))- (shrinkSmart ((from <$>) . shrinkDLTest d . to))- $ \(Smart _ script) ->- withDLScript d k (to script)--forAllMappedScripts_ ::- (DynLogicModel s, Testable a, Show rep) =>- (rep -> DynLogicTest s) ->- (DynLogicTest s -> rep) ->- DynFormula s ->- (Actions s -> a) ->- Property-forAllMappedScripts_ to from f k =- QC.withSize $ \n ->- let d = unDynFormula f n- in forAll (sized $ (from <$>) . generateDLTest d) $- withDLScript d k . to--withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property-withDLScript d k test =- validDLTest d test .&&. (applyMonitoring d test . property $ k (scriptFromDL test))--withDLScriptPrefix :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property-withDLScriptPrefix f k test =- QC.withSize $ \n ->- let d = unDynFormula f n- test' = unfailDLTest d test- in validDLTest d test' .&&. (applyMonitoring d test' . property $ k (scriptFromDL test'))--generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)-generateDLTest d size = generate chooseNextStep d 0 (initialStateFor d) size []--generate ::- (Monad m, DynLogicModel s) =>- (s -> Int -> DynLogic s -> m (NextStep s)) ->- DynLogic s ->- Int ->- s ->- Int ->- [TestStep s] ->- m (DynLogicTest s)-generate chooseNextStepFun d n s size as =- case badActions d s of- [] ->- if n > sizeLimit size- then return $ Looping (reverse as)- else do- let preferred = if n > size then stopping d else noStopping d- useStep StoppingStep _ = return $ DLScript (reverse as)- useStep (Stepping (Do (var := act)) d') _ =- generate- chooseNextStepFun- d'- (n + 1)- (nextState s act var)- size- (Do (var := act) : as)- useStep (Stepping (Witness a) d') _ =- generate- chooseNextStepFun- d'- n- s- size- (Witness a : as)- useStep NoStep alt = alt- foldr- (\step k -> do try <- chooseNextStepFun s n step; useStep try k)- (return $ Stuck (reverse as) s)- [preferred, noAny preferred, d, noAny d]- bs -> return $ BadPrecondition (reverse as) bs s--sizeLimit :: Int -> Int-sizeLimit size = 2 * size + 20--initialStateFor :: StateModel s => DynLogic s -> s-initialStateFor _ = initialState--stopping :: DynLogic s -> DynLogic s-stopping EmptySpec = EmptySpec-stopping Stop = Stop-stopping (After act k) = After act k-stopping (AfterAny _) = EmptySpec-stopping (Alt b d d') = Alt b (stopping d) (stopping d')-stopping (Stopping d) = d-stopping (Weight w d) = Weight w (stopping d)-stopping (ForAll _ _) = EmptySpec-stopping (Monitor f d) = Monitor f (stopping d)--noStopping :: DynLogic s -> DynLogic s-noStopping EmptySpec = EmptySpec-noStopping Stop = EmptySpec-noStopping (After act k) = After act k-noStopping (AfterAny k) = AfterAny k-noStopping (Alt b d d') = Alt b (noStopping d) (noStopping d')-noStopping (Stopping _) = EmptySpec-noStopping (Weight w d) = Weight w (noStopping d)-noStopping (ForAll q f) = ForAll q f-noStopping (Monitor f d) = Monitor f (noStopping d)--noAny :: DynLogic s -> DynLogic s-noAny EmptySpec = EmptySpec-noAny Stop = Stop-noAny (After act k) = After act k-noAny (AfterAny _) = EmptySpec-noAny (Alt b d d') = Alt b (noAny d) (noAny d')-noAny (Stopping d) = Stopping (noAny d)-noAny (Weight w d) = Weight w (noAny d)-noAny (ForAll q f) = ForAll q f-noAny (Monitor f d) = Monitor f (noAny d)--nextSteps :: DynLogic s -> [(Double, DynLogic s)]-nextSteps EmptySpec = []-nextSteps Stop = [(1, Stop)]-nextSteps (After act k) = [(1, After act k)]-nextSteps (AfterAny k) = [(1, AfterAny k)]-nextSteps (Alt _ d d') = nextSteps d ++ nextSteps d'-nextSteps (Stopping d) = nextSteps d-nextSteps (Weight w d) = [(w * w', s) | (w', s) <- nextSteps d, w * w' > never]-nextSteps (ForAll q f) = [(1, ForAll q f)]-nextSteps (Monitor _f d) = nextSteps d--chooseOneOf :: [(Double, DynLogic s)] -> Gen (DynLogic s)-chooseOneOf steps = frequency [(round (w / never), return s) | (w, s) <- steps]--never :: Double-never = 1.0e-9--data NextStep s- = StoppingStep- | Stepping (TestStep s) (DynLogic s)- | NoStep--chooseNextStep :: DynLogicModel s => s -> Int -> DynLogic s -> Gen (NextStep s)-chooseNextStep s n d =- case nextSteps d of- [] -> return NoStep- steps -> do- chosen <- chooseOneOf steps- case chosen of- EmptySpec -> return NoStep- Stop -> return StoppingStep- After (Some a) k ->- return $ Stepping (Do $ Var n := a) (k (nextState s a (Var n)))- AfterAny k -> do- m <- keepTryingUntil 100 (arbitraryAction s) $- \case- Some act -> precondition s act && not (restricted act)- Error _ -> False- case m of- Nothing -> return NoStep- Just (Some a) ->- return $- Stepping- (Do $ Var n := a)- (k (nextState s a (Var n)))- Just Error{} -> error "impossible"- ForAll q f -> do- x <- generateQ q- return $ Stepping (Witness x) (f x)- After Error{} _ -> error "chooseNextStep: After Error"- Alt{} -> error "chooseNextStep: Alt"- Stopping{} -> error "chooseNextStep: Stopping"- Weight{} -> error "chooseNextStep: Weight"- Monitor{} -> error "chooseNextStep: Monitor"--chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => s -> Int -> DynLogic s -> m (NextStep s)-chooseUniqueNextStep s n d =- case snd <$> nextSteps d of- [] -> return NoStep- [EmptySpec] -> return NoStep- [Stop] -> return StoppingStep- [After (Some a) k] -> return $ Stepping (Do $ Var n := a) (k (nextState s a (Var n)))- _ -> fail "chooseUniqueNextStep: non-unique action in DynLogic"--keepTryingUntil :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)-keepTryingUntil 0 _ _ = return Nothing-keepTryingUntil n g p = do- x <- g- if p x then return $ Just x else scale (+ 1) $ keepTryingUntil (n - 1) g p--shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s]-shrinkDLTest _ (Looping _) = []-shrinkDLTest d tc =- [ test | as' <- shrinkScript d (getScript tc), let test = makeTestFromPruned d (pruneDLTest d as'),- -- Don't shrink a non-executable test case to an executable one.- case (tc, test) of- (DLScript _, _) -> True- (_, DLScript _) -> False- _ -> True- ]--shrinkScript :: DynLogicModel t => DynLogic t -> [TestStep t] -> [[TestStep t]]-shrinkScript dl steps = shrink' dl steps initialState- where- shrink' _ [] _ = []- shrink' d (step : as) s =- []- : reverse (takeWhile (not . null) [drop (n - 1) as | n <- iterate (* 2) 1])- ++ case step of- Do (Var i := act) ->- [Do (Var i := act') : as | Some act' <- shrinkAction s act]- Witness a ->- -- When we shrink a witness, allow one shrink of the- -- rest of the script... so assuming the witness may be- -- used once to construct the rest of the test. If used- -- more than once, we may need double shrinking.- [ Witness a' : as' | a' <- shrinkWitness d a, as' <- as : shrink' (stepDLtoDL d s (Witness a')) as s- ]- ++ [ step : as'- | as' <- shrink' (stepDLtoDL d s step) as $- case step of- Do (var := act) -> nextState s act var- Witness _ -> s- ]--shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a]-shrinkWitness (ForAll (q :: Quantification a) _) (a :: a') =- case eqT @a @a' of- Just Refl | isaQ q a -> shrinkQ q a- _ -> []-shrinkWitness (Alt _ d d') a = shrinkWitness d a ++ shrinkWitness d' a-shrinkWitness (Stopping d) a = shrinkWitness d a-shrinkWitness (Weight _ d) a = shrinkWitness d a-shrinkWitness (Monitor _ d) a = shrinkWitness d a-shrinkWitness _ _ = []---- The result of pruning a list of actions is a list of actions that--- could have been generated by the dynamic logic.-pruneDLTest :: DynLogicModel s => DynLogic s -> [TestStep s] -> [TestStep s]-pruneDLTest dl = prune [dl] initialState- where- prune [] _ _ = []- prune _ _ [] = []- prune ds s (Do (var := act) : rest)- | precondition s act =- case [d' | d <- ds, d' <- stepDL d s (Do $ var := act)] of- [] -> prune ds s rest- ds' ->- Do (var := act)- : prune ds' (nextState s act var) rest- | otherwise =- prune ds s rest- prune ds s (Witness a : rest) =- case [d' | d <- ds, d' <- stepDL d s (Witness a)] of- [] -> prune ds s rest- ds' -> Witness a : prune ds' s rest--stepDL :: DynLogicModel s => DynLogic s -> s -> TestStep s -> [DynLogic s]-stepDL (After a k) s (Do (var := act))- | a == Some act = [k (nextState s act var)]-stepDL (AfterAny k) s (Do (var := act))- | not (restricted act) = [k (nextState s act var)]-stepDL (Alt _ d d') s step = stepDL d s step ++ stepDL d' s step-stepDL (Stopping d) s step = stepDL d s step-stepDL (Weight _ d) s step = stepDL d s step-stepDL (ForAll (q :: Quantification a) f) _ (Witness (a :: a')) =- case eqT @a @a' of- Just Refl -> [f a | isaQ q a]- Nothing -> []-stepDL (Monitor _f d) s step = stepDL d s step-stepDL _ _ _ = []--stepDLtoDL :: DynLogicModel s => DynLogic s -> s -> TestStep s -> DynLogic s-stepDLtoDL d s step = case stepDL d s step of- [] -> EmptySpec- ds -> foldr1 (Alt Demonic) ds--propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property-propPruningGeneratedScriptIsNoop d =- forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest d) $ \test ->- let script = case test of- BadPrecondition s _ _ -> s- Looping s -> s- Stuck s _ -> s- DLScript s -> s- in script == pruneDLTest d script--getScript :: DynLogicTest s -> [TestStep s]-getScript (BadPrecondition s _ _) = s-getScript (Looping s) = s-getScript (Stuck s _) = s-getScript (DLScript s) = s--makeTestFromPruned :: DynLogicModel s => DynLogic s -> [TestStep s] -> DynLogicTest s-makeTestFromPruned dl = make dl initialState- where- make d s as | not (null bad) = BadPrecondition as bad s- where- bad = badActions d s- make d s []- | stuck d s = Stuck [] s- | otherwise = DLScript []- make d curStep (step : steps) =- case make- (stepDLtoDL d curStep step)- ( case step of- Do (var := act) -> nextState curStep act var- Witness _ -> curStep- )- steps of- BadPrecondition as bad s -> BadPrecondition (step : as) bad s- Stuck as s -> Stuck (step : as) s- DLScript as -> DLScript (step : as)- Looping{} -> error "makeTestFromPruned: Looping"---- | If failed, return the prefix up to the failure. Also prunes the test in case the model has--- changed.-unfailDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> DynLogicTest s-unfailDLTest d test = makeTestFromPruned d $ pruneDLTest d steps- where- steps = case test of- BadPrecondition as _ _ -> as- Stuck as _ -> as- DLScript as -> as- Looping as -> as--stuck :: DynLogicModel s => DynLogic s -> s -> Bool-stuck EmptySpec _ = True-stuck Stop _ = False-stuck (After _ _) _ = False-stuck (AfterAny _) s =- not $- canGenerate- 0.01- (arbitraryAction s)- ( \case- Some act ->- precondition s act- && not (restricted act)- Error _ -> False- )-stuck (Alt Angelic d d') s = stuck d s && stuck d' s-stuck (Alt Demonic d d') s = stuck d s || stuck d' s-stuck (Stopping d) s = stuck d s-stuck (Weight w d) s = w < never || stuck d s-stuck (ForAll _ _) _ = False-stuck (Monitor _ d) s = stuck d s--validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property-validDLTest _ (DLScript _) = property True-validDLTest _ (Stuck as _) = counterexample ("Stuck\n" ++ (unlines . map (" " ++) . lines $ show as)) False-validDLTest _ (Looping as) = counterexample ("Looping\n" ++ (unlines . map (" " ++) . lines $ show as)) False-validDLTest _ (BadPrecondition as bads _s) = counterexample ("BadPrecondition\n" ++ show as ++ "\n" ++ unlines (showBad <$> bads)) False- where- showBad (Error s) = s- showBad a = show a--scriptFromDL :: DynLogicTest s -> Actions s-scriptFromDL (DLScript s) = Actions [a | Do a <- s]-scriptFromDL _ = Actions []--badActions :: StateModel s => DynLogic s -> s -> [Any (Action s)]-badActions EmptySpec _ = []-badActions Stop _ = []-badActions (After (Some a) _) s- | precondition s a = []- | otherwise = [Some a]-badActions (After (Error m) _) _s = [Error m]-badActions (AfterAny _) _ = []-badActions (Alt _ d d') s = badActions d s ++ badActions d' s-badActions (Stopping d) s = badActions d s-badActions (Weight w d) s = if w < never then [] else badActions d s-badActions (ForAll _ _) _ = []-badActions (Monitor _ d) s = badActions d s--applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property-applyMonitoring d (DLScript s) p =- case findMonitoring d initialState s of- Just f -> f p- Nothing -> p-applyMonitoring _ Stuck{} p = p-applyMonitoring _ Looping{} p = p-applyMonitoring _ BadPrecondition{} p = p--findMonitoring :: DynLogicModel s => DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)-findMonitoring Stop _s [] = Just id-findMonitoring (After (Some a) k) s (Do (var := a') : as)- | Some a == Some a' = findMonitoring (k s') s' as- where- s' = nextState s a' var-findMonitoring (AfterAny k) s as@(Do (_var := a) : _)- | not (restricted a) = findMonitoring (After (Some a) k) s as-findMonitoring (Alt _b d d') s as =- -- Give priority to monitoring matches to the left. Combining both- -- results in repeated monitoring from always, which is unexpected.- findMonitoring d s as <|> findMonitoring d' s as-findMonitoring (Stopping d) s as = findMonitoring d s as-findMonitoring (Weight _ d) s as = findMonitoring d s as-findMonitoring (ForAll (_q :: Quantification a) k) s (Witness (a :: a') : as) =- case eqT @a @a' of- Just Refl -> findMonitoring (k a) s as- Nothing -> Nothing-findMonitoring (Monitor m d) s as =- (m .) <$> findMonitoring d s as-findMonitoring _ _ _ = Nothing
+ src/Test/QuickCheck/DynamicLogic/Internal.hs view
@@ -0,0 +1,815 @@+module Test.QuickCheck.DynamicLogic.Internal where++import Control.Applicative+import Control.Arrow (second)+import Control.Monad+import Data.Typeable+import Test.QuickCheck hiding (generate)+import Test.QuickCheck.DynamicLogic.CanGenerate+import Test.QuickCheck.DynamicLogic.Quantify+import Test.QuickCheck.DynamicLogic.SmartShrinking+import Test.QuickCheck.DynamicLogic.Utils qualified as QC+import Test.QuickCheck.StateModel++-- | A `DynFormula` may depend on the QuickCheck size parameter+newtype DynFormula s = DynFormula {unDynFormula :: Int -> DynLogic s}++-- | Base Dynamic logic formulae language.+-- Formulae are parameterised+-- over the type of state `s` to which they apply. A `DynLogic` value+-- cannot be constructed directly, one has to use the various "smart+-- constructors" provided, see the /Building formulae/ section.+data DynLogic s+ = -- | False+ EmptySpec+ | -- | True+ Stop+ | -- | After any action the predicate should hold+ AfterAny (DynPred s)+ | -- | Choice (angelic or demonic)+ Alt ChoiceType (DynLogic s) (DynLogic s)+ | -- | Prefer this branch if trying to stop.+ Stopping (DynLogic s)+ | -- | After a specific action the predicate should hold+ forall a.+ (Eq (Action s a), Show (Action s a), Typeable a) =>+ After (Action s a) (Var a -> DynPred s)+ | Error String (DynPred s)+ | -- | Adjust the probability of picking a branch+ Weight Double (DynLogic s)+ | -- | Generating a random value+ forall a.+ QuantifyConstraints a =>+ ForAll (Quantification a) (a -> DynLogic s)+ | -- | Apply a QuickCheck property modifier (like `tabulate` or `collect`)+ Monitor (Property -> Property) (DynLogic s)++data ChoiceType = Angelic | Demonic+ deriving (Eq, Show)++type DynPred s = Annotated s -> DynLogic s++-- * Building formulae++-- | Ignore this formula, i.e. backtrack and try something else. @forAllScripts ignore (const True)@+-- will discard all test cases (equivalent to @False ==> True@).+ignore :: DynFormula s+ignore = DynFormula . const $ EmptySpec++-- | `True` for DL formulae.+passTest :: DynFormula s+passTest = DynFormula . const $ Stop++-- | Given `f` must be `True` given /any/ state.+afterAny :: (Annotated s -> DynFormula s) -> DynFormula s+afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f 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) ->+ DynFormula s+after act f = DynFormula $ \n -> After act $ \x s -> unDynFormula (f x s) n++-- | Disjunction for DL formulae.+-- Is `True` if either formula is `True`. The choice is /angelic/, ie. it is+-- always made by the "caller". This is mostly important in case a test is+-- `Stuck`.+(|||) :: DynFormula s -> DynFormula s -> DynFormula s+-- In formulae, we use only angelic choice. But it becomes demonic+-- after one step (that is, the choice has been made).+DynFormula f ||| DynFormula g = DynFormula $ \n -> Alt Angelic (f n) (g n)++-- | First-order quantification of variables.+-- Formula @f@ is `True` iff. it is `True` /for all/ possible values of `q`. The+-- underlying framework will generate values of `q` and check the formula holds+-- for those values. `Quantifiable` values are thus values that can be generated+-- and checked and the `Test.QuickCheck.DynamicLogic.Quantify` module defines+-- basic combinators to build those from building blocks.+forAllQ ::+ Quantifiable q =>+ q ->+ (Quantifies q -> DynFormula s) ->+ DynFormula s+forAllQ q f+ | isEmptyQ q' = ignore+ | otherwise = DynFormula $ \n -> ForAll q' $ ($ n) . unDynFormula . f+ where+ q' = quantify q++-- | Adjust weight for selecting formula.+-- This is mostly useful in relation with `(|||)` combinator, in order to tweak the+-- priority for generating the next step(s) of the test that matches the formula.+weight :: Double -> DynFormula s -> DynFormula s+weight w f = DynFormula $ Weight w . unDynFormula f++-- | Get the current QuickCheck size parameter.+withSize :: (Int -> DynFormula s) -> DynFormula s+withSize f = DynFormula $ \n -> unDynFormula (f n) n++-- | Prioritise doing this if we are+-- trying to stop generation.+toStop :: DynFormula s -> DynFormula s+toStop (DynFormula f) = DynFormula $ Stopping . f++-- | Successfully ends the test.+done :: Annotated s -> DynFormula s+done _ = passTest++-- | Ends test with given error message.+errorDL :: String -> DynFormula s+errorDL s = DynFormula . const $ Error s (const EmptySpec)++-- | Embed QuickCheck's monitoring functions (eg. `label`, `tabulate`) in+-- a formula.+-- This is useful to improve the reporting from test execution, esp. in the+-- case of failures.+monitorDL :: (Property -> Property) -> DynFormula s -> DynFormula s+monitorDL m (DynFormula f) = DynFormula $ Monitor m . f++-- | Formula should hold at any state.+-- In effect this leads to exploring alternatives from a given state `s` and ensuring+-- formula holds in all those states.+always :: (Annotated s -> DynFormula s) -> (Annotated s -> DynFormula s)+always p s = withSize $ \n -> toStop (p s) ||| p s ||| weight (fromIntegral n) (afterAny (always p))++data FailingAction s+ = ErrorFail String+ | forall a. (Typeable a, Eq (Action s a)) => ActionFail (Action s a)++instance StateModel s => HasVariables (FailingAction s) where+ getAllVariables ErrorFail{} = mempty+ getAllVariables (ActionFail a) = getAllVariables a++instance StateModel s => Eq (FailingAction s) where+ ErrorFail s == ErrorFail s' = s == s'+ ActionFail (a :: Action s a) == ActionFail (a' :: Action s a')+ | Just Refl <- eqT @a @a' = a == a'+ _ == _ = False++instance StateModel s => Show (FailingAction s) where+ show (ErrorFail s) = "Error " ++ show s+ show (ActionFail a) = show a++data DynLogicTest s+ = BadPrecondition (TestSequence s) (FailingAction s) (Annotated s)+ | Looping (TestSequence s)+ | Stuck (TestSequence s) (Annotated s)+ | DLScript (TestSequence s)++data Witnesses r where+ Do :: r -> Witnesses r+ Witness :: QuantifyConstraints a => a -> Witnesses r -> Witnesses r++discardWitnesses :: Witnesses r -> r+discardWitnesses (Do r) = r+discardWitnesses (Witness _ k) = discardWitnesses k++pattern Witnesses :: Witnesses () -> r -> Witnesses r+pattern Witnesses w r <- ((\wit -> (void wit, discardWitnesses wit)) -> (w, r))+ where+ Witnesses w r = r <$ w++{-# COMPLETE Witnesses #-}++deriving instance Functor Witnesses+deriving instance Foldable Witnesses+deriving instance Traversable Witnesses++instance Eq r => Eq (Witnesses r) where+ Do r == Do r' = r == r'+ Witness (a :: a) k == Witness (a' :: a') k' =+ case eqT @a @a' of+ Just Refl -> a == a' && k == k'+ Nothing -> False+ _ == _ = False++instance Show r => Show (Witnesses r) where+ show (Do r) = "Do $ " ++ show r+ show (Witness a k) = "Witness (" ++ show a ++ " :: " ++ show (typeOf a) ++ ")\n" ++ show k -- TODO++type TestStep s = Witnesses (Step s)++newtype TestSequence s = TestSeq (Witnesses (TestContinuation s))+ deriving (Show, Eq)++data TestContinuation s+ = ContStep (Step s) (TestSequence s)+ | ContStop++pattern TestSeqStop :: TestSequence s+pattern TestSeqStop = TestSeq (Do ContStop)++pattern TestSeqStep :: Step s -> TestSequence s -> TestSequence s+pattern TestSeqStep s ss = TestSeq (Do (ContStep s ss))++-- The `()` are the constraints required to use the pattern, and the `(Typeable a, ...)` are the+-- ones provided when you do (including a fresh type variable `a`).+-- See https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html#typing-of-pattern-synonyms+pattern TestSeqWitness :: () => forall a. QuantifyConstraints a => a -> TestSequence s -> TestSequence s+pattern TestSeqWitness a ss <- TestSeq (Witness a (TestSeq -> ss))+ where+ TestSeqWitness a (TestSeq ss) = TestSeq (Witness a ss)++{-# COMPLETE TestSeqWitness, TestSeqStep, TestSeqStop #-}++deriving instance StateModel s => Show (TestContinuation s)+deriving instance StateModel s => Eq (TestContinuation s)++consSeq :: TestStep s -> TestSequence s -> TestSequence s+consSeq step ss = TestSeq $ flip ContStep ss <$> step++unconsSeq :: TestSequence s -> Maybe (TestStep s, TestSequence s)+unconsSeq (TestSeq ss) =+ case discardWitnesses ss of+ ContStop -> Nothing+ ContStep s rest -> Just (s <$ ss, rest)++unstopSeq :: TestSequence s -> Maybe (Witnesses ())+unstopSeq (TestSeq ss) =+ case discardWitnesses ss of+ ContStop -> Just $ () <$ ss+ ContStep{} -> Nothing++pattern TestSeqStopW :: Witnesses () -> TestSequence s+pattern TestSeqStopW w <- (unstopSeq -> Just w)+ where+ TestSeqStopW w = TestSeq (ContStop <$ w)++pattern (:>) :: TestStep s -> TestSequence s -> TestSequence s+pattern step :> ss <- (unconsSeq -> Just (step, ss))+ where+ step :> ss = consSeq step ss++{-# COMPLETE TestSeqStopW, (:>) #-}++nullSeq :: TestSequence s -> Bool+nullSeq TestSeqStop = True+nullSeq _ = False++dropSeq :: Int -> TestSequence s -> TestSequence s+dropSeq n _ | n < 0 = error "dropSeq: negative number"+dropSeq 0 ss = ss+dropSeq _ TestSeqStop = TestSeqStop+dropSeq n (TestSeqWitness _ ss) = dropSeq (n - 1) ss+dropSeq n (TestSeqStep _ ss) = dropSeq (n - 1) ss++getContinuation :: TestSequence s -> TestSequence s+getContinuation (TestSeq w) = case discardWitnesses w of+ ContStop -> TestSeqStop+ ContStep _ s -> s++unlines' :: [String] -> String+unlines' [] = ""+unlines' xs = init $ unlines xs++prettyTestSequence :: VarContext -> TestSequence s -> String+prettyTestSequence ctx ss = unlines' $ zipWith (++) ("do " : repeat " ") $ prettySeq ss+ where+ prettySeq (TestSeqStopW w) = prettyWitnesses w+ prettySeq (Witnesses w step :> ss') = prettyWitnesses w ++ show (WithUsedVars ctx step) : prettySeq ss'++prettyWitnesses :: Witnesses () -> [String]+prettyWitnesses (Witness a w) = ("_ <- forAllQ $ exactlyQ $ " ++ show a) : prettyWitnesses w+prettyWitnesses Do{} = []++instance StateModel s => Show (DynLogicTest s) where+ show (BadPrecondition ss bad s) =+ prettyTestSequence (usedVariables ss <> allVariables bad) ss+ ++ "\n -- In state: "+ ++ show s+ ++ "\n "+ ++ prettyBad bad+ where+ prettyBad :: FailingAction s -> String+ prettyBad (ErrorFail e) = "assert " ++ show e ++ " False"+ prettyBad (ActionFail a) = "action $ " ++ show a ++ " -- Failed precondition\n pure ()"+ show (Looping ss) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n -- Looping"+ show (Stuck ss s) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n -- Stuck in state " ++ show s+ show (DLScript ss) = prettyTestSequence (usedVariables ss) ss ++ "\n pure ()\n"++usedVariables :: forall s. StateModel s => TestSequence s -> VarContext+usedVariables = go initialAnnotatedState+ where+ go :: Annotated s -> TestSequence s -> VarContext+ go aState TestSeqStop = allVariables (underlyingState aState)+ go aState (TestSeqWitness a ss) = allVariables a <> go aState ss+ go aState (TestSeqStep step@(_ := act) ss) =+ allVariables act+ <> allVariables (underlyingState aState)+ <> go (nextStateStep step aState) ss++-- | Restricted calls are not generated by "AfterAny"; they are included+-- in tests explicitly using "After" in order to check specific+-- 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 _ = False++-- * Generate Properties++-- | Simplest "execution" function for `DynFormula`.+-- Turns a given a `DynFormula` paired with an interpreter function to produce some result from an++--- `Actions` sequence into a proper `Property` than can then be run by QuickCheck.+forAllScripts ::+ (DynLogicModel s, Testable a) =>+ DynFormula s ->+ (Actions s -> a) ->+ Property+forAllScripts = forAllMappedScripts id id++-- | `Property` function suitable for formulae without choice.+forAllUniqueScripts ::+ (DynLogicModel s, Testable a) =>+ Int ->+ Annotated s ->+ DynFormula s ->+ (Actions s -> a) ->+ Property+forAllUniqueScripts n s f k =+ QC.withSize $ \sz ->+ let d = unDynFormula f sz+ in case generate chooseUniqueNextStep d n s 500 of+ Nothing -> counterexample "Generating Non-unique script in forAllUniqueScripts" False+ Just test -> validDLTest d test . applyMonitoring d test . property $ k (scriptFromDL test)++-- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose.+forAllMappedScripts ::+ (DynLogicModel s, Testable a) =>+ (rep -> DynLogicTest s) ->+ (DynLogicTest s -> rep) ->+ DynFormula s ->+ (Actions s -> a) ->+ Property+forAllMappedScripts to from f k =+ QC.withSize $ \n ->+ let d = unDynFormula f n+ in forAllShrinkBlind+ (Smart 0 <$> sized ((from <$>) . generateDLTest d))+ (shrinkSmart ((from <$>) . shrinkDLTest d . to))+ $ \(Smart _ script) ->+ withDLScript d k (to script)++withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property+withDLScript d k test =+ validDLTest d test . applyMonitoring d test . property $ k (scriptFromDL test)++withDLScriptPrefix :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property+withDLScriptPrefix f k test =+ QC.withSize $ \n ->+ let d = unDynFormula f n+ test' = unfailDLTest d test+ in validDLTest d test' . applyMonitoring d test' . property $ k (scriptFromDL test')++generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)+generateDLTest d size = generate chooseNextStep d 0 (initialStateFor d) size++onDLTestSeq :: (TestSequence s -> TestSequence s) -> DynLogicTest s -> DynLogicTest s+onDLTestSeq f (BadPrecondition ss bad s) = BadPrecondition (f ss) bad s+onDLTestSeq f (Looping ss) = Looping (f ss)+onDLTestSeq f (Stuck ss s) = Stuck (f ss) s+onDLTestSeq f (DLScript ss) = DLScript (f ss)++consDLTest :: TestStep s -> DynLogicTest s -> DynLogicTest s+consDLTest step = onDLTestSeq (step :>)++consDLTestW :: Witnesses () -> DynLogicTest s -> DynLogicTest s+consDLTestW w = onDLTestSeq (addW w)+ where+ addW Do{} ss = ss+ addW (Witness a w') ss = TestSeqWitness a (addW w' ss)++generate ::+ (Monad m, DynLogicModel s) =>+ (Annotated s -> Int -> DynLogic s -> m (NextStep s)) ->+ DynLogic s ->+ Int ->+ Annotated s ->+ Int ->+ m (DynLogicTest s)+generate chooseNextStepFun d n s size =+ if n > sizeLimit size+ then return $ Looping TestSeqStop+ else do+ let preferred = if n > size then stopping d else noStopping d+ useStep (BadAction (Witnesses ws bad)) _ = return $ BadPrecondition (TestSeqStopW ws) bad s+ useStep StoppingStep _ = return $ DLScript TestSeqStop+ useStep (Stepping step d') _ =+ case discardWitnesses step of+ var := act ->+ consDLTest step+ <$> generate+ chooseNextStepFun+ d'+ (n + 1)+ (computeNextState s act var)+ size+ useStep NoStep alt = alt+ foldr+ (\step k -> do try <- chooseNextStepFun s n step; useStep try k)+ (return $ Stuck TestSeqStop s)+ [preferred, noAny preferred, d, noAny d]++sizeLimit :: Int -> Int+sizeLimit size = 2 * size + 20++initialStateFor :: StateModel s => DynLogic s -> Annotated s+initialStateFor _ = initialAnnotatedState++stopping :: DynLogic s -> DynLogic s+stopping EmptySpec = EmptySpec+stopping Stop = Stop+stopping (After act k) = After act k+stopping (Error m k) = Error m k+stopping (AfterAny _) = EmptySpec+stopping (Alt b d d') = Alt b (stopping d) (stopping d')+stopping (Stopping d) = d+stopping (Weight w d) = Weight w (stopping d)+stopping (ForAll _ _) = EmptySpec -- ???+stopping (Monitor f d) = Monitor f (stopping d)++noStopping :: DynLogic s -> DynLogic s+noStopping EmptySpec = EmptySpec+noStopping Stop = EmptySpec+noStopping (After act k) = After act k+noStopping (Error m k) = Error m k+noStopping (AfterAny k) = AfterAny k+noStopping (Alt b d d') = Alt b (noStopping d) (noStopping d')+noStopping (Stopping _) = EmptySpec+noStopping (Weight w d) = Weight w (noStopping d)+noStopping (ForAll q f) = ForAll q f+noStopping (Monitor f d) = Monitor f (noStopping d)++noAny :: DynLogic s -> DynLogic s+noAny EmptySpec = EmptySpec+noAny Stop = Stop+noAny (After act k) = After act k+noAny (Error m k) = Error m k+noAny (AfterAny _) = EmptySpec+noAny (Alt b d d') = Alt b (noAny d) (noAny d')+noAny (Stopping d) = Stopping (noAny d)+noAny (Weight w d) = Weight w (noAny d)+noAny (ForAll q f) = ForAll q f+noAny (Monitor f d) = Monitor f (noAny d)++nextSteps :: DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]+nextSteps = nextSteps' generateQ++nextSteps' :: Monad m => (forall a. Quantification a -> m a) -> DynLogic s -> m [(Double, Witnesses (DynLogic s))]+nextSteps' _ EmptySpec = pure []+nextSteps' _ Stop = pure [(1, Do $ Stop)]+nextSteps' _ (After act k) = pure [(1, Do $ After act k)]+nextSteps' _ (Error m k) = pure [(1, Do $ Error m k)]+nextSteps' _ (AfterAny k) = pure [(1, Do $ AfterAny k)]+nextSteps' gen (Alt _ d d') = (++) <$> nextSteps' gen d <*> nextSteps' gen d'+nextSteps' gen (Stopping d) = nextSteps' gen d+nextSteps' gen (Weight w d) = do+ steps <- nextSteps' gen d+ pure [(w * w', s) | (w', s) <- steps, w * w' > never]+nextSteps' gen (ForAll q f) = do+ x <- gen q+ map (second $ Witness x) <$> nextSteps' gen (f x)+nextSteps' gen (Monitor _f d) = nextSteps' gen d++chooseOneOf :: [(Double, a)] -> Gen a+chooseOneOf steps = frequency [(round (w / never), return s) | (w, s) <- steps]++never :: Double+never = 1.0e-9++data NextStep s+ = StoppingStep+ | Stepping (Witnesses (Step s)) (DynLogic s)+ | NoStep+ | BadAction (Witnesses (FailingAction s))++chooseNextStep :: DynLogicModel s => Annotated s -> Int -> DynLogic s -> Gen (NextStep s)+chooseNextStep s n d = do+ nextSteps d >>= \case+ [] -> return NoStep+ steps -> do+ let bads = concatMap (findBad . snd) steps+ findBad = traverse $ flip badActions s+ case bads of+ [] -> do+ chosen <- chooseOneOf steps+ let takeStep = \case+ Stop -> return StoppingStep+ After a k ->+ return $ Stepping (Do $ mkVar n := a) (k (mkVar n) (computeNextState s a (mkVar n)))+ AfterAny k -> do+ m <- keepTryingUntil 100 (computeArbitraryAction s) $+ \case+ Some act -> computePrecondition s act && not (restricted act)+ case m of+ Nothing -> return NoStep+ Just (Some a) ->+ return $+ Stepping+ (Do $ mkVar n := a)+ (k (computeNextState s a (mkVar n)))+ EmptySpec -> error "chooseNextStep: EmptySpec"+ ForAll{} -> error "chooseNextStep: ForAll"+ Error{} -> error "chooseNextStep: Error"+ Alt{} -> error "chooseNextStep: Alt"+ Stopping{} -> error "chooseNextStep: Stopping"+ Weight{} -> error "chooseNextStep: Weight"+ Monitor{} -> error "chooseNextStep: Monitor"+ go (Do d') = takeStep d'+ go (Witness a step) =+ go step+ >>= pure . \case+ StoppingStep -> StoppingStep -- TODO: This is a bit fishy+ Stepping step' dl -> Stepping (Witness a step') dl+ NoStep -> NoStep+ BadAction bad -> BadAction (Witness a bad)+ go chosen+ b : _ -> return $ BadAction b++chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => Annotated s -> Int -> DynLogic s -> m (NextStep s)+chooseUniqueNextStep s n d = do+ steps <- map snd <$> nextSteps' (const bad) d+ case steps of+ [] -> return NoStep+ [Do EmptySpec] -> return NoStep+ [Do Stop] -> return StoppingStep+ [Do (After a k)] -> return $ Stepping (Do $ mkVar n := a) (k (mkVar n) (computeNextState s a (mkVar n)))+ _ -> bad+ where+ bad = fail "chooseUniqueNextStep: non-unique action in DynLogic"++keepTryingUntil :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)+keepTryingUntil 0 _ _ = return Nothing+keepTryingUntil n g p = do+ x <- g+ if p x then return $ Just x else scale (+ 1) $ keepTryingUntil (n - 1) g p++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.+ case (tc, test) of+ (DLScript _, _) -> True+ (_, DLScript _) -> False+ _ -> True+ ]++nextStateStep :: StateModel s => Step s -> Annotated s -> Annotated s+nextStateStep (var := act) s = computeNextState s act var++shrinkScript :: DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s]+shrinkScript = shrink' initialAnnotatedState+ where+ shrink' :: DynLogicModel s => Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]+ shrink' s d ss = structural s d ss ++ nonstructural s d ss++ nonstructural s d (TestSeqWitness a ss) =+ [ TestSeqWitness a' ss'+ | a' <- shrinkWitness d a+ , ss' <- ss : shrink' s (stepDLSeq d s $ TestSeqWitness a TestSeqStop) ss+ ]+ nonstructural s d (TestSeqStep step@(var := act) ss) =+ [TestSeqStep (unsafeCoerceVar var := act') ss | Some act' <- computeShrinkAction s act]+ ++ [ TestSeqStep step ss'+ | ss' <-+ shrink'+ (nextStateStep step s)+ (stepDLStep d s step)+ ss+ ]+ nonstructural _ _ TestSeqStop = []++ structural _ _ TestSeqStopW{} = []+ structural s d (step :> rest) =+ TestSeqStop+ : reverse (takeWhile (not . nullSeq) [dropSeq (n - 1) rest | n <- iterate (* 2) 1])+ ++ map (step :>) (shrink' (nextStateStep (discardWitnesses step) s) (stepDLSeq d s (step :> TestSeqStop)) rest)++shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a]+shrinkWitness (ForAll (q :: Quantification a) _) (a :: a') =+ case eqT @a @a' of+ Just Refl | isaQ q a -> shrinkQ q a+ _ -> []+shrinkWitness (Alt _ d d') a = shrinkWitness d a ++ shrinkWitness d' a+shrinkWitness (Stopping d) a = shrinkWitness d a+shrinkWitness (Weight _ d) a = shrinkWitness d a+shrinkWitness (Monitor _ d) a = shrinkWitness d a+shrinkWitness EmptySpec{} _ = []+shrinkWitness Stop{} _ = []+shrinkWitness Error{} _ = []+shrinkWitness After{} _ = []+shrinkWitness AfterAny{} _ = []++-- The result of pruning a list of actions is a prefix of a list of actions that+-- could have been generated by the dynamic logic.+pruneDLTest :: DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s+pruneDLTest dl = prune [dl] initialAnnotatedState+ where+ prune [] _ _ = TestSeqStop+ prune _ _ TestSeqStop = TestSeqStop+ prune ds s (TestSeqWitness a ss) =+ case [d' | d <- ds, d' <- stepDLW d a] of+ [] -> prune ds s ss+ ds' -> TestSeqWitness a $ prune ds' s ss+ prune ds s (TestSeqStep step@(_ := act) ss)+ | computePrecondition s act =+ case [d' | d <- ds, d' <- stepDL d s (Do step)] of+ [] -> prune ds s ss+ ds' -> TestSeqStep step $ prune ds' (nextStateStep step s) ss+ | otherwise = prune ds s ss++stepDL :: DynLogicModel s => DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]+stepDL (After a k) s (Do (var := act))+ -- TOOD: make this nicer when we migrate to 9.2 where we can just bind+ -- the type variables cleanly and do `Just Refl <- eqT ...` here instead.+ | Some a == Some act = [k (unsafeCoerceVar var) (computeNextState s act (unsafeCoerceVar var))]+stepDL (AfterAny k) s (Do (var := act))+ | not (restricted act) = [k (computeNextState s act var)]+stepDL (Alt _ d d') s step = stepDL d s step ++ stepDL d' s step+stepDL (Stopping d) s step = stepDL d s step+stepDL (Weight _ d) s step = stepDL d s step+stepDL (ForAll (q :: Quantification a) f) s (Witness (a :: a') step) =+ case eqT @a @a' of+ Just Refl -> [d | isaQ q a, d <- stepDL (f a) s step]+ Nothing -> []+stepDL (Monitor _f d) s step = stepDL d s step+stepDL _ _ _ = []++stepDLW :: forall a s. (DynLogicModel s, Typeable a) => DynLogic s -> a -> [DynLogic s]+stepDLW (ForAll (q :: Quantification a') k) a =+ case eqT @a @a' of+ Just Refl -> [k a | isaQ q a]+ Nothing -> []+stepDLW (Alt _ d d') a = stepDLW d a ++ stepDLW d' a+stepDLW (Monitor _ d) a = stepDLW d a+stepDLW (Weight _ d) a = stepDLW d a+stepDLW (Stopping d) a = stepDLW d a+stepDLW _ _ = []++stepDLSeq :: DynLogicModel s => DynLogic s -> Annotated s -> TestSequence s -> DynLogic s+stepDLSeq d _ (TestSeqStopW Do{}) = d+stepDLSeq d s (TestSeqStopW (Witness a w)) = stepDLSeq (stepDLWitness d a) s (TestSeqStopW w)+stepDLSeq d s (step@(Witnesses _ (var := act)) :> ss) =+ stepDLSeq (demonicAlt $ stepDL d s step) (computeNextState s act var) ss++stepDLWitness :: forall a s. (DynLogicModel s, Typeable a) => DynLogic s -> a -> DynLogic s+stepDLWitness d a = demonicAlt $ stepDLW d a++stepDLStep :: DynLogicModel s => DynLogic s -> Annotated s -> Step s -> DynLogic s+stepDLStep d s step = stepDLSeq d s (TestSeqStep step TestSeqStop)++demonicAlt :: [DynLogic s] -> DynLogic s+demonicAlt [] = EmptySpec+demonicAlt ds = foldr1 (Alt Demonic) ds++propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property+propPruningGeneratedScriptIsNoop d =+ forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest d) $ \test ->+ let script = case test of+ BadPrecondition s _ _ -> s+ Looping s -> s+ Stuck s _ -> s+ DLScript s -> s+ in script == pruneDLTest d script++getScript :: DynLogicTest s -> TestSequence s+getScript (BadPrecondition s _ _) = s+getScript (Looping s) = s+getScript (Stuck s _) = s+getScript (DLScript s) = s++makeTestFromPruned :: DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s+makeTestFromPruned dl = make dl initialAnnotatedState+ where+ make d s TestSeqStop+ | b : _ <- badActions d s = BadPrecondition TestSeqStop b s+ | stuck d s = Stuck TestSeqStop s+ | otherwise = DLScript TestSeqStop+ make d s (TestSeqWitness a ss) =+ onDLTestSeq (TestSeqWitness a) $+ make+ (stepDLWitness d a)+ s+ ss+ make d s (TestSeqStep step ss) =+ onDLTestSeq (TestSeqStep step) $+ make+ (stepDLStep d s step)+ (nextStateStep step s)+ ss++-- | If failed, return the prefix up to the failure. Also prunes the test in case the model has+-- changed.+unfailDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> DynLogicTest s+unfailDLTest d test = makeTestFromPruned d $ pruneDLTest d steps+ where+ steps = case test of+ BadPrecondition as _ _ -> as+ Stuck as _ -> as+ DLScript as -> as+ Looping as -> as++stuck :: DynLogicModel s => DynLogic s -> Annotated s -> Bool+stuck EmptySpec _ = True+stuck Stop _ = False+stuck (After _ _) _ = False+stuck (Error _ _) _ = False+stuck (AfterAny _) s =+ not $+ canGenerate+ 0.01+ (computeArbitraryAction s)+ ( \case+ Some act ->+ computePrecondition s act+ && not (restricted act)+ )+stuck (Alt Angelic d d') s = stuck d s && stuck d' s+stuck (Alt Demonic d d') s = stuck d s || stuck d' s+stuck (Stopping d) s = stuck d s+stuck (Weight w d) s = w < never || stuck d s+stuck (ForAll _ _) _ = False+stuck (Monitor _ d) s = stuck d s++validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property -> Property+validDLTest _ Stuck{} _ = False ==> False+validDLTest _ test@DLScript{} p = counterexample (show test) p+validDLTest _ test _ = counterexample (show test) False++scriptFromDL :: DynLogicTest s -> Actions s+scriptFromDL (DLScript s) = Actions $ sequenceSteps s+scriptFromDL _ = Actions []++sequenceSteps :: TestSequence s -> [Step s]+sequenceSteps (TestSeq ss) =+ case discardWitnesses ss of+ ContStop -> []+ ContStep s ss' -> s : sequenceSteps ss'++badActionsGiven :: StateModel s => DynLogic s -> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]+badActionsGiven Stop _ _ = []+badActionsGiven EmptySpec _ _ = []+badActionsGiven AfterAny{} _ _ = []+badActionsGiven (ForAll _ k) s (Witness a step) =+ case cast a of+ Just a' -> Witness a' <$> badActionsGiven (k a') s step+ _ -> []+badActionsGiven (Alt _ d d') s w = badActionsGiven d s w ++ badActionsGiven d' s w+badActionsGiven (Stopping d) s w = badActionsGiven d s w+badActionsGiven (Weight k d) s w = if k < never then [] else badActionsGiven d s w+badActionsGiven (Monitor _ d) s w = badActionsGiven d s w+badActionsGiven d s (Do _) = Do <$> badActions d s+badActionsGiven Error{} _ _ = []+badActionsGiven After{} _ _ = []++badActions :: StateModel s => DynLogic s -> Annotated s -> [FailingAction s]+badActions EmptySpec _ = []+badActions Stop _ = []+badActions (After a _) s+ | computePrecondition s a = []+ | otherwise = [ActionFail a]+badActions (Error m _) _s = [ErrorFail m]+badActions (AfterAny _) _ = []+badActions (Alt _ d d') s = badActions d s ++ badActions d' s+badActions (Stopping d) s = badActions d s+badActions (Weight w d) s = if w < never then [] else badActions d s+badActions (ForAll _ _) _ = []+badActions (Monitor _ d) s = badActions d s++applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property+applyMonitoring d (DLScript s) p =+ case findMonitoring d initialAnnotatedState s of+ Just f -> f p+ Nothing -> p+applyMonitoring _ Stuck{} p = p+applyMonitoring _ Looping{} p = p+applyMonitoring _ BadPrecondition{} p = p++findMonitoring :: DynLogicModel s => DynLogic s -> Annotated s -> TestSequence s -> Maybe (Property -> Property)+findMonitoring Stop _s TestSeqStop = Just id+findMonitoring (After a k) s (TestSeqStep (var := a') as)+ -- TODO: do nicely with eqT instead (avoids `unsafeCoerceVar`)+ | Some a == Some a' = findMonitoring (k (unsafeCoerceVar var) s') s' as+ where+ s' = computeNextState s a' (unsafeCoerceVar var)+findMonitoring (AfterAny k) s as@(TestSeqStep (_var := a) _)+ | not (restricted a) = findMonitoring (After a $ const k) s as+findMonitoring (Alt _b d d') s as =+ -- Give priority to monitoring matches to the left. Combining both+ -- results in repeated monitoring from always, which is unexpected.+ findMonitoring d s as <|> findMonitoring d' s as+findMonitoring (Stopping d) s as = findMonitoring d s as+findMonitoring (Weight _ d) s as = findMonitoring d s as+findMonitoring (ForAll (_q :: Quantification a) k) s (TestSeq (Witness (a :: a') as)) =+ case eqT @a @a' of+ Just Refl -> findMonitoring (k a) s (TestSeq as)+ Nothing -> Nothing+findMonitoring (Monitor m d) s as =+ (m .) <$> findMonitoring d s as+findMonitoring _ _ _ = Nothing
src/Test/QuickCheck/DynamicLogic/Quantify.hs view
@@ -5,6 +5,7 @@ -- a `t`, shrink a `t`, and recognise a generated `t`. module Test.QuickCheck.DynamicLogic.Quantify ( Quantification (isaQ),+ QuantifyConstraints, isEmptyQ, generateQ, shrinkQ,@@ -27,6 +28,7 @@ import System.Random import Test.QuickCheck import Test.QuickCheck.DynamicLogic.CanGenerate+import Test.QuickCheck.StateModel -- | A `Quantification` over a type @a@ is a generator that can be used with -- `Plutus.Contract.Test.ContractModel.forAllQ` to generate random values in@@ -71,8 +73,8 @@ (guard (a <= b) >> Just (choose r)) is (filter is . shrink)- where- is x = a <= x && x <= b+ where+ is x = a <= x && x <= b -- | Pick a random value from a list. Treated as an empty choice if the list is empty: --@@ -81,10 +83,10 @@ -- @ elementsQ :: Eq a => [a] -> Quantification a elementsQ as = Quantification g (`elem` as) (\a -> takeWhile (/= a) as)- where- g- | null as = Nothing- | otherwise = Just (elements as)+ where+ g+ | null as = Nothing+ | otherwise = Just (elements as) -- | Choose from a weighted list of quantifications. Treated as an `Control.Applicative.empty` -- choice if no quantification has weight > 0.@@ -97,13 +99,13 @@ ) (isa iqs) (shr iqs)- where- isa [] _ = False- isa ((i, q) : iqs) a = (i > 0 && isaQ q a) || isa iqs a- shr [] _ = []- shr ((i, q) : iqs) a =- [a' | i > 0, isaQ q a, a' <- shrQ q a]- ++ shr iqs a+ where+ isa [] _ = False+ isa ((i, q) : iqs) a = (i > 0 && isaQ q a) || isa iqs a+ shr [] _ = []+ shr ((i, q) : iqs) a =+ [a' | i > 0, isaQ q a, a' <- shrQ q a]+ ++ shr iqs a -- | Choose from a list of quantifications. Same as `frequencyQ` with all weights the same (and > -- 0).@@ -143,6 +145,8 @@ (\(a, a') -> isaQ q a && isaQ q' a') (\(a, a') -> map (,a') (shrQ q a) ++ map (a,) (shrQ q' a')) +type QuantifyConstraints a = (Eq a, Show a, Typeable a, HasVariables a)+ -- | Generalization of `Quantification`s, which lets you treat lists and tuples of quantifications -- as quantifications. For instance, --@@ -152,7 +156,7 @@ -- ... -- @ class- (Eq (Quantifies q), Show (Quantifies q), Typeable (Quantifies q)) =>+ QuantifyConstraints (Quantifies q) => Quantifiable q where -- | The type of values quantified over.@@ -165,7 +169,7 @@ -- | Computing the actual `Quantification`. quantify :: q -> Quantification (Quantifies q) -instance (Eq a, Show a, Typeable a) => Quantifiable (Quantification a) where+instance QuantifyConstraints a => Quantifiable (Quantification a) where type Quantifies (Quantification a) = a quantify = id @@ -176,9 +180,9 @@ instance (Quantifiable a, Quantifiable b, Quantifiable c) => Quantifiable (a, b, c) where type Quantifies (a, b, c) = (Quantifies a, Quantifies b, Quantifies c) quantify (a, b, c) = mapQ (to, from) (quantify a `pairQ` (quantify b `pairQ` quantify c))- where- to (a, (b, c)) = (a, b, c)- from (a, b, c) = (a, (b, c))+ where+ to (a, (b, c)) = (a, b, c)+ from (a, b, c) = (a, (b, c)) instance (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d) => Quantifiable (a, b, c, d) where type@@ -186,9 +190,9 @@ (Quantifies a, Quantifies b, Quantifies c, Quantifies d) quantify (a, b, c, d) = mapQ (to, from) (quantify a `pairQ` (quantify b `pairQ` (quantify c `pairQ` quantify d)))- where- to (a, (b, (c, d))) = (a, b, c, d)- from (a, b, c, d) = (a, (b, (c, d)))+ where+ to (a, (b, (c, d))) = (a, b, c, d)+ from (a, b, c, d) = (a, (b, (c, d))) instance (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d, Quantifiable e) =>@@ -199,9 +203,9 @@ (Quantifies a, Quantifies b, Quantifies c, Quantifies d, Quantifies e) quantify (a, b, c, d, e) = mapQ (to, from) (quantify a `pairQ` (quantify b `pairQ` (quantify c `pairQ` (quantify d `pairQ` quantify e))))- where- to (a, (b, (c, (d, e)))) = (a, b, c, d, e)- from (a, b, c, d, e) = (a, (b, (c, (d, e))))+ where+ to (a, (b, (c, (d, e)))) = (a, b, c, d, e)+ from (a, b, c, d, e) = (a, (b, (c, (d, e)))) instance Quantifiable a => Quantifiable [a] where type Quantifies [a] = [Quantifies a]@@ -209,10 +213,10 @@ quantify (a : as) = mapQ (to, from) (pairQ (quantify a) (quantify as)) `whereQ` (not . null)- where- to (x, xs) = x : xs- from (x : xs) = (x, xs)- from [] = error "quantify: impossible"+ where+ to (x, xs) = x : xs+ from (x : xs) = (x, xs)+ from [] = error "quantify: impossible" validQuantification :: Show a => Quantification a -> Property validQuantification q =
src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs view
@@ -6,9 +6,9 @@ -- Smart type wrapper in Test.QuickCheck.Modifiers. shrinkSmart :: (a -> [a]) -> Smart a -> [Smart a] shrinkSmart shr (Smart i x) = take i' ys `ilv` drop i' ys- where- ys = [Smart j y | (j, y) <- [0 ..] `zip` shr x]- i' = 0 `max` (i - 2)- [] `ilv` bs = bs- as `ilv` [] = as- (a : as) `ilv` (b : bs) = a : b : (as `ilv` bs)+ where+ ys = [Smart j y | (j, y) <- [0 ..] `zip` shr x]+ i' = 0 `max` (i - 2)+ [] `ilv` bs = bs+ as `ilv` [] = as+ (a : as) `ilv` (b : bs) = a : b : (as `ilv` bs)
+ src/Test/QuickCheck/Extras.hs view
@@ -0,0 +1,15 @@+module Test.QuickCheck.Extras where++import Control.Monad.Reader+import Control.Monad.State+import Test.QuickCheck.Monadic++runPropertyStateT :: Monad m => PropertyM (StateT s m) a -> s -> PropertyM m (a, s)+runPropertyStateT p s0 = MkPropertyM $ \k -> do+ m <- unPropertyM (do a <- p; s <- run get; return (a, s)) $ fmap lift . k+ return $ evalStateT m s0++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
src/Test/QuickCheck/StateModel.hs view
@@ -8,33 +8,45 @@ -- be generated and executed against some /actual/ implementation code to define monadic `Property` -- to be asserted by QuickCheck. module Test.QuickCheck.StateModel (+ module Test.QuickCheck.StateModel.Variables, StateModel (..), RunModel (..),- Any (..),+ WithUsedVars (..),+ Annotated (..), Step (..), LookUp,- Var (..), -- we export the constructors so that users can construct test cases Actions (..), pattern Actions, EnvEntry (..), pattern (:=?), Env, Realized,+ Generic, stateAfter, runActions,- runActionsInState, lookUpVar, lookUpVarMaybe,+ initialAnnotatedState,+ computeNextState,+ computePrecondition,+ computeArbitraryAction,+ computeShrinkAction, ) where import Control.Monad+import Control.Monad.Identity import Control.Monad.Reader import Control.Monad.State+import Control.Monad.Writer (WriterT) import Data.Data import Data.Kind+import Data.List+import Data.Set qualified as Set+import GHC.Generics import Test.QuickCheck as QC import Test.QuickCheck.DynamicLogic.SmartShrinking import Test.QuickCheck.Monadic+import Test.QuickCheck.StateModel.Variables -- | The typeclass users implement to define a model against which to validate some implementation. --@@ -56,7 +68,9 @@ -- somewhat redundant with the generator's conditions, class ( forall a. Show (Action state a)+ , forall a. HasVariables (Action state a) , Show state+ , HasVariables state ) => StateModel state where@@ -87,15 +101,13 @@ actionName = head . words . show -- | Generator for `Action` depending on `state`.- -- The generated values are wrapped in `Any` type to allow the model to /not/ generate an action under- -- some circumstances: Any generated `Error` value will be ignored when generating a trace for testing.- arbitraryAction :: state -> Gen (Any (Action state))+ arbitraryAction :: VarContext -> state -> Gen (Any (Action state)) -- | Shrinker for `Action`. -- Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness -- of property-based testing.- shrinkAction :: Typeable a => state -> Action state a -> [Any (Action state)]- shrinkAction _ _ = []+ shrinkAction :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)]+ shrinkAction _ _ _ = [] -- | Initial state of generated traces. initialState :: state@@ -114,12 +126,16 @@ precondition :: state -> Action state a -> Bool precondition _ _ = True +deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))+ -- TODO: maybe it makes sense to write -- out a long list of these instances type family Realized (m :: Type -> Type) a :: Type type instance Realized IO a = a type instance Realized (StateT s m) a = Realized m a type instance Realized (ReaderT r m) a = Realized m a+type instance Realized (WriterT w m) a = Realized m a+type instance Realized Identity a = a class Monad m => RunModel state m where -- | Perform an `Action` in some `state` in the `Monad` `m`. This@@ -176,19 +192,7 @@ Nothing -> error $ "Variable " ++ show v ++ " is not bound!" Just a -> a -data Any f where- Some :: (Typeable a, Eq (f a)) => f a -> Any f- Error :: String -> Any f--deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))--instance Eq (Any f) where- Some (a :: f a) == Some (b :: f b) =- case eqT @a @b of- Just Refl -> a == b- Nothing -> False- Error s == Error s' = s == s'- _ == _ = False+data WithUsedVars a = WithUsedVars VarContext a data Step state where (:=) ::@@ -199,14 +203,21 @@ infix 5 := -deriving instance (forall a. Show (Action state a)) => Show (Step state)+instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where+ getAllVariables (var := act) = Set.insert (Some var) $ getAllVariables act -newtype Var a = Var Int- deriving (Eq, Ord, Show, Typeable, Data)+instance Show (Step state) where+ show (var := act) = show var ++ " <- action $ " ++ show act +instance Show (WithUsedVars (Step state)) where+ show (WithUsedVars ctx (var := act)) =+ if isWellTyped var ctx+ then show var ++ " <- action $ " ++ show act+ else "action $ " ++ show act+ instance Eq (Step state) where- (Var i := act) == (Var j := act') =- i == j && Some act == Some act'+ (v := act) == (v' := act') =+ unsafeCoerceVar v == v' && Some act == Some act' -- Action sequences use Smart shrinking, but this is invisible to -- client code because the extra Smart constructor is concealed by a@@ -216,6 +227,7 @@ -- but were then rejected by their precondition. data Actions state = Actions_ [String] (Smart [Step state])+ deriving (Generic) pattern Actions :: [Step state] -> Actions state pattern Actions as <-@@ -231,110 +243,144 @@ instance Eq (Actions state) where Actions as == Actions as' = as == as' -instance (forall a. Show (Action state a)) => Show (Actions state) where- showsPrec d (Actions as)- | d > 10 = ("(" ++) . shows (Actions as) . (")" ++)- | null as = ("Actions []" ++)- | otherwise =- ("Actions \n [" ++)- . foldr- (.)- (shows (last as) . ("]" ++))- [shows a . (",\n " ++) | a <- init as]+instance StateModel state => Show (Actions state) where+ show (Actions as) =+ let as' = WithUsedVars (usedVariables (Actions as)) <$> as+ in intercalate "\n" $ zipWith (++) ("do " : repeat " ") (map show as' ++ ["pure ()"]) -instance (StateModel state) => Arbitrary (Actions state) where+usedVariables :: forall state. StateModel state => Actions state -> VarContext+usedVariables (Actions as) = go initialAnnotatedState as+ where+ go :: Annotated state -> [Step state] -> VarContext+ go aState [] = allVariables (underlyingState aState)+ go aState ((var := act) : steps) =+ allVariables act+ <> allVariables (underlyingState aState)+ <> go (computeNextState aState act var) steps++instance StateModel state => Arbitrary (Actions state) where arbitrary = do- (as, rejected) <- arbActions initialState 1+ (as, rejected) <- arbActions initialAnnotatedState 1 return $ Actions_ rejected (Smart 0 as)- where- arbActions :: 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) -> do- (as, rejected) <- arbActions (nextState s act (Var step)) (step + 1)- return ((Var step := act) : as, rej ++ rejected)- Just Error{} -> error "impossible"- 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 $ arbitraryAction s- case a of- Some act ->- if precondition s act- then return (Just (Some act), rej)- else go (m + 1) n (actionName act : rej)- Error _ ->- go (m + 1) n rej+ 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) -> 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 act : rej) shrink (Actions_ rs as) = map (Actions_ rs) (shrinkSmart (map (prune . map fst) . shrinkList shrinker . withStates) as)- where- shrinker (Var i := act, s) = [(Var i := act', s) | Some act' <- shrinkAction s act]+ where+ shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act' <- computeShrinkAction s act] +-- Running state models++data Annotated state = Metadata+ { vars :: VarContext+ , underlyingState :: state+ }++instance Show state => Show (Annotated state) where+ show (Metadata ctx s) = show ctx ++ " |- " ++ show s++initialAnnotatedState :: StateModel state => Annotated state+initialAnnotatedState = Metadata mempty initialState++computePrecondition :: StateModel state => Annotated state -> Action state a -> Bool+computePrecondition s a =+ all (\(Some v) -> v `isWellTyped` vars s) (getAllVariables a)+ && precondition (underlyingState s) a++computeNextState ::+ (StateModel state, Typeable a) =>+ Annotated state ->+ Action state a ->+ Var a ->+ Annotated state+computeNextState s a v = Metadata (extendContext (vars s) v) (nextState (underlyingState s) a v)++computeArbitraryAction ::+ StateModel state =>+ Annotated state ->+ Gen (Any (Action state))+computeArbitraryAction s = arbitraryAction (vars s) (underlyingState s)++computeShrinkAction ::+ (Typeable a, StateModel state) =>+ Annotated state ->+ Action state a ->+ [Any (Action state)]+computeShrinkAction s = shrinkAction (vars s) (underlyingState s)+ prune :: StateModel state => [Step state] -> [Step state]-prune = loop initialState- where- loop _s [] = []- loop s ((var := act) : as)- | precondition s act =- (var := act) : loop (nextState s act var) as- | otherwise =- loop s as+prune = loop initialAnnotatedState+ where+ loop _s [] = []+ loop s ((var := act) : as)+ | computePrecondition s act =+ (var := act) : loop (computeNextState s act var) as+ | otherwise =+ loop s as -withStates :: StateModel state => [Step state] -> [(Step state, state)]-withStates = loop initialState- where- loop _s [] = []- loop s ((var := act) : as) =- (var := act, s) : loop (nextState s act var) as+withStates :: StateModel state => [Step state] -> [(Step state, Annotated state)]+withStates = loop initialAnnotatedState+ where+ loop _s [] = []+ loop s ((var := act) : as) =+ (var := act, s) : loop (computeNextState s act var) as -stateAfter :: StateModel state => Actions state -> state-stateAfter (Actions actions) = loop initialState actions- where- loop s [] = s- loop s ((var := act) : as) = loop (nextState s act var) as+stateAfter :: StateModel state => Actions state -> Annotated state+stateAfter (Actions actions) = loop initialAnnotatedState actions+ where+ loop s [] = s+ loop s ((var := act) : as) = loop (computeNextState s act var) as runActions :: forall state m. (StateModel state, RunModel state m) => Actions state ->- PropertyM m (state, Env m)-runActions = runActionsInState @_ @m initialState--runActionsInState ::- forall state m.- (StateModel state, RunModel state m) =>- state ->- Actions state ->- PropertyM m (state, Env m)-runActionsInState st (Actions_ rejected (Smart _ actions)) = loop st [] actions- where- loop _s env [] = do- unless (null rejected) $- monitor (tabulate "Actions rejected by precondition" rejected)- return (_s, reverse env)- loop s env ((Var n := act) : as) = do- pre $ precondition s act- ret <- run (perform s act (lookUpVar env))- let name = actionName act- monitor (tabulate "Actions" [name])- let var = Var n- s' = nextState s act var- env' = (var :== ret) : env- monitor (monitoring @state @m (s, s') act (lookUpVar env') ret)- b <- run $ postcondition (s, s') act (lookUpVar env) ret- assert b- loop s' env' as+ PropertyM m (Annotated state, Env m)+runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState [] actions+ where+ loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)+ loop _s env [] = do+ unless (null rejected) $+ monitor (tabulate "Actions rejected by precondition" rejected)+ return (_s, reverse env)+ loop s env ((v := act) : as) = do+ pre $ computePrecondition s act+ ret <- run (perform (underlyingState s) act (lookUpVar env))+ let name = actionName act+ monitor (tabulate "Actions" [name])+ let var = unsafeCoerceVar v+ s' = computeNextState s act var+ env' = (var :== ret) : env+ monitor (monitoring @state @m (underlyingState s, underlyingState s') act (lookUpVar env') ret)+ b <- run $ postcondition @state @m (underlyingState s, underlyingState s') act (lookUpVar env) ret+ assert b+ loop s' env' as
+ src/Test/QuickCheck/StateModel/Variables.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-}++module Test.QuickCheck.StateModel.Variables (+ Var,+ Any (..),+ HasVariables (..),+ HasNoVariables,+ VarContext,+ mkVar,+ ctxAtType,+ arbitraryVar,+ shrinkVar,+ extendContext,+ isWellTyped,+ allVariables,+ unsafeCoerceVar,+) where++import Data.Data+import Data.List+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Ord+import Data.Set (Set)+import Data.Set qualified as Set+import GHC.Generics+import Test.QuickCheck as QC++-- | A symbolic variable for a value of type `a`+newtype Var a = Var Int+ deriving (Eq, Ord, Typeable, Data)++mkVar :: Int -> Var a+mkVar = Var++instance Show (Var a) where+ show (Var i) = "var" ++ show i++-- | This type class gives you a way to get all the symbolic variables that+-- appear in a value.+class HasVariables a where+ getAllVariables :: a -> Set (Any Var)+ default getAllVariables :: (Generic a, GenericHasVariables (Rep a)) => a -> Set (Any Var)+ getAllVariables = genericGetAllVariables . from++instance HasVariables a => HasVariables (Smart a) where+ getAllVariables (Smart _ a) = getAllVariables a++instance Typeable a => HasVariables (Var a) where+ getAllVariables = Set.singleton . Some++instance (HasVariables k, HasVariables v) => HasVariables (Map k v) where+ getAllVariables = getAllVariables . Map.toList++instance HasVariables a => HasVariables (Set a) where+ getAllVariables = getAllVariables . Set.toList++newtype HasNoVariables a = HasNoVariables a++instance HasVariables (HasNoVariables a) where+ getAllVariables _ = mempty++deriving via HasNoVariables Integer instance HasVariables Integer+deriving via HasNoVariables Int instance HasVariables Int+deriving via HasNoVariables Char instance HasVariables Char++data Any f where+ Some :: (Typeable a, Eq (f a)) => f a -> Any f++instance Eq (Any f) where+ Some (a :: f a) == Some (b :: f b) =+ case eqT @a @b of+ Just Refl -> a == b+ Nothing -> False++instance (forall a. Ord (f a)) => Ord (Any f) where+ compare (Some (a :: f a)) (Some (a' :: f a')) =+ case eqT @a @a' of+ Just Refl -> compare a a'+ Nothing -> compare (typeRep a) (typeRep a')++newtype VarContext = VarCtx (Set (Any Var))+ deriving (Semigroup, Monoid) via Set (Any Var)++instance Show VarContext where+ show (VarCtx vs) =+ "[" ++ intercalate ", " (map showBinding . sortBy (comparing getIdx) $ Set.toList vs) ++ "]"+ where+ getIdx (Some (Var i)) = i+ showBinding :: Any Var -> String+ -- The use of typeRep here is on purpose to avoid printing `Var` unnecessarily.+ showBinding (Some v) = show v ++ " :: " ++ show (typeRep v)++isWellTyped :: Typeable a => Var a -> VarContext -> Bool+isWellTyped v (VarCtx ctx) = Some v `Set.member` ctx++-- TODO: check the invariant that no variable index is used+-- twice at different types. This is generally not an issue+-- because lookups take types into account (so it *shouldn't*+-- cause an issue, but it might be good practise to crash+-- if the invariant is violated anyway as it is evidence that+-- something is horribly broken at the use site).+extendContext :: Typeable a => VarContext -> Var a -> VarContext+extendContext (VarCtx ctx) v = VarCtx $ Set.insert (Some v) ctx++allVariables :: HasVariables a => a -> VarContext+allVariables = VarCtx . getAllVariables++ctxAtType :: Typeable a => VarContext -> [Var a]+ctxAtType (VarCtx vs) = [v | Some (cast -> Just v) <- Set.toList vs]++arbitraryVar :: Typeable a => VarContext -> Gen (Var a)+arbitraryVar = elements . ctxAtType++shrinkVar :: Typeable a => VarContext -> Var a -> [Var a]+shrinkVar ctx v = filter (< v) $ ctxAtType ctx++unsafeCoerceVar :: Var a -> Var b+unsafeCoerceVar (Var i) = Var i++instance {-# OVERLAPPABLE #-} (Generic a, GenericHasVariables (Rep a)) => HasVariables a++class GenericHasVariables f where+ genericGetAllVariables :: f k -> Set (Any Var)++instance GenericHasVariables f => GenericHasVariables (M1 i c f) where+ genericGetAllVariables = genericGetAllVariables . unM1++instance HasVariables c => GenericHasVariables (K1 i c) where+ genericGetAllVariables = getAllVariables . unK1++instance GenericHasVariables U1 where+ genericGetAllVariables _ = mempty++instance (GenericHasVariables f, GenericHasVariables g) => GenericHasVariables (f :*: g) where+ genericGetAllVariables (x :*: y) = genericGetAllVariables x <> genericGetAllVariables y++instance (GenericHasVariables f, GenericHasVariables g) => GenericHasVariables (f :+: g) where+ genericGetAllVariables (L1 x) = genericGetAllVariables x+ genericGetAllVariables (R1 x) = genericGetAllVariables x