Module Property.CTL

type state =
| True
| P of atomic_proposition
| And of state * state
| Not of state
| E of path
| A of path
and path =
| X of state
| U of state * state
| F of state
| G of state
val sexp_of_state : state -> Sexplib0.Sexp.t
val sexp_of_path : path -> Sexplib0.Sexp.t
val t : state

True

Proposition

val (&:) : state -> state -> state

And

val (~:) : state -> state

Not

val ax : ?n:int -> state -> state

On all paths in the next state

val ex : ?n:int -> state -> state

On some path in the next state

val au : state -> state -> state

On all paths u holds.

val eu : state -> state -> state

On some path u holds

val af : state -> state

On all paths finally holds

val ef : state -> state

On some path finally holds

val ag : state -> state

On all paths globally holds

val eg : state -> state

On some path globally holds

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

Convert property to a string

val atomic_propositions : state -> atomic_proposition list

Find all atomic propositions in the formula

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