Copyright	(c) Ivan Perez 2017
License	BSD3
Maintainer	ivan.perez@keera.co.uk
Safe Haskell	Safe-Inferred
Language	Haskell2010

FRP.Dunai.LTLFuture

Description

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.

Synopsis

data TPred m a where
- 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 :: (Functor m, Applicative m, Monad m) => (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
evalT :: (Functor m, Applicative m, Monad m) => TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool

Documentation

data TPred m a where Source #

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

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

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

Returns True if the temporal proposition is currently true.