Formula<T> class abstract

Base class for all temporal logic formulas.

Represents a proposition or a combination of propositions using logical or temporal operators. Subclasses define specific operators like And, Or, Not, Next, Always, Eventually, etc., or represent atomic conditions like AtomicProposition.

The type parameter T indicates the type of the state object found within a TraceEvent in a Trace. Formulas are evaluated against these traces.

Formulas are typically immutable and represent the structure of a logical assertion.

See also:

• evaluateTrace in evaluator.dart for the primary evaluation logic.
• AtomicProposition for basic conditions.
• And, Or, Not, Implies for boolean logic.
• Next, Always, Eventually, Until, WeakUntil, Release for LTL operators.
• (In temporal_logic_mtl) EventuallyTimed, AlwaysTimed, UntilTimed for MTL operators.

Implementers

• Always
• And
• AtomicProposition
• Eventually
• Implies
• Next
• Not
• Or
• Release
• Until
• WeakUntil

Constructors

Formula.new()

const

Properties

hashCode → int

The hash code for this object.

no setter, inherited

runtimeType → Type

A representation of the runtime type of the object.

no setter, inherited

Methods

always() → Always<T>

Creates an ALWAYS (Globally) operator for this formula. G(this)

and(Formula<T> formula) → And<T>

Creates a logical conjunction (AND) with another formula. this && formula

eventually() → Eventually<T>

Creates an EVENTUALLY (Finally) operator for this formula. F(this)

implies(Formula<T> formula) → Implies<T>

Creates a logical implication (IMPLIES) with another formula. this -> formula

next() → Next<T>

Creates a NEXT operator for this formula. X(this)

noSuchMethod(Invocation invocation) → dynamic

Invoked when a nonexistent method or property is accessed.

inherited

not() → Not<T>

Creates a logical negation (NOT) of this formula. !this

or(Formula<T> formula) → Or<T>

Creates a logical disjunction (OR) with another formula. this || formula

release(Formula<T> formula) → Release<T>

Creates a RELEASE operator with another formula. this R formula

toString() → String

Returns a string representation of the formula, useful for debugging.

override

until(Formula<T> formula) → Until<T>

Creates an UNTIL operator with another formula. this U formula

weakUntil(Formula<T> formula) → WeakUntil<T>

Creates a WEAK UNTIL operator with another formula. this W formula

Operators

operator ==(Object other) → bool

The equality operator.

inherited