sig
  type ('s, 'v, 'k, 'o) t = {
    m : ('s, 'k) Bdd.mem;
    t : 's -> ('v, ('s, 'k) Bdd.node) Common.span;
    o : 's -> 'o;
    output_check : 's -> 's -> bool;
    state_info : 's Common.formatter;
  }
  val trace :
    ?exclude:'s ->
    'v Common.formatter ->
    'k Common.formatter ->
    'o Common.formatter -> ('s, 'v, 'k, 'o) Automata.SDFA.t -> 's -> unit
  val size : ('s, 'a, 'b, 'c) Automata.SDFA.t -> 's list -> int * int
  val generic_output_check : ('s -> 'o) -> 's -> 's -> bool
end