%{      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqr s t u v w x y z { | } ~  <(C) 2017, ATS Advanced Telematic Systems GmbH, Jacob Stanley BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)Safe6DOT"Higher-order traversable functors.Higher-order version of .Higher-order foldable functors.Higher-order version of .Higher-order functors.Higher-order version of . (C) 2017, Jacob Stanley BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None%&/234IConcrete values.Symbolic values. Symbolic variable names. Opaque values..Useful if you want to put something without a E instance inside something which you'd like to be able to display.jReferences are the potential or actual result of executing an action. They are parameterised by either  or ' depending on the phase of the test. variables are the potential results of actions. These are used when generating the sequence of actions to execute. They allow actions which occur later in the sequence to make use of the result of an action which came earlier in the sequence. variables are the actual results of actions. These are used during test execution. They provide access to the actual runtime value of a variable.(Take the value from a concrete variable.0Take the value from an opaque concrete variable.  !"          !"-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None%&DOT1The initial model is polymorphic in the type of references it uses, so that it can be used both in the pre- and the post-condition check.2ZPost-conditions are checked after the actions have been executed and we got a response.3BWhen we execute our actions we have access to concrete references.4The transition function must be polymorphic in the type of variables used, as it is used both while generating and executing.5oPre-conditions are checked while generating, at this stage we do not yet have access to concrete references.6:Shrinking should preserve the response type of the action.7TWhen generating actions we have access to a model containing symbolic references.8cAn untyped action is an action where the response type is hidden away using an existential type.We need to hide the response type when generating actions, because in general the actions we want to generate will have different response types; and thus we can only type the generating function if we hide the response type. 123456789 123456789 897654321123456789-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)Safe:Lifts  to properties.;/Lifts a plain property into a monadic property.<jWrite a metaproperty on the output of QuickChecking a property using a boolean predicate on the output.=.Same as above, but using a property predicate.>DGiven shrinkers for the components of a pair we can shrink the pair.?&Same above, but for homogeneous pairs.:;<=>?:;<=>?:;<=?>:;<=>?(C) 2017, Jacob Stanley BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)NoneOT@Environment errors.C0A mapping of symbolic values to concrete values.FCreate an empty environment.G;Insert a symbolic / concrete pairing in to the environment.HCast a  in to a concrete value.I]Turns an environment in to a function for looking up a concrete value from a symbolic one.JOConvert a symbolic structure to a concrete one, using the provided environment. @ABCDEFGHIJ @ABCDEFGHIJ CDE@ABFGHIJ@ABCDEFGHIJ-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None%&2:DO A process id.QaAn internal action is an action together with the symbolic variable that will hold its result.S.Forks are used to represent parallel programs.UVA parallel program is an abstract datatype that represents three sequences of actions; a sequential prefix and two parallel suffixes. Analogous to the sequential case, the user shows how to generate, shrink, execute and modelcheck individual actions, and then the below combinators lift those things to whole parallel programs.XQA (sequential) program is an abstract datatype representing a list of actions.The idea is that the user shows how to generate, shrink, execute and modelcheck individual actions, and then the below combinators lift those things to whole programs.OPQRSTUVWXYZ[\]^_ OPQRSTUVWXYZ XYZUVWOPSTQR OPQRSTUVWXYZ[\]^_-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)5Mats Daniel Gustafsson <daniel@advancedtelematic.com> provisionalnon-portable (GHC extensions)NonegEvent invocation or response.jBGiven a history, and output from processes generate Doc with boxesghijghijghij ghij-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None:OTlAGenerate programs whose actions all respect their pre-conditions.mFilter out invalid actions from a program. An action is invalid if either its pre-condition doesn't hold, or it uses references that are not in scope.n-Returns the set of references an action uses.oVGiven a shrinker of typed actions we can lift it to a shrinker of internal actions.p=Shrink a program in a pre-condition and scope respecting way.qwFor each action in a program, check that if the pre-condition holds for the action, then so does the post-condition.l#Name supply for symbolic variables.mWhere Set Var is the scope.nopProgram to shrink.qLThe model with symbolic references is used to check pre-conditions against.LWhile the one with concrete referenes is used for checking post-conditions.lmnopqlmnopqlmnopq -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)NoneOTr\Scope-check a program, i.e. make sure that no action uses a reference that doesn't exist.s)Same as above, but for parallel programs.rsrsrsrs -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None %&:ADOTtUA history is a trace of invocations and responses from running a parallel program.wNGenerate a parallel program whose actions all respect their pre-conditions.xIShrink a parallel program in a pre-condition and scope respecting way.yRun a parallel program, by first executing the prefix sequentially and then the suffixes in parallel, and return the history (or trace) of the execution.z?Check if a history from a parallel execution can be linearised.tuvwxyzHistory to be checked.tuvwxyzwxyztuvtuvwxyz -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None:{2Check if two lists of actions are equal modulo \alpha -conversion.|2Check if two forks of actions are equal modulo \alpha -conversion.{The two input programs.|The two input forks.{|{|{| -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None:OT}This function is like a  for sequential programs.~ORun a sequential program and check if your model agrees with your semantics.Same as above, except with the possibility to setup some resource for the runner to use. The resource could be a database connection for example.This function is like a  for parallel programs.@Run a parallel program and collect the history of the execution.DSame as above, but with the possibility of setting up some resource.}/Predicate that should hold for all programs.~RunnerSetup a resource.Tear down the resource.8Predicate that should hold for all parallel programs.8Predicate that should hold for the execution history.Setup a resource.Tear down the resource.& 123456789UXtz}~ X}~Utz}~  !"#$%&'()*+,-./0123456789:;<=>?@@ABCDEFGHIJJKLMNOPQRSTUUVVWWXXYZZ[\]^_`abcdefghijklmnopqr s t u u v w x y z { | } ~           5quickcheck-state-machine-0.1.0-K8zkcV9DXMpAJVx0Gu0AdI Test.StateMachine.Types.HFunctor"Test.StateMachine.Types.ReferencesTest.StateMachine.Types Test.StateMachine.Internal.Utils,Test.StateMachine.Internal.Types.Environment Test.StateMachine.Internal.Types*Test.StateMachine.Internal.Utils.BoxDrawer%Test.StateMachine.Internal.Sequential%Test.StateMachine.Internal.ScopeCheck#Test.StateMachine.Internal.Parallel(Test.StateMachine.Internal.AlphaEqualityTest.StateMachine HTraversable htraverse HFoldablehfoldMapHFunctorhfmapConcreteSymbolicVarOpaqueunOpaque Referenceconcreteopaque$fOrd1Concrete $fEq1Concrete$fShow1Concrete$fShowConcrete$fOrd1Symbolic $fEq1Symbolic$fReadSymbolic$fShow1Symbolic$fShowSymbolic $fShowOpaque$fHFoldableReference$fHFunctorReference$fHTraversableReference$fShowReference$fOrdReference $fEqReference $fEqOpaque $fOrdOpaque$fEqVar$fOrdVar $fShowVar$fNumVar $fReadVar $fEqConcrete $fOrdConcrete$fFunctorConcrete$fFoldableConcrete$fTraversableConcrete $fOrdSymbolic $fEqSymbolic InitialModel Postcondition Semantics Transition PreconditionShrinker GeneratorUntypedanyP liftPropertyshrinkPropertyHelpershrinkPropertyHelper' shrinkPair' shrinkPairEnvironmentErrorEnvironmentValueNotFoundEnvironmentTypeError Environment unEnvironmentemptyEnvironmentinsertConcrete reifyDynamicreifyEnvironmentreify$fShowEnvironment$fEqEnvironmentError$fOrdEnvironmentError$fShowEnvironmentErrorPidInternalForkParallelProgramunParallelProgramProgram unProgram$fShowParallelProgram $fReadProgram $fShowProgram$fMonoidProgram $fEqProgram$fEqFork $fFunctorFork $fShowFork $fOrdFork $fReadFork$fEqPid $fShowPid EventTypeOpenCloseexec$fShowEventTypegenerateProgram filterInvalid getUsedVarsliftShrinkInternal shrinkProgram checkProgram scopeCheckscopeCheckParallelHistory unHistorygenerateParallelProgramshrinkParallelProgramexecuteParallelProgramcheckParallelProgramalphaEq alphaEqFork forAllProgramrunAndCheckProgramrunAndCheckProgram'forAllParallelProgramrunParallelProgramrunParallelProgram'baseData.Traversabletraverse Data.FoldablefoldMapGHC.BasefmapGHC.ShowShowany Data.DynamicDynamicCmdTopStartActiveDeactiveRetBottomEventcompilesizeadjustnexttoEvent compilePrefix Operation HistoryEventInvocationEvent ResponseEventUntypedConcreteHistory'getProcessIdEventtakeInvocationsfindCorrespondingResp linearTree linearise toBoxDrawings canonical canonical' canonicalFork'QuickCheck-2.9.2-8nJqNls0Q836oDXpGGg3LDTest.QuickCheck.Property forAllShrink