!>\\      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                  ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [ Safe\]^_`abc-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)Safe1EX7   !"#$%&'()*+,-./01234567 !"#$%  &'()*+,-./0123456 )5*5+5,5-5.5/80814233241Safe-8>HSUVX :;<=>?@ABC >?@A<=B:;C(C) 2017, Jacob Stanley BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)None &'17=>?M#YZ[\]^_`abcdefbc`a^_\]defYZ[-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)None1"&quickcheck-state-machineSAn operation packs up an invocation event with its corresponding response event.quickcheck-state-machinegGiven a history, return all possible interleavings of invocations and corresponding response events.(C) 2018, HERE Europe B.V. BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)NoneM%1(C) 2017, Jacob Stanley BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)NoneMSX0quickcheck-state-machineEnvironment errors.quickcheck-state-machine0A mapping of symbolic values to concrete values.quickcheck-state-machineCreate an empty environment.quickcheck-state-machine;Insert a symbolic / concrete pairing in to the environment.quickcheck-state-machineCast a d in to a concrete value.quickcheck-state-machine]Turns an environment in to a function for looking up a concrete value from a symbolic one.quickcheck-state-machineRConvert a symbolic structure to a concrete one, using the provided environment. -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)None 1456>MSX6quickcheck-state-machine(Previously symbolically executed command?Invariant: the variables must be the variables in the response.RYZ[\]^_`abcdef#None -.8=>?HUVXk<quickcheck-state-machine"The names of all possible commands=This is used for things like tagging, coverage checking, etc.quickcheck-state-machineName of this particular commandquickcheck-state-machineName of all possible commandsquickcheck-state-machineConvenience wrapper for  -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)5Mats Daniel Gustafsson <daniel@advancedtelematic.com> provisionalnon-portable (GHC extensions)None4BSquickcheck-state-machineEvent invocation or response.quickcheck-state-machineBGiven a history, and output from processes generate Doc with boxes 9(C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)Safe4X^ quickcheck-state-machineFMore permissive notion of shrinking where a value can shrink to itself For example mshrink 3 == [0, 2] -- standard QuickCheck shrink shrinkS 3 == [Shrunk True 0, Shrunk True 2, Shrunk False 3]This is primarily useful when shrinking composite structures: the combinators here keep track of whether something was shrunk  somewhere( in the structure. For example, we have  shrinkListS (shrinkPairS shrinkS shrinkS) [(1,3),(2,4)] == [ Shrunk True [] -- removed all elements of the list , Shrunk True [(2,4)] -- removed the first , Shrunk True [(1,3)] -- removed the second , Shrunk True [(0,3),(2,4)] -- shrinking the '1' , Shrunk True [(1,0),(2,4)] -- shrinking the '3' , Shrunk True [(1,2),(2,4)] -- .. , Shrunk True [(1,3),(0,4)] -- shrinking the '2' , Shrunk True [(1,3),(1,4)] -- .. , Shrunk True [(1,3),(2,0)] -- shrinking the '4' , Shrunk True [(1,3),(2,2)] -- .. , Shrunk True [(1,3),(2,3)] -- .. , Shrunk False [(1,3),(2,4)] -- the original unchanged list ]quickcheck-state-machine/Lifts a plain property into a monadic property.quickcheck-state-machineLifts e to f.quickcheck-state-machine A variant of # with an explicit show function.quickcheck-state-machineLifts g to properties.quickcheck-state-machineDGiven shrinkers for the components of a pair we can shrink the pair.quickcheck-state-machine&Same above, but for homogeneous pairs.hquickcheck-state-machineLike i, but retries n times.quickcheck-state-machine&Shrink list without shrinking elements  -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)None "#$->@AHPX_quickcheck-state-machineEnvironment required during quickcheck-state-machine(The model we're starting validation fromquickcheck-state-machineReference renumberingWhen a command Command .. [Var i, ..]is changed during validation to Command .. [Var j, ..]then any subsequent uses of Var i should be replaced by Var j. This is recorded in  . When we remove8 the first command altogether (during shrinking), then Var i won't appear in the : and shrank candidates that contain commands referring to Var i! should be considered as invalid.quickcheck-state-machine'Counter (for generating new references)quickcheck-state-machine<Shrink commands in a pre-condition and scope respecting way.quickcheck-state-machineCValidate list of commands, optionally shrinking one of the commands2The input to this function is a list of commands (), for example [A, B, C, D, E, F, G, H]The result is a list of X, i.e. a list of lists. The outermost list is used for all the shrinking possibilities. For example, let's assume we haven't shrunk something yet, and therefore need to shrink one of the commands. Let's further assume that only commands B and E can be shrunk, to B1, B2 and E1, E2, E3 respectively. Then the result will look something like f[ -- outermost list recording all the shrink possibilities [A', B1', C', D', E' , F', G', H'] -- B shrunk to B1 , [A', B1', C', D', E' , F', G', H'] -- B shrunk to B2 , [A', B' , C', D', E1', F', G', H'] -- E shrunk to E1 , [A', B' , C', D', E2', F', G', H'] -- E shrunk to E2 , [A', B' , C', D', E3', F', G', H'] -- E shrunk to E3 ]where one of the commands has been shrunk and all commands have been validated and renumbered (references updated). So, in this example, the result will contain at most 5 lists; it may contain fewer, since some of these lists may not be valid.If we _did_ already shrink something, then no commands will be shrunk, and the resulting list will either be empty (if the list of commands was invalid) or contain a single4 element with the validated and renumbered commands."quickcheck-state-machineSPrint distribution of commands and fail if some commands have not been executed.quickcheck-state-machineMinimum number of commands.quickcheck-state-machine Predicate.quickcheck-state-machineMinimum number of commands.quickcheck-state-machineMinimum number of commands.quickcheck-state-machineMinimum number of commands.quickcheck-state-machineMaximum number of commands.quickcheck-state-machine#Check invariant and post-condition?   !"#$%   !#$"% -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)None$>SX'quickcheck-state-machineGenerate parallel commands.Parallel commands are generated as follows. We begin by generating sequential commands and then splitting this list in two at some index. The first half will be used as the prefix.nThe second half will be used to build suffixes. For example, starting from the following sequential commands: , B, C, D, E, F, G, H, I]6We split it in two, giving us the prefix and the rest: ,prefix: [A, B] rest: [C, D, E, F, G, H, I]%We advance the model with the prefix. Make a suffix: we take commands from rest* as long as these are parallel safe (see j). This means that the pre-conditions (using the 'advanced' model) of each of those commands will hold no matter in which order they are executed.Say this is true for  [C, D, E], but not anymore for F, maybe because F depends on one of  [C, D, E]O. Then we divide this 'chunk' in two by splitting it in the middle, obtaining [C] and [D, E].. These two halves of the chunk (stored as a E) will later be executed in parallel. Together they form one suffix.1Then the model is advanced using the whole chunk  [C, D, E]. Think of it as a barrier after executing the two halves of the chunk in parallel. Then this process of building a chunk/suffix repeats itself, starting from  Make a suffix using the 'advanced' model.4In the end we might end up with something like this: \ % % [C] %%% % [F, G] % [A, B] %%$ %%%%$ % % [D, E] % % [H, I] %jquickcheck-state-machinesA list of commands is parallel safe if the pre-conditions for all commands hold in all permutations of the list.(quickcheck-state-machine1Apply the transition of some commands to a model.)quickcheck-state-machineIShrink a parallel program in a pre-condition and scope respecting way..quickcheck-state-machineTry 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./quickcheck-state-machinehTakes the output of parallel program runs and pretty prints a counterexample if any of the runs fail.0quickcheck-state-machineyDraw an ASCII diagram of the history of a parallel program. Useful for seeing how a race condition might have occured.&quickcheck-state-machine Predicate.(quickcheck-state-machine The model.quickcheck-state-machine The commands.,quickcheck-state-machine/How many times to execute the parallel program./quickcheck-state-machine Output of +. &'()*+,-./0 &')*+,-.0/(-(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalnon-portable (GHC extensions)NoneX   !"#$%&'()*+,-./0123456YZ[\^`def!"#$%&+,/!%!"#$&+,/^`\edYZ[f -(C) 2017, ATS Advanced Telematic Systems GmbH BSD-style (see the file LICENSE)0Stevan Andjelkovic <stevan.andjelkovic@here.com> provisionalportableSafeUVҽ4quickcheck-state-machine(Partial) functions.5quickcheck-state-machine Relations.9quickcheck-state-machineSubset.'boolean ([1, 2] `isSubsetOf` [3, 2, 1])True:quickcheck-state-machine Set equality.boolean ([1, 1, 2] ~= [2, 1])TrueEquickcheck-state-machineDomain restriction.(['a'] <| [ ('a', "apa"), ('b', "bepa") ] [('a',"apa")]Fquickcheck-state-machineCodomain restriction.*[ ('a', "apa"), ('b', "bepa") ] |> ["apa"] [('a',"apa")]Gquickcheck-state-machineDomain substraction.)['a'] <-| [ ('a', "apa"), ('b', "bepa") ][('b',"bepa")]Hquickcheck-state-machineCodomain substraction.:[ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"][('b',"bepa"),('c',"cepa")]B[ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa", "cepa"][('b',"bepa")]G[ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"] |-> ["cepa"][('b',"bepa")]Iquickcheck-state-machineThe image of a relation.Jquickcheck-state-machine Overriding.![('a', "apa")] <+ [('a', "bepa")][('a',"bepa")]![('a', "apa")] <+ [('b', "bepa")][('a',"apa"),('b',"bepa")]Kquickcheck-state-machineDirect product.Lquickcheck-state-machineParallel product.Wquickcheck-state-machine Application.[quickcheck-state-machine Assignment.$singleton 'a' "apa" .! 'a' .= "bepa"[('a',"bepa")]$singleton 'a' "apa" .! 'b' .= "bepa"[('a',"apa"),('b',"bepa")]+123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[+6789:54132;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[112131768795:5E4F4G4H4J4K4L4Y4Z9 [4k !"#$%&'()*+,-./0!123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijjkllmmnnoopqrstuvwxyz{|}~                                          ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [\]^_`abcdefghigjdkl mgno pq5quickcheck-state-machine-0.6.0-LSB9KqOf7Vm4DfY8PJnoGQTest.StateMachine.LogicTest.StateMachine.Types.Rank2"Test.StateMachine.Types.ReferencesTest.StateMachine.Types.HistoryTest.StateMachine.Types.GenSym#Test.StateMachine.Types.EnvironmentTest.StateMachine.Types!Test.StateMachine.ConstructorNameTest.StateMachine.BoxDrawerTest.StateMachine.UtilsTest.StateMachine.SequentialTest.StateMachine.ParallelTest.StateMachine.ZPaths_quickcheck_state_machineTest.QuickCheck.Monadic forAllShrinkTest.StateMachineValueVFalseVTrueCounterexampleBotCFstSndEitherCImpliesCNotC PredicateCForallCExistsCBooleanC AnnotateC Predicate:==:/=:<:<=:>:>=ElemNotElemLogicBotTop:&&:||:=>NotForallExistsBooleanAnnotatedual strongNegbooleanlogic predicate.==./=.<.<=.>.>=elemnotElem.//.&&.||.=>forallexists $fShowValue$fShowCounterexample$fShowPredicate TraversabletraverseFoldablefoldMapFunctorfmapgfmap<$>gfoldMap gtraverse$fFunctorkRec1 $fFunctorkM1 $fFunctork:.: $fFunctork:*: $fFunctork:+: $fFunctorkK1 $fFunctorkU1$fFoldablekRec1 $fFoldablekM1$fFoldablek:.:$fFoldablek:*:$fFoldablek:+: $fFoldablekK1 $fFoldablekU1$fTraversablekRec1$fTraversablekM1$fTraversablek:.:$fTraversablek:*:$fTraversablek:+:$fTraversablekK1$fTraversablekU1OpaqueunOpaque ReferenceConcreteSymbolicVar referenceconcreteopaque$fOrd1Symbolic $fEq1Symbolic$fToExprSymbolic$fShow1Symbolic$fToExprConcrete$fOrd1Concrete $fEq1Concrete$fShow1Concrete$fShowReference$fOrdReference $fEqReference$fTraversableTYPEReference$fFoldableTYPEReference$fFunctorTYPEReference$fToExprReference$fToExprOpaque $fShowOpaque$fEqVar$fOrdVar $fShowVar $fGenericVar $fToExprVar$fGenericReference $fEqOpaque $fOrdOpaque$fShowConcrete $fOrdSymbolic $fEqSymbolic$fShowSymbolic OperationCrash HistoryEvent InvocationResponse ExceptionPidunPidHistory'History unHistorymakeOperations interleavings$fEqPid $fShowPid$fShowOperation$fShowHistoryEvent$fEqHistoryEvent $fShowHistory $fEqHistoryCounterGenSym runGenSymgenSym newCounter$fFunctorGenSym$fApplicativeGenSym $fMonadGenSymEnvironmentErrorEnvironmentValueNotFoundEnvironmentTypeError Environment unEnvironmentemptyEnvironmentinsertConcreteinsertConcretes reifyDynamicreifyEnvironmentreify$fSemigroupEnvironment$fMonoidEnvironment$fShowEnvironment$fEqEnvironmentError$fOrdEnvironmentError$fShowEnvironmentErrorParallelCommandsPairproj1proj2ParallelCommandsFprefixsuffixesReasonOkPreconditionFailedPostconditionFailedInvariantBrokenExceptionThrownCommands unCommandsCommand StateMachine initModel transition precondition postcondition invariant generator distributionshrinker semanticsmocklengthCommandsfromPairtoPair$fSemigroupCommands$fMonoidCommands $fEqReason $fShowReason$fEqPair $fOrdPair $fShowPair $fFunctorPair$fFoldablePair$fTraversablePair$fShowParallelCommandsF$fShowCommands $fShowCommand CommandNamescmdNamecmdNames commandName$fCommandNameskRec1$fCommandNamesk:*:$fCommandNamesk:+:$fCommandNameskM1$fCommandNameskM10$fCommandNameskM11$fCommandNameskK1$fCommandNameskU1Fork EventTypeOpenCloseexec$fShowEventType $fFunctorForkShrunk wasShrunkshrunk liftProperty whenFailMforAllShrinkShowanyP shrinkPair' shrinkPair suchThatOneOfoldCovershrinkS shrinkListS shrinkListS' shrinkPairS shrinkPairS' $fShowShrunk$fFunctorShrunk ShouldShrink MustShrink DontShrink ValidateEnvveModelveScope veCounterforAllCommandsgenerateCommandsgenerateCommandsStatemeasureFrequencycalculateFrequency getUsedVarsshrinkCommandsinitValidateEnvshrinkAndValidate runCommandsgetChanContentsexecuteCommandsprettyPrintHistoryprettyCommandscheckCommandNames commandNamescommandNamesInOrdertransitionMatrixforAllParallelCommandsgenerateParallelCommands advanceModelshrinkParallelCommandsshrinkAndValidateParallelrunParallelCommandsrunParallelCommandsNTimesexecuteParallelCommands lineariseprettyParallelCommands toBoxDrawings:<->:/->:->FunRelconsunion intersect isSubsetOf~=emptyidentity singletondomaincodomaincomposefcomposeinverse lookupDom lookupCod<||><-||->image<+<**><||> isTotalRel isSurjRelisTotalSurjRel isPartialFun isTotalFun isPartialInj isTotalInj isPartialSurj isTotalSurj isBijection!!?.%.!.=version getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileNamebase Data.DynamicDynamic*QuickCheck-2.12.6.1-4a6Ozz7bfHzLQyA4XOD1DcTest.QuickCheck.PropertywhenFail PropertyM Data.FoldableanysuchThatMaybeNTest.QuickCheck.Gen suchThatMaybe parallelSafe