electrod

Formal analysis for the Electrod formal pivot language
IN THIS PACKAGE
type tcomp =
| Lte
| Lt
| Gte
| Gt
| Eq
| Neq
type t = private
| Comp of tcomp * term * term
| True
| False
| Atomic of Atomic.t
| Not of t
| And of t * t
| Or of t * t
| Imp of t * t
| Iff of t * t
| Xor of t * t
| Ite of t * t * t
| X of t
| F of t
| G of t
| Y of t
| O of t
| H of t
| U of t * t
| R of t * t
| S of t * t
| T of t * t
and term = private
| Num of int
| Plus of term * term
| Minus of term * term
| Neg of term
| 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