Up

Module Make (State : State)

Parameters

Signature

module Field : sig .. end
module Variable : sig .. end
module Assignment : sig .. end
module Expression : sig .. end
type t

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.

val sexp_of_t : t -> Sexplib.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.

val negate : t -> t
val conj : t list -> t
val disj : t list -> t
val next : t -> t

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).

val until : t -> t -> t

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).

val release : t -> t -> t

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.Std.Time.t -> t

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

val after : Core.Std.Time.t -> t

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

val before_var : ?add:Core.Std.Time.Span.t -> Core.Std.Time.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.Std.Time.Span.t -> Core.Std.Time.t Variable.t -> t

after_var ~add v is true if the state has time greater or equal to v + add.

val field_predicate : ?description:string -> 'a Field.t -> ('a -> bool) -> t

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))

val has : 'a Field.t -> t
val implies : t -> t -> t
val eventually : t -> t
val always : t -> t
module O : sig .. end
val validate : t -> unit Core.Std.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.Std.Log.t -> ?allow_nonmonotonic_times:bool -> t -> State.t Async.Std.Pipe.Reader.t -> bool Async.Std.Deferred.t Core.Std.Or_error.t

eval t input returns true if there exists an assignment E such that input |= t, E.

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