package electrod

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 -> pp_generated:bool -> t -> Outcome.t
Sourceval pp : ?margin:int -> Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.