val sexp_of_property : property -> Sexplib0.Sexp.tval sexp_of_t : t -> Sexplib0.Sexp.tval create :
?outputs:Hardcaml.Signal.t Base.list ->
name:Base.string ->
property Base.list ->
tcreate ?outputs ~name properties creates a NuSMV model with the provided name.
properties is a list of LTL and/or CTL formula that should be satified by the circuit. During construction all atomic_propositions (which are the signals in the design used to build the temporal formula) are created as outputs. They are given the prefix "__ap_" which should not otherwise be used to name signals.
The important part of the circuit is traced back from the atomic_propositions. However, it is possible to include the complete circuit if required by passing outputs.
val circuit : t -> Hardcaml.Circuit.tReturn the circuit generated for the NuSMV model.
val write : Stdio.Out_channel.t -> t -> Base.unitWrite the NuSMV model to a file.
module Counter_example_trace : sig ... endmodule Proof_result : sig ... endmodule Output_parser : sig ... endval run : t -> Proof_result.t Base.listmodule Circuit_properties : sig ... endmodule With_interface
(I : Hardcaml.Interface.S)
(O : Hardcaml.Interface.S) :
sig ... end