| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Cooked.Ltl
Description
This modules provides the infrastructure to modify sequences of transactions using LTL formulaes with atomic modifications. This idea is to describe when to apply certain modifications within a trace.
Synopsis
- data Ltl a
- ltlNot' :: a -> Ltl a
- ltlOr' :: a -> a -> Ltl a
- ltlAnd' :: a -> a -> Ltl a
- ltlNext' :: a -> Ltl a
- ltlAny :: [Ltl a] -> Ltl a
- ltlAny' :: [a] -> Ltl a
- ltlAll :: [Ltl a] -> Ltl a
- ltlAll' :: [a] -> Ltl a
- ltlDelay :: Integer -> Ltl a -> Ltl a
- ltlDelay' :: Integer -> a -> Ltl a
- ltlEventually :: Ltl a -> Ltl a
- ltlEventually' :: a -> Ltl a
- ltlAlways :: Ltl a -> Ltl a
- ltlAlways' :: a -> Ltl a
- ltlWhenPossible :: Ltl a -> Ltl a
- ltlWhenPossible' :: a -> Ltl a
- ltlIfPossible :: Ltl a -> Ltl a
- ltlIfPossible' :: a -> Ltl a
- ltlImplies :: Ltl a -> Ltl a -> Ltl a
- ltlImplies' :: a -> a -> Ltl a
- ltlNever :: Ltl a -> Ltl a
- ltlNever' :: a -> Ltl a
- data Requirement a
- = Apply a
- | EnsureFailure a
- data LtlOp modification builtin :: Type -> Type where
- type StagedLtl modification builtin = Staged (LtlOp modification builtin)
- singletonBuiltin :: builtin a -> StagedLtl modification builtin a
- class Monad m => MonadLtl modification m where
- class ModInterpBuiltin modification builtin m where
- modifyAndInterpBuiltin :: builtin a -> Either (m a) ([Requirement modification] -> m a)
- interpStagedLtl :: forall modification builtin m. (MonadPlus m, ModInterpBuiltin modification builtin m) => forall a. StagedLtl modification builtin a -> m a
LTL formulas
Type of LTL formulas with atomic formulas of type a. Think of a as a
type of "modifications", then a value of type Ltl a describes where to
apply Requirements in a trace.
Constructors
| LtlTruth | The modification that always applies but does nothing. |
| LtlFalsity | The modification that never applies (i.e. always fails). |
| LtlAtom a | The atomic modification, applying at the current time step. |
| LtlNot (Ltl a) | Assert that the given formula must not hold at the current time step i.e. that the appropriate modifications fail. |
| LtlOr (Ltl a) (Ltl a) | Disjunction will be interpreted in an "intuitionistic" way, i.e. as branching into the "timeline" where the left disjunct holds and the one where the right disjunct holds. In that sense, it is an exclusive or, as it does not introduce the branch where both disjuncts hold. |
| LtlAnd (Ltl a) (Ltl a) | Conjunction will be interpreted as "apply both modifications". Attention: The "apply both" operation will be user-defined for atomic modifications, so that conjunction may for example fail to be commutative if the operation on atomic modification is not commutative. In particular, this is the case for tweaks, where the second modification will be applied first, to be consistent with nested modifications. |
| LtlNext (Ltl a) | Assert that the given formula holds at the next time step. |
| LtlUntil (Ltl a) (Ltl a) | Assert that the first formula holds at least until the second one begins to hold, which must happen ltlEventually. The following holds: a `LtlUntil` b <=> b `LtlOr` (a `LtlAnd` LtlNext (a `LtlUntil` b))
|
| LtlRelease (Ltl a) (Ltl a) | Assert that the second formula has to hold up to and including the
point when the first begins to hold; if that ltlNever happens, the second
formula has to remain true forever. View this as dual to a `LtlRelease` b <=> b `LtlAnd` (a `LtlOr` LtlNext (a `LtlRelease` b))
|
LTL combinators
ltlAny :: [Ltl a] -> Ltl a Source #
Produces an Ltl formula which consists of the disjunction of all the formulas in the input list.
ltlAny' :: [a] -> Ltl a Source #
Same as ltlAny, but first wraps the elements in the input list in atomic
formulas.
ltlAll :: [Ltl a] -> Ltl a Source #
Produces an Ltl formula which consists of the conjunction of all the formulas in the input list.
ltlAll' :: [a] -> Ltl a Source #
Same as ltlAll, but first wraps the elements in the input list in atomic
formulas.
ltlDelay :: 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.
ltlDelay' :: Integer -> a -> Ltl a Source #
Same as ltlDelay, but first wraps the input in an atomic formula.
ltlEventually :: Ltl a -> Ltl a Source #
Produces an Ltl formula which ensures the input formula eventually holds.
ltlEventually' :: a -> Ltl a Source #
Same as ltlEventually, but first wraps the input in an atomic formula.
ltlAlways :: Ltl a -> Ltl a Source #
Produces an Ltl formula which ensures the input formula always holds.
ltlAlways' :: a -> Ltl a Source #
Same as ltlAlways, but first wraps the input in an atomic formula.
ltlWhenPossible :: Ltl a -> Ltl a Source #
Produces an Ltl formula which applies a formula whenever possible, while ignoring steps when it is not.
ltlWhenPossible' :: a -> Ltl a Source #
Same as ltlWhenPossible, but first wraps the input in an atomic formula.
ltlIfPossible :: Ltl a -> Ltl a Source #
Produces an Ltl formula which either ensure the given formula does not hold, or apply its modifications.
ltlIfPossible' :: a -> Ltl a Source #
Same as ltlIfPossible, but first wraps the input in an atomic formula.
ltlImplies :: Ltl a -> Ltl a -> Ltl a Source #
Produces a formula that succeeds if the first formula does not hold, or if both formulas hold.
ltlImplies' :: a -> a -> Ltl a Source #
Same as ltlImplies but first wraps the inputs in atomic formulas.
Using LTL formulas to modify computations
data Requirement a Source #
Requirements implied by a given Ltl formula at a given time step
Constructors
| Apply a | Apply this modification now |
| EnsureFailure a | Ensure this modification fails now |
data LtlOp modification builtin :: Type -> Type where Source #
Operations that either allow to use a builtin, or to modify a computation
using an Ltl formula.
Constructors
| WrapLtl :: Ltl modification -> StagedLtl modification builtin a -> LtlOp modification builtin a | |
| Builtin :: builtin a -> LtlOp modification builtin a |
Instances
type StagedLtl modification builtin = Staged (LtlOp modification builtin) Source #
An AST of builtins wrapped into an Ltl setting
singletonBuiltin :: builtin a -> StagedLtl modification builtin a Source #
Builds a singleton instruction in a StagedLtl monad
class Monad m => MonadLtl modification m where Source #
Depicts the ability to modify a computation with an Ltl formula
class ModInterpBuiltin modification builtin m where Source #
Depicts the ability to modify and interpret builtins in a given domain. Each builtin can either:
- be interpreted directly through
Left, in which case it will not be considered as a timestep in a trace. - be modified and only then interpreted through
Right, in which case it will be considered as a timestep in a trace.
Methods
modifyAndInterpBuiltin :: builtin a -> Either (m a) ([Requirement modification] -> m a) Source #
Instances
| ModInterpBuiltin MockChainTweak MockChainBuiltin InterpMockChain Source # | |
Defined in Cooked.MockChain.Staged Methods modifyAndInterpBuiltin :: forall (a :: k). MockChainBuiltin a -> Either (InterpMockChain a) ([Requirement MockChainTweak] -> InterpMockChain a) Source # | |
Arguments
| :: forall modification builtin m. (MonadPlus m, ModInterpBuiltin modification builtin m) | |
| => forall a. StagedLtl modification builtin a | A staged computation |
| -> m a | Interpretation of the computation |
Interprets a StagedLtl computation based on an interpretation of
builtin with respect to possible modifications. This unfolds as follows:
- When a builtin is met, which is directly interpreted, we return the
associated computation, with no changes to the
Ltlstate. - When a builtin is met, which requires a modification, we return the modified interpretation, and consume the current modification requirements.
- When a wrapped computation is met, we store the new associated formula, and ensure that when the computation ends, the formula is finished.