Safe Haskell	Safe-Inferred
Language	Haskell2010

Hermod.ReCon.LTL.ContinuousFormula

Synopsis

data ContinuousFormula ty
- = Atom ty (Set PropConstraint)
- | Or (ContinuousFormula ty) (ContinuousFormula ty)
- | And (ContinuousFormula ty) (ContinuousFormula ty)
- | Not (ContinuousFormula ty)
- | Implies (ContinuousFormula ty) (ContinuousFormula ty)
- | Top
- | Bottom
- | PropIntForall VariableIdentifier (ContinuousFormula ty)
- | PropTextForall VariableIdentifier (ContinuousFormula ty)
- | PropIntForallN VariableIdentifier (Set IntValue) (ContinuousFormula ty)
- | PropTextForallN VariableIdentifier (Set TextValue) (ContinuousFormula ty)
- | PropIntExists VariableIdentifier (ContinuousFormula ty)
- | PropTextExists VariableIdentifier (ContinuousFormula ty)
- | PropIntExistsN VariableIdentifier (Set IntValue) (ContinuousFormula ty)
- | PropTextExistsN VariableIdentifier (Set TextValue) (ContinuousFormula ty)
- | PropIntBinRel BinRel IntTerm IntTerm
- | PropTextEq TextTerm TextValue
retract :: Formula event ty -> Maybe (ContinuousFormula ty)
interp :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey HomogeneousFormula
eval :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey Bool

Documentation

data ContinuousFormula ty Source #

Default name: φ.

The continuous counterpart of Formula: all temporal connectives are absent. A ContinuousFormula is evaluated against a single event (or time unit) rather than a sequence, making it a purely propositional / first-order assertion about the present moment.

Constructors

Atom ty (Set PropConstraint)	ty c̄
Or (ContinuousFormula ty) (ContinuousFormula ty)	φ ∨ ψ
And (ContinuousFormula ty) (ContinuousFormula ty)	φ ∧ ψ
Not (ContinuousFormula ty)	¬ φ
Implies (ContinuousFormula ty) (ContinuousFormula ty)	φ ⇒ ψ
Top	⊤
Bottom	⊥
PropIntForall VariableIdentifier (ContinuousFormula ty)	∀x ∈ ℤ. φ — x ranges over all integers
PropTextForall VariableIdentifier (ContinuousFormula ty)	∀x ∈ Text. φ — x ranges over all strings
PropIntForallN VariableIdentifier (Set IntValue) (ContinuousFormula ty)	∀x ∈ v̄. φ — x ranges over the given integers
PropTextForallN VariableIdentifier (Set TextValue) (ContinuousFormula ty)	∀x ∈ v̄. φ — x ranges over the given strings
PropIntExists VariableIdentifier (ContinuousFormula ty)	∃x ∈ ℤ. φ — x ranges over all integers
PropTextExists VariableIdentifier (ContinuousFormula ty)	∃x ∈ Text. φ — x ranges over all strings
PropIntExistsN VariableIdentifier (Set IntValue) (ContinuousFormula ty)	∃x ∈ v̄. φ — x ranges over the given integers
PropTextExistsN VariableIdentifier (Set TextValue) (ContinuousFormula ty)	∃x ∈ v̄. φ — x ranges over the given strings
PropIntBinRel BinRel IntTerm IntTerm	t rel t (integer)
PropTextEq TextTerm TextValue	t = v (text)

Instances

Instances details

Show ty => Show (ContinuousFormula ty) Source #
Instance details Defined in Hermod.ReCon.LTL.ContinuousFormula Methods showsPrec :: Int -> ContinuousFormula ty -> ShowS Source # show :: ContinuousFormula ty -> String Source # showList :: [ContinuousFormula ty] -> ShowS Source #
Eq ty => Eq (ContinuousFormula ty) Source #
Instance details Defined in Hermod.ReCon.LTL.ContinuousFormula Methods (==) :: ContinuousFormula ty -> ContinuousFormula ty -> Bool Source # (/=) :: ContinuousFormula ty -> ContinuousFormula ty -> Bool Source #
Ord ty => Ord (ContinuousFormula ty) Source #
Instance details Defined in Hermod.ReCon.LTL.ContinuousFormula Methods compare :: ContinuousFormula ty -> ContinuousFormula ty -> Ordering Source # (<) :: ContinuousFormula ty -> ContinuousFormula ty -> Bool Source # (<=) :: ContinuousFormula ty -> ContinuousFormula ty -> Bool Source # (>) :: ContinuousFormula ty -> ContinuousFormula ty -> Bool Source # (>=) :: ContinuousFormula ty -> ContinuousFormula ty -> Bool Source # max :: ContinuousFormula ty -> ContinuousFormula ty -> ContinuousFormula ty Source # min :: ContinuousFormula ty -> ContinuousFormula ty -> ContinuousFormula ty Source #

retract :: Formula event ty -> Maybe (ContinuousFormula ty) Source #

Retract a Formula into a ContinuousFormula, returning Nothing if the formula contains any temporal connective.

interp :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey HomogeneousFormula Source #

Algorithm for (e ⊧ φ): checks each Atom against the event type and substitutes property constraints with the event's concrete values, yielding a HomogeneousFormula ready for decision.

eval :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey Bool Source #

Decide (e ⊧ φ).