evaluateLtl<T> function

bool evaluateLtl<T>(Formula<T> formula, List<T> traceStates)

Evaluates a classic LTL (Linear Temporal Logic) formula on a given list of states.

This is a convenience wrapper around evaluateTrace for scenarios where only the sequence of states matters, and explicit timing information is not required or available. It simplifies LTL evaluation by automatically converting the input list into a Trace with default (e.g., 1ms) intervals between states.

Use this function for pure LTL checking without time constraints.

Behavior:

1. Checks if the input traceStates list is empty. If so, returns false (common convention for LTL on empty traces, though Always is technically true).
2. Creates a Trace<T> using Trace.fromList, assigning incremental timestamps.
3. Calls the main evaluateTrace function, starting the evaluation from the beginning of this generated trace (startIndex = 0).
4. Returns only the boolean holds field from the EvaluationResult.

Limitations:

• No Time Semantics: This function discards any real-world timing. Formulas involving specific time bounds (like those in Metric Temporal Logic) cannot be correctly evaluated using this function.
• Empty Trace Handling: Returns false for empty traces, which might differ from the strict mathematical semantics for operators like Always (which is vacuously true on empty traces). This behavior aligns with practical expectations where properties are usually checked on non-empty executions.

Parameters:

• formula: The LTL Formula to evaluate.
• traceStates: The ordered sequence of states (type T).

Returns: true if the formula holds for the sequence according to standard LTL semantics evaluated from the start; false otherwise (including for empty traceStates).

Implementation

bool evaluateLtl<T>(Formula<T> formula, List<T> traceStates) {
  if (traceStates.isEmpty) {
    // LTL evaluation on an empty trace is often considered false for most practical formulas,
    // especially those involving Eventually or Until. Returning false aligns with prior behavior.
    return false;
  }
  // Convert the list to a Trace (using default 1ms interval)
  final timedTrace = Trace<T>.fromList(traceStates);
  // Use the primary trace evaluator, starting at index 0.
  final result = evaluateTrace(timedTrace, formula);
  return result.holds;
}