Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
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
.