To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
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
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
`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.
val to_string : t -> string
val time : t -> Core.Time_ns.t option