package electrod

  1. Overview
  2. Docs

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