Documentation

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 modifications. Since it does not make (obvious) sense to talk of a negated modification or of one modification (possibly in the future) to imply another modification, implication and negation are absent.

Split an LTL formula that describes a modification of a computation into a list of (doNow, doLater) pairs, where

• doNow is the modification to be applied to the current time step,
• doLater is an LTL formula describing the modification that should be applied from the next time step onwards, and

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.

Modifications should form a Monoid, where mempty is the do-nothing modification, and <> is the composition of modifications. We interpret a <> b as the modification that first applies b and then a. Attention: Since we use <> to define conjunction, if <> is not commutative, conjunction will also fail to be commutative!

Say we're passing around more than one formula from each time step to the next, where the intended meaning of a list of formulas is the modification that applies the first formula in the list first, then the second formula, then the third and so on. We'd still like to compute a list of (doNow, doLater) pairs as in nowLater, only that the doLater should again be a list of formulas.

The idea is that a value of type Staged (LtlOp modification builtin) a describes a set of (monadic) computations that return an a such that

• every step of the computations that returns a b is reified as a builtin b, and
• every step can be modified by a modification.

Operations for computations that can be modified using LTL formulas.

The freer monad on op. We think of this as the AST of a computation with operations of types op a.

Interpret a Staged computation into a suitable domain, using the function interpBuiltin to interpret the builtins.

Interpret a Staged computation into a suitable domain, using the function interpBuiltin to interpret the builtins. At the end of the computation, prune branches that still have unfinished modifications applied to them. See the discussion on the regression test case for PRs 110 and 131 in hs for a discussion on why this function has to exist.

To be a suitable semantic domain for computations modified by LTL formulas, a monad m has to

• have the right builtin functions, which can be modified by the right modifications,
• be a MonadPlus, because one LTL formula might yield different modified versions of the computation, and

This type class only requires from the user to specify how to interpret the (modified) builtins. In order to do so, it passes around the formulas that are to be applied to the next time step in a StateT. A common idiom to modify an operation should be this:

interpBuiltin op =
 get
   >>= msum
     . map (\(now, later) -> applyModification now op <* put later)
     . nowLaterList

(But to write this, modification has to be a Monoid to make nowLaterList work!) Look at the tests for this module and at Cooked.MockChain.Monad.Staged for examples of how to use this type class.

Monads that allow modifications with LTL formulas.