electrod

Formal analysis for the Electrod formal pivot language
IN THIS PACKAGE
type ltl = SMV_LTL.t
type atomic = SMV_LTL.Atomic.t
type t = private {
elo : Elo.t;
init : (string * ltl) Iter.t;
invariant : (string * ltl) Iter.t;
trans : (string * ltl) Iter.t;
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:Libelectrod__Solver.script_type -> keep_files:bool -> no_analysis:bool -> elo:Elo.t -> file:string -> bmc:int option -> t -> Outcome.t
val pp : ?margin:int -> Format.formatter -> t -> unit