To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.0

Library

Module

Module type

Parameter

Class

Class type

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.

`val to_string : t -> string`

`val time : t -> Core.Time_ns.t option`