1. Overview
  2. Docs

Using linear temporal logic (LTL) to run online queries on sequences of states. A state is a record and the formula talks about values of the fields in this record.

Given an LTL formula phi with variables var(phi), an assignment E of values to variables in var(phi), and a sequence of states xs, there is a satisfaction relation xs |= phi, E. The function Naive.eval gives the precise definition of this relation.

Given a formula phi and a pipe of states input the function query returns a pipe of all variable assignments E such that input |= phi, E (some assigment sets may be given in an implicit form - see documentation of query). Often a satisfying assignment can be determined without waiting for the end of the input pipe.

query phi input works by keeping track of a set of constraints of the form (phi', E') such that any variable assignment E that satisfies phi and has not been returned yet must refine E' and satisfy xs |= phi', E' where xs is the remaining part of input. See the top of .ml for more details.

We use an optimization that allows many useful queries to run in linear time in the size of the input. If we detect that a particular constraint (phi, E) is not going to change unless a particular field has a particular value, we put the constraint to sleep in a hashtable with the (field, value) pair as the key. You can check whether the optimization works as expected in your case by using the ?debug argument of query with `Info level and checking in the output that the number of active constraints remains constant. See the top of .ml for more details.

The worst-case runtime of the query is super-exponential in the size of the formula. This is unlikely to be a problem in practice.

See base/async/extended/examples/ for an example of use.

type t
val to_string : t -> string
val time : t -> Core.Time_ns.t option