copilot-libraries-4.8: Libraries for the Copilot language.

Safe Haskell | Safe-Inferred
Language | Haskell2010

Copilot.Library.MTL

Description

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

Synopsis

- eventually :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
- eventuallyPrev :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
- always :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
- alwaysBeen :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
- until :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
- release :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
- since :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
- trigger :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
- matchingUntil :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
- matchingRelease :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
- matchingSince :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
- matchingTrigger :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool

# Documentation

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

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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