cooked-validators
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Ltl formulas

data Ltl a Source #

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))

LtlUntil could technically be defined as the above formula using Haskell's laziness, but is left as a constructor to have a counterpart for LtlRelease, which cannot.

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 LtlUntil. The following holds:

a `LtlRelease` b <=> b `LtlAnd` (a `LtlOr` LtlNext (a `LtlRelease` b))

LtlRelease needs it own constructor, as it is considered valid on an empty computation, which the above formula is not in most cases.

Instances

Instances details
Functor Ltl Source # 
Instance details

Defined in Cooked.Ltl

Methods

fmap :: (a -> b) -> Ltl a -> Ltl b #

(<$) :: a -> Ltl b -> Ltl a #

RunnableMockChain FullEffs Source # 
Instance details

Defined in Cooked.MockChain.Instances

Methods

runMockChain :: MockChainState -> Sem FullEffs a -> [RawMockChainReturn a] Source #

Show a => Show (Ltl a) Source # 
Instance details

Defined in Cooked.Ltl

Methods

showsPrec :: Int -> Ltl a -> ShowS #

show :: Ltl a -> String #

showList :: [Ltl a] -> ShowS #

Eq a => Eq (Ltl a) Source # 
Instance details

Defined in Cooked.Ltl

Methods

(==) :: Ltl a -> Ltl a -> Bool #

(/=) :: Ltl a -> Ltl a -> Bool #

Ltl combinators

ltlNot' :: a -> Ltl a Source #

Same as LtlNot, but first wraps the input in an atomic formula.

ltlOr' :: a -> a -> Ltl a Source #

Same as LtlOr, but first wraps the inputs in atomic formulas.

ltlAnd' :: a -> a -> Ltl a Source #

Same as LtlAnd, but first wraps the inputs in atomic formulas.

ltlNext' :: a -> Ltl a Source #

Same as LtlNext, but first wraps the input in an atomic formula.

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.

ltlNever :: Ltl a -> Ltl a Source #

Produces an Ltl formula ensuring the given formula always fails.

ltlNever' :: a -> Ltl a Source #

Same as ltlNever, but first wraps the input in an atomic formula.

Ltl helpers,

nowLaterList :: [Ltl a] -> [([Requirement a], [Ltl a])] Source #

For each Ltl formula that describes a modification of a computation in a list, split it into a list of (doNow, doLater) pairs, and then appropriately combine the results. The result of the splitting is bound to the following semantics:

  • doNow is the list of modifications to be consecutively either applied to the current time step (Apply), or that should fail at the current time step (EnsureFailure)
  • doLater is an Ltl formula describing the modification that should be applied from the next time step onwards.

The return value is a list because a formula might be satisfied in different ways. For example, the modification described by a LtlUntil b might be accomplished by applying the modification b right now, or by applying a right now and a LtlUntil b from the next step onwards; the returned list will contain these two options.

finished :: Ltl a -> Bool Source #

If there are no more steps and the next step should satisfy the given formula: Are we finished, i.e. was the initial formula satisfied by now?

Laying out modifications on time using Ltl

data ModifyGlobally a :: Effect Source #

An effect to modify a computation with an Ltl formula. The idea is that the formula pinpoints locations where Requirements should be enforced.

Instances

Instances details
RunnableMockChain FullEffs Source # 
Instance details

Defined in Cooked.MockChain.Instances

Methods

runMockChain :: MockChainState -> Sem FullEffs a -> [RawMockChainReturn a] Source #

InterpretAlone extraEff => RunnableMockChain (ExtendedStagedEffs extraEff) Source # 
Instance details

Defined in Cooked.MockChain.Instances

Methods

runMockChain :: MockChainState -> Sem (ExtendedStagedEffs extraEff) a -> [RawMockChainReturn a] Source #

modifyLtl :: forall a r b. Member (ModifyGlobally a) r => Ltl a -> Sem r b -> Sem r b Source #

Lays out an Ltl formula to be used for modification within the execution of the wrapped computation. See ModifyLocally for how to consume and use the laid out modifications.

runModifyGlobally :: forall mod effs a. Members '[State [Ltl mod], NonDet] effs => Sem (ModifyGlobally mod ': effs) a -> Sem effs a Source #

Running the ModifyGlobally effect requires to have access of the current list of Ltl formulas, and to have access to an empty computation.

A new formula is appended at the head of the current list of formula. Then, the actual computation is run, after which the newly added formula must be finished, otherwise the empty computation is returned.

Locally applying laid out modifications

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

Instances

Instances details
Show a => Show (Requirement a) Source # 
Instance details

Defined in Cooked.Ltl

Methods

showsPrec :: Int -> Requirement a -> ShowS #

show :: Requirement a -> String #

showList :: [Requirement a] -> ShowS #

Eq a => Eq (Requirement a) Source # 
Instance details

Defined in Cooked.Ltl

Methods

(==) :: Requirement a -> Requirement a -> Bool #

(/=) :: Requirement a -> Requirement a -> Bool #

data ModifyLocally a :: Effect Source #

An effect to request and consume the list of requirements that should be enforced at the current time step.

Instances

Instances details
RunnableMockChain FullEffs Source # 
Instance details

Defined in Cooked.MockChain.Instances

Methods

runMockChain :: MockChainState -> Sem FullEffs a -> [RawMockChainReturn a] Source #

getRequirements :: Member (ModifyLocally a) effs => Sem effs [Requirement a] Source #

Reads and consumes a modification from the context, typically laid out by ModifyGlobally further up the stack of effects.

runModifyLocally :: forall modification effs a. Members '[State [Ltl modification], NonDet] effs => Sem (ModifyLocally modification : effs) a -> Sem effs a Source #

Running the ModifyLocally effect requires to have access to the current list of Ltl formulas, and to be able to branch.

The function nowLaterList is invoked to fetch the various paths implied by the current formulas, and a branching is performed to explore all of them. The new formulas for next steps are stored, and each path is given the requirements to enforce at the current time step.