LTL

This module provides a simple way of applying LTL formulas to lists, or streams of input, to determine if a given formula matches some or all of that input.

Formulas are written exactly as you would in LTL, but using names instead of the typical symbols, for example:

always (is even `until` is odd)

Use run to apply a formula to a list of inputs, returning either Left if it needs more input to determine the truth of the formula, or Right if it could determine truth from some prefix of that input.

Use step to advance a formula by a single input. The return value has the same meaning as run, but allows you to apply it in cases whether you don't necessarily have all the inputs at once, such as feeding input gradually within a conduit to check for logic failures.

For the meaning of almost all the functions in the module, see https://en.wikipedia.org/wiki/Linear_temporal_logic

Documentation

type LTL a = Machine a (Result a)

newtype Machine a b

Constructors

Machine

Fields

• step :: a -> Either (Machine a b) b

Instances

Functor (Machine a)

Defined in LTL

Methods

fmap :: (a0 -> b) -> Machine a a0 -> Machine a b

(<$) :: a0 -> Machine a b -> Machine a a0

data Reason a

Constructors

HitBottom String

Rejected a

BothFailed (Reason a) (Reason a)

LeftFailed (Reason a)

RightFailed (Reason a)

Instances

Show a => Show (Reason a)

Defined in LTL

Methods

showsPrec :: Int -> Reason a -> ShowS

show :: Reason a -> String

showList :: [Reason a] -> ShowS

Generic (Reason a)

Defined in LTL

Associated Types

type Rep (Reason a) :: Type -> Type

Methods

from :: Reason a -> Rep (Reason a) x

to :: Rep (Reason a) x -> Reason a

NFData a => NFData (Reason a)

Defined in LTL

Methods

rnf :: Reason a -> ()

type Rep (Reason a)

Defined in LTL

type Rep (Reason a) = D1 (MetaData "Reason" "LTL" "simple-ltl-2.0.0-CClEARD0nN73zoUIcmDo22" False) ((C1 (MetaCons "HitBottom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: C1 (MetaCons "Rejected" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))) :+: (C1 (MetaCons "BothFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))) :+: (C1 (MetaCons "LeftFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))) :+: C1 (MetaCons "RightFailed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))))))

data Result a

Constructors

Failure (Reason a)

Success

Instances

Show a => Show (Result a)

Defined in LTL

Methods

showsPrec :: Int -> Result a -> ShowS

show :: Result a -> String

showList :: [Result a] -> ShowS

Generic (Result a)

Defined in LTL

Associated Types

type Rep (Result a) :: Type -> Type

Methods

from :: Result a -> Rep (Result a) x

to :: Rep (Result a) x -> Result a

NFData a => NFData (Result a)

Defined in LTL

Methods

rnf :: Result a -> ()

type Rep (Result a)

Defined in LTL

type Rep (Result a) = D1 (MetaData "Result" "LTL" "simple-ltl-2.0.0-CClEARD0nN73zoUIcmDo22" False) (C1 (MetaCons "Failure" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))) :+: C1 (MetaCons "Success" PrefixI False) (U1 :: Type -> Type))

run :: Machine a b -> [a] -> Either (Machine a b) b

neg :: LTL a -> LTL a

Negate a formula: ¬ p

top :: LTL a

⊤, or "true"

bottom :: String -> LTL a

⊥, or "false"

accept :: (a -> LTL a) -> LTL a

Given an input element, provide a formula to determine its truth. These can be nested, making it possible to have conditional formulas.

reject :: (a -> LTL a) -> LTL a

The opposite in meaning to accept, defined simply as 'neg . accept'.

and :: LTL a -> LTL a -> LTL a

Boolean conjunction: ∧

or :: LTL a -> LTL a -> LTL a

Boolean disjunction: ∨

next :: LTL a -> LTL a

The "next" temporal modality, typically written 'X p' or '◯ p'.

until :: LTL a -> LTL a -> LTL a

The "until" temporal modality, typically written 'p U q'.

weakUntil :: LTL a -> LTL a -> LTL a

Weak until.

release :: LTL a -> LTL a -> LTL a

Release, the dual of until.

strongRelease :: LTL a -> LTL a -> LTL a

Strong release.

implies :: LTL a -> LTL a -> LTL a

Logical implication: p → q

eventually :: LTL a -> LTL a

Eventually the formula will hold, typically written F p or ◇ p.

always :: LTL a -> LTL a

Always the formula must hold, typically written G p or □ p.

truth :: Bool -> LTL a

True if the given Haskell boolean is true.

test :: (a -> Bool) -> LTL a

Another name for is.

is :: (a -> Bool) -> LTL a

True if the given predicate on the input is true.

eq :: Eq a => a -> LTL a

Check for equality with the input.

showResult :: Show a => Either (LTL a) (Result a) -> String

Render a step result as a string.