| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Cooked
Description
Re-exports the entirety of the library, which is always eventually necessary when writing large test-suites.
Synopsis
- module Cooked.Wallet
- module Cooked.Validators
- module Cooked.Tweak
- module Cooked.Skeleton
- module Cooked.ShowBS
- module Cooked.Pretty
- module Cooked.Output
- module Cooked.MockChain
- module Cooked.InitialDistribution
- module Cooked.Currencies
- module Cooked.Conversion
- module Cooked.Attack
- class Monad m => MonadModal m where
- type Modification m :: Type
- modifyLtl :: Ltl (Modification m) -> m a -> m a
- data Ltl a
Documentation
module Cooked.Wallet
module Cooked.Validators
module Cooked.Tweak
module Cooked.Skeleton
module Cooked.ShowBS
module Cooked.Pretty
module Cooked.Output
module Cooked.MockChain
module Cooked.InitialDistribution
module Cooked.Currencies
module Cooked.Conversion
module Cooked.Attack
class Monad m => MonadModal m where Source #
Monads that allow modifications with LTL formulas.
Associated Types
type Modification m :: Type Source #
Methods
modifyLtl :: Ltl (Modification m) -> m a -> m a Source #
Instances
| MonadModal (Staged (LtlOp modification builtin)) 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 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.
Constructors
| LtlTruth | The "do nothing" modification that never fails |
| LtlFalsity | The modification that never applies (i.e. always fails) |
| LtlAtom a | The modification that applies a given atomic modification at the | current time step |
| 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. |
| 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 eventually. The formulas a `LtlUntil` b and
> b are equivalent. |
| LtlRelease (Ltl a) (Ltl a) | Assert that the second formula has to be true up to and including the
point when the first one becomes true; if that never happens, the second
formula has to remain true forever. View this as dual to a `LtlRelease` b and
> b are equivalent. |