Module Property.LTL

type path =
| True
| P of atomic_proposition
| Pn of atomic_proposition
| And of path * path
| Or of path * path
| Not of path
| X of path
| U of path * path
| R of path * path
| F of path
| G of path
val sexp_of_path : path -> Sexplib0.Sexp.t
val vdd : path

True

val gnd : path

False

Proposition

val (&:) : path -> path -> path

And

val (|:) : path -> path -> path

Or

val (~:) : path -> path

Not

val (^:) : path -> path -> path

Xor

val (==>:) : path -> path -> path

Implication

val (<>:) : path -> path -> path

Does not equal

val (==:) : path -> path -> path

Equals

val x : ?n:int -> path -> path

In the next step

val u : path -> path -> path

In u a b a holds at least until b holds

val r : path -> path -> path

Release

val f : path -> path

Finally(/eventually)

val g : path -> path

Globally/(always)

val w : path -> path -> path

Weak until

val to_string : ?name:( atomic_proposition -> string ) -> path -> string

Convert property to a string

val atomic_propositions : path -> atomic_proposition list

Find all atomic propositions in the formula

val map_atomic_propositions : path -> f:( atomic_proposition -> atomic_proposition ) -> path

Apply f to all atomic propositions in the formula

val depth : path -> int

Maximum nested depth of formula

val nnf : path -> path

Convert to negative normal form.

val limit_depth : int -> path -> path

Rewrite the formula only look a limited distance into the future.