package electrod

  1. Overview
  2. Docs
Formal analysis for the Electrod formal pivot language

Install 

dune-project
 Dependency

github.com Readme Changelog MPL-2.0 License Edit opam file Versions (10)

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

  1. D
    David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2

doc/electrod.libelectrod/Libelectrod/Solver/module-type-LTL/index.html

Module type Solver.LTLSource

Abstract type of LTL (contains pElo connectives as well as basic counting capabilities).

type tcomp =
  1. | Lte
  2. | Lt
  3. | Gte
  4. | Gt
  5. | Eq
  6. | Neq
type 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
and 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
val true_ : t
val false_ : t
val atomic : Atomic.t -> t
val not_ : t -> t
val and_ : t -> t Lazy.t -> t
val or_ : t -> t Lazy.t -> t
val implies : t -> t Lazy.t -> t
val xor : t -> t -> t
val iff : t -> t -> t
val conj : t list -> t
val disj : t list -> t
val wedge : range:'a Iter.t -> ('a -> t Lazy.t) -> t
val vee : range:'a Iter.t -> ('a -> t Lazy.t) -> t
val ifthenelse : t -> t -> t -> t
val next : t -> t
val always : t -> t
val eventually : t -> t
val yesterday : t -> t
val once : t -> t
val historically : t -> t
val until : t -> t -> t
val releases : t -> t -> t
val since : t -> t -> t
val triggered : t -> t -> t
val num : int -> term
val plus : term -> term -> term
val minus : term -> term -> term
val neg : term -> term
val count : t list -> term
val comp : tcomp -> term -> term -> t
val lt : tcomp
val lte : tcomp
val gt : tcomp
val gte : tcomp
val eq : tcomp
val neq : tcomp
module Infix : sig ... end
val pp : Format.formatter -> t -> unit
val pp_gather_variables : ?next_is_X:bool -> Atomic.t Iter.t ref -> Format.formatter -> t -> unit