h&1.e      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ Safe-Inferred 589:;>2quickcheck-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-Inferred589:;> 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 589:;> quickcheck-dynamicThis combinator captures the 'smart shrinking' implemented for the Smart type wrapper in Test.QuickCheck.Modifiers. Safe-Inferred 589:;>  Safe-Inferred%&)*5689:;> (quickcheck-dynamic Perform an , in some state 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 1 function.The Lookup parameter provides an  environment2 to lookup `Var a` instances from previous steps.+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 0 to some end state,A generator for traces of ,s, the . function,An 0,A  transition function, 1, that "interprets" each , and producing some new state.For finer grained control over the testing process, one can also define:/: 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,2: Filters generated , depending on the state. When 2! 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 2? can be somewhat redundant with the generator's conditions,39: This function is evaluated during test execution after *ing the action, it allows the model to express expectations about the output of actual code given some "transition".,quickcheck-dynamic The type of , relevant for this state.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..quickcheck-dynamicGenerator for , depending on state'. 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./quickcheck-dynamic Shrinker for ,. Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness of property-based testing.0quickcheck-dynamic"Initial state of generated traces.1quickcheck-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 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.2quickcheck-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.3quickcheck-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.4quickcheck-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 state, the ,, the current environment to Lookup and the value produced by * while executing this step.! !#"$%&'()*+,-./0123456789:;!+,-./01234()*!#" '5$%&9:;768 5%5 Safe-Inferred)*589:;>+hIquickcheck-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.Tquickcheck-dynamicBase Dynamic logic formulae language. Formulae are parameterised over the type of state s to which they apply. A T 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 )Uquickcheck-dynamicA U, may depend on the QuickCheck size parameterVquickcheck-dynamic for DL formulae.Wquickcheck-dynamic for DL formulae.Xquickcheck-dynamicGiven f must be  given any state.Yquickcheck-dynamicGiven f must be  after some action. f2 is passed the state resulting from executing the ,.Zquickcheck-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 Q.[quickcheck-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 Z 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.aquickcheck-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.bquickcheck-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.cquickcheck-dynamic"Simplest "execution" function for U. Turns a given a U paired with an interpreter function to produce some result from andquickcheck-dynamic/ function suitable for formulae without choice.fquickcheck-dynamic Creates a  from U= 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 IJKLMNOPQRSTUVWXYZ[\]^_`abcdefghij"TSUIJNOPQRKLMVWXYZ[\]^_`abcehifgdj Safe-Inferred 589:;>. pquickcheck-dynamicThe p monad provides a nicer interface to dynamic logic formulae than the plain API. It's a continuation monad producing a U5 formula, with a state component threaded through.yquickcheck-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 IJKLMNOPQRTpqrstuvwxyz{|}~pqrstuvwxyz{|~}TIJNOPQRKLM !"#$%&'()*+,,-./01234566789:;<=>?@A*BCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdef g)hijklmnopqrstuvwxyz{|}~gk /quickcheck-dynamic-1.1.0-5sN5nlMrFHtIicHTrfLZmy(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 StateModelAction actionNamearbitraryAction shrinkAction initialState nextState precondition postcondition monitoringlookUpVarMaybe lookUpVarinvertLookupVarMaybe stateAfter runActionsrunActionsInState$fEqAny$fEqStep$fArbitraryActions $fShowActions $fEqActions$fSemigroupActions$fEqVar$fOrdVar $fShowVar $fDataVar $fShowStep $fShowAny$fShowEnvEntry 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.BaseFunctorMonadTest.QuickCheck.Monadicghc-prim GHC.TypesFalseTest.QuickCheck.PropertyProperty EmptySpecStopAfterAnyAltStoppingAfterWeightForAllMonitortabulatecollectTruelabel unfailDLTest