-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A library for stateful property-based testing -- -- Please see the README on GitHub at -- https://github.com/input-output-hk/quickcheck-dynamic#readme @package quickcheck-dynamic @version 3.1.0 module Test.QuickCheck.DynamicLogic.CanGenerate -- | canGenerate prob g p returns False if we are sure -- Prob(g generates x satisfying p) >= prob otherwise -- True (and we know such an x can be generated). canGenerate :: Double -> Gen a -> (a -> Bool) -> Bool module Test.QuickCheck.DynamicLogic.SmartShrinking -- | This combinator captures the 'smart shrinking' implemented for the -- Smart type wrapper in Test.QuickCheck.Modifiers. shrinkSmart :: (a -> [a]) -> Smart a -> [Smart a] module Test.QuickCheck.DynamicLogic.Utils withSize :: Testable prop => (Int -> prop) -> Property module Test.QuickCheck.Extras runPropertyStateT :: Monad m => PropertyM (StateT s m) a -> s -> PropertyM m (a, s) runPropertyReaderT :: Monad m => PropertyM (ReaderT e m) a -> e -> PropertyM m a module Test.QuickCheck.StateModel.Variables -- | A symbolic variable for a value of type a data Var a data Any f [Some] :: (Typeable a, Eq (f a)) => f a -> Any f -- | This type class gives you a way to get all the symbolic variables that -- appear in a value. class HasVariables a getAllVariables :: HasVariables a => a -> Set (Any Var) getAllVariables :: (HasVariables a, Generic a, GenericHasVariables (Rep a)) => a -> Set (Any Var) newtype HasNoVariables a HasNoVariables :: a -> HasNoVariables a data VarContext mkVar :: Int -> Var a ctxAtType :: Typeable a => VarContext -> [Var a] arbitraryVar :: Typeable a => VarContext -> Gen (Var a) shrinkVar :: Typeable a => VarContext -> Var a -> [Var a] extendContext :: Typeable a => VarContext -> Var a -> VarContext isWellTyped :: Typeable a => Var a -> VarContext -> Bool allVariables :: HasVariables a => a -> VarContext unsafeCoerceVar :: Var a -> Var b unsafeNextVarIndex :: VarContext -> Int instance Data.Data.Data a => Data.Data.Data (Test.QuickCheck.StateModel.Variables.Var a) instance GHC.Classes.Ord (Test.QuickCheck.StateModel.Variables.Var a) instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Variables.Var a) instance GHC.Base.Monoid Test.QuickCheck.StateModel.Variables.VarContext instance GHC.Base.Semigroup Test.QuickCheck.StateModel.Variables.VarContext instance GHC.Show.Show a => GHC.Show.Show (Test.QuickCheck.StateModel.Variables.HasNoVariables a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.QuickCheck.StateModel.Variables.HasNoVariables a) instance Test.QuickCheck.StateModel.Variables.HasVariables GHC.Num.Integer.Integer instance Test.QuickCheck.StateModel.Variables.HasVariables GHC.Types.Int instance Test.QuickCheck.StateModel.Variables.HasVariables GHC.Types.Char instance Test.QuickCheck.StateModel.Variables.HasVariables GHC.Word.Word8 instance Test.QuickCheck.StateModel.Variables.HasVariables GHC.Word.Word16 instance Test.QuickCheck.StateModel.Variables.HasVariables GHC.Word.Word32 instance Test.QuickCheck.StateModel.Variables.HasVariables GHC.Word.Word64 instance Test.QuickCheck.StateModel.Variables.HasVariables a => Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.Modifiers.Smart a) instance Data.Typeable.Internal.Typeable a => Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.StateModel.Variables.Var a) instance (Test.QuickCheck.StateModel.Variables.HasVariables k, Test.QuickCheck.StateModel.Variables.HasVariables v) => Test.QuickCheck.StateModel.Variables.HasVariables (Data.Map.Internal.Map k v) instance Test.QuickCheck.StateModel.Variables.HasVariables a => Test.QuickCheck.StateModel.Variables.HasVariables (Data.Set.Internal.Set a) instance Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.StateModel.Variables.HasNoVariables a) instance (GHC.Generics.Generic a, Test.QuickCheck.StateModel.Variables.GenericHasVariables (GHC.Generics.Rep a)) => Test.QuickCheck.StateModel.Variables.HasVariables a instance Test.QuickCheck.StateModel.Variables.HasVariables c => Test.QuickCheck.StateModel.Variables.GenericHasVariables (GHC.Generics.K1 i c) instance Test.QuickCheck.StateModel.Variables.GenericHasVariables f => Test.QuickCheck.StateModel.Variables.GenericHasVariables (GHC.Generics.M1 i c f) instance Test.QuickCheck.StateModel.Variables.GenericHasVariables GHC.Generics.U1 instance (Test.QuickCheck.StateModel.Variables.GenericHasVariables f, Test.QuickCheck.StateModel.Variables.GenericHasVariables g) => Test.QuickCheck.StateModel.Variables.GenericHasVariables (f GHC.Generics.:*: g) instance (Test.QuickCheck.StateModel.Variables.GenericHasVariables f, Test.QuickCheck.StateModel.Variables.GenericHasVariables g) => Test.QuickCheck.StateModel.Variables.GenericHasVariables (f GHC.Generics.:+: g) instance GHC.Show.Show Test.QuickCheck.StateModel.Variables.VarContext instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Variables.Any f) instance (forall a. GHC.Classes.Ord (f a)) => GHC.Classes.Ord (Test.QuickCheck.StateModel.Variables.Any f) instance GHC.Show.Show (Test.QuickCheck.StateModel.Variables.Var a) -- | Simple (stateful) Model-Based Testing library for use with Haskell -- QuickCheck. -- -- This module provides the basic machinery to define a StateModel -- from which traces can be generated and executed against some -- actual implementation code to define monadic Property to -- be asserted by QuickCheck. module Test.QuickCheck.StateModel -- | The typeclass users implement to define a model against which to -- validate some implementation. -- -- To implement a StateModel, user needs to provide at least the -- following: -- -- -- -- For finer grained control over the testing process, one can also -- define: -- -- class (forall a. Show (Action state a), forall a. HasVariables (Action state a), Show state, HasVariables state) => StateModel state where { -- | The type of Action relevant for this state. -- -- This is expected to be defined as a GADT where the a -- parameter is instantiated to some observable output from the SUT a -- given action is expected to produce. For example, here is a fragment -- of the `Action RegState` (taken from the RegistryModel module) -- : -- -- 
    --   data Action RegState a where
    --     Spawn      ::                           Action RegState ThreadId
    --     Register   :: String -> Var ThreadId -> Action RegState (Either ErrorCall ())
    --     KillThread :: Var ThreadId           -> Action RegState ()
    --
-- -- The Spawn action should produce a ThreadId, whereas -- the KillThread action does not return anything. data Action state a; } -- | Display name for Action. This is useful to provide sensible -- statistics about the distribution of Actions run when checking -- a property. -- -- Default implementation uses a poor-man's string manipulation method to -- extract the constructor name from the value. actionName :: StateModel state => Action state a -> String -- | Generator for Action depending on state. arbitraryAction :: StateModel state => 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 :: (StateModel state, Typeable a) => VarContext -> state -> Action state a -> [Any (Action state)] -- | Initial state of generated traces. initialState :: StateModel state => state -- | Transition function for the model. The `Var a` parameter is useful to -- keep reference to actual value of type a produced by -- performing the Action inside the state so that -- further actions can use Lookup to retrieve that data. This -- allows the model to be ignorant of those values yet maintain some -- references that can be compared and looked for. nextState :: (StateModel state, Typeable a) => state -> Action state a -> Var a -> state -- | Precondition for filtering generated Action. This function is -- applied before the action is performed, it is useful to refine -- generators that can produce more values than are useful. precondition :: StateModel state => state -> Action state a -> Bool class Monad m => RunModel state m -- | Perform an Action in some state in the Monad -- m. This is the function that's used to exercise the actual -- stateful implementation, usually through various side-effects as -- permitted by m. It produces a value of type a, eg. -- some observable output from the Action that should later be -- kept in the environment through a `Var a` also passed to the -- nextState function. -- -- The Lookup parameter provides an environment to lookup -- `Var a` instances from previous steps. perform :: forall a. (RunModel state m, Typeable a) => state -> Action state a -> LookUp m -> m (Realized m a) -- | Postcondition on the a value produced at some step. The -- result is asserted and will make the property fail should it be -- False. This is useful to check the implementation produces -- expected values. postcondition :: forall a. RunModel state m => (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool -- | Allows the user to attach additional information to the -- Property at each step of the process. This function is given -- the full transition that's been executed, including the start and -- ending state, the Action, the current environment to -- Lookup and the value produced by perform while -- executing this step. monitoring :: forall a. RunModel state m => (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property newtype PostconditionM m a PostconditionM :: WriterT (Endo Property, Endo Property) m a -> PostconditionM m a [runPost] :: PostconditionM m a -> WriterT (Endo Property, Endo Property) m a data WithUsedVars a WithUsedVars :: VarContext -> a -> WithUsedVars a data Annotated state Metadata :: VarContext -> state -> Annotated state [vars] :: Annotated state -> VarContext [underlyingState] :: Annotated state -> state data Step state [:=] :: (Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state infix 5 := type LookUp m = forall a. Typeable a => Var a -> Realized m a data Actions state Actions_ :: [String] -> Smart [Step state] -> Actions state pattern Actions :: [Step state] -> Actions state data EnvEntry m [:==] :: Typeable a => Var a -> Realized m a -> EnvEntry m infix 5 :== pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m type Env m = [EnvEntry m] type family Realized (m :: Type -> Type) a :: Type -- | Representable types of kind *. This class is derivable in GHC -- with the DeriveGeneric flag on. -- -- A Generic instance must satisfy the following laws: -- -- 
--   from . to ≡ id
--   to . from ≡ id
--
class Generic a -- | Apply the property transformation to the property after evaluating the -- postcondition. Useful for collecting statistics while avoiding -- duplication between monitoring and postcondition. monitorPost :: Monad m => (Property -> Property) -> PostconditionM m () -- | Acts as counterexample if the postcondition fails. counterexamplePost :: Monad m => String -> PostconditionM m () stateAfter :: StateModel state => Actions state -> Annotated state runActions :: forall state m. (StateModel state, RunModel state m) => Actions state -> PropertyM m (Annotated state, Env m) lookUpVar :: Typeable a => Env m -> Var a -> Realized m a lookUpVarMaybe :: forall a m. Typeable a => Env m -> Var a -> Maybe (Realized m a) initialAnnotatedState :: StateModel state => Annotated state computeNextState :: (StateModel state, Typeable a) => Annotated state -> Action state a -> Var a -> Annotated state computePrecondition :: StateModel state => Annotated state -> Action state a -> Bool computeArbitraryAction :: StateModel state => Annotated state -> Gen (Any (Action state)) computeShrinkAction :: (Typeable a, StateModel state) => Annotated state -> Action state a -> [Any (Action state)] instance Control.Monad.Trans.Class.MonadTrans Test.QuickCheck.StateModel.PostconditionM instance GHC.Base.Monad m => GHC.Base.Monad (Test.QuickCheck.StateModel.PostconditionM m) instance GHC.Base.Applicative m => GHC.Base.Applicative (Test.QuickCheck.StateModel.PostconditionM m) instance GHC.Base.Functor m => GHC.Base.Functor (Test.QuickCheck.StateModel.PostconditionM m) instance GHC.Generics.Generic (Test.QuickCheck.StateModel.Actions state) instance (forall a. GHC.Show.Show (Test.QuickCheck.StateModel.Action state a)) => GHC.Show.Show (Test.QuickCheck.StateModel.Variables.Any (Test.QuickCheck.StateModel.Action state)) instance Test.QuickCheck.StateModel.StateModel state => Test.QuickCheck.Arbitrary.Arbitrary (Test.QuickCheck.StateModel.Actions state) instance GHC.Show.Show state => GHC.Show.Show (Test.QuickCheck.StateModel.Annotated state) instance GHC.Base.Semigroup (Test.QuickCheck.StateModel.Actions state) instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Actions state) instance Test.QuickCheck.StateModel.StateModel state => GHC.Show.Show (Test.QuickCheck.StateModel.Actions state) instance (forall a. Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.StateModel.Action state a)) => Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.StateModel.Step state) instance GHC.Show.Show (Test.QuickCheck.StateModel.Step state) instance GHC.Show.Show (Test.QuickCheck.StateModel.WithUsedVars (Test.QuickCheck.StateModel.Step state)) instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Step state) -- | This module defines Quantifications, which are used together with -- forAllQ in DynamicLogic. A `Quantification t` can be used to generate -- a t, shrink a t, and recognise a generated -- t. module Test.QuickCheck.DynamicLogic.Quantify -- | A Quantification over a type a is a generator that can -- be used with forAllQ to generate random values in DL scenarios. -- In addition to a QuickCheck generator a Quantification contains -- a shrinking strategy that ensures that shrunk values stay in the range -- of the generator. data Quantification a type QuantifyConstraints a = (Eq a, Show a, Typeable a, HasVariables a) isEmptyQ :: Quantification a -> Bool generateQ :: Quantification a -> Gen a shrinkQ :: Quantification a -> a -> [a] -- | Pack up an Arbitrary instance as a Quantification. -- Treats all values as being in range. arbitraryQ :: Arbitrary a => Quantification a -- | Generates exactly the given value. Does not shrink. exactlyQ :: Eq a => a -> Quantification a -- | Pick a random value from a list. Treated as an empty choice if the -- list is empty: -- -- 
--   forAllQ (elementsQ []) == empty
--
elementsQ :: Eq a => [a] -> Quantification a -- | Choose from a list of quantifications. Same as frequencyQ with -- all weights the same (and > 0). oneofQ :: [Quantification a] -> Quantification a -- | Choose from a weighted list of quantifications. Treated as an -- empty choice if no quantification has weight > 0. frequencyQ :: [(Int, Quantification a)] -> Quantification a -- | Quantification is not a Functor, since it also keeps -- track of the range of the generators. However, if you have two -- functions to :: a -> b from :: b -> a satisfying -- from . to = id you can go from a quantification over -- a to one over b. Note that the from -- function need only be defined on the image of to. mapQ :: (a -> b, b -> a) -> Quantification a -> Quantification b -- | Restrict the range of a quantification. whereQ :: Quantification a -> (a -> Bool) -> Quantification a -- | Generate a random value in a given range (inclusive). chooseQ :: (Arbitrary a, Random a, Ord a) => (a, a) -> Quantification a -- | Wrap a `Gen a` generator in a `Quantification a`. Uses given shrinker. withGenQ :: Gen a -> (a -> [a]) -> Quantification a -- | Wrap a Quantification in HasNoVariables to indicate that you -- know what you're doing and there are no symbolic variables in the -- thing you are quantifying over. WARNING: use this function carefully -- as there is no guarantee that you won't get bitten by very strange -- failures if you were in fact not honest about the lack of variables. hasNoVariablesQ :: Quantification a -> Quantification (HasNoVariables a) validQuantification :: Show a => Quantification a -> Property -- | Generalization of Quantifications, which lets you treat lists -- and tuples of quantifications as quantifications. For instance, -- -- 
--   ...
--   (die1, die2) <- forAllQ (chooseQ (1, 6), chooseQ (1, 6))
--   ...
--
class QuantifyConstraints (Quantifies q) => Quantifiable q where { -- | The type of values quantified over. -- -- 
    --   Quantifies (Quantification a) = a
    --
type Quantifies q; } -- | Computing the actual Quantification. quantify :: Quantifiable q => q -> Quantification (Quantifies q) instance Test.QuickCheck.DynamicLogic.Quantify.QuantifyConstraints a => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (Test.QuickCheck.DynamicLogic.Quantify.Quantification a) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable c) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b, c) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable c, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable d) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b, c, d) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable c, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable d, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable e) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b, c, d, e) instance Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable [a] module Test.QuickCheck.DynamicLogic.Internal -- | A DynFormula may depend on the QuickCheck size parameter newtype DynFormula s DynFormula :: (Int -> DynLogic s) -> DynFormula s [unDynFormula] :: DynFormula s -> 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 :: DynLogic s -- | True Stop :: DynLogic s -- | After any action the predicate should hold AfterAny :: DynPred s -> DynLogic s -- | Choice (angelic or demonic) Alt :: ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s -- | Prefer this branch if trying to stop. Stopping :: DynLogic s -> DynLogic s -- | After a specific action the predicate should hold After :: Action s a -> (Var a -> DynPred s) -> DynLogic s Error :: String -> DynPred s -> DynLogic s -- | Adjust the probability of picking a branch Weight :: Double -> DynLogic s -> DynLogic s -- | Generating a random value ForAll :: Quantification a -> (a -> DynLogic s) -> DynLogic s -- | Apply a QuickCheck property modifier (like tabulate or -- collect) Monitor :: (Property -> Property) -> DynLogic s -> DynLogic s data ChoiceType Angelic :: ChoiceType Demonic :: ChoiceType type DynPred s = Annotated s -> DynLogic s -- | 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 -- | True for DL formulae. passTest :: DynFormula s -- | Given f must be True given any state. afterAny :: (Annotated 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), Show (Action s a)) => Action s a -> (Var a -> Annotated 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 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 -- | Get the current QuickCheck size parameter. withSize :: (Int -> DynFormula s) -> DynFormula s -- | Prioritise doing this if we are trying to stop generation. toStop :: DynFormula s -> DynFormula s -- | Successfully ends the test. done :: Annotated 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 :: (Annotated s -> DynFormula s) -> Annotated s -> DynFormula s data FailingAction s ErrorFail :: String -> FailingAction s ActionFail :: Action s a -> FailingAction s data DynLogicTest s BadPrecondition :: TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s Looping :: TestSequence s -> DynLogicTest s Stuck :: TestSequence s -> Annotated s -> DynLogicTest s DLScript :: TestSequence s -> DynLogicTest s data Witnesses r [Do] :: r -> Witnesses r [Witness] :: QuantifyConstraints a => a -> Witnesses r -> Witnesses r discardWitnesses :: Witnesses r -> r pattern Witnesses :: Witnesses () -> r -> Witnesses r type TestStep s = Witnesses (Step s) newtype TestSequence s TestSeq :: Witnesses (TestContinuation s) -> TestSequence s data TestContinuation s ContStep :: Step s -> TestSequence s -> TestContinuation s ContStop :: TestContinuation s pattern TestSeqStop :: TestSequence s pattern TestSeqStep :: Step s -> TestSequence s -> TestSequence s pattern TestSeqWitness :: () => forall a. QuantifyConstraints a => a -> TestSequence s -> TestSequence s consSeq :: TestStep s -> TestSequence s -> TestSequence s unconsSeq :: TestSequence s -> Maybe (TestStep s, TestSequence s) unstopSeq :: TestSequence s -> Maybe (Witnesses ()) pattern TestSeqStopW :: Witnesses () -> TestSequence s pattern (:>) :: TestStep s -> TestSequence s -> TestSequence s nullSeq :: TestSequence s -> Bool dropSeq :: Int -> TestSequence s -> TestSequence s getContinuation :: TestSequence s -> TestSequence s unlines' :: [String] -> String prettyTestSequence :: VarContext -> TestSequence s -> String prettyWitnesses :: Witnesses () -> [String] usedVariables :: forall s. StateModel s => TestSequence s -> VarContext -- | 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 restricted :: DynLogicModel s => Action s a -> Bool -- | Simplest "execution" function for DynFormula. Turns a given a -- DynFormula paired with an interpreter function to produce some -- result from an forAllScripts :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> Property -- | Property function suitable for formulae without choice. forAllUniqueScripts :: (DynLogicModel s, Testable a) => Annotated s -> DynFormula s -> (Actions s -> a) -> Property -- | 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 withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property withDLScriptPrefix :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s) onDLTestSeq :: (TestSequence s -> TestSequence s) -> DynLogicTest s -> DynLogicTest s consDLTest :: TestStep s -> DynLogicTest s -> DynLogicTest s consDLTestW :: Witnesses () -> DynLogicTest s -> DynLogicTest s generate :: (Monad m, DynLogicModel s) => (Annotated s -> Int -> DynLogic s -> m (NextStep s)) -> DynLogic s -> Int -> Annotated s -> Int -> m (DynLogicTest s) sizeLimit :: Int -> Int initialStateFor :: StateModel s => DynLogic s -> Annotated s stopping :: DynLogic s -> DynLogic s noStopping :: DynLogic s -> DynLogic s noAny :: DynLogic s -> DynLogic s nextSteps :: DynLogic s -> Gen [(Double, Witnesses (DynLogic s))] nextSteps' :: Monad m => (forall a. Quantification a -> m a) -> DynLogic s -> m [(Double, Witnesses (DynLogic s))] chooseOneOf :: [(Double, a)] -> Gen a never :: Double data NextStep s StoppingStep :: NextStep s Stepping :: Witnesses (Step s) -> DynLogic s -> NextStep s NoStep :: NextStep s BadAction :: Witnesses (FailingAction s) -> NextStep s chooseNextStep :: DynLogicModel s => Annotated s -> Int -> DynLogic s -> Gen (NextStep s) chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => Annotated s -> Int -> DynLogic s -> m (NextStep s) keepTryingUntil :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a) shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s] nextStateStep :: StateModel s => Step s -> Annotated s -> Annotated s shrinkScript :: DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s] shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a] pruneDLTest :: DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s stepDL :: DynLogicModel s => DynLogic s -> Annotated s -> TestStep s -> [DynLogic s] stepDLW :: forall a s. (DynLogicModel s, Typeable a) => DynLogic s -> a -> [DynLogic s] stepDLSeq :: DynLogicModel s => DynLogic s -> Annotated s -> TestSequence s -> DynLogic s stepDLWitness :: forall a s. (DynLogicModel s, Typeable a) => DynLogic s -> a -> DynLogic s stepDLStep :: DynLogicModel s => DynLogic s -> Annotated s -> Step s -> DynLogic s demonicAlt :: [DynLogic s] -> DynLogic s propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property getScript :: DynLogicTest s -> TestSequence s makeTestFromPruned :: DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s -- | 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 stuck :: DynLogicModel s => DynLogic s -> Annotated s -> Bool validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property -> Property scriptFromDL :: DynLogicTest s -> Actions s sequenceSteps :: TestSequence s -> [Step s] badActionsGiven :: StateModel s => DynLogic s -> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)] badActions :: StateModel s => DynLogic s -> Annotated s -> [FailingAction s] applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property findMonitoring :: DynLogicModel s => DynLogic s -> Annotated s -> TestSequence s -> Maybe (Property -> Property) instance GHC.Show.Show Test.QuickCheck.DynamicLogic.Internal.ChoiceType instance GHC.Classes.Eq Test.QuickCheck.DynamicLogic.Internal.ChoiceType instance Test.QuickCheck.StateModel.StateModel s => GHC.Classes.Eq (Test.QuickCheck.DynamicLogic.Internal.TestSequence s) instance Test.QuickCheck.StateModel.StateModel s => GHC.Show.Show (Test.QuickCheck.DynamicLogic.Internal.TestSequence s) instance GHC.Base.Functor Test.QuickCheck.DynamicLogic.Internal.Witnesses instance Data.Foldable.Foldable Test.QuickCheck.DynamicLogic.Internal.Witnesses instance Data.Traversable.Traversable Test.QuickCheck.DynamicLogic.Internal.Witnesses instance Test.QuickCheck.StateModel.StateModel s => GHC.Show.Show (Test.QuickCheck.DynamicLogic.Internal.TestContinuation s) instance Test.QuickCheck.StateModel.StateModel s => GHC.Classes.Eq (Test.QuickCheck.DynamicLogic.Internal.TestContinuation s) instance Test.QuickCheck.StateModel.StateModel s => GHC.Show.Show (Test.QuickCheck.DynamicLogic.Internal.DynLogicTest s) instance GHC.Classes.Eq r => GHC.Classes.Eq (Test.QuickCheck.DynamicLogic.Internal.Witnesses r) instance GHC.Show.Show r => GHC.Show.Show (Test.QuickCheck.DynamicLogic.Internal.Witnesses r) instance Test.QuickCheck.StateModel.StateModel s => Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.DynamicLogic.Internal.FailingAction s) instance Test.QuickCheck.StateModel.StateModel s => GHC.Classes.Eq (Test.QuickCheck.DynamicLogic.Internal.FailingAction s) instance Test.QuickCheck.StateModel.StateModel s => GHC.Show.Show (Test.QuickCheck.DynamicLogic.Internal.FailingAction s) -- | Monadic interface for writing Dynamic Logic properties. -- -- 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 Internal module and it might make sense -- depending on the context and the kind of properties one wants to -- express. module Test.QuickCheck.DynamicLogic -- | The DL monad provides a nicer interface to dynamic logic -- formulae than the plain API. It's a continuation monad producing a -- DynFormula formula, with a state component (with variable -- context) threaded through. data DL s a action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a) anyAction :: DL s () anyActions :: Int -> DL s () anyActions_ :: DL s () stopping :: DL s () weight :: Double -> DL s () getSize :: DL s Int getModelStateDL :: DL s s getVarContextDL :: DL s VarContext forAllVar :: forall a s. Typeable a => DL s (Var a) -- | Fail if the boolean is False. -- -- Equivalent to -- -- 
--   assert msg b = unless b (fail msg)
--
assert :: String -> Bool -> DL s () assertModel :: String -> (s -> Bool) -> DL s () monitorDL :: (Property -> Property) -> DL s () -- | Generate a random value using the given Quantification (or -- list/tuple of quantifications). Generated values will only shrink to -- smaller values that could also have been generated. forAllQ :: Quantifiable q => q -> DL s (Quantifies q) -- | Generate a random value using the given Quantification (or -- list/tuple of quantifications). Generated values will only shrink to -- smaller values that could also have been generated. forAllNonVariableQ :: QuantifyConstraints (HasNoVariables a) => Quantification a -> DL s a forAllDL :: (DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> Property forAllMappedDL :: (DynLogicModel s, Testable a) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> (Actions s -> srep) -> DL s () -> (srep -> a) -> Property forAllUniqueDL :: (DynLogicModel s, Testable a) => Annotated s -> DL s () -> (Actions s -> a) -> Property -- | 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 restricted :: DynLogicModel s => Action s a -> Bool instance GHC.Base.Functor (Test.QuickCheck.DynamicLogic.DL s) instance GHC.Base.Applicative (Test.QuickCheck.DynamicLogic.DL s) instance GHC.Base.Alternative (Test.QuickCheck.DynamicLogic.DL s) instance GHC.Base.Monad (Test.QuickCheck.DynamicLogic.DL s) instance Control.Monad.Fail.MonadFail (Test.QuickCheck.DynamicLogic.DL s)