Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

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

## Synopsis

- type LTL a = Machine a (Result a)
- newtype Machine a b = Machine {}
- data Reason a
- = HitBottom String
- | Rejected a
- | BothFailed (Reason a) (Reason a)
- | LeftFailed (Reason a)
- | RightFailed (Reason a)

- type Result a = Maybe (Reason a)
- run :: Machine a b -> [a] -> Either (Machine a b) b
- neg :: LTL a -> LTL a
- top :: LTL a
- bottom :: String -> LTL a
- accept :: (a -> LTL a) -> LTL a
- reject :: (a -> LTL a) -> LTL a
- and :: LTL a -> LTL a -> LTL a
- or :: LTL a -> LTL a -> LTL a
- next :: LTL a -> LTL a
- until :: LTL a -> LTL a -> LTL a
- weakUntil :: LTL a -> LTL a -> LTL a
- release :: LTL a -> LTL a -> LTL a
- strongRelease :: LTL a -> LTL a -> LTL a
- implies :: LTL a -> LTL a -> LTL a
- eventually :: LTL a -> LTL a
- always :: LTL a -> LTL a
- truth :: Bool -> LTL a
- test :: (a -> Bool) -> LTL a
- is :: (a -> Bool) -> LTL a
- eq :: Eq a => a -> LTL a
- showResult :: Show a => Either (LTL a) (Result a) -> String

# Documentation

HitBottom String | |

Rejected a | |

BothFailed (Reason a) (Reason a) | |

LeftFailed (Reason a) | |

RightFailed (Reason a) |

## Instances

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

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

always (accept (n -> next (eq (succ n))))

One way to read this would be: "for every input n, always accept n if its next element is the successor".

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

The opposite in meaning to `accept`

, defined simply as 'neg . accept'.

eventually :: LTL a -> LTL a Source #

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