| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
LTL
Description
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
Constructors
| 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.