%      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~       !"#$-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)NoneSTY 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.DGiven shrinkers for the components of a pair we can shrink the pair.&Same above, but for homogeneous pairs. A variant of # with an explicit show function. &Remove duplicate elements from a list.  Drop last n elements of a list. *Indexing starting from the back of a list.   -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)Safe0CV" ! "*)$#%&'(+,-.""#$%&'()* !+, -.  !"#$%&'()*%3&2'19(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)SafeF#3%Extracting constructors from actions.4Constructor of a given action.50Total number of constructors in the action type.6A constructor name is a string.3546767834534567<(C) 2017, ATS Advanced Telematic Systems GmbH, Jacob Stanley BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)Safe7FQV);"Higher-order traversable functors.<Higher-order version of (.=Higher-order foldable functors.>Higher-order version of ).?Higher-order functors.@Higher-order version 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)None0ADerive ?, =, ;.B B ''Action ===> instance ; Action where ... CDerive the body of <.D D ''Action ===> instance = Action where ... EDerive the body of >.F F ''Action ===> instance ? Action where ... GDerive the body of @.ABCDEFGABCDEFG+,-./0(C) 2017, Jacob Stanley BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None&'0345KAHConcrete values.JSymbolic values.LSymbolic variable names.NOpaque values..Useful if you want to put something without a 1E instance inside something which you'd like to be able to display.QjReferences are the potential or actual result of executing an action. They are parameterised by either J or H' depending on the phase of the test.J 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.H variables are the actual results of actions. These are used during test execution. They provide access to the actual runtime value of a variable.S(Take the value from a concrete variable.T0Take the value from an opaque concrete variable. HIJKLMNOPQRST QRSTNOPJKHILMHIJKLMNOPQR-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None "#&'3FQVY z+How to run the monad used by the semantics.|"The result of executing an action.BWhen we execute our actions we have access to concrete references.The 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.ZPost-conditions are checked after the actions have been executed and we got a response.The transition function must be polymorphic in the type of variables used, as it is used both while generating and executing.oPre-conditions are checked while generating, at this stage we do not yet have access to concrete references.:Shrinking should preserve the response type of the action.TWhen generating actions we have access to a model containing symbolic references.3Same as above, but with possibly failing semantics.aA (non-failing) state machine record bundles up all functionality needed to perform our tests.cAn 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.WHelper for lifting non-failing semantics to a possibly failing state machine record.<34567;<=>?@HIJKLMNOPQRSTvwxyz{|}~$|}~{zvwxyvwxy|}~  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)Nonek Given a name ''Action , derive 1 for  (Action v a) and ( Action), and 2 (Action Symbolic). See , , and 3. ! ''Action ===> deriving instance 2 v => 1 (Action v a). ! ''Action ===> deriving instance 1 ( Action) 3   derivingShow1` ''Action ===> instance Show1 (Action Symbolic) where liftShowsPrec _ _ _ act _ = show act 45Gather 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 Q fields.  ''Action ===> instance 3 Action where ... 5 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)NoneozDerive instances of , , , . ABDF AFDB (C) 2017, Jacob Stanley BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)NoneQVx4Environment errors.0A mapping of symbolic values to concrete values.Create an empty environment.;Insert a symbolic / concrete pairing in to the environment.Cast a 6 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&'03<F+ A process id.aAn internal action is an action together with the symbolic variable that will hold its result.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)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None &'CFKQV(SAn 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)5Mats Daniel Gustafsson <daniel@advancedtelematic.com> provisionalnon-portable (GHC extensions)None3=Event invocation or response.BGiven a history, and output from processes generate Doc with boxes789:;<=>?-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None"#<QVAGenerate 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 result 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)None &'<>?QVNGenerate 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.-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)1Stevan Andjelkovic <stevan@advancedtelematic.com> provisionalnon-portable (GHC extensions)None "#<>?QSTV This function is like a  forAllShrink for sequential programs. Variant of G which returns the generated and shrunk program if the property fails.Wrapper around  using the ; specification to generate and shrink sequential programs. Variant of  with counterexamples.9Testable property of sequential programs derived from a  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  forAllShrink for parallel programs.0Wrapper around 'forAllParallelProgram using the 9 specification to generate and shrink parallel programs. Variant of  with counterexamples.9Testable property of parallel programs derived from a  specification.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.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 'runParallelProgram.N34567;<=>?@HIJKLMNOPQRSTvwxyz{|}~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, 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")]&      !"#$&      !"#$A !"#$%&'()*+,-./0123456789:;<=>?@ABC4DEFGHIJKLMNOPQRSTUVWXYZ[\]]^^__``abbcdefghijklmnopqrstuvwxyz{|}~                              !"#$%&'()*+,-./*01*+2*34556789*:;*<= > ? @*ABC?DEFGHIIJK5quickcheck-state-machine-0.3.1-BogIEpzqta1FmV5UsumIr0Test.StateMachine Test.StateMachine.Internal.UtilsTest.StateMachine.Logic Test.StateMachine.Types.Generics Test.StateMachine.Types.HFunctor#Test.StateMachine.Types.HFunctor.TH"Test.StateMachine.Types.ReferencesTest.StateMachine.Types#Test.StateMachine.Types.Generics.THTest.StateMachine.TH,Test.StateMachine.Internal.Types.Environment Test.StateMachine.Internal.TypesTest.StateMachine.Types.History*Test.StateMachine.Internal.Utils.BoxDrawer%Test.StateMachine.Internal.Sequential#Test.StateMachine.Internal.ParallelTest.StateMachine.ZTest.QuickCheck.Monadic forAllShrinkHFunctor HFoldable HTraversable ConstructorTest.StateMachine.Utils(QuickCheck-2.10.1-BUFYQzp5Pjm7JbQeTzW89lTest.QuickCheck.Test quickCheckanyP liftProperty whenFailMalwaysP shrinkPair' shrinkPairforAllShrinkShowforAllShrinkShowCnubdropLasttoLastgetChanContentsValueVFalseVTrueCounterexampleBotCFstSndEitherCImpliesCNotC PredicateC AnnotateC Predicate:==:/=:<:<=:>:>=ElemNotElemLogicBotTop:&&:||:=>NotAnnotatedual strongNeglogic predicate $fShowLogic$fShowCounterexample $fShowValue$fShowPredicate Constructors constructor nConstructors$fShowConstructor$fEqConstructor$fOrdConstructor htraversehfoldMaphfmapderiveHClassesderiveHTraversable mkhtraversederiveHFoldable mkhfoldMapderiveHFunctormkhfmapConcreteSymbolicVarOpaqueunOpaque Referenceconcreteopaque$fHFoldableReference$fHFunctorReference$fHTraversableReference$fShowReference$fOrdReference $fEqReference $fShowOpaque$fShow1Symbolic$fOrd1Symbolic $fEq1Symbolic$fShow1Concrete$fOrd1Concrete $fEq1Concrete $fEqOpaque $fOrdOpaque$fEqVar$fOrdVar $fShowVar$fNumVar $fReadVar $fEqConcrete $fOrdConcrete$fShowConcrete$fReadConcrete$fFunctorConcrete$fFoldableConcrete$fTraversableConcrete$fFoldableSymbolic$fReadSymbolic$fShowSymbolic $fOrdSymbolic $fEqSymbolic$fReadReferenceReasonOkPreconditionFailedPostconditionFailedRunner Semantics'ResultSuccessFail Semantics InitialModelPostcondition' Postcondition Transition' Transition PreconditionShrinker Generator StateMachine' StateMachine generator' shrinker' precondition' transition'postcondition'model' semantics'runner'Untyped stateMachine okTransitionokPostcondition okSemanticsppResult$fFunctorResult $fEqReason $fShowReason deriveShows deriveShowderiveShowUntyped mkShrinkerderiveConstructorsderiveTestClassesEnvironmentErrorEnvironmentValueNotFoundEnvironmentTypeError Environment unEnvironmentemptyEnvironmentinsertConcrete reifyDynamicreifyEnvironmentreify$fShowEnvironment$fEqEnvironmentError$fOrdEnvironmentError$fShowEnvironmentErrorPidInternalParallelProgramProgram unProgram programLengthparallelProgramLengthparallelProgramFromListparallelProgramToListparallelProgramAsListflattenParallelProgram$fReadInternal$fShowInternal $fEqInternal$fMonoidProgram $fEqProgram$fEqPid $fShowPid$fReadParallelProgram$fShowParallelProgram$fEqParallelProgram $fReadProgram $fShowProgram OperationUntypedConcrete HistoryEventInvocationEvent ResponseEventHistory'History unHistory ppHistorygetProcessIdEvent linearTree$fMonoidHistoryFork EventTypeOpenCloseexec$fShowEventType $fFunctorForkgenerateProgramgenerateProgram' filterInvalid getUsedVarsliftShrinkInternal validProgram shrinkProgramexecuteProgramgenerateParallelProgramshrinkParallelProgramvalidParallelProgramexecuteParallelProgram linearise toBoxDrawings forAllProgramforAllProgramCmonadicSequentialmonadicSequentialC runProgram prettyProgramcheckActionNames actionNamesmonadicParallelmonadicParallelCrunParallelProgramrunParallelProgram'prettyParallelProgramFunRelunion intersect isSubsetOf~=emptyidentity singletondomaincodomaincomposefcomposeinverse lookupDom lookupCod<||><-||->image<+<**><||> isTotalRel isSurjRelisTotalSurjRel isPartialFun isTotalFun isPartialInj isTotalInj isPartialSurj isTotalSurj isBijection!.%.!.=base Data.FoldableanyTest.QuickCheck.PropertywhenFail PropertyMData.TraversabletraversefoldMapGHC.Basefmap Dictionary classNamefunNamepureEapEGHC.ShowShowData.Functor.ClassesShow1 deriveShow1showConstraintsderiveconstructor Data.DynamicDynamicCmdStartActiveDeactiveRetBottomEventforAllParallelProgramC