-      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~        !"#$%&'()*+,  !"#$%&  !"#$%& !"#$%&   !"#$%&'=Takes a type and a list of variable names and declares them. (Add an include of a library ) Add an include of a header file -./*3printf, with and without a newline (nl) character. +'()*+'()+*'()*+,,,,H-./0123405WFor each typed variable, this type holds all its successive values in an infinite list C Beware : each element of one of those lists corresponds to a full Atom period,  not to a single clock tick. 6This is a generalization of U N which is used for storing Maps over values parameterized by different types. HIt is extensively used in the internals of Copilot, in conjunction with  g and i 789:;<=>?@ABCDE?A type is streamable iff a stream may emit values of that type $There are very strong links between E and 6 :  the types aggregated in 6 are exactly the E types 1 and that invariant should be kept (see methods) FBProvides access to the Map in a StreamableMaps which store values  of the good type GRProvides a way to modify (mostly used for insertions) the Map in a StreamableMaps % which store values of the good type HA default value for the type a. Its value is not important. IA constructor to produce an Atom value JA constructor to get an Atom! value from an external variable K5The argument only coerces the type, it is discarded. I Returns the format for outputting a value of this type with printf in C  For example %f for a float L>The same, only adds the wanted precision for floating points. M5The argument only coerces the type, it is discarded.  Returns the corresponding Atom type. NJLike Show, except that the formatting is exactly the same as the one of C P for example the booleans are first converted to 0 or 1, and floats and doubles  have the good precision. OLTo make customer C triggers. Only for Spec Bool (others through an error). P:Holds the complete specification of a distributed monitor QRContainer for all the instructions sending data, parameterised by different types R7An instruction to send data on a port at a given phase STA named stream UFContainer for mutually recursive streams, whose specifications may be " parameterized by different types #type Streams = StreamableMaps Spec VRSpecification of a stream, parameterized by the type of the values of the stream.  The only requirement on a is that it should be E. WXYZ[\]^_)Port over which to broadcast information `Phase of an Atom phase a Atom period b C file name c+Names of the streams or external variables d)Lookup into the map of the right type in 6 e)Lookup into the map of the right type in 6 / Launch an exception if the index is not in it fJust produce an Atom' value named after its first argument, W with an unspecified value. The second argument only coerces the type, it is discarded gJThis function is used to iterate on all the values in all the maps stored  by a 6!, accumulating a value over time hJThis function is used to iterate on all the values in all the maps stored  by a 6!, accumulating a value over time ijkOnly keeps in sm" the values whose key+type are in l. ; Also returns a bool saying whether all the elements in sm  were in l.  Works even if some elements in l are not in sm.  Not optimised at all lGet the Copilot variables. mAn empty streamableMaps. n-Verifies if its argument is equal to emptySM oDReplace all accepted special characters by sequences of underscores 123pD-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopDcba`_V^]\[ZYXWUTQRSPEFGHIJKLMNOCD6789:;<=>?@ABmndefghijkol5p-.32/041D-../00123456 789:;<=>?@AB789:;<=>?@ABCDDE FGHIJKLMNOFGHIJKLMNOPQRSSTUV^]\[ZYXWWXYZ[\]^_`abcdefghijklmnopqrstuAUsed for representing an error in the specification, detected by } vYIf an output depends of a future of an input it will be hard to compile to say the least w8Could be compiled, but would need bigger prophecyArrays xThe algorithm to compile Copilot specification can only work if there is no negative weighted closed path in the specification, as described in the original research paper yjeither a variable is not defined, or not with the good type ; there is no implicit conversion of types in Copilot zaif an external variable is sampled at phase 0 then there is no time for the stream to be updated {)A drop expression of less than 0 is used |the BNF is not respected 456}Check a Copilot specification. F If it is not compilable, then returns an error describing the issue.  Else, returns Nothing 78~qrstuvwxyz{|}~}u|{zyxwvqtsr~qtsrrstu|{zyxwvvwxyz{|}~"The main function of this module.  It takes a Copilot4 specification, the values of the monitored values, ( and returns the values of the streams. 9:;<=>?@ A Compiles an Copilot specification to an Atom one. UThe period is given as a Maybe : if it is Nothing, an optimal period will be chosen. BCDEFGHIJ KLMNOPQRSTUVWXYZ[\]_IBeware : crash without any possible recovery if a division by 0 happens. 2 Same risk with mod. Use div0 and mod0 if unsure. `As mod and div, except that if the division would be by 0, it is instead by the first argument. OBeware : both sides are executed, even if the result of one is later discarded ^_`abcdefghijklmnopqrst@opsF, opsF2 and opsF3 are feeded to Tests.Random.randomStreams. H They allows the random generated streams to include lots of operators. S If you add a new operator to Copilot, it would be nice to add it to one of those, C that way it could be used in the random streams used for testing. O opsF holds all the operators of arity 1, opsF2 of arity 2 and opsF3 of arity3 S They are StreamableMaps, because operators are sorted based on their return type. Stream variable reference A constant stream Drop i elements from a stream.  Just a trivial wrapper over the X constructor Define a stream variable. Allows to build a Q from specification U U  H Did s hold in the previous period? Has s always held? Did s> hold at some time in the past (including the current state)? Once s2. holds, in the following state (period), does s1 continuously hold?  Name of the C file to generate  Options to pass to the compiler The optional period Interpret the program or not Where to put the executable Which compiler to use 4Code to replace the default initialization and main A list of Copilot variable C  function name pairs. The C  funciton is called if the  Copilot stream becomes True.  The Stream must be of Booleans  and the C function must be of  type void  foo(void). This function is the core of Copilot : L it glues together analyser, interpreter and compiler, and does all the IO. X It can be called either from interface (which justs decodes the command-line argument) 2 or directly from the interactive prompt in ghci.  streams is a specification,   inputExts/ allows the user to give at runtime values for c the monitored variables. Useful for testing on randomly generated values and specifications, & or for the interpreted version.  be0 chooses between compilation or interpretation, S and if compilation is chosen (AtomToC) holds a few additionnal informations.  see description of    iterationsF just gives the number of periods the specification must be executed. h If you would rather execute it by hand, then just choose AtomToC for backEnd and 0 for iterations  verbose determines what is output. uvwxyz '{|If there',s no Streams, then generate random streams. }For distributed monitors. ~%Assign values to external variables. Set gcc options. RSet the period. If none is given, then the smallest feasible period is computed. Interpreting? +How many iterations are we simulating for? 8Verbosity level: OnlyErrors | DefaultVerbose | Verbose. *Random seed for generating Copilot specs. Name of the C file generated. 4The C compiler to use, as a path to the executable. 8Where to place the output C files (.c, .h, and binary). +Code to append above and below the C file. A list of Copilot variable C  function name pairs. The C  funciton is called if the  Copilot stream becomes True.  The Stream must be of Booleans  and the C function must be of  type void  foo(void) . There  should be no more than one  function per trigger variable. % Triggers fire in the same phase (1)  that output vars are assigned. iSets the environment for simulation by giving a mapping of external variables to lists of values. E.g.,  $ setE (emptySM {w32Map = fromList [("ext", [0,1..])]}) ...!sets the external variable names ext9 to take the natural numbers, up to the limit of Word32. )Sets the options for the compiler, e.g.,   setC "-O2" ...Sets gcc options. sManually set the period for the program. Otherwise, the minimum required period is computed automatically. E.g.,  setP 100 ...  < sets the period to be 100. The period must be at least 1. <Sets the number of iterations of the program to simulation:  setN 50  ' simulations the program for 50 steps. Set the verbosity level. JSets the compiler to use, given as a path to the executable. The default  is "gcc". HSets the directory into which the output of compiled programs should be ? placed. If the directory does not exist, it will be created. >Sets the code to precede and follow the copilot specification W If nothing, then code appropriate for communication with the interpreter is generated KGive C function triggers for Copilot Boolean streams. The tiggers fire if  the stream becoms true. The main function +Returns the smallest m <= n such that drop m s is true, and -1 if no  such m exists. Returns the smallest m <= n such that drop m s is false, and -1 if no  such m exists. Returns the largest m <= n such that drop m s is true, and -1 if no  such m exists. Returns the largest m <= n such that drop m s is false, and -1 if no  such m exists.  Property s holds for the next n periods. If n == 0, then s holds $ in the current period. We require n >= 0.  E.g., if p = always 2 sI, then we have the following relationship between the streams generated:    s => T T T T F F F F ...  p => T T F F F F F F ...    Property s holds at the next period.  Property s" holds at some period in the next n periods. If n == 0,  then s* holds in the current period. We require n >= 0.  E.g., if p = eventually 2 sI, then we have the following relationship between the streams generated:    s => F F F F T F T F ...  p => F F T T T T T T ...     until n s0 s1 means that eventually n s1, and up until at least the  period before s1 holds, s0 continuously holds.  release n s0 s1 means that either  always n s1, or s1 holds up to and  including the period at which s0 becomes true.         Summation.  Maximum value.  Minimum value.  Mean value. n must not overflow  for word size a1 for streams over which computation is peformed.                !"#$%&'()* !"#$%&'()* !"#$%&'()* !"#$%&'()*+,+,+,+,,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~   !" !# !$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnoopqrstuvwxyz{|}~y                                        !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUV J W X Y Z [ \ ] ^ _ ` a a b c d e f g h i j k l m n o p qrstuvwxyz{|}~                         copilot-0.22Language.Copilot.LanguageLanguage.Copilot.VariablesLanguage.Copilot.AdHocCLanguage.Copilot.HelpLanguage.Copilot.CoreLanguage.Copilot.AnalyserLanguage.Copilot.InterpreterLanguage.Copilot.AtomToCLanguage.Copilot.CompilerLanguage.Copilot.Tests.RandomLanguage.Copilot.Libs.PTLTLLanguage.Copilot.DispatchLanguage.Copilot.InterfaceLanguage.Copilot.Libs.ErrorChksLanguage.Copilot.Libs.IndexesLanguage.Copilot.Libs.LTL Language.Copilot.Libs.Statistics"Language.Copilot.Examples.Examples'Language.Copilot.Examples.PTLTLExamples&Language.Copilot.Examples.StatExamplesLanguage.Copilot.PrettyPrinter%Language.Copilot.Examples.LTLExamplesLanguage.CopilotbaseGHC.Num fromInteger-negateGHC.Real FractionalNumghc-primGHC.BoolBoolFalseTrue/signumabs*+abcdefghijklmnopqrstuvwxyzvarDeclincludeBracket includeQuote printfNewlineprintfhelpStr BoundedArrayB PhasedValuePhIndexes TmpSamplesOutputs ProphArrsVarsStreamableMapsSMbMapi8Mapi16Mapi32Mapi64Mapw8Mapw16Mapw32Mapw64MapfMapdMapSendablesend Streamable getSubMap updateSubMapunitatomConstructorexternalAtomConstructortypeId typeIdPrecatomTypeshowAsC makeTriggerDistributedStreamsSendsSendStreamStreamsSpecDropAppendF3F2FConstVarPVarPortPhasePeriodName getMaybeElemgetElemstreamToUnitValuefoldStreamableMapsfoldSendableMapsmapStreamableMapsmapStreamableMapsMfilterStreamableMapsgetVarsemptySM isEmptySM normalizeVarnextStSpecSet DropSpecSet FunSpecSet AllSpecSetErrorDependsOnFutureDependsOnClosePastNonNegativeWeightedClosedPathBadTypeBadSamplingPhaseBadDrop BadSyntaxcheck getAtomTypegetExternalVarsinterpretStreamsgetPrePostCode copilotToAtom OperatorsOperatorfromOp randomStreams CastIntTocastnotmoddivmod0div0<<=>=>==/=||&&^==>muxboolint8int16int32int64word8word16word32word64floatdoubleextBextI8extI16extI32extI64extW8extW16extW32extW64extFextDopsFopsF2opsF3varvarBvarI8varI16varI32varI64varW8varW16varW32varW64varFvarDsendW8constconstBconstI8constI16constI32constI64constW8constW16constW32constW64constFconstDdrop++.=..|previous alwaysBeeneventuallyPrevsinceVerboseDefaultVerbose OnlyErrors Iterations InterpretedNotInterpretedBackEnd InterpreterOptsAtomToCcNamegccOpts getPeriod interpreted outputDircompiler prePostCodetriggersdispatchOptionsbaseOptstest interpretcompileverifysetSsetEsetCsetPsetIsetNsetVsetRsetOsetGCCsetDirsetPP setTriggers interfacehelpnPosChknOneChkint16Chksoonest soonestFaillatest latestFailalwaysnext eventuallyuntilreleasesummaxminmeanfibt1t2t3t4t5yyzzxxenginedistgcdgcd' testCoercionstestCoercionsInt testRulesi8trap tstdatprvtprvtstdatABtABtstdatEPtEP tstdat1Sin tstdat2SintSintSinExtt0tMean printfPre printfPostnewlineArrIndex showIndentedshowRawgetValueWeight&&>||> syntaxCheckdefCheckextDeclspreCodevPrepostCode inputExtVars sampleExtVars outputVars initProphArr initOutputinitTmpSamplesmakeUpdateIndexmakeOutputIndexmakeRulemakeSend sampleVarsgetOptimalPeriod VariablesVNamemaxDropmaxSamplePhaseweightsContinueVarweightsContinuePVarweightsVarTypesweightsPVarTypesweightsAllSpecSetweightsFunSpecSetweightsDropSpecSetfoldRandomableMapsrandomWeightedaddRandomVNames addRandomSpec randomSpecaddRandomExternalrandomExternalValuesmkOpmkOp2mkOp3 mkOp2CoercemkOp2OrdmkOp2Eqnot_+$-$*$/$<$<=$>=$>$==$/=$||$&&$^$==>$mux_createMapFromElemscheckTriggerVars copilotToCgccCallexecuteshowVars preludeText optStreamsoptSendsoptExts optCompile optPeriod optInterpret optIterations optVerbose optRandomSeedoptCName optCompiler optOutputDiroptPrePostCode optTriggers createSeedgetStreamsVars getBackendchk soonestHlp latestHlp foldDropsoutputtSoonesttLatesttAlwaystFuturetUntil tRelease0 tRelease1