Copilot.Library.MTL

Metric Temporal Logic (MTL) over a discrete time domain consisting of sampled time values.

The operators in this module receive two additional arguments: a clock stream clk, indicating the current time, and a distance between samples dist. For the purposes of explaining the MTL aspects, we ignore those arguments. If you are using streams for which you can treat time as a discrete increasing number, you can safely assume that the clock is a counter (i.e., [0, 1, 2,...], which can be defined by the stream counter = [0] ++ counter) and the distance between samples is 1.

Documentation

eventually :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool

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).

eventuallyPrev :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool

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).

always :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool

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).

alwaysBeen :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool

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).

until :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

True 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.

release :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

True 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.

since :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

True 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.

trigger :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

True 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.

matchingUntil :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

Matching Until: Same semantics as until, except with both s1 and s0 needing to hold at time (t + d) instead of just s1.

matchingRelease :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

Matching Release: Same semantics as release, except with s1 or s0 needing to hold at time (t + d) instead of just s1.

matchingSince :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

Matching Since: Same semantics as since, except with both s1 and s0 needing to hold at time (t - d) instead of just s1.

matchingTrigger :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

Matching Trigger: Same semantics as trigger, except with s1 or s0 needing to hold at time (t - d) instead of just s1.