E      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalportableSafe (Partial) functions. Relations.Domain restriction.(['a'] <| [ ('a', "apa"), ('b', "bepa") ] [('a',"apa")]Codomain restriction.*[ ('a', "apa"), ('b', "bepa") ] |> ["apa"] [('a',"apa")]Domain substraction.)['a'] <-| [ ('a', "apa"), ('b', "bepa") ][('b',"bepa")]Codomain substraction.+[ ('a', "apa"), ('b', "bepa") ] |-> ["apa"][('b',"bepa")]The image of a relation. Overriding.![('a', "apa")] <+ [('a', "bepa")][('a',"bepa")]![('a', "apa")] <+ [('b', "bepa")][('a',"apa"),('b',"bepa")]Direct product.Parallel product.# Application.% Assignment.$singleton 'a' "apa" .! 'a' .= "bepa"[('a',"bepa")]$singleton 'a' "apa" .! 'b' .= "bepa"[('a',"apa"),('b',"bepa")]%  !"#$%%  !"#$%%  !"#$%%  !"#$%<(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%&/234I,Concrete values..Symbolic values.0Symbolic variable names.2Opaque values..Useful if you want to put something without a E instance inside something which you'd like to be able to display.5jReferences 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.7(Take the value from a concrete variable.80Take the value from an opaque concrete variable.,-./0123456789:;<=>?@ABCDE ,-./012345678 5678234./,-01,-./0123456789:;<=>?@ABCDE9(C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia BSD-style (see the file LICENSE)Li-yao Xia <lysxia@gmail.com> provisionalnon-portable (GHC extensions)SafeDZ%Extracting constructors from actions.[Constructor of a given action.\0Total number of constructors in the action type.]A constructor name is a string.Z[\]^_Z[\]^]^_Z[\Z[\]^_-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None%&DOT b+How to run the monad used by the semantics.cBWhen we execute our actions we have access to concrete references.d"The result of executing an action.gThe 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.hZPost-conditions are checked after the actions have been executed and we got a response.iThe transition function must be polymorphic in the type of variables used, as it is used both while generating and executing.joPre-conditions are checked while generating, at this stage we do not yet have access to concrete references.k:Shrinking should preserve the response type of the action.lTWhen generating actions we have access to a model containing symbolic references.m3Same as above, but with possibly failing semantics.waA (non-failing) state machine record bundles up all functionality needed to perform our tests.xcAn 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.zWHelper for lifting non-failing semantics to a possibly failing state machine record.bcdefghijklmnopqrstuvwxyz1&'()*+,-./012345678Z[\]^bcdfeghijklmnopqrstuvwxyzxywzmnopqrstuvlkjihgdefcb bcdefghijklm nopqrstuvwxyz-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None {Lifts  to properties.|/Lifts a plain property into a monadic property.}Lifts  to .~A property that tests prop repeatedly n2 times, failing as soon as any of the tests of prop fails.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.&Remove duplicate elements from a list. Drop last n elements of a list.*Indexing starting from the back of a list. {|}~ {|}~ {|}~ {|}~9(C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia BSD-style (see the file LICENSE)Li-yao Xia <lysxia@gmail.com> provisionalnon-portable (GHC extensions)None Given a name ''Action , derive  for  (Action v a) and (x Action). See  and . ! ''Action ===> deriving instance  v =>  (Action v a)@. ! ''Action ===> deriving instance  (x Action) 5Gather types of fields with parametric types to form Show% constraints for a derived instance.(Show1 v, Show a) for fields of type  Reference v aShow a for fields of type aThe Show1 vH constraint is separated so that we can easily remove it from the list.$( ''Action)% creates a generic shrinker of type (Action v a -> [Action v a]) which ignores 5 fields.  ''Action ===> instance Z Action where ... Kconstructor Foo{} = Constructor "Foo" constructor Bar{} = Constructor "Bar"      9(C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia BSD-style (see the file LICENSE)Li-yao Xia <lysxia@gmail.com> provisionalnon-portable (GHC extensions)NoneDerive *, (, &.  ''Action ===> instance & Action where ... Derive the body of '.  ''Action ===> instance ( Action where ... Derive the body of ).  ''Action ===> instance * Action where ... Derive the body of +.     9(C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia BSD-style (see the file LICENSE)Li-yao Xia <lysxia@gmail.com> provisionalnon-portable (GHC extensions)NoneDerive instances of , , , . 9(C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None{|}~ (C) 2017, Jacob Stanley BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)NoneOTEnvironment errors.0A mapping of symbolic values to concrete values.Create an empty environment.;Insert a symbolic / concrete pairing in to the environment.Cast a  in to a concrete value.]Turns an environment in to a function for looking up a concrete value from a symbolic one.OConvert a symbolic structure to a concrete one, using the provided environment.  -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None%&/2:D A process id.aAn internal action is an action together with the symbolic variable that will hold its result..Forks are used to represent parallel programs.VA 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.QA (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.+Returns the number of actions in a program.  -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)5Mats Daniel Gustafsson <daniel@advancedtelematic.com> provisionalnon-portable (GHC extensions)NoneEvent invocation or response.BGiven a history, and output from processes generate Doc with boxes !"#$%&'()*+,-  !"#$%&'()*+,--(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None%&ADITSAn operation packs up an invocation event with its corresponding response event.Untyped concrete actions./An event is either an invocation or a response.A trace is a list of events.,A history is a trace of a program execution.Pretty print a history.Get the process id of an event.gGiven a history, return all possible interleavings of invocations and corresponding response events../ ./-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None!":OTAGenerate programs whose actions all respect their pre-conditions.Filter 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.-Returns the set of references an action uses.VGiven a shrinker of typed actions we can lift it to a shrinker of internal actions.=Shrink a program in a pre-condition and scope respecting way.Execute a program and return a history, the final model and a property which contains the information of whether the execution respects the state machine model or not.#Name supply for symbolic variables.Where Set Var is the scope.Program to shrink.-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)NoneOT\Scope-check a program, i.e. make sure that no action uses a reference that doesn't exist.)Same as above, but for parallel programs.-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None %&:<=OTNGenerate a parallel program whose actions all respect their pre-conditions.IShrink a parallel program in a pre-condition and scope respecting way.Run a parallel program, by first executing the prefix sequentially and then the suffixes in parallel, and return the history (or trace) of the execution.Try to linearise a history of a parallel program execution using a sequential model. See the *Linearizability: a correctness condition for concurrent objects* paper linked to from the README for more info.yDraw an ASCII diagram of the history of a parallel program. Useful for seeing how a race condition might have occured.00-(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.12The two input forks.3123-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None !":<=OQRTThis function is like a 4 for sequential programs. Variant of G which returns the generated and shrunk program if the property fails.Wrapper around  using the w; specification to generate and shrink sequential programs. Variant of  with counterexamples.9Testable property of sequential programs derived from a w specification.^Takes the output of running a program and pretty prints a counterexample if the run failed.QPrint distribution of actions and fail if some actions have not been executed..Returns the frequency of actions in a program.This function is like a 4 for parallel programs. Variant of I which returns the generated and shrunk program if the property fails.Wrapper around  using the w9 specification to generate and shrink parallel programs. Variant of  with counterexamples.9Testable property of parallel programs derived from a w specification.Same as above, but with the ability to choose how many times each parallel program is executed. It can be important to tune this value in order to reveal race conditions. The more runs, the more likely we will find a bug, but it also takes longer.kTakes the output of a parallel program runs and pretty prints a counter example if any of the runs fail./Predicate that should hold for all programs./Predicate that should hold for all programs.,Predicate that should hold for all programs.,Predicate that should hold for all programs.8Predicate that should hold for all parallel programs.8Predicate that should hold for all parallel programs.5Predicate that should hold for all parallel programs.5Predicate that should hold for all parallel programs./How many times to execute the parallel program. Output of .E&'()*+,-./012345678Z[\]^bcdfeghijklmnopqrstuvwxyz5 !"#$%&'()*+,-./0123456789:;<=>?@ABCCDDEEFFGHHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~~                                  ! " # $ % & ' (  )* + , - . / 0 1 2 2 3 4 5 6 7 89:;<=>?@AB5quickcheck-state-machine-0.2.0-3TFk87s6NBgGVZP7iCSKaETest.StateMachineTest.StateMachine.Z Test.StateMachine.Types.HFunctor"Test.StateMachine.Types.References Test.StateMachine.Types.GenericsTest.StateMachine.Types Test.StateMachine.Internal.Utils#Test.StateMachine.Types.Generics.TH#Test.StateMachine.Types.HFunctor.THTest.StateMachine.TH,Test.StateMachine.Internal.Types.Environment Test.StateMachine.Internal.Types*Test.StateMachine.Internal.Utils.BoxDrawerTest.StateMachine.Types.History%Test.StateMachine.Internal.Sequential%Test.StateMachine.Internal.ScopeCheck#Test.StateMachine.Internal.Parallel(Test.StateMachine.Internal.AlphaEqualityHFunctor HFoldable HTraversable ConstructorTest.StateMachine.Utils'QuickCheck-2.9.2-8nJqNls0Q836oDXpGGg3LDTest.QuickCheck.Test quickCheckFunRelunion intersect isSubsetOf~=emptyidentity singletondomaincodomaincomposefcomposeinverse lookupDom lookupCod<||><-||->image<+<**><||> isTotalRel isSurjRelisTotalSurjRel isPartialFun isTotalFun isPartialInj isTotalInj isPartialSurj isTotalSurj isBijection!.!.= htraversehfoldMaphfmapConcreteSymbolicVarOpaqueunOpaque Referenceconcreteopaque$fShow1Concrete$fOrd1Concrete $fEq1Concrete$fShow1Symbolic$fOrd1Symbolic $fEq1Symbolic $fShowOpaque$fHFoldableReference$fHFunctorReference$fHTraversableReference$fShowReference$fOrdReference $fEqReference $fEqOpaque $fOrdOpaque$fEqVar$fOrdVar $fShowVar$fNumVar $fReadVar $fEqConcrete $fOrdConcrete$fShowConcrete$fReadConcrete$fFunctorConcrete$fFoldableConcrete$fTraversableConcrete$fFoldableSymbolic$fReadSymbolic$fShowSymbolic $fOrdSymbolic $fEqSymbolic$fReadReference Constructors constructor nConstructors$fShowConstructor$fEqConstructor$fOrdConstructorRunner SemanticsResultOkFail InitialModel Postcondition Transition PreconditionShrinker Generator StateMachine' StateMachine generator' shrinker' precondition' transition'postcondition'model' semantics'runner'Untyped stateMachineanyP liftProperty whenFailMalwaysPshrinkPropertyHelperCshrinkPropertyHelperC' shrinkPair' shrinkPairnubdropLasttoLast deriveShows deriveShowderiveShowUntyped mkShrinkerderiveConstructorsderiveHClassesderiveHTraversable mkhtraversederiveHFoldable mkhfoldMapderiveHFunctormkhfmapderiveTestClassesEnvironmentErrorEnvironmentValueNotFoundEnvironmentTypeError Environment unEnvironmentemptyEnvironmentinsertConcrete reifyDynamicreifyEnvironmentreify$fShowEnvironment$fEqEnvironmentError$fOrdEnvironmentError$fShowEnvironmentErrorPidInternalForkParallelProgramunParallelProgramProgram unProgram programLength$fReadInternal$fShowInternal $fEqInternal$fMonoidProgram $fEqProgram$fEqFork $fFunctorFork $fShowFork $fOrdFork $fReadFork$fEqPid $fShowPid$fReadParallelProgram$fShowParallelProgram $fReadProgram $fShowProgram EventTypeOpenCloseexec$fShowEventType OperationUntypedConcrete HistoryEventInvocationEvent ResponseEventHistory'History unHistory ppHistorygetProcessIdEvent linearTree$fMonoidHistorygenerateProgram filterInvalid getUsedVarsliftShrinkInternal shrinkProgramexecuteProgram scopeCheckscopeCheckParallelgenerateParallelProgramshrinkParallelProgramexecuteParallelProgram linearise toBoxDrawingsalphaEq alphaEqFork forAllProgramforAllProgramCmonadicSequentialmonadicSequentialC runProgram prettyProgramcheckActionNames actionNamesforAllParallelProgramforAllParallelProgramCmonadicParallelmonadicParallelCrunParallelProgramrunParallelProgram'prettyParallelProgrambaseData.Traversabletraverse Data.FoldablefoldMapGHC.BasefmapGHC.ShowShowanyTest.QuickCheck.PropertywhenFailTest.QuickCheck.Monadic PropertyMData.Functor.ClassesShow1showConstraintsderiveconstructor deriveShow'deriveShowUntyped'showConstraintsByConshowConstraintsByFieldgatherShowConstraints variableHead mkShrinker'shrinkerMatches listTupleP listTupleE listTuple shrinkable isReferencederiveConstructors' instanceHeadconstructorClausederivenConstructors Dictionary classNamefunNamepureEapE dictHFunctor dictHFoldabledictHTraversablereifying deriveIFormkFForhtraversalWithCxtForhtraversalBodyForhtraversalMatchForinfixE_htraversalFieldFor Data.DynamicDynamicCmdTopStartActiveDeactiveRetBottomEventcompilesizeadjustnexttoEvent compilePrefixtakeInvocationsfindCorrespondingRespanyP' canonical canonical' canonicalFork:quickcheck-with-counterexamples-1.0-5Ap4pfPOoOw6Wu024Kvy8lTest.QuickCheck.Counterexamples forAllShrink