#̾B      !"#$%&'()*+,-./0123456789:;<=>?@ A 'Clocks based on a base period and phase7(c) 2011 National Institute of Aerospace / Galois, Inc.Safecopilot-librariesConstructor for a B*. Note that period must be greater than 0.copilot-librariesConstructor for a CX. Note that phase must be greater than or equal to 0, and must be less than the period.copilot-libraries#Generate a clock that counts every n ticks, starting at tick m, by using an array of size n.copilot-libraries$This follows the same convention as 0, but uses a counter variable of integral type a rather than an array.copilot-librariesPeriod n of clockcopilot-librariesPhase m of clockcopilot-librariesClock signal - D on clock ticks, E otherwisecopilot-librariesPeriod n of clockcopilot-librariesPhase m of clockcopilot-librariesClock signal - D on clock ticks, E otherwisePast-Time Linear-Temporal Logic7(c) 2011 National Institute of Aerospace / Galois, Inc.Safecopilot-librariesDid s hold in the previous period?copilot-librariesHas s5 always held (up to and including the current state)?copilot-librariesDid s= hold at some time in the past (including the current state)?copilot-librariesOnce s2. holds, in the following state (period), does s1 continuously hold?Regular expression library7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe>AFcopilot-libraries!The regular expression data type.For our use, regular expressions describing a language with no words are not supported since empty languages would not match anything and just yield a Copilot stream of constant false values.Gcopilot-librariesA symbol's value can occur multiple times in a regular expression, e.g. "t(tfft)*". A running number "symbolNum" is used to make all symbols in a regular expression unique.Hcopilot-libraries$The symbols in a regular expression.I is any value of type tF (matches any symbol, the "point" character in a regular expression).Jcopilot-librariesParsers for single characters.Kcopilot-librariesParsers for single characters.Lcopilot-librariesParsers for single characters.Mcopilot-librariesParsers for single characters.Ncopilot-librariesParsers for single characters.Ocopilot-librariesParsers for single characters.Pcopilot-librariesParsers for single characters.Qcopilot-librariesParsers for single characters.Rcopilot-librariesParsers for single characters.Scopilot-librariesParsers for single characters.Tcopilot-librariesVA "followedBy" combinator for parsing, parses p, then p' and returns the result of p.Ucopilot-libraries;Parsing a string p' with prefix p, returning both in order.Vcopilot-librariesParsing a string p' with the character pD as an optional prefix, return the result with the optional prefix.;Parsing a string p' with prefix p, returning both in order.Wcopilot-libraries"case insensitive". Take one argument of type string, parses for the string in a case insensitive manner and yields the parsed string (preserving its case).Xcopilot-librariesParser for regular expressionsYcopilot-libraries:Parses the "." - point character used to match any symbol.copilot-libraries4Regular expression matching over an arbitrary stream copilot-librariesARegular expression matching over a collection of boolean streams.WRegular expressions can contain symbols, which are expanded to match specific streams.$For example, the regular expression: "<s0>(<s1>)+" Qwould match if you provide a map (association list) that assigns, to the symbol "s0"4, a stream that is true at the first sample, and to "s1"@, a stream that is true at every sample after the first sample.copilot-librariesThe stream to monitor.copilot-librariesThe regular expression.copilot-libraries1A stream indicating when to reset the monitor. copilot-librariesRegular expressioncopilot-libraries4A table with the stream associated to each symbol.copilot-libraries0A stream indicating when to reset the monitor.  Stream for a stack machine7(c) 2011 National Institute of Aerospace / Galois, Inc.SafeMAcopilot-librariespStack stream in which the pop signal has precedence over the push signal in case both are true in the same tickcopilot-librariespStack stream in which the push signal has precedence over the pop signal in case both are true in the same tickcopilot-librariesDepthcopilot-libraries Start valuecopilot-libraries Pop signalcopilot-libraries Push signalcopilot-libraries Push streamcopilot-libraries Stack topcopilot-librariesDepthcopilot-libraries Start valuecopilot-libraries Pop signalcopilot-libraries Push signalcopilot-libraries Push streamcopilot-libraries Stack top9Utility bounded-list functions (e.g., folds, scans, etc.)7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe~ copilot-librariesGiven a stream, produce an infinite list of streams dropping an increasing number of elements of the given stream. For example, for a given stream s, the expression tails s is equal to $[ drop 0 s, drop 1 s, drop 2 s, ...].copilot-librariesGiven a stream and a number, produce a finite list of streams dropping an increasing number of elements of the given stream, up to that number. For example, for a given stream s, the expression take 2 s is equal to [ drop 0 s, drop 1 s].copilot-librariesGiven a number, a function on streams, and two streams, fold from the left the function over the finite list of tails of the second stream (up to the given number). copilot-librariesGiven a number, a function on streams, and two streams, fold from the left the function over the finite list of tails of the second stream (up to the given number).This function differs from X in that it does not require an initial accumulator and it assumes the argument number n is positive.!copilot-librariesGiven a number, a function on streams, and two streams, fold from the right the function over the finite list of tails of the second stream (up to the given number)."copilot-librariesGiven a number, a function on streams, and two streams, fold from the right the function over the finite list of tails of the second stream (up to the given number).This function differs from !X in that it does not require an initial accumulator and it assumes the argument number n is positive.#copilot-librariesGiven a number, a function on streams, and two streams, fold from the left the function over the finite list of tails of the second stream (up to the given number).This function differs from 6 in that it returns the intermediate results as well.$copilot-librariesGiven a number, a function on streams, and two streams, fold from the right the function over the finite list of tails of the second stream (up to the given number).This function differs from !6 in that it returns the intermediate results as well.%copilot-librariesGiven a number, a function on streams, and two streams, fold from the left the function over the finite list of tails of the second stream (up to the given number).pThis function assumes the number of elements to scan is positive, and it also returns the intermediate results.&copilot-librariesGiven a number, a function on streams, and two streams, fold from the right the function over the finite list of tails of the second stream (up to the given number).pThis function assumes the number of elements to scan is positive, and it also returns the intermediate results.'copilot-librariesCase-like function: The index of the first predicate that is true in the predicate list selects the stream result. If no predicate is true, the last element is chosen (default element)(copilot-librariesIndex.GWARNING: Very expensive! Consider using this only for very short lists.)copilot-libraries(Cycle a list to form an infinite stream.  !"#$%&'() ) !"#$%&'(Basic bounded statistics7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe*copilot-libraries Summation.+copilot-librariesMaximum value.,copilot-librariesMinimum value.-copilot-libraries Mean value. n" must not overflow for word size a0 for streams over which computation is peformed..copilot-libraries5Mean value over the current set of streams passed in.*+,-.+,*-.8Metric Temporal Logic (MTL) over a discrete time domain.Safec /copilot-libraries@Eventually true in the future, within the time bounds specified.eventually l u clk dist s is true at time t if and only if s is true at some time t', where (t + l) <= t' <= (t + u).0copilot-libraries@True at some point in the past within the time bounds specified.eventuallyPrev l u clk dist s is true at time t if and only if s is true at some time t', where (t - u) <= t' <= (t - l).1copilot-libraries<Always true in the future, within the time bounds specified.always l u clk dist s is true at time t iff s is true at all times t' where (t + l) <= t' <= (t + u).2copilot-libraries:Always true in the past, within the time bounds specified.alwaysBeen l u clk dist s is true at time t iff s is true at all times t' where (t - u) <= t' <= (t - l).3copilot-librariesDTrue until another stream is true, within the time bounds specified.until l u clk dist s0 s1 is true at time t iff there exists a d, with  l <= d <= u , such that s1 is true at time (t + d), and for all times t' with t <= t' < t + d, s0 is true at those times.4copilot-librariesHTrue since another stream became true, within the time bounds specified.since l u clk dist s0 s1 is true at time t iff there exists a d, with  l <= d <= u , such that s1 is true at time (t - d), and for all times t' with t - d < t' <= t, s0 is true at those times.5copilot-libraries7True if a stream is true until another one releases it.release l u clk dist s0 s1 is true at time t iff for all d with  l <= d <= u! where there is a sample at time (t + d), s1 is true at time (t + d), or s0 has a true sample at some time t' with t <= t' < t + d.6copilot-libraries7True if a stream is true until another one releases it.Trigger: True at time t iff for all d with  l <= d <= u" where there is a sample at time (t - d), s1 is true at time (t - d), or s0! has a true sample at some time t' with t - d < t' <= t.7copilot-libraries"Matching Until: Same semantics as until, except with both s1 and s0 needing to hold at time (t + d) instead of just s1.8copilot-libraries"Matching Since: Same semantics as since, except with both s1 and s0 needing to hold at time (t - d) instead of just s1.9copilot-libraries$Matching Release: Same semantics as release, except with s1 or s0 needing to hold at time (t + d) instead of just s1.:copilot-libraries$Matching Trigger: Same semantics as trigger, except with s1 or s0 needing to hold at time (t - d) instead of just s1. /0123456789: /0123546798:-Bounded Linear Temporal Logic (LTL) operators7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe”;copilot-libraries Property s( holds at the next period. For example: T 0 1 2 3 4 5 6 7 s => F F F T F F T F ... next s => F F T F F T F ... (Note: s must have sufficient history to Z a value from it.<copilot-libraries Property s holds for the next n periods. We require n >= 0. If n == 0, then s' holds in the current period, e.g., if p = always 2 sI, then we have the following relationship between the streams generated: C 0 1 2 3 4 5 6 7 s => T T T F T T T T ... p => T F F F T T ... =copilot-libraries 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: 2s => F F F T F F F T ... p => F T T T F T T T ... >copilot-libraries until n s0 s1 means that eventually n s1+, and up until at least the period before s1 holds, s0 continuously holds.?copilot-librariesrelease n s0 s1 means that either  always n s1, or s10 holds up to and including the period at which s0 becomes true.=copilot-librariesncopilot-librariess;<=>?;=<>? 9Implementation of the Boyer-Moore Majority Vote Algorithm7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe+ʁ@copilot-libraries/Majority vote first pass: choosing a candidate.Acopilot-librariesZMajority vote second pass: checking that a candidate indeed has more than half the votes.@copilot-libraries Vote streamscopilot-librariesCandidate streamAcopilot-libraries Vote streamscopilot-librariesCandidate streamcopilot-libraries True if candidate holds majority@A@A  Main import module for libraries7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe&%  !"#$%&'()*+,-.;<=>?@A[    !"#$%&'()*+,-./0123456789:;<=>?@ABC;:<= D EFGHIJHIKLMNOPQRSTUVWXYZ[\]^_`abccopilot-libraries-3.2.1-inplaceCopilot.Library.ClocksCopilot.Library.PTLTLCopilot.Library.RegExpCopilot.Library.StacksCopilot.Library.UtilsCopilot.Library.StatisticsCopilot.Library.MTLCopilot.Library.LTLCopilot.Library.VotingCopilot.Library.Librariesperiodphaseclkclk1previous alwaysBeeneventuallyPrevsince copilotRegexpcopilotRegexpB$fSymbolParserInt64$fSymbolParserInt32$fSymbolParserInt16$fSymbolParserInt8$fSymbolParserWord64$fSymbolParserWord32$fSymbolParserWord16$fSymbolParserWord8$fSymbolParserBool$fSymbolParserP$fEqSym$fOrdSym $fShowSym $fEqNumSym $fShowNumSym $fShowRegExp$fEqPstackstack'tailstakenfoldlnfoldl1nfoldrnfoldr1nscanlnscanrnscanl1nscanr1case'!!cyclesummaxminmeanmeanNow eventuallyalwaysuntilreleasetrigger matchingUntil matchingSincematchingReleasematchingTriggernextmajority aMajorityPeriodPhaseghc-prim GHC.TypesTrueFalseRegExpNumSymSymAnylquoterquotelparenrparenstarplusqmarkpointminusnondigit followedBycPrefix optCPrefixciregexpanySymcopilot-language-3.2.1-inplace#Copilot.Language.Operators.Temporaldrop