Trace<T> class

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

This is the fundamental data structure against which temporal logic formulas (Formula) are evaluated. It captures the evolution of a system's state T over time.

Core Properties:

  • Immutability: Once created, a Trace cannot be modified. Operations that seem to modify a trace typically return a new Trace instance.
  • Monotonic Timestamps: The events list is guaranteed to have timestamps that are monotonically non-decreasing (i.e., events[i+1].timestamp >= events[i].timestamp for all valid i). This property is crucial for the semantics of most temporal logics and is enforced by an assertion in the default constructor (in debug mode).

Traces are used by evaluator functions (like those potentially found in evaluator.dart or specific logic packages like temporal_logic_mtl) to determine the truth value of a Formula over the recorded behavior.

See also:

  • TraceEvent, the individual elements comprising a trace.
  • Formula, the logical specifications evaluated over traces.
  • evaluateTrace (in evaluator.dart), the typical function for evaluation.
Annotations
  • @immutable

Constructors

Trace.new(List<TraceEvent<T>> events)
Creates a trace from a given list of TraceEvents.
Trace.empty()
Creates an empty trace with no events. Useful as a base case or initial value.
Trace.fromList(List<T> values, {Duration interval = const Duration(milliseconds: 1)})
Creates a Trace from a simple list of state values, assigning timestamps automatically with a fixed interval.
factory

Properties

events → List<TraceEvent<T>>
The ordered, unmodifiable sequence of timed events comprising this trace.
final
hashCode → int
The hash code for this object.
no setteroverride
isEmpty → bool
Returns true if the trace contains no events.
no setter
length → int
Returns the number of events (time points) in the trace.
no setter
runtimeType → Type
A representation of the runtime type of the object.
no setterinherited

Methods

noSuchMethod(Invocation invocation) → dynamic
Invoked when a nonexistent method or property is accessed.
inherited
toString() → String
Provides a string representation showing the sequence of events in the trace. Example: Trace(StateA @ 0ms, StateB @ 150ms, StateC @ 500ms)
override

Operators

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