sig
  module SDFA :
    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
  type ('s, 'v, 'k, 'o) sdfa = ('s, 'v, 'k, 'o) Automata.SDFA.t
  module SNFA :
    sig
      type ('s, 'set, 'v, 'k, 'o) t = {
        m : ('set, 'k) Bdd.mem;
        t : 's -> ('v, ('set, 'k) Bdd.node) Common.span;
        o : 's -> 'o;
        o0 : 'o;
        o2 : 'o -> 'o -> 'o;
        state_info : 's Common.formatter;
      }
      val reindex :
        ('s Common.hval, 's Common.hset, 'v, 'k, 'o) Automata.SNFA.t ->
        (int, Common.int_set, 'v, 'k, 'o) Automata.SNFA.t *
        ('s Common.hset -> Common.int_set)
      val size :
        (int, Common.int_set, 'a, 'b, 'c) Automata.SNFA.t ->
        Common.int_set -> int * int
    end
  type ('s, 't, 'v, 'k, 'o) snfa = ('s, 't, 'v, 'k, 'o) Automata.SNFA.t
  module SENFA :
    sig
      type 'v t = {
        e : (int * Bdd.formula * int) list;
        t : (int * 'v * int) list;
        o : int Common.set;
        size : int;
      }
    end
  type 'v senfa = 'v Automata.SENFA.t
end