With_interface (hardcaml_verify.Hardcaml_verify_kernel.Nusmv.With

Parameters

module I : Hardcaml.Interface.S

module O : Hardcaml.Interface.S

type model := t

type t

type ltl := Hardcaml.Property.LTL.path

type ctl := Hardcaml.Property.CTL.state

val create : 
  name:Base.string ->
  Hardcaml.Signal.t Hardcaml.Interface.Create_fn(I)(O).t ->
  t

val ltl : t -> ( ltl Base.array I.t, ltl Base.array O.t ) Circuit_properties.t

val ctl : t -> ( ctl Base.array I.t, ctl Base.array O.t ) Circuit_properties.t

val create_specification : t -> property Base.list -> model