temporal_logic_flutter_test library

Test utilities for Temporal Logic Flutter integrations.

This is the supported entry point for matchers and test helpers. Test code should prefer this library over importing files from src/.

Classes

Always<T>
Represents the temporal operator ALWAYS (G or □, also known as Globally).
AlwaysTimed<T>
Represents the timed always operator G_I φ (Globally within Interval).
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).
EventuallyTimed<T>
Represents the timed eventually operator F_I φ (Finally within Interval).
Formula<T>
Base class for all temporal logic formulas.
Implies<T>
Represents the logical implication (IMPLIES) of two formulas.
LtlCheckerWidget<S>
A widget that observes a stream of state S and displays whether a Linear Temporal Logic (LTL) formula holds true based on the sequence of states observed from the stream.
MtlCheckerWidget<S>
A widget that observes a stream of timed states TimedValue<S> and displays whether a temporal logic formula (LTL or MTL) holds true based on the timed sequence of states observed from the stream.
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).
ReleaseTimed<T>
Represents the timed release operator φ R_I ψ (Release within Interval).
StreamLtlChecker<S>
Provides evaluation of a Linear Temporal Logic (LTL) Formula against a stream of state values.
StreamMtlChecker<S>
Provides periodic evaluation of a temporal logic Formula (LTL/MTL) against a stream of time-stamped values. Incoming events are accumulated into an internal trace and evaluated on every new event.
StreamSustainedStateChecker<S>
Observes a stream of timed states TimedValue<S> and checks if a specific targetState is sustained for a given sustainDuration once entered.
SustainedStateCheckerWidget<S>
A widget that observes a stream of timed states TimedValue<S> and displays the result of checking if a targetState is sustained for a given sustainDuration once entered.
TimedValue<T>
Represents a value associated with a specific point in time (timestamp).
TimeInterval
Represents a closed time interval [lowerBound, upperBound] used in MTL formulas.
Trace<T>
Represents an immutable, ordered sequence of time-stamped events (TraceEvent).
TraceEvent<T>
Represents a single event or state observation within a Trace.
TraceRecorder<T>
Records a sequence of state changes over time to produce a Trace.
Until<T>
Represents the temporal operator UNTIL (U).
UntilTimed<T>
Represents the timed until operator φ U_I ψ (Until within Interval).
WeakUntil<T>
Represents the temporal operator WEAK UNTIL (W).
WeakUntilTimed<T>
Represents the timed weak until operator φ W_I ψ (Weak Until within Interval).

Enums

CheckStatus
Represents the status of a temporal check, especially for runtime monitoring.
StreamEvaluationStart
Defines where a stream checker evaluates a formula on the accumulated trace.

Functions

always<T>(Formula<T> operand) → Always<T>
Creates an ALWAYS (G) formula.
evaluateMtlTrace<T>(Trace<T> trace, Formula<T> formula, {int startIndex = 0}) → EvaluationResult
Evaluates a temporal logic formula (potentially including both LTL and MTL operators) against a given timed trace, starting from 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.
satisfiesLtl<T>(Formula<T> formula) → Matcher
A matcher that checks if a Trace satisfies a given 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.