FRP.Yampa.LTLFuture

Linear Temporal Logics based on SFs.

This module contains a definition of LTL with Next on top of Signal Functions.

LTL predicates are parameterized over an input. A basic proposition is a Signal Function that produces a boolean function.

Documentation

data TPred a where

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

Constructors

Prop :: SF a Bool -> TPred a

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

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

Not :: TPred a -> TPred a

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

Always :: TPred a -> TPred a

Eventually :: TPred a -> TPred a

Next :: TPred a -> TPred a

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

evalT :: TPred a -> SignalSampleStream a -> Bool

Evaluates a temporal predicate at time t=0 with a concrete sample stream.

Returns True if the temporal proposition is currently true.