evaluateTrace<T> function

EvaluationResult evaluateTrace<T>(Trace<T> trace, Formula<T> formula, { int startIndex = 0, })

Evaluates a temporal logic formula against a given timed trace starting from a specific startIndex.

This function acts as the main entry point for evaluating any Formula (including basic boolean logic, LTL operators, and potentially extended operators like those in MTL if handled by subclasses) against a formal Trace. It performs initial checks and delegates the core recursive logic to _evaluateFormula.

The evaluation semantic is typically point-based: the result indicates whether the formula holds true at the startIndex within the trace. Temporal operators inherently look at the suffix of the trace starting from startIndex.

Example Semantics:

• evaluateTrace(trace, Always(p), startIndex: 2) checks if p holds at indices 2, 3, 4, ... of the trace.
• evaluateTrace(trace, Eventually(q), startIndex: 5) checks if q holds at index 5 or any subsequent index.

Parameters:

• trace: The sequence of timed states/events (TraceEvent) to evaluate against. Must have monotonically non-decreasing timestamps.
• formula: The temporal logic formula (Formula) to evaluate.
• startIndex: The 0-based index in trace.events from which to begin evaluation. Defaults to 0 (evaluate from the start of the trace). Must be non-negative.

Returns: An EvaluationResult object containing:

• holds: Boolean indicating if the formula is satisfied at startIndex.
• reason: Optional explanation, especially if holds is false.
• relatedIndex / relatedTimestamp: Optional context about the specific point in the trace relevant to the result (e.g., where a violation occurred).

Handling of Trace Boundaries:

• A negative startIndex immediately results in a failure.
• Evaluating at or beyond the end of the trace (startIndex >= trace.length) is permissible. The outcome depends on the specific formula:
  • Always(f) is vacuously true on an empty suffix.
  • Eventually(f) is false on an empty suffix.
  • AtomicProposition(p) fails because there is no state to evaluate.
  • Other operators are handled recursively.

Implementation

EvaluationResult evaluateTrace<T>(Trace<T> trace, Formula<T> formula,
    {int startIndex = 0}) {
  // Initial checks might be added here, but core logic delegates to _evaluateFormula.
  // Bounds checking related to startIndex is often handled within the specific
  // operator logic as they look into the future of the trace.
  if (startIndex < 0) {
    // Returning failure here as negative indices are always invalid.
    return EvaluationResult.failure(
        'Start index $startIndex cannot be negative.',
        relatedIndex: startIndex);
  }
  // Allow startIndex >= trace.length, as some formulas (like G(p)) can be vacuously true
  // on an empty trace suffix.

  return _evaluateFormula(trace, formula, startIndex);
}