Safe Haskell	Safe-Inferred
Language	Haskell2010

Hermod.ReCon.LTL.Satisfy

Synopsis

data SatisfactionResult event ty
- = Satisfied
- | Unsatisfied (Relevance event ty)
satisfies :: (Event event ty, Ord event, Ord ty, Show ty, Foldable f) => OnMissingKey -> Formula event ty -> f event -> SatisfactionResult event ty
satisfiesS :: (Event event ty, Ord event, Ord ty, Show ty) => OnMissingKey -> Formula event ty -> Stream (Of event) IO () -> IORef (SatisfyMetrics event ty) -> IO (SatisfactionResult event ty)
data SatisfyMetrics event ty = SatisfyMetrics {
- eventsConsumed :: Word64
- currentFormula :: Formula event ty
- currentTimestamp :: Word64
}

Documentation

data SatisfactionResult event ty Source #

The result of checking satisfaction of a formula against a timeline. If unsatisfied, stores points in the timeline "relevant" to the formula.

Constructors

Satisfied
Unsatisfied (Relevance event ty)

Instances

Instances details

(Show event, Show ty) => Show (SatisfactionResult event ty) Source #
Instance details Defined in Hermod.ReCon.LTL.Satisfy Methods showsPrec :: Int -> SatisfactionResult event ty -> ShowS Source # show :: SatisfactionResult event ty -> String Source # showList :: [SatisfactionResult event ty] -> ShowS Source #
(Eq event, Eq ty) => Eq (SatisfactionResult event ty) Source #
Instance details Defined in Hermod.ReCon.LTL.Satisfy Methods (==) :: SatisfactionResult event ty -> SatisfactionResult event ty -> Bool Source # (/=) :: SatisfactionResult event ty -> SatisfactionResult event ty -> Bool Source #

satisfies :: (Event event ty, Ord event, Ord ty, Show ty, Foldable f) => OnMissingKey -> Formula event ty -> f event -> SatisfactionResult event ty Source #

Check if the formula is satisfied in the given event timeline.

satisfiesS :: (Event event ty, Ord event, Ord ty, Show ty) => OnMissingKey -> Formula event ty -> Stream (Of event) IO () -> IORef (SatisfyMetrics event ty) -> IO (SatisfactionResult event ty) Source #

Given a formula and a stream of events, forms an IO computation that returns a SatisfactionResult once the formula is equivalent to ⊤ or ⊥. This may happen either once the stream terminates or if the formula is falsified early by some prefix of the stream.

data SatisfyMetrics event ty Source #

Constructors

SatisfyMetrics
Fields eventsConsumed :: Word64 currentFormula :: Formula event ty currentTimestamp :: Word64 μs