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/ltl.ml for an example of use.