Module `Nusmv.With_interface`

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.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