h*L~D      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                         3.4.0  Safe-Inferred#()*/1679:;<=quickcheck-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#()*/1679:;<=quickcheck-dynamicThis combinator captures the 'smart shrinking' implemented for the Smart type wrapper in Test.QuickCheck.Modifiers. Safe-Inferred#()*/1679:;<=8 Safe-Inferred#()*/1679:;<= Safe-Inferred%()*/1679:;<=  quickcheck-dynamicThis type class gives you a way to get all the symbolic variables that appear in a value. quickcheck-dynamic(A symbolic variable for a value of type a     Safe-Inferred%()*/1679:;<="Lquickcheck-dynamic Perform an V 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 V that should later be kept in the environment through a `Var a` also passed to the \ function.The Lookup parameter provides an  environment2 to lookup `Var a` instances from previous steps.Mquickcheck-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.Nquickcheck-dynamic4Postcondition on the result of running a _negative_ V. The result is 0ed and will make the property fail should it be . 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.Oquickcheck-dynamic8Allows the user to attach additional 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 V, the current environment to Lookup and the value produced by L while executing this step.Pquickcheck-dynamic8Allows the user to attach additional information to the  if a positive action fails.quickcheck-dynamicThe result required of L depending on the W type of a state model. If there are no errors, `Error state = Void`, and so we don't need to specify if the action failed or not.Uquickcheck-dynamicThe typeclass users implement to define a model against which to validate some implementation.To implement a U/, user needs to provide at least the following:A datatype for V#s: Each test case is a sequence of V)s that's supposed to lead from some [ to some end state,A generator for traces of Vs, the Y function,An [,A  transition function, \, that "interprets" each V and producing some new .For finer grained control over the testing process, one can also define:Z: 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,^: Filters generated V depending on the . When ^! 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 V# still produces a valid trace. The ^? can be somewhat redundant with the generator's conditions,_+: Specifies when an action that fails it's ^ can still run as what is called a _negative_ action. This means that the action is (1) expected to fail and (2) not expected to change the model state. This is very useful for testing the checks and failure conditions in the SUT are implemented correctly. Should it be necessary to update the model state with e.g. book-keeping for a negative action one can define ] - but it is generally recommended to let this be as simple an action as possible.Vquickcheck-dynamic The type of V 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 () KillThread :: Var ThreadId -> Action RegState () The Spawn action should produce a ThreadId, whereas the  KillThread" action does not return anything.Wquickcheck-dynamicThe type of errors that actions can throw. If this is defined as anything other than  L< is required to return `Either (Error state) a` instead of a.Xquickcheck-dynamicDisplay name for V. This is useful to provide sensible statistics about the distribution of V s run when checking a property.Default implementation uses a poor-man's string manipulation method to extract the constructor name from the value.Yquickcheck-dynamicGenerator for V depending on .Zquickcheck-dynamic Shrinker for V. Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness of property-based testing.[quickcheck-dynamic"Initial state of generated traces.\quickcheck-dynamicTransition function for the model. The `Var a` parameter is useful to keep reference to actual value of type a produced by Ling the V 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.]quickcheck-dynamicTransition function for negative actions. Note that most negative testing applications should not require an implementation of this function!^quickcheck-dynamic%Precondition for filtering generated V. This function is applied before the action is performed, it is useful to refine generators that can produce more values than are useful._quickcheck-dynamicPrecondition for filtering an V that can meaningfully run but is supposed to fail. An action will run as a _negative_ action if the ^ fails and _ 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 ].bquickcheck-dynamicApply the property transformation to the property after evaluating the postcondition. Useful for collecting statistics while avoiding duplication between O and M.cquickcheck-dynamicActs as   if the postcondition fails. UVWXYZ[\]^_KLMNOPQRSEF6798<=BCD>?@AJ:;`GHaITbckledfhgij8UVWXYZ[\]^_KLMNOPQRSEF6798<=BCD>?@AJ:;`GHaITbckledfhgij=5H5 Safe-Inferred#()*/1679:;<=/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 to generate random values in DL scenarios.A  is similar to a , it groups together:)A standard QuickCheck _generator_ in the  monad, which can be "empty",A _shrinking_ strategy for generated values in the case of a failures ensuring they stay within the domain,A _predicate_ allowing finer grained control on generation and shrinking process, e.g in the case the range of the generator depends on trace context.,NOTE: Leaving the possibility of generating 3 is useful to simplify the generation process for  or  which may normally crash when the list to select elements from is empty. This makes writing DL formulas cleaner, removing the need to handle non-existence cases explicitly.quickcheck-dynamicConstruct a `Quantification a` from its constituents. Note the predicate provided is used to restrict both the range of values generated and the list of possible shrinked values.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.quickcheck-dynamicWrap a Quantification in   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.quickcheck-dynamicTurns a  into a ' to enable QuickChecking its validity. Safe-Inferred#()*/1679:;<=?8quickcheck-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.quickcheck-dynamicBase Dynamic logic formulae language. Formulae are parameterised over the type of state s to which they apply. A  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 )quickcheck-dynamicA , may depend on the QuickCheck size parameterquickcheck-dynamic True).quickcheck-dynamic for DL formulae.quickcheck-dynamicGiven f must be  given any state.quickcheck-dynamicGiven f must be  after some action. f2 is passed the state resulting from executing the V.quickcheck-dynamicGiven f must be  after some negative action. f2 is passed the state resulting from executing the V as a negative action.quickcheck-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 .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  combinator, in order to tweak the priority for generating the next step(s) of the test that matches the formula.quickcheck-dynamic*Get the current QuickCheck size parameter.quickcheck-dynamic;Prioritise doing this if we are trying to stop generation.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.quickcheck-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.quickcheck-dynamic"Simplest "execution" function for . Turns a given a  paired with an interpreter function to produce some result from anquickcheck-dynamic/ function suitable for formulae without choice.quickcheck-dynamic Creates a  from 9 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.  Safe-Inferred#()*/1679:;<=Dyquickcheck-dynamicThe  monad provides a nicer interface to dynamic logic formulae than the plain API. It's a continuation monad producing a  formula, with a state component (with variable context) threaded through.quickcheck-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.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.+ !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSSTUVWXYYZ[\]^_`abcddefghijklmnopqOrstuvwxyz{|}~i                         /quickcheck-dynamic-3.4.0-5jm8bgdYPgSHb9lOqRV763Test.QuickCheck.StateModel(Test.QuickCheck.DynamicLogic.CanGenerate+Test.QuickCheck.DynamicLogic.SmartShrinking"Test.QuickCheck.DynamicLogic.UtilsTest.QuickCheck.Extras$Test.QuickCheck.StateModel.Variables%Test.QuickCheck.DynamicLogic.Quantify%Test.QuickCheck.DynamicLogic.InternalTest.QuickCheck.DynamicLogicquickcheck-dynamic Spec.Dynamic RegistryModelTest.QuickCheckcounterexample"Plutus.Contract.Test.ContractModelforAllQControl.ApplicativeemptyQuantifybase GHC.GenericsGeneric canGenerate shrinkSmartwithSizerunPropertyStateTrunPropertyReaderT VarContextAnySomeHasNoVariables HasVariablesgetAllVariablesVarmkVar isEmptyCtx isWellTyped extendContext allVariables ctxAtType arbitraryVar shrinkVarunsafeCoerceVarunsafeNextVarIndex $fShowVar$fOrdAny$fEqAny$fHasVariablesHasNoVariables$fHasVariablesAny$fHasVariablesSet$fHasVariablesMap$fHasVariablesVar$fHasVariablesSmart$fShowVarContext$fGenericHasVariables:+:$fGenericHasVariables:*:$fGenericHasVariablesU1$fGenericHasVariablesK1$fGenericHasVariablesM1$fHasVariablesa$fSemigroupVarContext$fMonoidVarContext$fEqVar$fOrdVar $fDataVar$fHasVariablesWord64$fHasVariablesWord32$fHasVariablesWord16$fHasVariablesWord8$fHasVariablesChar$fHasVariablesInt$fHasVariablesInteger$fEqHasNoVariables$fShowHasNoVariables AnnotatedMetadatavarsunderlyingStateActionsActions_Step:=ActionWithPolarity polarActionpolarityPolarity PosPolarity NegPolarity WithUsedVarsEnvEntry:==EnvLookUpRunModelperform postconditionpostconditionOnFailure monitoringmonitoringFailurePostconditionMrunPostRealized StateModelActionError actionNamearbitraryAction shrinkAction initialState nextStatefailureNextState preconditionvalidFailingAction:=? monitorPostcounterexamplePostlookUpVarMaybe lookUpVarinitialAnnotatedStatecomputePreconditioncomputeNextStatecomputeArbitraryActioncomputeShrinkAction stateAfter runActions$fIsPerformResultea$fIsPerformResultVoida$fMonadTransPostconditionM$fShowPolarity $fHasVariablesActionWithPolarity$fEqStep$fShowWithUsedVars $fShowStep$fHasVariablesStep $fShowActions $fEqActions$fSemigroupActions$fShowAnnotated$fArbitraryActions$fGenericActions $fOrdPolarity $fEqPolarity$fFunctorPostconditionM$fApplicativePostconditionM$fMonadPostconditionM$fEqActionWithPolarity $fShowAny Quantifiable QuantifiesquantifyQuantifyConstraintsQuantificationisaQisEmptyQ generateQshrinkQwithGenQ arbitraryQexactlyQchooseQ elementsQ frequencyQoneofQmapQwhereQhasNoVariablesQvalidQuantification$fQuantifiableList$fQuantifiable(,,,,)$fQuantifiable(,,,)$fQuantifiable(,,)$fQuantifiable(,)$fQuantifiableQuantificationNextStep StoppingStepSteppingNoStep BadAction DynLogicModel restrictedTestContinuationContStepContStop TestSequenceTestSeqTestStep WitnessesDoWitness DynLogicTestBadPreconditionLoopingStuckDLScript FailingAction ErrorFail ActionFailDynPred ChoiceTypeAngelicDemonicDynLogic EmptySpecStopAfterAnyAltStoppingAfterWeightForAllMonitor DynFormula unDynFormula:> TestSeqStopWTestSeqWitness TestSeqStep TestSeqStopignorepassTestafterAny afterPolarafter afterNegative|||weighttoStopdoneerrorDL monitorDLalwaysdiscardWitnessesconsSeq unconsSeq unstopSeqnullSeqdropSeqgetContinuationunlines'prettyTestSequenceprettyWitnesses usedVariablesrestrictedPolar forAllScriptsforAllUniqueScriptsforAllMappedScripts withDLScriptwithDLScriptPrefixgenerateDLTest onDLTestSeq consDLTest consDLTestWgenerate sizeLimitinitialStateForstopping noStoppingnoAny nextSteps nextSteps' chooseOneOfneverchooseNextStepchooseUniqueNextStepkeepTryingUntil shrinkDLTest nextStateStep shrinkScript shrinkWitness pruneDLTeststepDLstepDLW stepDLSeq stepDLWitness stepDLStep demonicAlt propPruningGeneratedScriptIsNoop getScriptmakeTestFromPruned unfailDLTeststuck validDLTest scriptFromDL sequenceStepsbadActionsGiven badActionsapplyMonitoringfindMonitoring$fShowFailingAction$fEqFailingAction$fHasVariablesFailingAction$fShowWitnesses $fEqWitnesses$fShowDynLogicTest$fEqChoiceType$fShowChoiceType$fEqTestContinuation$fShowTestContinuation$fEqTestSequence$fShowTestSequence$fTraversableWitnesses$fFoldableWitnesses$fFunctorWitnessesDLaction failingAction anyAction anyActions anyActions_getSizegetModelStateDLgetVarContextDL forAllVarassert assertModelforAllNonVariableQforAllUniqueDLforAllDLforAllMappedDL $fMonadFailDL $fMonadDL$fAlternativeDL$fApplicativeDL $fFunctorDL mtl-2.3.1Control.Monad.State.ClassstateGHC.BaseMonad(QuickCheck-2.14.3-EzaT5hJZQaG6V1CwlPQFGfTest.QuickCheck.Monadicghc-prim GHC.TypesFalseTest.QuickCheck.PropertyProperty PerformResultVoidTest.QuickCheck.Arbitrary ArbitraryTest.QuickCheck.GenGen GHC.MaybeNothingelements frequencyFunctortabulatecollectTruelabel