Module temporal_ltl

Structs§

SafetyMonitor: An incremental monitor for the safety fragment G(p) (“p always holds”) — the practical Büchi-automaton acceptance for stream monitoring: it stays Safe while every streamed event satisfies p, and latches to Violated permanently on the first event that does not. Zero-heap.

evaluate_historically: Historically H p (past □): p held at every point in the trace (dual of Globally). Vacuously true on an empty trace (nothing in the past violated it).
evaluate_lock_lease
evaluate_ltl_trace
evaluate_once: Once O p (past ◇): p held at some point in the trace (the past-time dual of Finally).
evaluate_since: Since p S q: at the end of the trace, q held at some past point and p has held at every point since (inclusive of after q). Retrospective legal analysis (“the duty has held since the breach”). Zero-heap.
holds_globally_within: MTL bounded-globally G[t0, t0+window] inv: from the earliest trigger timestamp t0, the invariant must hold at every event whose timestamp lies in [t0, t0+window]. Returns true vacuously if no in-window events. Zero-heap.
holds_within: Metric temporal (MTL) “within”: after the EARLIEST occurrence of trigger (each event quin carries its timestamp in metadata), target must occur at some time t1 with t0 <= t1 <= t0 + window. Models deadlines — e.g. “remedy within 30 days of breach”. Zero-heap (two linear scans; no allocation).
predicate_interval: Extract the [first, last] timestamp interval over which predicate occurs in the timed trace (each event’s timestamp in metadata), or None if it never occurs. The bridge to the Allen Interval Algebra (interval_reasoning::allen_relation relates two such intervals).