Documentation

A property name (e.g. "thread", "node", etc.).

The type of variable identifiers used throughout the framework (LTL property variables and polynomial integer variables).

The numeric type used for integer event property values and polynomial arithmetic throughout the framework.

Text event property value.

i, j ::= i + i | int · x | int, where int is an arbitrary integer

Text term: a constant string or a variable ranging over strings.

Binary comparison relation on an ordered type.

Default name: c. A constraint inside an Atom, matching an event property against a term.

Default name: φ.

Formulas of a discrete-time Linear Temporal Logic (LTL) enriched with first-order quantification over event properties.

Time model. Time is a sequence of abstract units indexed by natural numbers. Each unit carries a finite multiset of typed events (see Event). The temporal connectives advance through this sequence:

• ◯ φ — next unit
• ☐ ᪲ₖ φ — every (k+1)-th unit from now, forever
• ☐ⁿ φ — for each of the next n units
• ♢ⁿ φ — for some unit within the next n
• φ |ⁿ ψ — φ until ψ, within n units

Parameterisation. The type parameter ty is the vocabulary of event types; event is the concrete event representation (see Event). Atoms (Atom ty cs) assert that the current unit contains an event of type ty whose properties satisfy the constraints cs.

First-order layer. Quantifiers ∀x ∈ ℤ, ∃x ∈ ℤ, ∀x ∈ Text, ∃x ∈ Text, and their finite-domain variants, bind variables that can appear in property constraints, integer comparison atoms (PropIntBinRel), and text equality atoms (PropTextEq). The resulting fragment is decidable: integer arithmetic is handled by Cooper's quantifier elimination; text quantifiers are decided by finite enumeration (see Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree).

Compute the total Relevance of the formula.

Set of relevant events.

It's useful to express temporal aspect of the formulas in a familiar time unit (e.g milliseconds). Yet, the LTL machinery works with nameless abstract time units. This function can be used to convert one into the other.

Controls evaluator behaviour when a formula atom references a property key that is absent from the event being evaluated.

• BottomOnMissingKey — treat the atom as unsatisfied (⊥); evaluation continues silently. Useful when events may legally omit optional fields.
• CrashOnMissingKey — throw an exception. Useful during development to catch formula/event-schema mismatches early.

Default name: e.

Interface between a concrete event representation a and the LTL evaluator. The functional dependency a -> ty fixes the event-type vocabulary once the event type is known.

Semantics. Each time unit presents a sequence of events to the evaluator. An Atom ty cs is satisfied by unit t if there exists an event e in t such that:

1. ofTy e ty holds, and
2. every constraint c ∈ cs matches e against intProps e ty or textProps e ty (see satisfiability-semantics.txt).

Precondition. intProps and textProps are only called when ofTy e ty is True; their behaviour is unspecified otherwise.