package electrod

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

Install

Dune 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/Elo_to_ltl1/Make/class-converter/index.html

Class Make.converterSource

constraint 'a = stack
inherit Libelectrod.Elo_recursor.recursor
method build_Add : stack -> Ltl.term -> Ltl.term -> Ltl.term
method build_All : stack -> G.quant
method build_And : stack -> ltl -> ltl -> ltl
method build_Block : stack -> ltl list -> ltl
method build_Card : stack -> Libelectrod.Elo.exp -> (Libelectrod.Tuple.t -> ltl) -> Ltl.term
method visit_Compr : stack -> (bool * int * Libelectrod.Elo.exp) list -> Libelectrod.Elo.fml list -> Libelectrod.Tuple.t -> ltl
method private allocate_sbs_to_tuples : G.exp Containers.List.t -> Libelectrod.Tuple.t -> Libelectrod.Tuple.t list
method private check_compr_disj : (bool * int * G.exp) list -> Libelectrod.Tuple.t list -> bool
method build_Compr : 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 : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_F : stack -> ltl -> ltl
method build_False : stack -> ltl
method build_G : stack -> ltl -> ltl
method build_Gt : stack -> Ltl.tcomp
method build_Gte : stack -> Ltl.tcomp
method build_H : stack -> ltl -> ltl
method build_IEq : stack -> Ltl.tcomp
method build_INEq : stack -> Ltl.tcomp
method build_Iden : stack -> Libelectrod.Tuple.t -> ltl
method build_Iff : stack -> ltl -> ltl -> ltl
method build_Imp : stack -> ltl -> ltl -> ltl
method build_In : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> ltl
method build_Inter : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_Join : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_LBin : stack -> Libelectrod.Elo.fml -> Libelectrod.Elo.lbinop -> Libelectrod.Elo.fml -> ltl -> (ltl -> ltl -> ltl) -> ltl -> ltl
method build_LProj : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_LUn : stack -> Libelectrod.Elo.lunop -> Libelectrod.Elo.fml -> (ltl -> ltl) -> ltl -> ltl
method build_Lt : stack -> Ltl.tcomp
method build_Lte : stack -> Ltl.tcomp
method build_Neg : stack -> Ltl.term -> Ltl.term
method build_No : stack -> G.quant
method build_None_ : stack -> Libelectrod.Tuple.t -> ltl
method build_Not : stack -> ltl -> ltl
method build_NotIn : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> ltl
method build_Num : stack -> int -> int -> Ltl.term
method build_O : stack -> ltl -> ltl
method build_Or : stack -> ltl -> ltl -> ltl
method build_Over : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_P : stack -> ltl -> ltl
method build_Prod : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method visit_Quant : stack -> Libelectrod.Elo.quant -> (bool * int * Libelectrod.Elo.exp) -> Libelectrod.Elo.fml list -> ltl
method build_Quant : 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 : stack -> ltl -> ltl -> ltl
method build_REq : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> ltl
method build_RNEq : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> ltl
method build_RProj : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_S : stack -> ltl -> ltl -> ltl
method build_Some_ : stack -> G.quant
method build_Sub : stack -> Ltl.term -> Ltl.term -> Ltl.term
method build_T : stack -> ltl -> ltl -> ltl
method build_Transpose : stack -> Libelectrod.Elo.exp -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_True : stack -> ltl
method build_U : stack -> ltl -> ltl -> ltl
method build_Union : stack -> G.exp -> G.exp -> (Libelectrod.Tuple.t -> ltl) -> (Libelectrod.Tuple.t -> ltl) -> Libelectrod.Tuple.t -> ltl
method build_Univ : stack -> Libelectrod.Tuple.t -> ltl
method build_Var : stack -> int -> int -> Libelectrod.Tuple.t -> ltl
method build_X : stack -> ltl -> ltl
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