package hardcaml

  1. Overview
  2. Docs
package hardcaml
Legend:
Library
Module
Module type
Parameter
Class
Class type
type state =
  1. | True
  2. | P of atomic_proposition
  3. | And of state * state
  4. | Not of state
  5. | E of path
  6. | A of path
and path =
  1. | X of state
  2. | U of state * state
  3. | F of state
  4. | 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