FRP.Dunai.LTLFuture

Future-time linear temporal logic implemented on top of monadic stream functions.

This module can be used to define LTL-like predicates on Monadic Stream Functions, and to evaluate them. The main entry point is the function evalT, which takes a temporal predicate, and a stream of inputs, and evaluates the predicate against the stream. Evaluation takes place at time 0, although it is possible to express conditions on future samples.

Disclaimer: This is not necessarily the same as LTL.

Documentation

data TPred m a where

Type representing future-time linear temporal logic with until and next.

Constructors

Prop :: MSF m a Bool -> TPred m a

And :: TPred m a -> TPred m a -> TPred m a

Or :: TPred m a -> TPred m a -> TPred m a

Not :: TPred m a -> TPred m a

Implies :: TPred m a -> TPred m a -> TPred m a

Always :: TPred m a -> TPred m a

Eventually :: TPred m a -> TPred m a

Next :: TPred m a -> TPred m a

Until :: TPred m a -> TPred m a -> TPred m a

tPredMap

Arguments

:: (Functor m, Applicative m, Monad m)

=> (MSF m a Bool -> m (MSF m a Bool))

Transformation to apply

-> TPred m a

Temporal predicate

-> m (TPred m a)

Apply a transformation to the leaves of a temporal predicate (to the SFs).

evalT :: (Functor m, Applicative m, Monad m) => TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool

Evaluates a temporal predicate at time T=0 against a sample stream.

Returns True if the temporal proposition is currently true.