úÎ!TDPZB      !"#$%&'()*+,-./0123456789:;<=>?@ A 'Clocks based on a base period and phase7(c) 2011 National Institute of Aerospace / Galois, Inc.SafeÌcopilot-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.Safexcopilot-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>  Stream for a stack machine7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe$pcopilot-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+A'copilot-librariesºCase-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-librariesQIndex. WARNING: Very expensive! Consider using this only for very short lists.  !"#$%&'() ) !"#$%&'(Basic bounded statistics7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe1¢*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.*+,-.+,*-.Safe2 /0123456789: /0123546798:-Bounded Linear Temporal Logic (LTL) operators7(c) 2011 National Institute of Aerospace / Galois, Inc.SafeF0;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 F 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+N@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.SafeOÂ%  !"#$%&'()*+,-.;<=>?@AG    !"#$%&'()*+,-./0123456789:;<=>?@ABC;:<= D EFGHIJHIKLMNO,copilot-libraries-3.0-JTxvSzo6iduHhnXGIOycflCopilot.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.TypesTrueFalse*copilot-language-3.0-AZG3s2OMrpkTKr0nRgNwY#Copilot.Language.Operators.Temporaldrop