Nusmv (hardcaml_verify.Hardcaml

include module type of Hardcaml_verify_kernel.Nusmv

type property =

| LTL of Hardcaml.Property.LTL.path

| CTL of Hardcaml.Property.CTL.state

val sexp_of_property : property -> Sexplib0.Sexp.t

type t

val sexp_of_t : t -> Sexplib0.Sexp.t

val create : 
  ?outputs:Hardcaml.Signal.t Base.list ->
  name:Base.string ->
  property Base.list ->
  t

create ?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.t

Return the circuit generated for the NuSMV model.

val write : Stdio.Out_channel.t -> t -> Base.unit

Write the NuSMV model to a file.

module Proof_result : sig ... end

module Output_parser : sig ... end

val run : t -> Proof_result.t Base.list

module Circuit_properties : sig ... end

module With_interface
  (I : Hardcaml.Interface.S)
  (O : Hardcaml.Interface.S) : 
  sig ... end

module Counter_example_trace : sig ... end