Provides a transformation from Electrod models to SMV models. Uses enumerations when possible.
module SMV_atom : Solver.ATOMIC_PROPOSITIONmodule SMV_LTL : sig ... endmodule SMV_file_format : sig ... endmodule Elo_to_SMV_LTL : sig ... endmodule Elo_to_SMV_model : sig ... endval pp : ?margin:int -> Format.formatter -> SMV_file_format.t -> unitval 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 ->
SMV_file_format.t ->
Outcome.tval run : Elo.t -> SMV_file_format.tval transfo : (Elo.t, SMV_file_format.t) Transfo.t