electrod

Formal analysis for the Electrod formal pivot language
IN THIS PACKAGE
constraint 'a = stack
method build_Add : 'a converter -> stack -> Ltl.term -> Ltl.term -> Ltl.term
method build_All : 'b -> stack -> G.quant
method build_And : 'b -> stack -> ltl -> ltl -> ltl
method build_Block : 'b -> stack -> ltl list -> ltl
method build_Card : 'b -> stack -> Libelectrod.Elo.exp -> ( Libelectrod.Tuple.t -> ltl ) -> Ltl.term
method visit_Compr : 'b -> stack -> (bool * int * Libelectrod.Elo.exp) list -> Libelectrod.Elo.fml list -> Libelectrod.Tuple.t -> ltl
method private allocate_sbs_to_tuples : 'b -> G.exp Containers.List.t -> Libelectrod.Tuple.t -> Libelectrod.Tuple.t list
method private check_compr_disj : 'b -> (bool * int * G.exp) list -> Libelectrod.Tuple.t list -> bool
method build_Compr : 'b -> stack -> (bool * int * Libelectrod.Elo.exp) list -> Libelectrod.Elo.fml list -> (bool * int * ( Libelectrod.Tuple.t -> ltl )) list -> ltl list -> Libelectrod.Tuple.t -> ltl
method build_Diff : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_F : 'b -> stack -> ltl -> ltl
method build_FIte : 'b -> stack -> Libelectrod.Elo.fml -> Libelectrod.Elo.fml -> Libelectrod.Elo.fml -> ltl -> ltl -> ltl -> ltl
method build_False : 'b -> stack -> ltl
method build_G : 'b -> stack -> ltl -> ltl
method build_Gt : 'b -> stack -> Ltl.tcomp
method build_Gte : 'b -> stack -> Ltl.tcomp
method build_H : 'b -> stack -> ltl -> ltl
method build_IEq : 'b -> stack -> Ltl.tcomp
method build_INEq : 'b -> stack -> Ltl.tcomp
method build_IUn : 'b -> stack -> Libelectrod.Elo.iunop -> Libelectrod.Elo.iexp -> ( Ltl.term -> Ltl.term ) -> Ltl.term -> Ltl.term
method build_Iden : 'b -> stack -> Libelectrod.Tuple.t -> ltl
method build_Iff : 'b -> stack -> ltl -> ltl -> ltl
method build_Imp : 'b -> stack -> ltl -> ltl -> ltl
method build_In : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> ltl
method build_Inter : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_Join : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_LBin : 'b -> stack -> Libelectrod.Elo.fml -> Libelectrod.Elo.lbinop -> Libelectrod.Elo.fml -> ltl -> ( ltl -> ltl -> ltl ) -> ltl -> ltl
method build_LProj : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_LUn : 'b -> stack -> Libelectrod.Elo.lunop -> Libelectrod.Elo.fml -> ( ltl -> ltl ) -> ltl -> ltl
method build_Lt : 'b -> stack -> Ltl.tcomp
method build_Lte : 'b -> stack -> Ltl.tcomp
method build_Name : 'b -> stack -> Libelectrod.Name.t -> Libelectrod.Name.t -> Libelectrod.Tuple.t -> ltl
method build_Neg : 'b -> stack -> Ltl.term -> Ltl.term
method build_No : 'b -> stack -> G.quant
method build_None_ : 'b -> stack -> Libelectrod.Tuple.t -> ltl
method build_Not : 'b -> stack -> ltl -> ltl
method build_NotIn : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> ltl
method build_Num : 'b -> stack -> int -> int -> Ltl.term
method build_O : 'b -> stack -> ltl -> ltl
method build_Or : 'b -> stack -> ltl -> ltl -> ltl
method build_Over : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_P : 'b -> stack -> ltl -> ltl
method build_Prime : 'b -> stack -> Libelectrod.Elo.exp -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_Prod : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method visit_Quant : 'b -> stack -> Libelectrod.Elo.quant -> (bool * int * Libelectrod.Elo.exp) -> Libelectrod.Elo.fml list -> ltl
method build_Quant : 'b -> stack -> Libelectrod.Elo.quant -> (bool * int * Libelectrod.Elo.exp) -> G.fml list -> G.quant -> (bool * int * ( Libelectrod.Tuple.t -> ltl )) -> ltl list -> ltl
method build_R : 'b -> stack -> ltl -> ltl -> ltl
method build_REq : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> ltl
method build_RNEq : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> ltl
method build_RProj : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_RTClos : 'b -> stack -> Libelectrod.Elo.exp -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_S : 'b -> stack -> ltl -> ltl -> ltl
method build_Some_ : 'b -> stack -> G.quant
method build_Sub : 'b -> stack -> Ltl.term -> Ltl.term -> Ltl.term
method build_T : 'b -> stack -> ltl -> ltl -> ltl
method build_TClos : 'b -> stack -> Libelectrod.Elo.exp -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_Transpose : 'b -> stack -> Libelectrod.Elo.exp -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_True : 'b -> stack -> ltl
method build_U : 'b -> stack -> ltl -> ltl -> ltl
method build_Union : 'b -> stack -> G.exp -> G.exp -> ( Libelectrod.Tuple.t -> ltl ) -> ( Libelectrod.Tuple.t -> ltl ) -> Libelectrod.Tuple.t -> ltl
method build_Univ : 'b -> stack -> Libelectrod.Tuple.t -> ltl
method build_Var : 'b -> stack -> int -> int -> Libelectrod.Tuple.t -> ltl
method build_X : 'b -> stack -> ltl -> ltl