Always<T> class final

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

Formula: G operand or [] operand

Evaluates to true at time t if the operand formula holds at the current time t and all future time points in the trace.

Evaluation Details:

If evaluated on an empty suffix of the trace (i.e., i >= trace.length), Always evaluates to true (vacuously true).

Inheritance

Constructors

hashCode → int: The hash code for this object.
no setterinherited
operand → Formula<T>: The formula that must hold globally.
final
runtimeType → Type: A representation of the runtime type of the object.
no setterinherited

always() → Always<T>: Creates an ALWAYS (Globally) operator for this formula. G(this)
inherited
and(Formula<T> formula) → And<T>: Creates a logical conjunction (AND) with another formula. this && formula
inherited
eventually() → Eventually<T>: Creates an EVENTUALLY (Finally) operator for this formula. F(this)
inherited
implies(Formula<T> formula) → Implies<T>: Creates a logical implication (IMPLIES) with another formula. this -> formula
inherited
next() → Next<T>: Creates a NEXT operator for this formula. X(this)
inherited
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
inherited
or(Formula<T> formula) → Or<T>: Creates a logical disjunction (OR) with another formula. this || formula
inherited
release(Formula<T> formula) → Release<T>: Creates a RELEASE operator with another formula. this R formula
inherited
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
inherited
weakUntil(Formula<T> formula) → WeakUntil<T>: Creates a WEAK UNTIL operator with another formula. this W formula
inherited