package electrod

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

Install

Dune Dependency

Authors

Maintainers

Sources

electrod-0.2.3.tbz
sha256=7371c45e28b84a1955d117ef2c798d545febb87c74f596b6efe24965e4b28f31
sha512=e579db68ac05e30b0985f7d90080a82697de18c12e818d48bd7029cea8844571423f08d5881accbf8a0cbeb7df7de9b5b95ff5fe813330a6c92448a0901cdfe7

doc/electrod.libelectrod/Libelectrod/Elo_to_smv1/SMV_file_format/index.html

Module Elo_to_smv1.SMV_file_formatSource

Sourcetype ltl = SMV_LTL.t
Sourcetype t = private {
  1. elo : Elo.t;
  2. init : (string * ltl) Iter.t;
  3. invariant : (string * ltl) Iter.t;
  4. trans : (string * ltl) Iter.t;
  5. property : string * ltl;
}
Sourceval make : elo:Elo.t -> init:(string * ltl) Iter.t -> invariant:(string * ltl) Iter.t -> trans:(string * ltl) Iter.t -> property:(string * ltl) -> t
Sourceval analyze : conversion_time:Mtime.span -> cmd:string -> script:Libelectrod__Solver.script_type -> keep_files:bool -> no_analysis:bool -> elo:Elo.t -> file:string -> bmc:int option -> t -> Outcome.t
Sourceval pp : ?margin:int -> Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.