package hardcaml

  1. Overview
  2. Docs
package hardcaml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Property.LTLSource

Sourcetype path =
  1. | True
  2. | P of atomic_proposition
  3. | Pn of atomic_proposition
  4. | And of path * path
  5. | Or of path * path
  6. | Not of path
  7. | X of path
  8. | U of path * path
  9. | R of path * path
  10. | F of path
  11. | G of path
Sourceval sexp_of_path : path -> Sexplib0.Sexp.t
Sourceval vdd : path

True

Sourceval gnd : path

False

Proposition

Sourceval (&:) : path -> path -> path

And

Sourceval (|:) : path -> path -> path

Or

Sourceval (~:) : path -> path

Not

Sourceval (^:) : path -> path -> path

Xor

Sourceval (==>:) : path -> path -> path

Implication

Sourceval (<>:) : path -> path -> path

Does not equal

Sourceval (==:) : path -> path -> path

Equals

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

In the next step

Sourceval u : path -> path -> path

In u a b a holds at least until b holds

Sourceval r : path -> path -> path

Release

Sourceval f : path -> path

Finally(/eventually)

Sourceval g : path -> path

Globally/(always)

Sourceval w : path -> path -> path

Weak until

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

Convert property to a string

Sourceval atomic_propositions : path -> atomic_proposition list

Find all atomic propositions in the formula

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

Apply f to all atomic propositions in the formula

Sourceval depth : path -> int

Maximum nested depth of formula

Sourceval nnf : path -> path

Convert to negative normal form.

Sourceval limit_depth : int -> path -> path

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

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