| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Cooked.Ltl.Combinators
Description
This module provides helpers for writing common LTL expressions.
Documentation
anyOf :: [a] -> Ltl a Source #
Same as anyOf', but first wraps the elements in the input list in atomic
formulas.
allOf :: [a] -> Ltl a Source #
Same as allOf', but first wraps the elements in the input list in atomic
formulas.
anyOf' :: [Ltl a] -> Ltl a Source #
Produces an Ltl formula which consists of the disjunction of all the formulas in the input list.
allOf' :: [Ltl a] -> Ltl a Source #
Produces an Ltl formula which consists of the conjunction of all the formulas in the input list.
delay :: Integer -> a -> Ltl a Source #
Same as delay', but first wraps the elements in the input list in atomic
formulas.
delay' :: Integer -> Ltl a -> Ltl a Source #
Produces an Ltl formula which consists of the delay of the input formula by
n time steps, if n > 0. Otherwise, leaves the formula unchanged.
eventually :: a -> Ltl a Source #
Same as eventually', but first wraps the elements in the input list in
atomic formulas.
eventually' :: Ltl a -> Ltl a Source #
Produces an Ltl formula which consists the input formula eventually holds
Same as always', but first wraps the elements in the input list in
atomic formulas.