package electrod

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

Module Solver.LTL_from_AtomicSource

Builds an LTL implementation out of an implementation of atomicic propositions.

Parameters

Signature

module Atomic = At
Sourcetype tcomp =
  1. | Lte
  2. | Lt
  3. | Gte
  4. | Gt
  5. | Eq
  6. | Neq
Sourcetype t = private
  1. | Comp of tcomp * term * term
  2. | True
  3. | False
  4. | Atomic of Atomic.t
  5. | Not of t
  6. | And of t * t
  7. | Or of t * t
  8. | Imp of t * t
  9. | Iff of t * t
  10. | Xor of t * t
  11. | Ite of t * t * t
  12. | X of t
  13. | F of t
  14. | G of t
  15. | Y of t
  16. | O of t
  17. | H of t
  18. | U of t * t
  19. | R of t * t
  20. | S of t * t
  21. | T of t * t
Sourceand term = private
  1. | Num of int
  2. | Plus of term * term
  3. | Minus of term * term
  4. | Neg of term
  5. | Count of t list
Sourceval true_ : t
Sourceval false_ : t
Sourceval atomic : Atomic.t -> t
Sourceval not_ : t -> t
Sourceval and_ : t -> t Lazy.t -> t
Sourceval or_ : t -> t Lazy.t -> t
Sourceval implies : t -> t Lazy.t -> t
Sourceval xor : t -> t -> t
Sourceval iff : t -> t -> t
Sourceval conj : t list -> t
Sourceval disj : t list -> t
Sourceval wedge : range:'a Iter.t -> ('a -> t Lazy.t) -> t
Sourceval vee : range:'a Iter.t -> ('a -> t Lazy.t) -> t
Sourceval ifthenelse : t -> t -> t -> t
Sourceval next : t -> t
Sourceval always : t -> t
Sourceval eventually : t -> t
Sourceval yesterday : t -> t
Sourceval once : t -> t
Sourceval historically : t -> t
Sourceval until : t -> t -> t
Sourceval releases : t -> t -> t
Sourceval since : t -> t -> t
Sourceval triggered : t -> t -> t
Sourceval num : int -> term
Sourceval plus : term -> term -> term
Sourceval minus : term -> term -> term
Sourceval neg : term -> term
Sourceval count : t list -> term
Sourceval comp : tcomp -> term -> term -> t
Sourceval lt : tcomp
Sourceval lte : tcomp
Sourceval gt : tcomp
Sourceval gte : tcomp
Sourceval eq : tcomp
Sourceval neq : tcomp
Sourcemodule Infix : sig ... end
Sourceval pp : Format.formatter -> t -> unit
Sourceval pp_gather_variables : ?next_is_X:bool -> Atomic.t Iter.t ref -> Format.formatter -> t -> unit
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