diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/quickcheck-dynamic.cabal b/quickcheck-dynamic.cabal --- a/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic.cabal @@ -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 diff --git a/src/Test/QuickCheck/DynamicLogic.hs b/src/Test/QuickCheck/DynamicLogic.hs --- a/src/Test/QuickCheck/DynamicLogic.hs +++ b/src/Test/QuickCheck/DynamicLogic.hs @@ -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) diff --git a/src/Test/QuickCheck/DynamicLogic/CanGenerate.hs b/src/Test/QuickCheck/DynamicLogic/CanGenerate.hs --- a/src/Test/QuickCheck/DynamicLogic/CanGenerate.hs +++ b/src/Test/QuickCheck/DynamicLogic/CanGenerate.hs @@ -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 diff --git a/src/Test/QuickCheck/DynamicLogic/Core.hs b/src/Test/QuickCheck/DynamicLogic/Core.hs deleted file mode 100644 --- a/src/Test/QuickCheck/DynamicLogic/Core.hs +++ /dev/null @@ -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 diff --git a/src/Test/QuickCheck/DynamicLogic/Internal.hs b/src/Test/QuickCheck/DynamicLogic/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/DynamicLogic/Internal.hs @@ -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 diff --git a/src/Test/QuickCheck/DynamicLogic/Quantify.hs b/src/Test/QuickCheck/DynamicLogic/Quantify.hs --- a/src/Test/QuickCheck/DynamicLogic/Quantify.hs +++ b/src/Test/QuickCheck/DynamicLogic/Quantify.hs @@ -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 = diff --git a/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs b/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs --- a/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs +++ b/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs @@ -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) diff --git a/src/Test/QuickCheck/Extras.hs b/src/Test/QuickCheck/Extras.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/Extras.hs @@ -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 diff --git a/src/Test/QuickCheck/StateModel.hs b/src/Test/QuickCheck/StateModel.hs --- a/src/Test/QuickCheck/StateModel.hs +++ b/src/Test/QuickCheck/StateModel.hs @@ -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 diff --git a/src/Test/QuickCheck/StateModel/Variables.hs b/src/Test/QuickCheck/StateModel/Variables.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Variables.hs @@ -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