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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct