UntilTimed<T> class final

Represents the timed until operator φ U_I ψ (Until within Interval).

Asserts that there exists a point k in the trace suffix starting from i such that:

  1. The time difference timestamp(k) - timestamp(i) falls within the interval I.
  2. The right formula ψ holds at point k.
  3. For all points j such that i <= j < k, the left formula φ holds.

Example: requesting.untilTimed(granted, TimeInterval.upTo(Duration(seconds: 2))) asserts that requesting holds until granted becomes true, and that granted becomes true within 2 seconds.

Inheritance

Constructors

UntilTimed(Formula<T> left, Formula<T> right, TimeInterval interval)
Creates a timed until formula φ U_I ψ.
const

Properties

hashCode → int
The hash code for this object.
no setterinherited
interval → TimeInterval
The time interval I within which right must become true.
final
left → Formula<T>
The formula φ that must hold until right becomes true.
final
The formula ψ that must eventually become true within the interval.
final
runtimeType → Type
A representation of the runtime type of the object.
no setterinherited

Methods

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

Operators

operator ==(Object other) → bool
The equality operator.
inherited