temporal_logic_core library

Classes

Always<T>

Represents the temporal operator ALWAYS (G or □, also known as Globally).

And<T>

Represents the logical conjunction (AND) of two formulas.

AtomicProposition<T>

Represents an atomic proposition, a basic condition evaluated on a state.

EvaluationResult

Represents the outcome of evaluating a Formula against a Trace.

Eventually<T>

Represents the temporal operator EVENTUALLY (F or ◇, also known as Finally).

Formula<T>

Base class for all temporal logic formulas.

Implies<T>

Represents the logical implication (IMPLIES) of two formulas.

Next<T>

Represents the temporal operator NEXT (X or ○).

Not<T>

Represents the logical negation (NOT) of a formula.

Or<T>

Represents the logical disjunction (OR) of two formulas.

Release<T>

Represents the temporal operator RELEASE (R).

TimedValue<T>

Represents a value associated with a specific point in time (timestamp).

Trace<T>

Represents an immutable, ordered sequence of time-stamped events (TraceEvent).

TraceEvent<T>

Represents a single event or state observation within a Trace.

Until<T>

Represents the temporal operator UNTIL (U).

WeakUntil<T>

Represents the temporal operator WEAK UNTIL (W).

Functions

always<T>(Formula<T> operand) → Always<T>

Creates an ALWAYS (G) formula.

evaluateLtl<T>(Formula<T> formula, List<T> traceStates) → bool

Evaluates a classic LTL (Linear Temporal Logic) formula on a given list of states.

evaluateTrace<T>(Trace<T> trace, Formula<T> formula, {int startIndex = 0}) → EvaluationResult

Evaluates a temporal logic formula against a given timed trace starting from a specific startIndex.

event<T>(bool predicate(T stateOrEvent), {String? name}) → AtomicProposition<T>

Creates an atomic proposition Formula based on an event predicate.

eventually<T>(Formula<T> operand) → Eventually<T>

Creates an EVENTUALLY (F) formula.

next<T>(Formula<T> operand) → Next<T>

Creates a NEXT (X) formula.

release<T>(Formula<T> left, Formula<T> right) → Release<T>

Creates a RELEASE (R) formula.

state<T>(bool pred(T state), {String? name}) → AtomicProposition<T>

Creates an atomic proposition based on a state predicate. Alias for constructing an AtomicProposition formula.

until<T>(Formula<T> left, Formula<T> right) → Until<T>

Creates an UNTIL (U) formula.

weakUntil<T>(Formula<T> left, Formula<T> right) → WeakUntil<T>

Creates a WEAK UNTIL (W) formula.