Formal analysis for the Electrod formal pivot language


module Ltl : Solver.LTL


type ltl = Ltl.t
type atomic = 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: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