package electrod

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

Install 

dune-project
 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-0.3.2.tbz
sha256=c58502de17f5b8d739963b5b5d7c761883305bc2b6464fc37769aae4bb31a28c
sha512=bc15032cbda06b0eb64d55cc7800d6c992c0823bb86609ddc5e56744fd0c76ea25b4f4ad7cafdee6fcaa2f109e48ca99f4270919f9a2ea4c7bf53f30b0ee3677

doc/electrod.libelectrod/Libelectrod/Elo_to_model1/Make/argument-3-Model/index.html

Parameter Make.Model

type 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;
}
val make : elo:Elo.t -> init:(string * ltl) Iter.t -> invariant:(string * ltl) Iter.t -> trans:(string * ltl) Iter.t -> property:(string * ltl) -> t
val analyze : conversion_time:Mtime.span -> cmd:string -> script:Solver.script_type -> keep_files:bool -> no_analysis:bool -> elo:Elo.t -> file:string -> bmc:int option -> t -> Outcome.t

analyze domain script filename model runs the solver on model (filename helps creating a temporary file name): in case of Error, the result contains the POSIX error code and the error string output by the solver. If script is None, then a default command script is used; otherwise it contains the name of a script file. elo is the Electrod model (used to interpret back a resulting trace).

If no_analysis is set to true, then no analysis is done (but the files are still generated and may be kept) and the function returns No_trace!

val pp : ?margin:int -> Format.formatter -> t -> unit