-- 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.3.1 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) 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.Break (TypeError ...) (GHC.Generics.Rep a), GHC.Generics.Generic a, Test.QuickCheck.StateModel.Variables.GenericHasVariables (GHC.Generics.Rep a)) => Test.QuickCheck.StateModel.Variables.HasVariables a instance Test.QuickCheck.StateModel.Variables.GenericHasVariables f => Test.QuickCheck.StateModel.Variables.GenericHasVariables (GHC.Generics.M1 i c f) instance Test.QuickCheck.StateModel.Variables.HasVariables c => Test.QuickCheck.StateModel.Variables.GenericHasVariables (GHC.Generics.K1 i c) 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 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.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 -- | Transition function for negative actions. Note that most negative -- testing applications should not require an implementation of this -- function! failureNextState :: (StateModel state, Typeable a) => state -> Action state 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 -- | Precondition for filtering an Action that can meaningfully run -- but is supposed to fail. An action will run as a _negative_ action if -- the precondition fails and validFailingAction succeeds. -- A negative action should have _no effect_ on the model state. This may -- not be desierable in all situations - in which case one can override -- this semantics for book-keeping in failureNextState. validFailingAction :: 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 -- | Postcondition on the result of running a _negative_ Action. The -- result is asserted and will make the property fail should it be -- False. This is useful to check the implementation produces e.g. -- the expected errors or to check that the SUT hasn't been updated -- during the execution of the negative action. postconditionOnFailure :: 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 -> ActionWithPolarity state a -> Step state infix 5 := data Polarity PosPolarity :: Polarity NegPolarity :: Polarity data ActionWithPolarity state a ActionWithPolarity :: Action state a -> Polarity -> ActionWithPolarity state a [polarAction] :: ActionWithPolarity state a -> Action state a [polarity] :: ActionWithPolarity state a -> Polarity 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 :: forall state. 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 -> ActionWithPolarity state a -> Var a -> Annotated state computePrecondition :: StateModel state => Annotated state -> ActionWithPolarity state a -> Bool computeArbitraryAction :: StateModel state => Annotated state -> Gen (Any (ActionWithPolarity state)) computeShrinkAction :: forall state a. (Typeable a, StateModel state) => Annotated state -> ActionWithPolarity state a -> [Any (ActionWithPolarity state)] -- | Indicate that the result of an action (in perform) should not -- be inspected by the postcondition or appear in a positive test. Useful -- when we want to give a type for an Action like `SomeAct :: -- Action SomeState SomeType` instead of `SomeAct :: Action SomeState -- (Either SomeError SomeType)` but still need to return something in -- perform in the failure case. failureResult :: HasCallStack => a 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.Classes.Eq Test.QuickCheck.StateModel.Polarity instance GHC.Classes.Ord Test.QuickCheck.StateModel.Polarity 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 GHC.Classes.Eq (Test.QuickCheck.StateModel.Action state a) => GHC.Classes.Eq (Test.QuickCheck.StateModel.ActionWithPolarity state a) 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) instance Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.StateModel.Action state a) => Test.QuickCheck.StateModel.Variables.HasVariables (Test.QuickCheck.StateModel.ActionWithPolarity state a) instance GHC.Show.Show Test.QuickCheck.StateModel.Polarity -- | 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 :: ActionWithPolarity 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 afterPolar :: (Typeable a, Eq (Action s a), Show (Action s a)) => ActionWithPolarity s a -> (Var a -> 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 -- | Given f must be True after some negative -- action. f is passed the state resulting from executing the -- Action as a negative action. afterNegative :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> (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 :: ActionWithPolarity 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 restrictedPolar :: DynLogicModel s => ActionWithPolarity 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 :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s] shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a] pruneDLTest :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s stepDL :: DynLogicModel s => DynLogic s -> Annotated s -> TestStep s -> [DynLogic s] stepDLW :: forall s a. (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 :: forall s. 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 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.TestSequence s) 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.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) failingAction :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s () 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)