Library

Module

Module type

Parameter

Class

Class type

## Parameters

## Signature

`module Field : sig ... end`

`module Variable : sig ... end`

`module Assignment : sig ... end`

`module Expression : sig ... end`

An LTL formula. Evaluates to true or false given a sequence of states and an assignment of variables (written `xs |= t, values`

). Our solver finds all satisfying assignments.

Some formulas are not defined on empty sequences. Validation will reject such formulas along with formulas in which an argument of a `next`

operator is not defined on empty sequences - see `validate`

below for details.

`include sig ... end`

`val sexp_of_t : t -> Ppx_sexp_conv_lib.Sexp.t`

`val const : bool -> t`

`val eq : 'a Variable.t -> 'a Field.t -> t`

Undefined on empty sequences.

`x :: _ |= (eq v fld), values`

if the state `x`

contains field `fld`

and `State.get fld x = Assignment.find_exn values v`

.

In particular, the negation of this formula is true if a field does not exist.

`val predicate : ?description:string -> bool Expression.t -> t`

Undefined on empty sequences.

`x :: _ |= (predicate p), values`

if `Expression.eval p x values`

evaluates to `true`

(the function `Expression.eval`

is not exposed in this mli).

Example:

```
let gt var fld =
predicate Expression.(map2 (variable var) (field fld) ~f:(>))
```

If expression evaluation produces failure (refers to a missing field), its value is considered false.

`next a`

means "the tail of the sequence satisfies `a`

". `a`

must be defined on empty sequences.

`next a`

is false if the sequence is empty.

`x :: xs |= (next a), values`

if `xs |= a, values`

.

Because of behaviour on empty sequences `next (negate a)`

is not the same as `negate (next a)`

.

`until a b`

means "b eventually happens, and a holds at all times until that (non-inclusive)".

False on an empty sequence.

`x :: xs |= (until a b), values`

if `x :: xs |= b, values`

or (`x :: xs |= a, values`

and `xs |= (until a b), values`

)

You almost always want to use the special case `eventually`

(see below).

`release a b = negate (until (negate a) (negate b))`

means "b must hold until a happens (inclusive); if a never happens, b must hold forever."

True on an empty sequence.

`x :: xs |= (release a b), values`

if `x :: xs |= b, values`

and (`x :: xs |= a, values`

or `xs |= (release a b), values`

)

You almost always want to use the special case `always`

(see below).

`val before : Core.Time_ns.t -> t`

`before t`

is true if the state has time less or equal to `t`

. `before t`

is false if the time is `None`

.

`val after : Core.Time_ns.t -> t`

`after t`

is true if the state has time greater or equal to `t`

. `after t`

is false if the time is `None`

.

`val before_var : ?add:Core.Time_ns.Span.t -> Core.Time_ns.t Variable.t -> t`

`before_var ~add v`

is true if the state has time less or equal to `v + add`

.

`val after_var : ?add:Core.Time_ns.Span.t -> Core.Time_ns.t Variable.t -> t`

`after_var ~add v`

is true if the state has time greater or equal to `v + add`

.

`field_predicate fld f`

is a predicate that is true if the state contains `fld`

and the value of `fld`

satisfies `f`

:

`field_predicate fld f`

= `predicate Expression.(map ~f (field fld))`

`module O : sig ... end`

`val validate : t -> unit Core.Or_error.t`

If `validate`

returns `Ok`

then so do `eval`

and `query`

. A formula may be rejected for several reasons:

1 Its value is not defined for empty sequences. This is the case for `predicate`

and `eq`

formulas that refer to the initial state of the sequence. Validation requires that both in the top-level formula and in the argument of each `next`

operator every `predicate`

or `eq`

occurs underneath an `until`

or `release`

.

2 The solver cannot reorder the clauses such that each variable is constrained by an equality before being used in an inequality or a predicate. A subformula `x != 12`

is rejected, but a subformula `(x != 12) /\ (x == 12)`

is accepted. See the top of the .ml file for the description of the solving algorithm that goes into more detail.

Condition 2 guarantees that the set of all variable assignments that satisfy the formula is explicit: it can be described as ` complete(E1) U ... U complete(En) `

where `E1, ..., En`

are variable assignments (possibly undefined for some variables of the formula) and `complete(E)`

is the set of all assignments that refine `E`

. This representation is returned by `query`

below.

```
val eval :
?debug:Async.Log.t ->
?allow_nonmonotonic_times:bool ->
?allow_missing_times:bool ->
t ->
State.t Async.Pipe.Reader.t ->
bool Async.Deferred.t Core.Or_error.t
```

`eval t input`

returns `true`

if there exists an assignment `E`

such that `input |= t, E`

.

```
val query :
?debug:Async.Log.t ->
?allow_nonmonotonic_times:bool ->
?allow_missing_times:bool ->
t ->
State.t Async.Pipe.Reader.t ->
Assignment.t Async.Pipe.Reader.t Core.Or_error.t
```