h&1N.      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ Safe-Inferred()*568Gquickcheck-dynamiccanGenerate 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). Safe-Inferred()*568 quickcheck-dynamicGeneralization of s, which lets you treat lists and tuples of quantifications as quantifications. For instance,  ... (die1, die2) <-   (  (1, 6),   (1, 6)) ... quickcheck-dynamic#The type of values quantified over.  ( a) = a quickcheck-dynamicComputing the actual .quickcheck-dynamicA  over a type a) is a generator that can be used with   to generate random values in DL scenarios. In addition to a QuickCheck generator a  contains a shrinking strategy that ensures that shrunk values stay in the range of the generator. quickcheck-dynamicWrap a `Gen a` generator in a `Quantification a`. Uses given shrinker. quickcheck-dynamic Pack up an  instance as a &. Treats all values as being in range. quickcheck-dynamic3Generates exactly the given value. Does not shrink. quickcheck-dynamic5Generate a random value in a given range (inclusive). quickcheck-dynamicPick a random value from a list. Treated as an empty choice if the list is empty:   (  []) ==   quickcheck-dynamic>Choose from a weighted list of quantifications. Treated as an  / choice if no quantification has weight > 0.quickcheck-dynamic/Choose from a list of quantifications. Same as ( with all weights the same (and > 0).quickcheck-dynamic is not a , 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.quickcheck-dynamic'Restrict the range of a quantification.    Safe-Inferred()*568 quickcheck-dynamicThis combinator captures the 'smart shrinking' implemented for the Smart type wrapper in Test.QuickCheck.Modifiers. Safe-Inferred()*568 1 Safe-Inferred()*568Z )quickcheck-dynamic Perform an . in some  in the  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 . that should later be kept in the environment through a `Var a` also passed to the 3 function.The Lookup parameter provides an  environment2 to lookup `Var a` instances from previous steps.*quickcheck-dynamicPostcondition on the a- value produced at some step. The result is 0ed and will make the property fail should it be . This is useful to check the implementation produces expected values.+quickcheck-dynamic-Allows the user to attach information to the  at each step of the process. This function is given the full transition that's been executed, including the start and ending , the ., the current environment to Lookup and the value produced by ) while executing this step.-quickcheck-dynamicThe typeclass users implement to define a model against which to validate some implementation.To implement a -/, user needs to provide at least the following:A datatype for .#s: Each test case is a sequence of .)s that's supposed to lead from some 2 to some end state,A generator for traces of .s, the 0 function,An 2,A  transition function, 3, that "interprets" each . and producing some new .For finer grained control over the testing process, one can also define:1: Shrinking is an important part of MBT as it allows QuickCheck engine to look for simpler test cases when something goes wrong which makes troubleshooting easier,4: Filters generated . depending on the . When 4! is False then the action is rejected and a new one is tried. This is also useful when shrinking a trace in order to ensure that removing some .# still produces a valid trace. The 4? can be somewhat redundant with the generator's conditions,.quickcheck-dynamic The type of . relevant for this .3This 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    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./quickcheck-dynamicDisplay name for .. This is useful to provide sensible statistics about the distribution of . s run when checking a property.Default implementation uses a poor-man's string manipulation method to extract the constructor name from the value.0quickcheck-dynamicGenerator for . depending on '. The generated values are wrapped in ! type to allow the model to not> generate an action under some circumstances: Any generated #; value will be ignored when generating a trace for testing.1quickcheck-dynamic Shrinker for .. Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness of property-based testing.2quickcheck-dynamic"Initial state of generated traces.3quickcheck-dynamicTransition function for the model. The `Var a` parameter is useful to keep reference to actual value of type a produced by )ing the . inside the ! 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.4quickcheck-dynamic%Precondition for filtering generated .. This function is applied before the action is performed, it is useful to refine generators that can produce more values than are useful.! !#"$%&'()*+,-./0123456789:;!-./01234()*+!#" '5$%6&,9:;87 5%5 Safe-Inferred()*568*Hquickcheck-dynamic&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.Squickcheck-dynamicBase Dynamic logic formulae language. Formulae are parameterised over the type of state s to which they apply. A S value cannot be constructed directly, one has to use the various "smart constructors" provided, see the Building formulae section.quickcheck-dynamicFalsequickcheck-dynamicTruequickcheck-dynamic*After any action the predicate should holdquickcheck-dynamicChoice (angelic or demonic)quickcheck-dynamic%Prefer this branch if trying to stop.quickcheck-dynamic1After a specific action the predicate should holdquickcheck-dynamic*Adjust the probability of picking a branchquickcheck-dynamicGenerating a random valuequickcheck-dynamic+Apply a QuickCheck property modifier (like  or )Tquickcheck-dynamicA T, may depend on the QuickCheck size parameterUquickcheck-dynamic for DL formulae.Vquickcheck-dynamic for DL formulae.Wquickcheck-dynamicGiven f must be  given any state.Xquickcheck-dynamicGiven f must be  after some action. f2 is passed the state resulting from executing the ..Yquickcheck-dynamic!Disjunction for DL formulae. Is  if either formula is . The choice is angelic, ie. it is always made by the "caller". This is mostly important in case a test is P.Zquickcheck-dynamic2First-order quantification of variables. Formula f is  iff. it is  for all possible values of q4. The underlying framework will generate values of q0 and check the formula holds for those values.  values are thus values that can be generated and checked and the  module defines basic combinators to build those from building blocks.[quickcheck-dynamicAdjust weight for selecting formula. This is mostly useful in relation with Y combinator, in order to tweak the priority for generating the next step(s) of the test that matches the formula.^quickcheck-dynamicSuccessfully ends the test._quickcheck-dynamic#Ends test with given error message.`quickcheck-dynamic-Embed QuickCheck's monitoring functions (eg. , ) in a formula. This is useful to improve the reporting from test execution, esp. in the case of failures.aquickcheck-dynamicFormula should hold at any state. In effect this leads to exploring alternatives from a given state s1 and ensuring formula holds in all those states.bquickcheck-dynamic"Simplest "execution" function for T. Turns a given a T paired with an interpreter function to produce some result from ancquickcheck-dynamic/ function suitable for formulae without choice.equickcheck-dynamic Creates a  from T= with some specialised isomorphism for shrinking purpose. ??quickcheck-dynamicIf failed, return the prefix up to the failure. Also prunes the test in case the model has changed.5 HIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghi"SRTHIMNOPQJKLUVWXYZ[\]^_`abdghefci Safe-Inferred()*568-oquickcheck-dynamicThe o monad provides a nicer interface to dynamic logic formulae than the plain API. It's a continuation monad producing a T5 formula, with a state component threaded through.xquickcheck-dynamicFail if the boolean is False. Equivalent to #assert msg b = unless b (fail msg) {quickcheck-dynamic(Generate a random value using the given  (or list/tuple of quantifications). Generated values will only shrink to smaller values that could also have been generated.1 HIJKLMNOPQSopqrstuvwxyz{|}~opqrstuvwxyz{}~|SHIMNOPQJKL !"#$%&'()*+,,-./0123456789:;<=>?@AB*CDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdef g)hijklmnopqrstuvwxyz{|}~gk /quickcheck-dynamic-2.0.0-HlvmsvKYAOv4UCs28ZZPrz(Test.QuickCheck.DynamicLogic.CanGenerate%Test.QuickCheck.DynamicLogic.Quantify+Test.QuickCheck.DynamicLogic.SmartShrinking"Test.QuickCheck.DynamicLogic.UtilsTest.QuickCheck.StateModel!Test.QuickCheck.DynamicLogic.CoreTest.QuickCheck.DynamicLogic"Plutus.Contract.Test.ContractModelforAllQControl.Applicativeempty Spec.Dynamic RegistryModelQuantify canGenerate Quantifiable QuantifiesquantifyQuantificationisaQisEmptyQ generateQshrinkQwithGenQ arbitraryQexactlyQchooseQ elementsQ frequencyQoneofQmapQwhereQvalidQuantification$fQuantifiable[]$fQuantifiable(,,,,)$fQuantifiable(,,,)$fQuantifiable(,,)$fQuantifiable(,)$fQuantifiableQuantification shrinkSmartwithSizeActionsActions_VarStep:=AnySomeErrorEnvEntry:==EnvLookUpRunModelperform postcondition monitoringRealized StateModelAction actionNamearbitraryAction shrinkAction initialState nextState precondition:=?lookUpVarMaybe lookUpVar stateAfter runActionsrunActionsInState$fEqAny$fEqStep$fArbitraryActions $fShowActions $fEqActions$fSemigroupActions$fEqVar$fOrdVar $fShowVar $fDataVar $fShowStep $fShowAny DynLogicModel restrictedTestStepDoWitness DynLogicTestBadPreconditionLoopingStuckDLScriptDynPredDynLogic DynFormulaignorepassTestafterAnyafter|||weighttoStopdoneerrorDL monitorDLalways forAllScriptsforAllUniqueScriptsforAllScripts_forAllMappedScriptsforAllMappedScripts_ withDLScriptwithDLScriptPrefix propPruningGeneratedScriptIsNoop$fShowTestStep $fEqTestStep$fShowDynLogicTest$fEqChoiceType$fShowChoiceTypeDLaction anyAction anyActions anyActions_stoppinggetSizegetModelStateDLassert assertModelforAllUniqueDLforAllDL forAllDL_forAllMappedDLforAllMappedDL_ withDLTest $fMonadFailDL $fMonadDL$fAlternativeDL$fApplicativeDL $fFunctorDL(QuickCheck-2.14.2-9EAFA6afNUqGbN355JryFuTest.QuickCheck.Arbitrary ArbitrarybaseGHC.BaseFunctor mtl-2.2.2Control.Monad.State.ClassstateMonadTest.QuickCheck.Monadicghc-prim GHC.TypesFalseTest.QuickCheck.PropertyProperty EmptySpecStopAfterAnyAltStoppingAfterWeightForAllMonitortabulatecollectTruelabel unfailDLTest