package electrod

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

Install

Dune Dependency

Authors

Maintainers

Sources

electrod-0.7.1.tbz
sha256=e5d2278c99128621110cd015dafcbcae9792bbf2c8bb09d7b02c57d50fa28075
sha512=e08ecf720d35b6ee72f37d780cc3da22f61e22314ffd093ff3314fb89684b863b5c96c97375d48bcb4ba2838ec8f61a495105c989f292c5dbcd095e14f52bdba

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.